Changeset 1316 for src/Cminor/syntax.ma
 Timestamp:
 Oct 7, 2011, 12:26:39 PM (8 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src

Property
svn:mergeinfo
set to
/Deliverables/D3.3/idlookupbranch merged eligible

Property
svn:mergeinfo
set to

src/Cminor/syntax.ma
r1224 r1316 2 2 include "common/FrontEndOps.ma". 3 3 include "common/CostLabel.ma". 4 include "utilities/lists.ma". 5 include "utilities/option.ma". 4 6 5 7 (* TODO: consider making the typing stricter. *) … … 13 15  Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t 14 16  Ecost : ∀t. costlabel → expr t → expr t. 17 18 (* Assert a predicate on every variable or parameter identifier. *) 19 let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝ 20 match 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 30 lemma 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 38 axiom Label : String. 15 39 16 40 inductive stmt : Type[0] ≝ … … 29 53  St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt 30 54  St_return : option (Σt. expr t) → stmt 31  St_label : ident → stmt → stmt32  St_goto : ident → stmt55  St_label : identifier Label → stmt → stmt 56  St_goto : identifier Label → stmt 33 57  St_cost : costlabel → stmt → stmt. 58 59 let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ 60 match 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 70 lemma 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. *) 79 definition stmt_vars : (ident → Prop) → stmt → Prop ≝ 80 λP,s. 81 match 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 92 definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝ 93 λP,s. 94 match s with 95 [ St_label l _ ⇒ P l 96  St_goto l ⇒ P l 97  _ ⇒ True 98 ]. 99 100 lemma 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 110 lemma 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 128 lemma 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. *) 132 let rec labels_of (s:stmt) : list (identifier Label) ≝ 133 match 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 ]. 34 142 35 143 record internal_function : Type[0] ≝ … … 39 147 ; f_stacksize : nat 40 148 ; 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 41 151 }. 42 152
Note: See TracChangeset
for help on using the changeset viewer.