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

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

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

File size: 4.0 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "utilities/lists.ma".
5include "utilities/option.ma".
6
7definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
8λtag,A,m,i. lookup … m i ≠ None ?.
9
10(* TODO: consider making the typing stricter. *)
11
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'
17| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
18| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
19| Ecost : ∀t. costlabel → expr t → expr t.
20
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
41inductive stmt : Type[0] ≝
42| St_skip : stmt
43| St_assign : ∀t. ident → expr t → stmt
44| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
45(* ident for returned value, expression to identify fn, args. *)
46| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
47| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
48| St_seq : stmt → stmt → stmt
49| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
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 *)
54| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
55| St_return : option (Σt. expr t) → stmt
56| St_label : ident → stmt → stmt
57| St_goto : ident → stmt
58| St_cost : costlabel → stmt → stmt.
59
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
98record internal_function : Type[0] ≝
99{ f_return    : option typ
100; f_params    : list (ident × typ)
101; f_vars      : list (ident × typ)
102; f_stacksize : nat
103; f_body      : stmt
104; f_bound     : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars))
105}.
106
107definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.