Changeset 1153 for Deliverables/D3.3/idlookupbranch/Clight/Cexec.ma
 Timestamp:
 Aug 30, 2011, 6:55:12 PM (8 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch
 Property svn:mergeinfo changed
/src merged: 11101132,11361150
 Property svn:mergeinfo changed

Deliverables/D3.3/idlookupbranch/Clight/Cexec.ma
r1058 r1153 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) ≝ … … 534 500 535 501 let rec make_initial_state (p:clight_program) : res (genv × state) ≝ 536 do ge ← globalenv Genv ?? p;537 do m0 ← init_mem Genv ?? p;502 do ge ← globalenv Genv ?? (fst ??) p; 503 do m0 ← init_mem Genv ?? (fst ??) p; 538 504 do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); 539 505 do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); … … 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.