Changeset 1626 for src/Cminor/syntax.ma
- Timestamp:
- Dec 19, 2011, 2:48:33 PM (9 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.