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

Last change on this file since 1104 was 1104, checked in by campbell, 8 years ago

A little more tidying.

File size: 5.2 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "utilities/lists.ma".
5include "utilities/option.ma".
6
7(* TODO: consider making the typing stricter. *)
8
9inductive expr : typ → Type[0] ≝
10| Id : ∀t. ident → expr t
11| Cst : ∀t. constant → expr t
12| Op1 : ∀t,t'. unary_operation → expr t → expr t'
13| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
14| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
15| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
16| Ecost : ∀t. costlabel → expr t → expr t.
17
18(* Assert a predicate on every variable or parameter identifier. *)
19let rec expr_vars (t:typ) (e:expr t) (P:ident → Prop) on e : Prop ≝
20match e with
21[ Id _ i ⇒ P i
22| Cst _ _ ⇒ True
23| Op1 _ _ _ e ⇒ expr_vars ? e P
24| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
25| Mem _ _ _ e ⇒ expr_vars ? e P
26| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
27| Ecost _ _ e ⇒ expr_vars ? e P
28].
29
30lemma expr_vars_mp : ∀t,e,P,Q.
31  (∀i. P i → Q i) → expr_vars t e P → expr_vars t e Q.
32#t0 #e elim e normalize /3/
33[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
34  % /3/
35| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
36] qed.
37
38axiom Label : String.
39
40inductive stmt : Type[0] ≝
41| St_skip : stmt
42| St_assign : ∀t. ident → expr t → stmt
43| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
44(* ident for returned value, expression to identify fn, args. *)
45| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
46| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
47| St_seq : stmt → stmt → stmt
48| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
49| St_loop : stmt → stmt
50| St_block : stmt → stmt
51| St_exit : nat → stmt
52(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
53| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
54| St_return : option (Σt. expr t) → stmt
55| St_label : identifier Label → stmt → stmt
56| St_goto : identifier Label → stmt
57| St_cost : costlabel → stmt → stmt.
58
59let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
60match s with
61[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
62| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
63| St_loop s' ⇒ P s ∧ stmt_P P s'
64| St_block s' ⇒ P s ∧ stmt_P P s'
65| St_label _ s' ⇒ P s ∧ stmt_P P s'
66| St_cost _ s' ⇒ P s ∧ stmt_P P s'
67| _ ⇒ P s
68].
69
70lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
71#P * normalize /2/
72[ #s1 #s2 * * /2/
73| #sz #sg #e #s1 #s2 * * /2/
74| 3,4: #s * /2/
75| 5,6: #i #s normalize * /2/
76] qed.
77
78(* Assert a predicate on every variable or parameter identifier. *)
79definition stmt_vars : (ident → Prop) → stmt → Prop ≝
80λP,s.
81match s with
82[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
83| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
84| 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
85| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
86| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
87| St_switch _ _ e _ _ ⇒ expr_vars ? e P
88| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
89| _ ⇒ True
90].
91
92definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
93λP,s.
94match s with
95[ St_label l _ ⇒ P l
96| St_goto l ⇒ P l
97| _ ⇒ True
98].
99
100lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
101#P #Q #H #s elim s /2/
102[ #s1 #s2 #H1 #H2 normalize * * /4/
103| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
104| #s #H * /5/
105| #s #H * /5/
106| #l #s #H * /5/
107| #l #s #H * /5/
108] qed.
109
110lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s.
111#P #Q #H #s elim s normalize
112[ //
113| #t #id #e * /4/
114| #t #r #q #e1 #e2 * /4/
115| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
116| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
117| #s1 #s2 #H1 #H2 * /3/
118| #sz #sg #e #s1 #s2 #H1 #H2 /5/
119| 8,9: #s #H1 #H2 /2/
120| //
121| /5/
122| * normalize [ // | *; normalize /3/ ]
123| /2/
124| //
125| /2/
126] qed.
127
128lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
129#P #Q #H #s elim s normalize /2/ qed.
130
131(* Get labels from a Cminor statement. *)
132let rec labels_of (s:stmt) : list (identifier Label) ≝
133match s with
134[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
135| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
136| St_loop s ⇒ labels_of s
137| St_block s ⇒ labels_of s
138| St_label l s ⇒ l::(labels_of s)
139| St_cost _ s ⇒ labels_of s
140| _ ⇒ [ ]
141].
142
143record internal_function : Type[0] ≝
144{ f_return    : option typ
145; f_params    : list (ident × typ)
146; f_vars      : list (ident × typ)
147; f_stacksize : nat
148; f_body      : stmt
149; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
150                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
151}.
152
153definition Cminor_program ≝ program (fundef internal_function) unit.
Note: See TracBrowser for help on using the repository browser.