Changeset 1626 for src/Cminor/syntax.ma
 Timestamp:
 Dec 19, 2011, 2:48:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/syntax.ma
r1605 r1626 16 16 17 17 (* Assert a predicate on every variable or parameter identifier. *) 18 let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝18 let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝ 19 19 match e with 20 [ Id _ i ⇒ P i20 [ Id t i ⇒ P i t 21 21  Cst _ _ ⇒ True 22 22  Op1 _ _ _ e ⇒ expr_vars ? e P … … 28 28 29 29 lemma expr_vars_mp : ∀t,e,P,Q. 30 (∀i . P i → Q i) → expr_vars t e P → expr_vars t e Q.30 (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q. 31 31 #t0 #e elim e normalize /3/ 32 32 [ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2 … … 42 42  St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt 43 43 (* ident for returned value, expression to identify fn, args. *) 44  St_call : option ident→ expr (ASTptr Code) → list (𝚺t. expr t) → stmt44  St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt 45 45  St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt 46 46  St_seq : stmt → stmt → stmt … … 76 76 77 77 (* Assert a predicate on every variable or parameter identifier. *) 78 definition stmt_vars : (ident → Prop) → stmt → Prop ≝78 definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝ 79 79 λP,s. 80 80 match s with 81 [ St_assign _ i e ⇒ P i∧ expr_vars ? e P81 [ St_assign t i e ⇒ P i t ∧ expr_vars ? e P 82 82  St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 83  St_call oi e es ⇒ match oi with [ None ⇒ True  Some i ⇒ P i] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es83  St_call oi e es ⇒ match oi with [ None ⇒ True  Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es 84 84  St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es 85 85  St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P … … 107 107 ] qed. 108 108 109 lemma stmt_vars_mp : ∀P,Q. (∀i . P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.109 lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s. 110 110 #P #Q #H #s elim s normalize 111 111 [ // … … 146 146 ; f_stacksize : nat 147 147 ; f_body : stmt 148 ; f_inv : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧ 148 (* Ensure that variables appear in the params and vars list with the 149 correct typ; and that all goto labels used are declared. *) 150 ; f_inv : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧ 149 151 stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body 150 152 }.
Note: See TracChangeset
for help on using the changeset viewer.