Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/Clight/Cexec.ma

    r1058 r1153  
    77include "Clight/TypeComparison.ma".
    88
    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) with
    18    [ None ⇒ λe1.?
    19    | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
    20      [ 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_inject
    37   on a:option (res ?) to res (Sig ? ?).
    38 coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject
    39   on _c:res (Sig ? ?) to res ?.
    40 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
    41   on _c:Sig ? ? to ?.
    42 *)
    439definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    4410  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
     
    181147λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
    182148
    183 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
    184    a structurally smaller value, we break out the surrounding Expr constructor
    185    and use exec_lvalue'. *)
    186 
    187149axiom BadlyTypedTerm : String.
    188150axiom UnknownIdentifier : String.
     
    190152axiom FailedLoad : String.
    191153axiom 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'. *)
    192158
    193159let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
     
    534500
    535501let 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;
    538504  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    539505  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    584550  | S n' ⇒
    585551      ! 〈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';
    597553      ret ? 〈t ⧺ t',s''〉
    598554  ]
Note: See TracChangeset for help on using the changeset viewer.