Changeset 2025 for src/RTLabs
 Timestamp:
 Jun 7, 2012, 3:51:11 PM (8 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1960 r2025 563 563 well_cost_labelled_state s → 564 564 well_cost_labelled_state s'. 565 #ge #s #tr' #s' #EV cases (eval_p erserves … EV)565 #ge #s #tr' #s' #EV cases (eval_preserves … EV) 566 566 [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // 567 567  #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ … … 772 772 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 773 773 stack_preserved doesnt_end_with_ret s1 s2. 774 #ge0 #s1 #s2 #tr #CL #EV inversion (eval_p erserves … EV)774 #ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV) 775 775 [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/ 776 776  #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/ … … 794 794 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct 795 795  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct 796 inversion (eval_p erserves … EV)796 inversion (eval_preserves … EV) 797 797 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct 798 798  #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct … … 808 808 ] 809 809  #s1 #r #S1 #E1 #E2 #E3 #_ destruct 810 inversion (eval_p erserves … EV)810 inversion (eval_preserves … EV) 811 811 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct 812 812  #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct … … 834 834 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct 835 835  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct 836 inversion (eval_p erserves … EV)836 inversion (eval_preserves … EV) 837 837 [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct 838 838  #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct … … 848 848 ] 849 849  #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd 850 inversion (eval_p erserves … EV)850 inversion (eval_preserves … EV) 851 851 [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct 852 852  #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct … … 1446 1446 *) 1447 1447 @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct 1448 inversion (eval_p erserves … EVAL)1448 inversion (eval_preserves … EVAL) 1449 1449 [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct 1450 1450 >(eval_steps … EVAL) in E2; #En normalize in En; … … 1471 1471 /3/ 1472 1472  #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct 1473 #EVAL #NC %2 inversion (eval_p erserves … EVAL)1473 #EVAL #NC %2 inversion (eval_preserves … EVAL) 1474 1474 [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct 1475 1475  #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct … … 1526 1526 soundly_labelled_state s'. 1527 1527 #ge #s #tr #s' #ENV #EV #S 1528 inversion (eval_p erserves … EV)1528 inversion (eval_preserves … EV) 1529 1529 [ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct 1530 1530 whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S … … 1632 1632 RTLabs_is_final s' = None ?. 1633 1633 #ge #s #tr #s' #EV 1634 inversion (eval_p erserves … EV) //1634 inversion (eval_preserves … EV) // 1635 1635 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL 1636 1636 @⊥ @(absurd ?? CL) @refl … … 1718 1718  #s1 #r #S #E1 #E2 #E3 #E4 TERMINATES destruct 1719 1719 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct 1720 inversion (eval_p erserves … EV)1720 inversion (eval_preserves … EV) 1721 1721 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 TRACE_OK destruct ] 1722 1722 #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 TRACE_OK destruct … … 1831 1831 @bind_ok #f #_ 1832 1832 #E destruct 1833 #EV #SP inversion (eval_p erserves … EV)1833 #EV #SP inversion (eval_preserves … EV) 1834 1834 [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct 1835 1835 inversion SP 
src/RTLabs/semantics.ma
r1999 r2025 1 2 (* XXX NB: I haven't checked all of these semantics against the prototype3 compilers yet! *)4 1 5 2 include "basics/lists/list.ma". … … 267 264 ] qed. 268 265 269 lemma eval_p erserves : ∀ge,s,tr,s'.266 lemma eval_preserves : ∀ge,s,tr,s'. 270 267 eval_statement ge s = Value ??? 〈tr,s'〉 → 271 268 state_rel ge s s'.
Note: See TracChangeset
for help on using the changeset viewer.