source: src/Cminor/syntax.ma @ 1713

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

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

File size: 5.9 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "basics/lists/list.ma".
5
6(* TODO: consider making the typing stricter. *)
7
8inductive expr : typ → Type[0] ≝
9| Id : ∀t. ident → expr t
10| Cst : ∀t. constant → expr t
11| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
12| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
13| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
14| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
15| Ecost : ∀t. costlabel → expr t → expr t.
16
17(* Assert a predicate on every variable or parameter identifier. *)
18let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
19match e with
20[ Id t i ⇒ P i t
21| Cst _ _ ⇒ True
22| Op1 _ _ _ e ⇒ expr_vars ? e P
23| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
24| Mem _ _ _ e ⇒ expr_vars ? e P
25| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
26| Ecost _ _ e ⇒ expr_vars ? e P
27].
28
29lemma expr_vars_mp : ∀t,e,P,Q.
30  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
31#t0 #e elim e normalize /3/
32[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
33  % /3/
34| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
35] qed.
36
37axiom Label : String.
38
39inductive stmt : Type[0] ≝
40| St_skip : stmt
41| St_assign : ∀t. ident → expr t → stmt
42| St_store : ∀t,r. memory_chunk → expr (ASTptr r) → expr t → stmt
43(* ident for returned value, expression to identify fn, args. *)
44| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
45(* We don't use these at the moment, and they're getting in the way.
46| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
47*)
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 : identifier Label → stmt → stmt
57| St_goto : identifier Label → stmt
58| St_cost : costlabel → stmt → stmt.
59
60let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
61match s with
62[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
63| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
64| St_loop s' ⇒ P s ∧ stmt_P P s'
65| St_block s' ⇒ P s ∧ stmt_P P s'
66| St_label _ s' ⇒ P s ∧ stmt_P P s'
67| St_cost _ s' ⇒ P s ∧ stmt_P P s'
68| _ ⇒ P s
69].
70
71lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
72#P * normalize /2/
73[ #s1 #s2 * * /2/
74| #sz #sg #e #s1 #s2 * * /2/
75| 3,4: #s * /2/
76| 5,6: #i #s normalize * /2/
77] qed.
78
79(* Assert a predicate on every variable or parameter identifier. *)
80definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
81λP,s.
82match s with
83[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
84| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
85| 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
86(*
87| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
88*)
89| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
90| St_switch _ _ e _ _ ⇒ expr_vars ? e P
91| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
92| _ ⇒ True
93].
94
95definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
96λP,s.
97match s with
98[ St_label l _ ⇒ P l
99| St_goto l ⇒ P l
100| _ ⇒ True
101].
102
103lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
104#P #Q #H #s elim s /2/
105[ #s1 #s2 #H1 #H2 normalize * * /4/
106| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
107| #s #H * /5/
108| #s #H * /5/
109| #l #s #H * /5/
110| #l #s #H * /5/
111] qed.
112
113lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
114#P #Q #H #s elim s normalize
115[ //
116| #t #id #e * /4/
117| #t #r #q #e1 #e2 * /4/
118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
119(*
120| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
121*)
122| #s1 #s2 #H1 #H2 * /3/
123| #sz #sg #e #s1 #s2 #H1 #H2 /5/
124| 7,8: #s #H1 #H2 /2/
125| //
126| /5/
127| * normalize [ // | *; normalize /3/ ]
128| /2/
129| //
130| /2/
131] qed.
132
133lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
134#P #Q #H #s elim s normalize /2/ qed.
135
136(* Get labels from a Cminor statement. *)
137let rec labels_of (s:stmt) : list (identifier Label) ≝
138match s with
139[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
140| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
141| St_loop s ⇒ labels_of s
142| St_block s ⇒ labels_of s
143| St_label l s ⇒ l::(labels_of s)
144| St_cost _ s ⇒ labels_of s
145| _ ⇒ [ ]
146].
147
148record internal_function : Type[0] ≝
149{ f_return    : option typ
150; f_params    : list (ident × typ)
151; f_vars      : list (ident × typ)
152; f_distinct  : distinct_env … (f_params @ f_vars)
153; f_stacksize : nat
154; f_body      : stmt
155     (* Ensure that variables appear in the params and vars list with the
156        correct typ; and that all goto labels used are declared. *)
157; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
158                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
159}.
160
161(* We define two closely related versions of Cminor, the first with the original
162   initialisation data for global variables, and the second where the code is
163   responsible for initialisation and we only give the size of each variable. *)
164
165definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
166
167definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.