Changeset 1626 for src/Cminor/syntax.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r1605 r1626  
    1616
    1717(* 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 ≝
     18let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
    1919match e with
    20 [ Id _ i ⇒ P i
     20[ Id t i ⇒ P i t
    2121| Cst _ _ ⇒ True
    2222| Op1 _ _ _ e ⇒ expr_vars ? e P
     
    2828
    2929lemma 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.
    3131#t0 #e elim e normalize /3/
    3232[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
     
    4242| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
    4343(* ident for returned value, expression to identify fn, args. *)
    44 | St_call : option ident → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     44| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4545| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
    4646| St_seq : stmt → stmt → stmt
     
    7676
    7777(* Assert a predicate on every variable or parameter identifier. *)
    78 definition stmt_vars : (ident → Prop) → stmt → Prop ≝
     78definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
    7979λP,s.
    8080match s with
    81 [ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
     81[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
    8282| 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 ]) es
     83| 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
    8484| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8585| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
     
    107107] qed.
    108108
    109 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
     109lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
    110110#P #Q #H #s elim s normalize
    111111[ //
     
    146146; f_stacksize : nat
    147147; 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 ∧
    149151                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
    150152}.
Note: See TracChangeset for help on using the changeset viewer.