Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r485 r487  
    55include "IOMonad.ma".
    66
     7(*
    78include "Plogic/russell_support.ma".
    8 
    9 ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
     9*)
     10definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
    1011  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
    1112
    12 ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝
     13definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝
    1314  λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.
    14   (match a return λa'.a=a' → res (sigma A P) with
     15  (match a return λa'.a=a' → res (Sig A P) with
    1516   [ None ⇒ λe1.?
    1617   | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
    1718     [ Error ⇒ λ_. Error ?
    18      | OK c ⇒ λe2. OK ? (sig_intro A P c ?)
     19     | OK c ⇒ λe2. OK ? (dp A P c ?)
    1920     ]) (refl ? b)
    2021   ]) (refl ? a).
    21 ##[ nrewrite > e1 in p; nnormalize; *;
    22 ##| nrewrite > e1 in p; nrewrite > e2; nnormalize; //
    23 ##] nqed.
    24 
    25 ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝
     22[ >e1 in p; normalize; *;
     23| >e1 in p >e2 normalize; //
     24] qed.
     25
     26definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝
    2627  λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒
    27     match b with [ sig_intro w p ⇒ OK ? w] ].
    28 
    29 ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝
    30   λA,P,a.match a with [ sig_intro w p ⇒ w].
    31 
    32 ncoercion err_inject :
    33   ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject
    34   on a:option (res ?) to res (sigma ? ?).
    35 ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject
    36   on _c:res (sigma ? ?) to res ?.
    37 ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject
    38   on _c:sigma ? ? to ?.
    39 
    40 ndefinition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
     28    match b with [ dp w p ⇒ OK ? w] ].
     29
     30definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝
     31  λA,P,a.match a with [ dp w p ⇒ w].
     32
     33coercion err_inject :
     34  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject
     35  on a:option (res ?) to res (Sig ? ?).
     36coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject
     37  on _c:res (Sig ? ?) to res ?.
     38coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
     39  on _c:Sig ? ? to ?.
     40
     41definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
    4142  λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ].
    4243
    43 ndefinition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
     44definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
    4445  λv,ty. match v in val with
    4546  [ Vint i ⇒ match ty with
     
    6263  ].
    6364
    64 nlemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
    65 #v ty r H; nelim H; #v t H'; nelim H';
    66   ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    67   ##| #p b i i0 s; @ true; @; //
    68   ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    69   ##| #i s; @ false; @; //;
    70   ##| #r r' t; @ false; @; //;
    71   ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    72   ##]
    73 nqed.
     65lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
     66#v #ty #r #H elim H; #v #t #H' elim H';
     67  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
     68  | #p #b #i #i0 #s %{ true} % //
     69  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
     70  | #i #s %{ false} % //;
     71  | #r #r' #t %{ false} % //;
     72  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
     73  ]
     74qed.
    7475
    7576(* Prove a few minor results to make proof obligations easy. *)
    7677
    77 nlemma bind_OK: ∀A,B,P,e,f.
     78lemma bind_OK: ∀A,B,P,e,f.
    7879  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    7980  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
    80 #A B P e f; nelim e; /2/; nqed.
    81 
    82 nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
    83   (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    84   match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
    85 #A B P P' e f; nelim e;
    86 ##[ #v0; nelim v0; #v Hv IH; napply IH;
    87 ##| #_; napply I;
    88 ##] nqed.
    89 
    90 nlemma bind2_OK: ∀A,B,C,P,e,f.
     81#A #B #P #e #f elim e; /2/; qed.
     82
     83lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
     84  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
     85  match bind (Sig A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
     86#A #B #P #P' #e #f elim e;
     87[ #v0 elim v0; #v #Hv #IH @IH
     88| #_ @I
     89] qed.
     90
     91lemma bind2_OK: ∀A,B,C,P,e,f.
    9192  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    9293  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
    93 #A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
    94 
    95 nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
     94#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
     95
     96lemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (Sig (A×B) P). ∀f:A → B → res C.
    9697  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    9798  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
    98 #A B C P P' e f; nelim e; //;
    99 #v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
    100 
    101 nlemma opt_bind_OK: ∀A,B,P,e,f.
     99#A #B #C #P #P' #e #f elim e; //;
     100#v0 elim v0; #v elim v; #v1 #v2 #Hv #IH @IH //; qed.
     101
     102lemma opt_bind_OK: ∀A,B,P,e,f.
    102103  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
    103104  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
    104 #A B P e f; nelim e; nnormalize; /2/; nqed.
    105 
    106 nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
     105#A #B #P #e #f elim e; normalize; /2/; qed.
     106(*
     107lemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
    107108  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
    108   match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
    109 #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
    110 ##[ #H; napply (False_ind … H);
    111 ##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
    112 ##] nqed.
    113 
     109  match match eject ?? e with [ pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
     110#A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
     111[ #H @(False_ind … H)
     112| #e'' cases e''; #a #b #Pab #H normalize; /2/;
     113] qed.
     114*)
    114115(*
    115116nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
    116 #A B e; ncases e; //; nqed.
     117#A #B #e cases e; //; qed.
    117118*)
    118119
    119 ndefinition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
     120definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
    120121λm:mem. λi:int. λty:type. λty':type.
    121122match eq i zero with
     
    134135].
    135136
    136 ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
     137definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
    137138λm:mem. λv:val. λty:type. λty':type.
    138139match v with
     
    165166| Vptr p b ofs ⇒
    166167    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    167     do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
     168    do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
    168169    do s' ← match ty' with
    169170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
     
    174175| Vnull r ⇒
    175176    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
    176     do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
     177    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
    177178    do s' ← match ty' with
    178179         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
     
    182183].
    183184
    184 ndefinition load_value_of_type' ≝
    185 λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
     185definition load_value_of_type' ≝
     186λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair psp loc ⇒
    186187  load_value_of_type ty m psp loc ofs ] ].
    187188
     
    190191   and use exec_lvalue'. *)
    191192
    192 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
     193let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
    193194match e with
    194195[ Expr e' ty ⇒
     
    210211  | Eaddrof a ⇒
    211212      do 〈plo,tr〉 ← exec_lvalue ge en m a;
    212       OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
     213      OK ? 〈match plo with [ pair pl ofs ⇒ match pl with [ pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
    213214  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
    214215  | Eunop op a ⇒
     
    282283match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    283284
    284 nlemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
    285 #A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed.
     285lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
     286#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
    286287
    287288(* We define a special induction principle tailored to the recursive definition
    288289   above. *)
    289290
    290 ndefinition is_not_lvalue: expr_descr → Prop ≝
     291definition is_not_lvalue: expr_descr → Prop ≝
    291292λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
    292293
    293 ndefinition Plvalue ≝ λP:(expr → Prop).λe,ty.
     294definition Plvalue ≝ λP:(expr → Prop).λe,ty.
    294295match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
    295296
    296297(* TODO: Can we do this sensibly with a map combinator? *)
    297 nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
     298let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
    298299match l with
    299300[ nil ⇒ OK ? 〈nil val, E0〉
     
    304305].
    305306
    306 (* Don't really want to use subset rather than sigma here, but can't be bothered
    307    with *another* set of coercions. XXX: why do I have to get the recursive
    308    call's property manually? *)
    309 
    310 nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝
     307let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
    311308match l with
    312 [ nil ⇒ Some ? 〈en, m〉
     309[ nil ⇒ 〈en, m〉
    313310| cons h vars ⇒
    314   match h with [ mk_pair id ty ⇒
    315     match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
    316       match exec_alloc_variables (set … id b1 en) m1 vars with
    317       [ sig_intro r p ⇒ r ]
    318 ]]]. nwhd;
    319 ##[ //;
    320 ##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
    321     #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    322 napply (alloc_variables_cons … IH); /2/;
    323 nqed.
     311  match h with [ pair id ty ⇒
     312    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
     313      exec_alloc_variables (set … id b1 en) m1 vars
     314]]].
    324315
    325316(* TODO: can we establish that length params = length vs in advance? *)
    326 nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2)
     317let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem
    327318  match params with
    328   [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
    329   | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
     319  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? ]
     320  | cons idty params' ⇒ match idty with [ pair id ty ⇒
    330321      match vs with
    331       [ nil ⇒ Some ? (Error ?)
    332       | cons v1 vl ⇒ Some ? (
     322      [ nil ⇒ Error ?
     323      | cons v1 vl ⇒
    333324          do b ← opt_to_res ? (get … id e);
    334325          do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
    335           err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
     326          exec_bind_parameters e m1 params' vl
    336327      ]
    337328  ] ].
    338 nwhd; //;
    339 napply opt_bind_OK; #b eb;
    340 napply opt_bind_OK; #m1 em1;
    341 napply sig_bind_OK; #m2 Hm2;
    342 napply (bind_parameters_cons … eb em1 Hm2);
    343 nqed.
    344 
    345 alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
    346 alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
    347 ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
    348 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    349 ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
    350 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    351 ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    352 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    353 
    354 nlet rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
     329
     330definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
     331#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
     332definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
     333#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
     334definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
     335#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
     336
     337let rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝
    355338match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    356339[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     
    424407        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    425408        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    426 ]. ndestruct; //; nqed.
    427 
    428 ndefinition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
     409]. destruct; //; qed.
     410
     411definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
    429412λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
    430413
    431 nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     414let rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
    432415match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
    433416[ Kstop ⇒ ?
     
    435418| _ ⇒ ?
    436419].
    437 ##[ ##1,8: @1; //
    438 ##| ##*: @2; /2/
    439 ##] nqed.
    440 
    441 ndefinition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
     420[ 1,8: %1 ; //
     421| *: %2 ; /2/
     422] qed.
     423
     424definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
    442425λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
    443426[ Sskip ⇒ inl ?? (refl ??)
    444427| _ ⇒ inr ?? (nmk ? (λH.?))
    445 ]. ndestruct;
    446 nqed.
     428]. destruct
     429qed.
    447430
    448431(* Checking types of values given to / received from an external function call. *)
    449432
    450 ndefinition eventval_type : ∀ty:typ. Type
     433definition eventval_type : ∀ty:typ. Type[0]
    451434λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
    452435
    453 ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
     436definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    454437λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
    455438
    456 ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
     439definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    457440λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
    458441
    459 nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
     442lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    460443  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    461 #ty; ncases ty; nnormalize; //; nqed.
    462 
    463 ndefinition convert_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v)
     444#ty cases ty; normalize; //; qed.
     445
     446definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val
    464447λev,ty.
    465448match ty with
    466 [ ASTint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
    467 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
    468 | _ ⇒ Some ? (Error ?)
    469 ]. nwhd; //; nqed.
    470 
    471 ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v)
     449[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
     450| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
     451| _ ⇒ Error ?
     452].
     453
     454definition check_eventval' : ∀v:val. ∀ty:typ. res eventval
    472455λv,ty.
    473456match ty with
    474 [ ASTint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
    475 | ASTfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
     457[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
     458| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    476459| _ ⇒ Some ? (Error ?)
    477 ]. nwhd; //; nqed.
    478 
    479 nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
     460].
     461
     462let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    480463match vs with
    481 [ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
     464[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
    482465| cons v vt ⇒
    483466  match tys with
    484   [ nil ⇒ Some ? (Error ?)
    485   | cons ty tyt ⇒ Some ? (
     467  [ nil ⇒ Error ?
     468  | cons ty tyt ⇒
    486469    do ev ← check_eventval' v ty;
    487470    do evt ← check_eventval_list vt tyt;
    488     OK ? ((sig_eject ?? ev)::evt))
    489   ]
    490 ]. nwhd; //;
    491 napply sig_bind_OK; #ev Hev;
    492 napply sig_bind_OK; #evt Hevt;
    493 nnormalize; /2/;
    494 nqed.
     471    OK ? (ev::evt)
     472  ]
     473].
    495474
    496475(* IO monad *)
     
    498477(* Interactions are function calls that return a value and do not change
    499478   the rest of the Clight program's state. *)
    500 nrecord io_out : Type
     479record io_out : Type[0]
    501480{ io_function: ident
    502481; io_args: list eventval
     
    504483}.
    505484
    506 ndefinition io_in ≝ λo. eventval_type (io_in_typ o).
    507 
    508 ndefinition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
     485definition io_in ≝ λo. eventval_type (io_in_typ o).
     486
     487definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
    509488λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
    510489
    511 ndefinition ret: ∀T. T → (IO io_out io_in T) ≝
     490definition ret: ∀T. T → (IO io_out io_in T) ≝
    512491λT,x.(Value ?? T x).
    513492
    514493(* execution *)
    515494
    516 ndefinition store_value_of_type' ≝
     495definition store_value_of_type' ≝
    517496λty,m,l,v.
    518 match l with [ mk_pair pl ofs ⇒
    519   match pl with [ mk_pair pcl loc ⇒
     497match l with [ pair pl ofs ⇒
     498  match pl with [ pair pcl loc ⇒
    520499    store_value_of_type ty m pcl loc ofs v ] ].
    521500
    522 nlet rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
     501let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
    523502match st with
    524503[ State f s k e m ⇒
     
    639618  | Sgoto lbl ⇒
    640619      match find_label lbl (fn_body f) (call_cont k) with
    641       [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
     620      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
    642621      | None ⇒ Wrong ???
    643622      ]
     
    647626  match f0 with
    648627  [ Internal f ⇒
    649     match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
    650       ! m2 ← err_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs);
     628    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
     629      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
    651630      ret ? 〈E0, State f (fn_body f) k e m2〉
    652631    ]
    653632  | External f argtys retty ⇒
    654       ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
     633      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
    655634      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
    656635      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
     
    662641    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    663642    | Some r' ⇒
    664       match r' with [ mk_pair l ty ⇒
     643      match r' with [ pair l ty ⇒
    665644       
    666645          ! m' ← store_value_of_type' ty m l res;
     
    672651].
    673652
    674 nlet rec make_initial_state (p:clight_program) : res (genv × state) ≝
     653let rec make_initial_state (p:clight_program) : res (genv × state) ≝
    675654  do ge ← globalenv Genv ?? p;
    676655  do m0 ← init_mem Genv ?? p;
    677656  do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    678   do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
     657  do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? it | inr _ ⇒ None ? ]);
    679658  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    680659  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    681660
    682 ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
    683 #st; nelim st;
    684 ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
    685 ##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
    686 ##| #v k m; ncases k;
    687   ##[ ncases v;
    688     ##[ ##2: #i; @1; @ i; //;
    689     ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    690     ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    691     ##| #r; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    692     ##| #r b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    693     ##]
    694   ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
    695   ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
    696   ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
    697   ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
    698   ##]
    699 ##] nqed.
    700 
    701 nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
     661definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
     662#st elim st;
     663[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
     664| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
     665| #v #k #m cases k;
     666  [ cases v;
     667    [ 2: #i %1 ; %{ i} //;
     668    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     669    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     670    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     671    | #r #b #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
     672    ]
     673  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
     674  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
     675  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
     676  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
     677  ]
     678] qed.
     679
     680let rec exec_steps (n:nat) (ge:genv) (s:state) :
    702681 IO io_out io_in (trace×state) ≝
    703682match is_final_state s with
     
    724703
    725704(* A (possibly non-terminating) execution.   *)
    726 ncoinductive execution : Type
     705coinductive execution : Type[0]
    727706| e_stop : trace → int → mem → execution
    728707| e_step : trace → state → execution → execution
     
    730709| e_interact : ∀o:io_out. (io_in o → execution) → execution.
    731710
    732 ndefinition mem_of_state : state → mem ≝
     711definition mem_of_state : state → mem ≝
    733712λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    734713
     
    737716   state. *)
    738717
    739 nlet corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
     718let corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
    740719match s with
    741720[ Wrong ⇒ e_wrong
    742 | Value v ⇒ match v with [ mk_pair t s' ⇒
     721| Value v ⇒ match v with [ pair t s' ⇒
    743722    match is_final_state s' with
    744723    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
     
    748727
    749728
    750 ndefinition exec_inf : clight_program → execution ≝
     729definition exec_inf : clight_program → execution ≝
    751730λp.
    752731  match make_initial_state p with
     
    755734  ].
    756735
    757 nremark execution_cases: ∀e.
     736lemma execution_cases: ∀e.
    758737 e = match e with [ e_stop tr r m ⇒ e_stop tr r m | e_step tr s e ⇒ e_step tr s e
    759738 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
    760 #e; ncases e; //; nqed.
    761 
    762 nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
     739#e cases e; //; qed.
     740
     741lemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
    763742match s with
    764743[ Wrong ⇒ e_wrong
    765 | Value v ⇒ match v with [ mk_pair t s' ⇒
     744| Value v ⇒ match v with [ pair t s' ⇒
    766745    match is_final_state s' with
    767746    [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
     
    769748| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    770749].
    771 #ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s;
    772 ##[ #o k
    773 ##| #x; ncases x; #tr s'; ncases s';
    774   ##[ #fn st k env m
    775   ##| #fd args k mem
    776   ##| #v k mem; (* for final state check *) ncases k;
    777     ##[ ncases v; ##[ ##2,3: #v' ##| ##4: #r ##| ##5: #sp loc off ##]
    778     ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##]
    779   ##]
    780 ##| ##]
    781 nwhd in ⊢ (??%%); //;
    782 nqed.
    783 
     750#ge #s >(execution_cases (exec_inf_aux …)) cases s;
     751[ #o #k
     752| #x cases x; #tr #s' cases s';
     753  [ #fn #st #k #env #m
     754  | #fd #args #k #mem
     755  | #v #k #mem (* for final state check *) cases k;
     756    [ cases v; [ 2,3: #v' | 4: #r | 5: #sp #loc #off ]
     757    | #s' #k' | 3,4: #e #s' #k' | 5,6: #e #s' #s'' #k' | #k' | #a #b #c #d ]
     758  ]
     759| ]
     760whd in ⊢ (??%%); //;
     761qed.
     762
Note: See TracChangeset for help on using the changeset viewer.