Ignore:
Timestamp:
Jul 25, 2011, 2:58:10 PM (9 years ago)
Author:
campbell
Message:

Experimental branch where lookups of local variables in Cminor code always
succeed.

File:
1 edited

Legend:

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

    r961 r1087  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
     4include "utilities/lists.ma".
     5include "utilities/option.ma".
     6
     7definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     8λtag,A,m,i. lookup … m i ≠ None ?.
    49
    510(* TODO: consider making the typing stricter. *)
     
    1318| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1419| Ecost : ∀t. costlabel → expr t → expr t.
     20
     21(* Assert a predicate on every variable or parameter identifier. *)
     22let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     23match e with
     24[ Id _ i ⇒ P i
     25| Cst _ _ ⇒ True
     26| Op1 _ _ _ e ⇒ expr_vars ? e P
     27| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     28| Mem _ _ _ e ⇒ expr_vars ? e P
     29| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
     30| Ecost _ _ e ⇒ expr_vars ? e P
     31].
     32
     33lemma expr_vars_mp : ∀t,e,P,Q.
     34  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     35#t0 #e elim e normalize /3/
     36[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     37  % /3/
     38| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
     39] qed.
    1540
    1641inductive stmt : Type[0] ≝
     
    3358| St_cost : costlabel → stmt → stmt.
    3459
     60(* Assert a predicate on every variable or parameter identifier. *)
     61let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝
     62match s with
     63[ St_skip ⇒ True
     64| St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     65| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     66| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     67| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     68| St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P
     69| St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P
     70| St_loop s ⇒ stmt_vars s P
     71| St_block s ⇒ stmt_vars s P
     72| St_exit _ ⇒ True
     73| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     74| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     75| St_label _ s ⇒ stmt_vars s P
     76| St_goto _ ⇒ True
     77| St_cost _ s ⇒ stmt_vars s P
     78].
     79
     80lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q.
     81#P #Q #H #s elim s normalize
     82[ //
     83| #t #id #e * /4/
     84| #t #r #q #e1 #e2 * /4/
     85| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     86| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     87| #s1 #s2 #H1 #H2 * /3/
     88| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     89| 8,9: #s #H1 #H2 /2/
     90| //
     91| /5/
     92| * normalize [ // | *; normalize /3/ ]
     93| /2/
     94| //
     95| /2/
     96] qed.
     97
    3598record internal_function : Type[0] ≝
    3699{ f_return    : option typ
     
    39102; f_stacksize : nat
    40103; f_body      : stmt
     104; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
    41105}.
    42106
Note: See TracChangeset for help on using the changeset viewer.