Changeset 2468 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Nov 15, 2012, 6:12:57 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2441 r2468 581 581 ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i). 582 582 #castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result 583 elim castee_val 584 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ]583 elim castee_val 584 [ 1:  2: #sz' #i  3:  4: #ptr ] 585 585 [ 2:  *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ] 586 586 whd in ⊢ ((??%?) → ?); … … 613 613 #sz #sg #v1 #v2 #m #r 614 614 elim v1 615 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ]615 [ 1:  2: #sz' #i  3:  4: #ptr ] 616 616 whd in ⊢ ((??%?) → ?); normalize nodelta 617 617 >classify_add_int normalize nodelta #H destruct 618 618 elim v2 in H; 619 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ]619 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 620 620 whd in ⊢ ((??%?) → ?); #H destruct 621 621 elim (sz_eq_dec sz' sz'') 622 622 [ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/ 623 623  2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct 624 ] qed. 624 ] qed. 625 625 626 626 (* Inversion principle for integer subtraction. *) … … 629 629 #sz #sg #v1 #v2 #m #r 630 630 elim v1 631 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ]631 [ 1:  2: #sz' #i  3:  4: #ptr ] 632 632 whd in ⊢ ((??%?) → ?); normalize nodelta 633 633 >classify_sub_int normalize nodelta #H destruct 634 634 elim v2 in H; 635 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ]635 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 636 636 whd in ⊢ ((??%?) → ?); #H destruct 637 637 elim (sz_eq_dec sz' sz'') … … 652 652 #sz #sg #v1 #v2 #m 653 653 elim v1 654 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ]654 [ 1:  2: #sz' #i  3:  4: #ptr ] 655 655 [ 2:  *: #_ %1 %1 % #H @H ] 656 656 elim v2 657 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ]657 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 658 658 [ 2:  *: #_ %1 %2 % #H @H ] 659 659 whd in ⊢ ((??%?) → ?); normalize nodelta … … 663 663  2: #Hneq >intsize_eq_elim_false try assumption #_ 664 664 %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj // 665 ] qed. 665 ] qed. 666 666 667 667 (* "negative" inversion principle for integer subtraction *) … … 671 671 #sz #sg #v1 #v2 #m 672 672 elim v1 673 [ 1:  2: #sz' #i  3: #f  4:  5: #ptr ]673 [ 1:  2: #sz' #i  3:  4: #ptr ] 674 674 [ 2:  *: #_ %1 %1 % #H @H ] 675 675 elim v2 676 [ 1:  2: #sz'' #i'  3: #f'  4:  5: #ptr' ]676 [ 1:  2: #sz'' #i'  3:  4: #ptr' ] 677 677 [ 2:  *: #_ %1 %2 % #H @H ] 678 678 whd in ⊢ ((??%?) → ?); normalize nodelta … … 684 684 ] qed. 685 685 686 687 686 lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. 688 687 ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?. … … 690 689 elim op normalize in match (binop_simplifiable ?); #H destruct 691 690 elim v1 in H; 692 [ 1, 6:  2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I))  3,8: #f  4,9:  5,10: #ptr ]691 [ 1,5:  2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I))  3,7:  4,8: #ptr ] 693 692 #_ 694 693 whd in match (sem_binary_operation ??????); normalize nodelta … … 890 889 «〈false, Expr (Ecost l e2) ty〉, ?» 891 890 ] 892  Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» 891 (*  Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) 893 892 (*  Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *) 894 893 (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact … … 960 959 ] (refl ? e). 961 960 #ge #en #m 962 [ 1,3,5,6,7,8,9,10,11 ,12: %1 try @refl961 [ 1,3,5,6,7,8,9,10,11: %1 try @refl 963 962 cases (exec_expr ge en m e) #res 964 963 try (@(SimOk ???) //) … … 975 974 [ 1: @(simplify_int_implements_cast … Hsimpl_eq) 976 975  2: @(simplify_int_success_lt … Hsimpl_eq) ] 977  13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res978 try (@(SimOk ???) //) 979  1 4: elim (type_eq_dec ty (Tint target_sz target_sg))976 (* 14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res 977 try (@(SimOk ???) //) *) 978  12: elim (type_eq_dec ty (Tint target_sz target_sg)) 980 979 [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg) 981 980 destruct … … 985 984 @(SimOk ???) // 986 985 ] 987  1 5: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq986  13: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 988 987 [ 1: (* Proving preservation of the semantics for expressions. *) 989 988 cases Hexpr_sim … … 998 997 [ 1: * #val' #trace' normalize nodelta 999 998 cases val' normalize nodelta 1000 [ 1,2,3 ,4: #H1 destruct #H2 destruct #H3 destruct1001  5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)999 [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct 1000  4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) 1002 1001 cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq; 1003 1002 normalize nodelta … … 1027 1026 [ 1: * #val' #trace' normalize nodelta 1028 1027 cases val' normalize nodelta 1029 [ 1,2,3 ,4: #H1 destruct #H2 destruct #H3 destruct1030  5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)1028 [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct 1029  4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *) 1031 1030 destruct try @conj try @conj // 1032 1031 ] … … 1042 1041 ] 1043 1042 ] 1044  1 6: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq1043  14: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1045 1044 [ 1: (* Proving preservation of the semantics for expressions. *) 1046 1045 cases Hlvalue_sim … … 1056 1055 [ 1: * * #block #offset #trace' normalize nodelta 1057 1056 cases ty 1058 [ 2: #sz #sg  3: # fsz  4: #ptr_ty  5: #array_ty #array_sz  6: #domain #codomain1059  7: #structname #fieldspec  8: #unionname #fieldspec  9: #id ]1057 [ 2: #sz #sg  3: #ptr_ty  4: #array_ty #array_sz  5: #domain #codomain 1058  6: #structname #fieldspec  7: #unionname #fieldspec  8: #id ] 1060 1059 normalize nodelta try (#Heq destruct) 1061 1060 @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty) … … 1071 1070 @SimFailNicely 1072 1071 ] 1073  1 7: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq1072  15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq 1074 1073 [ 1: whd in match (exec_expr ge en m (Expr ??)); 1075 1074 whd in match (exec_expr ge en m (Expr ??)); … … 1085 1084  2: @SimFailNicely 1086 1085 ] 1087  1 8: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs Hdesired_eq1086  16: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs Hdesired_eq 1088 1087 inversion (Hinv_lhs ge en m) 1089 1088 [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true … … 1113 1112 whd in match (m_bind ?????); 1114 1113 (* specialize to the actual simplifiable operations. *) 1115 cases op in Hop_simplifiable_eq; 1116 [ 1,2:  *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ 1114 cases op in Hop_simplifiable_eq; 1115 [ 1,2:  *: normalize in ⊢ (% → ?); #H destruct (H) ] #_ 1117 1116 [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m) 1118 1117  2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ] … … 1180 1179 ] 1181 1180 ] ] ] ] 1182  1 9,20,21,22: destruct %1 try @refl1181  17,18,19,20: destruct %1 try @refl 1183 1182 elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs 1184 1183 elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs … … 1208 1207 ] 1209 1208 (* Jump to the cast cases *) 1210  23,30,31,32,33,34,35,36: %1 try @refl 1209 (* 21,30,31,32,33,34,35,36: *) 1210  21,27,28,29,30,31,32,33: 1211 %1 try @refl 1211 1212 [ 1,4,7,10,13,16,19,22: destruct // ] 1212 1213 elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq … … 1238 1239  2,4,6,8,10,12,14,16: destruct @SimFailNicely 1239 1240 ] 1240  2 4: destruct inversion (Hcastee_inv ge en m)1241  22: destruct inversion (Hcastee_inv ge en m) 1241 1242 [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 1242 1243 <Hresult_flag_2 in Hresult_flag; #Hcontr destruct … … 1269 1270 [ 2,4: * #Heq >Heq #_ elim target_sz // 1270 1271  1,3: #Hlt @(size_lt_to_le ?? Hlt) ] 1271 ] ] ] ] ] 1272  2 5,27: destruct1272 ] ] ] ] ] 1273  23,25: destruct 1273 1274 inversion (Hcast2 ge en m) 1274 1275 [ 1,3: (* Impossible case. *) … … 1298 1299 ] ] 1299 1300 ] ] 1300  2 6,28: destruct1301  24,26: destruct 1301 1302 inversion (Hcast2 ge en m) 1302 1303 [ 2,4: (* Impossible case. *) … … 1322 1323 ] 1323 1324 ] 1325 (* 1324 1326  29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1325 1327 @(Inv_eq ???????) // … … 1336 1338 normalize nodelta #H @H 1337 1339 ] 1338 ] 1339  3 7: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false Hdesired_eq1340 ] *) 1341  34: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false Hdesired_eq 1340 1342 inversion (Htrue_inv ge en m) 1341 1343 [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false … … 1393 1395 ] ] 1394 1396 ] ] ] ] ] ] ] 1395  3 8,39,40: destruct1397  35,36,37: destruct 1396 1398 elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq 1397 1399 elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq … … 1445 1447  2,4,6: @SimFailNicely 1446 1448 ] 1447  41,42: destruct1449  38,39: destruct 1448 1450 elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1449 1451 elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs … … 1481 1483  2,4: @SimFailNicely 1482 1484 ] 1483  4 3: destruct1485  40: destruct 1484 1486 cases (type_eq_dec ty (Tint target_sz target_sg)) 1485 1487 [ 1: #Htype_eq >Htype_eq >type_eq_identity … … 1490 1492 %1 // @SimOk #a #H @H 1491 1493 ] 1492  4 4: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq1494  41: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1493 1495 %1 try @refl 1494 1496 [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); … … 1498 1500 >Htype_eq 1499 1501 cases (typeof rec_expr1) normalize nodelta 1500 [ 2: #sz #sg  3: # fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ]1501 [ 1,2,3,4, 5,8,9: @SimFailNicely1502  6,7: cases Hsim_lvalue1502 [ 2: #sz #sg  3: #ty  4: #ty #n  5: #tl #ty  6: #id #fl  7: #id #fl  8: #ty ] 1503 [ 1,2,3,4,7,8: @SimFailNicely 1504  5,6: cases Hsim_lvalue 1503 1505 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely 1504 1506  1,3: cases (exec_lvalue ge en m rec_expr) … … 1513 1515 >Htype_eq 1514 1516 cases (typeof rec_expr1) normalize nodelta 1515 [ 2: #sz #sg  3: # fl  4: #ty  5: #ty #n  6: #tl #ty  7: #id #fl  8: #id #fl  9: #ty ]1516 [ 1,2,3,4, 5,8,9: @SimFailNicely1517  6,7: cases Hsim_lvalue1517 [ 2: #sz #sg  3: #ty  4: #ty #n  5: #tl #ty  6: #id #fl  7: #id #fl  8: #ty ] 1518 [ 1,2,3,4,7,8: @SimFailNicely 1519  5,6: cases Hsim_lvalue 1518 1520 [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely 1519 1521  1,3: cases (exec_lvalue ge en m rec_expr) … … 1526 1528 ] 1527 1529 ] 1528  4 5: destruct1530  42: destruct 1529 1531 inversion (Hinv ge en m) 1530 1532 [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_ … … 1561 1563 ] 1562 1564 ] 1563  4 6: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq1565  43: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1564 1566 %1 try @refl 1565 1567 [ 1: whd in match (exec_expr ??? (Expr ??)); … … 1574 1576 (* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls 1575 1577 * simplify_expr *) 1576  4 7, 48, 49: (* trivial const_int, const_float and var cases *)1578  44, 45: (* trivial const_int, const_float and var cases *) 1577 1579 try @conj try @conj try @refl 1578 1580 @SimOk #a #H @H 1579  50: (* Deref case *) destruct1581  46: (* Deref case *) destruct 1580 1582 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1581 1583 try @conj try @conj … … 1596 1598  1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ] 1597 1599  3: // ] 1598  51: (* Addrof *) destruct1600  47: (* Addrof *) destruct 1599 1601 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1600 1602 try @conj try @conj … … 1609 1611  2: @SimFailNicely 1610 1612  3: // ] 1611  52: (* Unop *) destruct1613  48: (* Unop *) destruct 1612 1614 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1613 1615 try @conj try @conj … … 1623 1625  2: @SimFailNicely 1624 1626  3: // ] 1625  53: (* Binop *) destruct1627  49: (* Binop *) destruct 1626 1628 elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1627 1629 elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs … … 1650 1652  3: // 1651 1653 ] 1652  5 4: (* Cast, fallback case *)1654  50: (* Cast, fallback case *) 1653 1655 try @conj try @conj try @refl 1654 1656 @SimOk #a #H @H 1655  5 5: (* Cast, success case *) destruct1657  51: (* Cast, success case *) destruct 1656 1658 inversion (Htrans_inv ge en m) 1657 1659 [ 1: (* contradiction *) … … 1680 1682 ] 1681 1683 ] 1682  5 6: (* Cast, "failure" case *) destruct1684  52: (* Cast, "failure" case *) destruct 1683 1685 inversion (Htrans_inv ge en m) 1684 1686 [ 2: (* contradiction *) … … 1700 1702 ] 1701 1703 ] 1702  5 7,58,59,60,61,62,63,64,68:1704  53,54,55,56,57,58,59,63: 1703 1705 try @conj try @conj try @refl 1704 1706 @SimOk #a #H @H 1705  6 5: destruct1707  60: destruct 1706 1708 elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond 1707 1709 elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true … … 1746 1748  3: // 1747 1749 ] 1748  6 6,67: destruct1750  61,62: destruct 1749 1751 elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs 1750 1752 elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs … … 1777 1779  3,6: // 1778 1780 ] 1779  6 9: (* record field *) destruct1781  64: (* record field *) destruct 1780 1782 elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1781 1783 try @conj try @conj … … 1785 1787 whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 1786 1788 [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta 1787 [ 2: #sz #sg  3: # fl  4: #ty'  5: #ty #n  6: #tl #ty'1788  7: #id #fl  8: #id #fl  9: #id ]1789 [ 2: #sz #sg  3: #ty'  4: #ty #n  5: #tl #ty' 1790  6: #id #fl  7: #id #fl  8: #id ] 1789 1791 try (@SimFailNicely) 1790 1792 cases Hsim_lvalue … … 1797 1799  2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *) 1798 1800 >Htype_eq cases (typeof rec_expr1) normalize nodelta 1799 [ 2: #sz #sg  3: # fl  4: #ty'  5: #ty #n  6: #tl #ty'1800  7: #id #fl  8: #id #fl  9: #id ]1801 [ 2: #sz #sg  3: #ty'  4: #ty #n  5: #tl #ty' 1802  6: #id #fl  7: #id #fl  8: #id ] 1801 1803 try (@SimFailNicely) 1802 1804 cases Hsim_lvalue … … 1808 1810 ] 1809 1811  3: // ] 1810  70: (* cost label *) destruct1812  65: (* cost label *) destruct 1811 1813 elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq 1812 1814 try @conj try @conj … … 1926 1928 1927 1929 definition expr_lvalue_ind_combined ≝ 1928 λP,Q,ci, cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.1930 λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. 1929 1931 conj ?? 1930 (expr_lvalue_ind P Q ci cflv vr dr ao uo bo ca cd ab ob sz fl co xx)1931 (lvalue_expr_ind P Q ci cflv vr dr ao uo bo ca cd ab ob sz fl co xx).1932 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx) 1933 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx). 1932 1934 1933 1935 lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2. … … 1944 1946 #ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined 1945 1947 [ 1: #sz #ty #i @SimOk #a normalize // 1946  2: #ty #f @SimOk #a normalize // 1947  3: * 1948 [ 1: #sz #i  2: #fl  3: #id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8: #cast_ty #e1 1949  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14: #cost #e1 ] 1948  2: * 1949 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 1950  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 1950 1951 #ty #Hsim_lvalue try // 1951 1952 whd in match (Plvalue ???); … … 1959 1960 @SimOk // ] 1960 1961 ] 1961  4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);1962  3: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); 1962 1963 cases (lookup SymbolTag block en v) normalize nodelta 1963 1964 [ 2: #block @SimOk // 1964 1965  1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk // 1965 1966 ] 1966  5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);1967  4: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????); 1967 1968 cases Hsim_expr 1968 1969 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ … … 1972 1973 @SimOk // ] 1973 1974 ] 1974  6: #ty #ed #ty' #Hsim_lvalue1975  5: #ty #ed #ty' #Hsim_lvalue 1975 1976 whd in match (exec_expr ????); whd in match (exec_expr ????); 1976 1977 whd in match (exec_lvalue ????); whd in match (exec_lvalue ????); … … 1982 1983 @SimOk // ] 1983 1984 ] 1984  7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));1985  6: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 1985 1986 cases Hsim 1986 1987 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ … … 1990 1991 @SimOk // ] 1991 1992 ] 1992  8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));1993  7: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 1993 1994 cases Hsim1 1994 1995 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ … … 2005 2006 ] 2006 2007 ] 2007  9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));2008  8: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2008 2009 cases Hsim 2009 2010 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ … … 2013 2014 @SimOk // ] 2014 2015 ] (* mergeable with 7 modulo intros *) 2015  10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));2016  9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2016 2017 cases Hsim1 2017 2018 [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/ … … 2031 2032 ] 2032 2033 ] 2033  1 1,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));2034  10,11: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??)); 2034 2035 cases Hsim1 2035 2036 [ 2,4: * #error #Hfail >Hfail @SimFailNicely … … 2052 2053 ] 2053 2054 ] 2054  1 3: #ty #sizeof_ty @SimOk normalize //2055  1 4: #ty #e #ty' #field #Hsim_lvalue2055  12: #ty #sizeof_ty @SimOk normalize // 2056  13: #ty #e #ty' #field #Hsim_lvalue 2056 2057 whd in match (exec_lvalue' ? en m (Efield ??) ty); 2057 2058 whd in match (exec_lvalue' ge' en m (Efield ??) ty); 2058 2059 normalize in match (typeof (Expr ??)); 2059 2060 cases ty' in Hsim_lvalue; normalize nodelta 2060 [ 2: #sz #sg  3: #fsz  4: #ptr_ty  5: #array_ty #array_sz  6:#domain #codomain2061  7: #structname #fieldspec  8: #unionname #fieldspec  9:#id ]2061 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 2062  #structname #fieldspec  #unionname #fieldspec  #id ] 2062 2063 #Hsim_lvalue 2063 2064 try (@SimFail /2 by ex_intro/) … … 2071 2072 @SimOk /2 by ex_intro/ ] 2072 2073 ] 2073  1 5: #ty #lab #e #Hsim2074  14: #ty #lab #e #Hsim 2074 2075 whd in match (exec_expr ??? (Expr ??)); 2075 2076 whd in match (exec_expr ??? (Expr ??)); … … 2081 2082 @SimOk // ] 2082 2083 ] (* cf case 7, again *) 2083  1 6: *2084 [ 1: #sz #i  2: #fl  3: #id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8:#cast_ty #e12085  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14:#cost #e1 ]2086 2087 [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_2088 2084  15: * 2085 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 2086  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 2087 #ty normalize in match (is_not_lvalue ?); 2088 [ 2,3,12: #Habsurd @(False_ind … Habsurd) ] #_ 2089 @SimFailNicely 2089 2090 ] qed. 2090 2091 … … 2095 2096 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); 2096 2097 cases e #ed #ty cases ed 2097 [ 1: #sz #i  2: #fl  3: #id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8:#cast_ty #e12098  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14:#cost #e1 ]2098 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 2099  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 2099 2100 elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) 2100 2101 * * try // … … 2111 2112 #ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?); 2112 2113 cases e #ed #ty cases ed 2113 [ 1: #sz #i  2: #fl  3: #id  4: #e1  5: #e1  6: #op #e1  7: #op #e1 #e2  8:#cast_ty #e12114  9: #cond #iftrue #iffalse  10: #e1 #e2  11: #e1 #e2  12: #sizeofty  13: #e1 #field  14:#cost #e1 ]2114 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 2115  #cond #iftrue #iffalse  #e1 #e2  #e1 #e2  #sizeofty  #e1 #field  #cost #e1 ] 2115 2116 elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m) 2116 2117 * * try // … … 2462 2463  2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd) 2463 2464  3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd) 2464  4: #r #Habsurd destruct (Habsurd) ] 2465  3, 4,9: #irrelevant #Habsurd destruct2465  4: #r #Habsurd destruct (Habsurd) ] 2466  3,8: #irrelevant #Habsurd destruct 2466 2467  *: #irrelevant1 #irrelevant2 #Habsurd destruct ] 2467 2468  2: (* Kseq stm' k' *) … … 2528 2529 (free_list m (blocks_of_env en)))} @conj 2529 2530 [ 1: //  2: %3 @cc_call // ] 2530  3, 4,9: #irrelevant #Habsurd destruct (Habsurd)2531  3,8: #irrelevant #Habsurd destruct (Habsurd) 2531 2532  *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ] 2532 2533 ] … … 2756 2757 [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta 2757 2758 whd in match (ret ??) in ⊢ (% → %); 2758 [ 2: #sz #sg  3: #fl  4: #ty'  5: #ty #n  6:#tl #ty'2759  7: #id #fl  8: #id #fl  9:#id ]2759 [  #sz #sg  #ty'  #ty #n  #tl #ty' 2760  #id #fl  #id #fl  #id ] 2760 2761 #H destruct (H) 2761 2762 %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))} … … 2897 2898 whd in match (exec_step ??) in ⊢ (% → %); 2898 2899 #Habsurd destruct (Habsurd) 2899 ] qed. 2900 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.