Changeset 2353 for src/Clight/labelSimulation.ma
 Timestamp:
 Sep 26, 2012, 6:14:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2338 r2353 264 264  cwl_stop : cont_with_labels Kstop Kstop 265 265  cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k') 266  cwl_while : ∀ue,e,us,s,c s,cpost,k,k'.266  cwl_while : ∀ue,e,us,s,cl,cs,cpost,k,k'. 267 267 cont_with_labels k k' → 268 cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k')) 268 (cl = None ? ∨ cl = Some ? cpost) → 269 cont_with_labels (Kwhile e s cl k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Some ? cpost) k') 269 270  cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'. 270 271 cont_with_labels k k' → … … 291 292 (* Extra matching states that we can reach that don't quite correspond to the 292 293 labelling function *) 293  swl_whilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → 294 state_with_labels_partial (State f (Swhile a s) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) 294  swl_whilestate : ∀g,f,ua,a,us,s,cl,cs,cpost,k,k',e,m. cont_with_labels k k' → 295 (cl = None ? ∨ cl = Some ? cpost) → 296 state_with_labels_partial (State f (Swhile a s cl) k e m) (State (\fst (label_function g f)) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us))) (Some ? cpost)) k' e m) 295 297  swl_dowhilestate : ∀g,f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → 296 298 state_with_labels_partial (State f (Sdowhile a s) k e m) (State (\fst (label_function g f)) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) … … 432 434  Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2))) 433 435  Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3)))) 434  Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))436  Swhile e s1 cl ⇒ ∀u1,u2,cs,cpost. cl = None ? ∨ cl = Some ? cpost → P (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2))) (Some ? cpost)) 435 437  Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip)) 436 438  Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip)) … … 447 449 @label_gen_elim #u2 // 448 450 [ 6: >shift_fst // 451  3: @label_gen_elim #u3 >shift_fst >shift_fst 452 cases C in E ⊢ %; /3/ 449 453  *: @label_gen_elim #u3 // 450 454 @label_gen_elim #u4 451 455 [ @label_gen_elim #u5 >shift_fst >shift_fst // 452  2,3:>shift_fst >shift_fst //456  >shift_fst >shift_fst // 453 457  @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst // 454 458 ] … … 529 533 @refl  // ] skip ] skip ] skip ] 530 534 ] 531  #e #s0 # IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost535  #e #s0 #cl #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost #CL 532 536 whd in match (find_label ?? k); normalize in match (find_label ?? k'); 533 537 @(lfl_IH s0 … IH) [ /2/ ] … … 671 675  #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{0} whd 672 676 whd in EX:(??%%); destruct /4/ 673  #ue #e0 #us0 #s0 #c s #cpost #k0 #k0' #K#_ #E1 #E2 #E3 destruct %{0}677  #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K #CL #_ #E1 #E2 #E3 destruct %{0} 674 678 whd in EX:(??%%); destruct whd /4/ 675 679  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct … … 761 765 whd in ⊢ (??%?); >label_expr_type >EX2 762 766 whd in ⊢ (??%?); % [1,3: <(E0_right tr) ] /4/ 763  #a #st # EX767  #a #st #cl #EX 764 768 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 765 769 cases (bindIO_inversion ??????? EX) EX * * #EX2 #EX 766 770 normalize in EX; destruct 767 whd in match (label_statement ??); @label_gen_elim #u1 768 @label_gen_elim #u2 769 whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 770 >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 771 >shift_fst 772 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 773 [ %{2}  %{3} ] whd 771 @blindly_label #u1 #u2 #cs #cpost * #CL destruct 772 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u1) #tr1' * #EX1' #T1 773 [ 1,2,3: %{1}  %{0} ] whd 774 774 whd in ⊢ (??%?); >EX1' 775 775 whd in ⊢ (??%?); >label_expr_type >EX2 776 whd in ⊢ (??%?); % [ 1,3: <(E0_right tr) ] /5/776 whd in ⊢ (??%?); whd % [ 1,3,5,7: <(E0_right tr) ] /5 by twel_new, swl_partial, swl_state, cwl_while, twel_app, or_introl, or_intror/ 777 777  #a #st #EX 778 778 normalize in EX; destruct … … 805 805 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 806 806 #u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 807  #ue #e0 #us0 #s0 #c s #cpost #k0 #k0' #K'#_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct807  #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 808 808  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 809 809  #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 815 815 ] 816 816 whd in match (label_statement ??); 817 [ 1, 6,7: %{0} % /3/818  2, 3,5: %{2}% /3/819  %{1}% /3/817 [ 1,3,7,8: %{0} % /3/ 818  2,5: %{1} whd % /3/ 819  4,6: %{2} whd % /3/ 820 820 ] 821 821  #EX inversion KL 822 822 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 823 823 #u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 824  #ue #e0 #us0 #s0 #c s #cpost #k0 #k0' #K'#_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct824  #ue #e0 #us0 #s0 #cl #cs #cpost #k0 #k0' #K' * #CL #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 825 825  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 826 826  #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 832 832 ] 833 833 whd in match (label_statement ??); 834 [ 1,2, 5,6,7: %{0} % /4/835  4: %{1} % /4/834 [ 1,2,3,6,7,8: %{0} % /4/ 835  5: %{1} % /4/ 836 836  cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 837 837 cases (bindIO_inversion ??????? EX) EX * * #EX2 #EX … … 897 897 %{0} % /3/ 898 898 ] 899  #u0 #f #ua #a #us #s #c s #cpost #k #k' #e #m #K#EX899  #u0 #f #ua #a #us #s #cl #cs #cpost #k #k' #e #m #K * #CL #EX 900 900 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 901 901 cases (bindIO_inversion ??????? EX) EX * * #EX2 #EX 902 902 whd in EX:(??%%); destruct 903 903 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 904 [ %{1}  %{2} ] whd904 [ 4: %{0}  1,2,3: %{1} ] whd 905 905 whd in ⊢ (??%?); >EX1' 906 906 whd in ⊢ (??%?); >label_expr_type >EX2 907 % [ 1,3: <(E0_right tr) ] /4/907 whd % [ 1,3,5,7: <(E0_right tr) ] /5/ 908 908  #u0 #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX 909 909 whd in EX:(??%%); destruct … … 991 991 #ge #s cases s 992 992 [ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %; 993 [ 11,14: #a  2,4, 6,7,12,13,15: #a #b  3,5: #a #b #c  8: #a #b #c #d ]993 [ 11,14: #a  2,4,7,12,13,15: #a #b  3,5,6: #a #b #c  8: #a #b #c #d ] 994 994 whd in ⊢ (??%? → ?); 995 [ 4, 6,8,9: #EX destruct ]995 [ 4,5,7,8: #EX destruct ] 996 996 [ cases a 997 997 [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct … … 1001 1001  cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct 1002 1002  @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct 1003  4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct1004 1003  @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct 1005 1004  @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a 1006 1005 [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct 1006  6,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct 1007 1007  cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct 1008 1008  cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct … … 1038 1038 [ #s #s' #S' #E1 #E2 #E3 destruct inversion S' 1039 1039 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct 1040  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct1040  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct 1041 1041  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct 1042 1042  #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
Note: See TracChangeset
for help on using the changeset viewer.