Changeset 1316 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Oct 7, 2011, 12:26:39 PM (9 years ago)
Author:
campbell
Message:

Merge in id-lookup-branch to trunk.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src

  • src/Cminor/syntax.ma

    r1224 r1316  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
     4include "utilities/lists.ma".
     5include "utilities/option.ma".
    46
    57(* TODO: consider making the typing stricter. *)
     
    1315| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    1416| Ecost : ∀t. costlabel → expr t → expr t.
     17
     18(* Assert a predicate on every variable or parameter identifier. *)
     19let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
     20match e with
     21[ Id _ i ⇒ P i
     22| Cst _ _ ⇒ True
     23| Op1 _ _ _ e ⇒ expr_vars ? e P
     24| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     25| Mem _ _ _ e ⇒ expr_vars ? e P
     26| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
     27| Ecost _ _ e ⇒ expr_vars ? e P
     28].
     29
     30lemma expr_vars_mp : ∀t,e,P,Q.
     31  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
     32#t0 #e elim e normalize /3/
     33[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     34  % /3/
     35| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
     36] qed.
     37
     38axiom Label : String.
    1539
    1640inductive stmt : Type[0] ≝
     
    2953| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    3054| St_return : option (Σt. expr t) → stmt
    31 | St_label : ident → stmt → stmt
    32 | St_goto : ident → stmt
     55| St_label : identifier Label → stmt → stmt
     56| St_goto : identifier Label → stmt
    3357| St_cost : costlabel → stmt → stmt.
     58
     59let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
     60match s with
     61[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     62| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
     63| St_loop s' ⇒ P s ∧ stmt_P P s'
     64| St_block s' ⇒ P s ∧ stmt_P P s'
     65| St_label _ s' ⇒ P s ∧ stmt_P P s'
     66| St_cost _ s' ⇒ P s ∧ stmt_P P s'
     67| _ ⇒ P s
     68].
     69
     70lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
     71#P * normalize /2/
     72[ #s1 #s2 * * /2/
     73| #sz #sg #e #s1 #s2 * * /2/
     74| 3,4: #s * /2/
     75| 5,6: #i #s normalize * /2/
     76] qed.
     77
     78(* Assert a predicate on every variable or parameter identifier. *)
     79definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     80λP,s.
     81match s with
     82[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     83| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
     84| 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
     85| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     86| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
     87| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     88| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     89| _ ⇒ True
     90].
     91
     92definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
     93λP,s.
     94match s with
     95[ St_label l _ ⇒ P l
     96| St_goto l ⇒ P l
     97| _ ⇒ True
     98].
     99
     100lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
     101#P #Q #H #s elim s /2/
     102[ #s1 #s2 #H1 #H2 normalize * * /4/
     103| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
     104| #s #H * /5/
     105| #s #H * /5/
     106| #l #s #H * /5/
     107| #l #s #H * /5/
     108] qed.
     109
     110lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
     111#P #Q #H #s elim s normalize
     112[ //
     113| #t #id #e * /4/
     114| #t #r #q #e1 #e2 * /4/
     115| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     116| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     117| #s1 #s2 #H1 #H2 * /3/
     118| #sz #sg #e #s1 #s2 #H1 #H2 /5/
     119| 8,9: #s #H1 #H2 /2/
     120| //
     121| /5/
     122| * normalize [ // | *; normalize /3/ ]
     123| /2/
     124| //
     125| /2/
     126] qed.
     127
     128lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
     129#P #Q #H #s elim s normalize /2/ qed.
     130
     131(* Get labels from a Cminor statement. *)
     132let rec labels_of (s:stmt) : list (identifier Label) ≝
     133match s with
     134[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     135| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     136| St_loop s ⇒ labels_of s
     137| St_block s ⇒ labels_of s
     138| St_label l s ⇒ l::(labels_of s)
     139| St_cost _ s ⇒ labels_of s
     140| _ ⇒ [ ]
     141].
    34142
    35143record internal_function : Type[0] ≝
     
    39147; f_stacksize : nat
    40148; f_body      : stmt
     149; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
     150                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    41151}.
    42152
Note: See TracChangeset for help on using the changeset viewer.