source: Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma @ 1087

Last change on this file since 1087 was 1087, checked in by campbell, 10 years ago

Experimental branch where lookups of local variables in Cminor code always
succeed.

File size: 4.0 KB
RevLine 
[751]1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
[1087]4include "utilities/lists.ma".
5include "utilities/option.ma".
[751]6
[1087]7definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
8λtag,A,m,i. lookup … m i ≠ None ?.
9
[880]10(* TODO: consider making the typing stricter. *)
[751]11
[880]12inductive expr : typ → Type[0] ≝
13| Id : ∀t. ident → expr t
14| Cst : ∀t. constant → expr t
15| Op1 : ∀t,t'. unary_operation → expr t → expr t'
16| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
[881]17| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
[880]18| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
19| Ecost : ∀t. costlabel → expr t → expr t.
20
[1087]21(* Assert a predicate on every variable or parameter identifier. *)
22let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
23match e with
24[ Id _ i ⇒ P i
25| Cst _ _ ⇒ True
26| Op1 _ _ _ e ⇒ expr_vars ? e P
27| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
28| Mem _ _ _ e ⇒ expr_vars ? e P
29| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
30| Ecost _ _ e ⇒ expr_vars ? e P
31].
32
33lemma expr_vars_mp : ∀t,e,P,Q.
34  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
35#t0 #e elim e normalize /3/
36[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
37  % /3/
38| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
39] qed.
40
[751]41inductive stmt : Type[0] ≝
42| St_skip : stmt
[880]43| St_assign : ∀t. ident → expr t → stmt
[881]44| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
[816]45(* ident for returned value, expression to identify fn, args. *)
[880]46| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
47| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
[751]48| St_seq : stmt → stmt → stmt
[880]49| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
[751]50| St_loop : stmt → stmt
51| St_block : stmt → stmt
52| St_exit : nat → stmt
53(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
[961]54| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
[880]55| St_return : option (Σt. expr t) → stmt
[751]56| St_label : ident → stmt → stmt
57| St_goto : ident → stmt
58| St_cost : costlabel → stmt → stmt.
59
[1087]60(* Assert a predicate on every variable or parameter identifier. *)
61let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝
62match s with
63[ St_skip ⇒ True
64| St_assign _ i e ⇒ P i ∧ expr_vars ? e P
65| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
66| 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
67| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
68| St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P
69| St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P
70| St_loop s ⇒ stmt_vars s P
71| St_block s ⇒ stmt_vars s P
72| St_exit _ ⇒ True
73| St_switch _ _ e _ _ ⇒ expr_vars ? e P
74| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
75| St_label _ s ⇒ stmt_vars s P
76| St_goto _ ⇒ True
77| St_cost _ s ⇒ stmt_vars s P
78].
79
80lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q.
81#P #Q #H #s elim s normalize
82[ //
83| #t #id #e * /4/
84| #t #r #q #e1 #e2 * /4/
85| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
86| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
87| #s1 #s2 #H1 #H2 * /3/
88| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
89| 8,9: #s #H1 #H2 /2/
90| //
91| /5/
92| * normalize [ // | *; normalize /3/ ]
93| /2/
94| //
95| /2/
96] qed.
97
[751]98record internal_function : Type[0] ≝
[886]99{ f_return    : option typ
100; f_params    : list (ident × typ)
101; f_vars      : list (ident × typ)
[751]102; f_stacksize : nat
103; f_body      : stmt
[1087]104; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
[751]105}.
106
107definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.