Changeset 1626 for src/Cminor/syntax.ma

Timestamp:

Dec 19, 2011, 2:48:33 PM (8 years ago)

Author:

campbell

Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:

• src/Cminor/syntax.ma (modified) (6 diffs)

src/Cminor/syntax.ma

@@ -16 +16 @@
 
 (* Assert a predicate on every variable or parameter identifier. *)
-let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
+let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
 match e with
-[ Id _ i ⇒ P i
+[ Id t i ⇒ P i t
 | Cst _ _ ⇒ True
 | Op1 _ _ _ e ⇒ expr_vars ? e P
@@ -28 +28 @@
 
 lemma expr_vars_mp : ∀t,e,P,Q.
-  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
+  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
 #t0 #e elim e normalize /3/ 
 [ #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
 (* ident for returned value, expression to identify fn, args. *)
-| St_call : option ident → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
+| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
 | St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
 | St_seq : stmt → stmt → stmt
@@ -76 +76 @@
 
 (* Assert a predicate on every variable or parameter identifier. *)
-definition stmt_vars : (ident → Prop) → stmt → Prop ≝
+definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
 λP,s.
 match s with
-[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
+[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
 | St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
-| 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 ]) es
+| 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
 | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
 | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
@@ -107 +107 @@
 ] qed.
 
-lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
+lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
 #P #Q #H #s elim s normalize
 [ //
@@ -146 +146 @@
 ; f_stacksize : nat
 ; f_body      : stmt
-; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
+     (* Ensure that variables appear in the params and vars list with the
+        correct typ; and that all goto labels used are declared. *)
+; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
                            stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
 }.