Changeset 1147 for src/Clight/Cexec.ma
 Timestamp:
 Aug 30, 2011, 4:09:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r1139 r1147 7 7 include "Clight/TypeComparison.ma". 8 8 9 (*10 include "Plogic/russell_support.ma".11 12 definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝13 λA,P,a.match a with [ None ⇒ False  Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True  OK z ⇒ P z ]].14 15 definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝16 λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.17 (match a return λa'.a=a' → res (Sig A P) with18 [ None ⇒ λe1.?19  Some b ⇒ λe1.(match b return λb'.b=b' → ? with20 [ Error ⇒ λ_. Error ?21  OK c ⇒ λe2. OK ? (dp A P c ?)22 ]) (refl ? b)23 ]) (refl ? a).24 [ >e1 in p; normalize; *;25  >e1 in p >e2 normalize; //26 ] qed.27 28 definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝29 λA,P,a.match a with [ Error m ⇒ Error ? m  OK b ⇒30 match b with [ dp w p ⇒ OK ? w] ].31 32 definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝33 λA,P,a.match a with [ dp w p ⇒ w].34 35 coercion err_inject :36 ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject37 on a:option (res ?) to res (Sig ? ?).38 coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject39 on _c:res (Sig ? ?) to res ?.40 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject41 on _c:Sig ? ? to ?.42 *)43 9 definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝ 44 10 λA,P,a. match a with [ Error _ ⇒ True  OK v ⇒ P v ]. … … 181 147 λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ]. 182 148 183 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with184 a structurally smaller value, we break out the surrounding Expr constructor185 and use exec_lvalue'. *)186 187 149 axiom BadlyTypedTerm : String. 188 150 axiom UnknownIdentifier : String. … … 190 152 axiom FailedLoad : String. 191 153 axiom FailedOp : String. 154 155 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with 156 a structurally smaller value, we break out the surrounding Expr constructor 157 and use exec_lvalue'. *) 192 158 193 159 let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝ … … 584 550  S n' ⇒ 585 551 ! 〈t,s'〉 ← exec_step ge s; 586 (* ! 〈t,s'〉 ← match s with 587 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ] 588  Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ] 589  Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ] 590 ] ;*) 591 ! 〈t',s''〉 ← match s' with 592 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ] 593  Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ] 594  Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ] 595 ] ; 596 (* ! 〈t',s''〉 ← exec_steps n' ge s';*) 552 ! 〈t',s''〉 ← exec_steps n' ge s'; 597 553 ret ? 〈t ⧺ t',s''〉 598 554 ]
Note: See TracChangeset
for help on using the changeset viewer.