1 | include "utilities/lists.ma". |
---|
2 | include "common/Globalenvs.ma". |
---|
3 | include "Cminor/syntax.ma". |
---|
4 | include "RTLabs/syntax.ma". |
---|
5 | |
---|
6 | definition env ≝ identifier_map SymbolTag register. |
---|
7 | definition label_env ≝ identifier_map SymbolTag label. |
---|
8 | definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝ |
---|
9 | λen,gen. foldr ?? |
---|
10 | (λidt,rsengen. |
---|
11 | let 〈id,ty〉 ≝ idt in |
---|
12 | let 〈rs,en,gen〉 ≝ rsengen in |
---|
13 | let 〈r,gen'〉 ≝ fresh … gen in |
---|
14 | 〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉. |
---|
15 | |
---|
16 | lemma populates_env : ∀l,e,u,l',e',u'. |
---|
17 | populate_env e u l = 〈l',e',u'〉 → |
---|
18 | ∀i. Exists ? (λx.\fst x = i) l → |
---|
19 | present ?? e' i. |
---|
20 | #l elim l |
---|
21 | [ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) * |
---|
22 | | * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?); |
---|
23 | * [ whd in ⊢ (??%? → ?) #E1 <E1 |
---|
24 | generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z |
---|
25 | whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E |
---|
26 | whd in E:(??%?); |
---|
27 | >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) |
---|
28 | whd >lookup_add_hit % #A destruct |
---|
29 | | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl) |
---|
30 | lapply (refl ? (populate_env e u tl)) |
---|
31 | cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *) |
---|
32 | * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u'' |
---|
33 | whd in ⊢ (??%? → ?) #E |
---|
34 | >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *) |
---|
35 | @lookup_add_oblivious |
---|
36 | @(IH … E1 ? H) |
---|
37 | ] |
---|
38 | ] qed. |
---|
39 | |
---|
40 | lemma populate_extends : ∀l,e,u,l',e',u'. |
---|
41 | populate_env e u l = 〈l',e',u'〉 → |
---|
42 | ∀i. present ?? e i → present ?? e' i. |
---|
43 | #l elim l |
---|
44 | [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct // |
---|
45 | | * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?); |
---|
46 | change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl) |
---|
47 | lapply (refl ? (populate_env e u tl)) |
---|
48 | cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0 |
---|
49 | >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E |
---|
50 | whd in E:(??%?) |
---|
51 | >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ] |
---|
52 | #i #H @lookup_add_oblivious @(IH … E0) @H |
---|
53 | ] qed. |
---|
54 | |
---|
55 | definition populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝ |
---|
56 | λen,gen. foldr ?? |
---|
57 | (λid,engen. |
---|
58 | let 〈en,gen〉 ≝ engen in |
---|
59 | let 〈r,gen'〉 ≝ fresh … gen in |
---|
60 | 〈add ?? en id r, gen'〉) 〈en, gen〉. |
---|
61 | |
---|
62 | lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?). |
---|
63 | lookup tag A m i ≠ None ?. |
---|
64 | #tag #A #m * #i #H @H |
---|
65 | qed. |
---|
66 | |
---|
67 | definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝ |
---|
68 | λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ]. |
---|
69 | cases H #H' cases (H' (refl ??)) qed. |
---|
70 | |
---|
71 | |
---|
72 | (* Add a statement to the graph, *without* updating the entry label. *) |
---|
73 | definition fill_in_statement : label → statement → internal_function → internal_function ≝ |
---|
74 | λl,s,f. |
---|
75 | mk_internal_function (f_labgen f) (f_reggen f) |
---|
76 | (f_result f) (f_params f) (f_locals f) |
---|
77 | (f_stacksize f) (add ?? (f_graph f) l s) |
---|
78 | (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?). |
---|
79 | @lookup_add_oblivious @lookup_sigma |
---|
80 | qed. |
---|
81 | |
---|
82 | (* Add a statement to the graph, making it the entry label. *) |
---|
83 | definition add_to_graph : label → statement → internal_function → internal_function ≝ |
---|
84 | λl,s,f. |
---|
85 | mk_internal_function (f_labgen f) (f_reggen f) |
---|
86 | (f_result f) (f_params f) (f_locals f) |
---|
87 | (f_stacksize f) (add ?? (f_graph f) l s) |
---|
88 | (dp ?? l ?) (dp ?? (f_exit f) ?). |
---|
89 | [ >lookup_add_hit % #E destruct |
---|
90 | | @lookup_add_oblivious @lookup_sigma |
---|
91 | ] qed. |
---|
92 | |
---|
93 | (* Add a statement with a fresh label to the start of the function. The |
---|
94 | statement is parametrised by the *next* instruction's label. *) |
---|
95 | definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝ |
---|
96 | λs,f. |
---|
97 | let 〈l,g〉 ≝ fresh … (f_labgen f) in |
---|
98 | let s' ≝ s (f_entry f) in |
---|
99 | (mk_internal_function g (f_reggen f) |
---|
100 | (f_result f) (f_params f) (f_locals f) |
---|
101 | (f_stacksize f) (add ?? (f_graph f) l s') |
---|
102 | (dp ?? l ?) (dp ?? (f_exit f) ?)). |
---|
103 | [ >lookup_add_hit % #E destruct |
---|
104 | | @lookup_add_oblivious @lookup_sigma |
---|
105 | ] qed. |
---|
106 | |
---|
107 | definition fresh_reg : internal_function → typ → register × internal_function ≝ |
---|
108 | λf,ty. |
---|
109 | let 〈r,g〉 ≝ fresh … (f_reggen f) in |
---|
110 | 〈r, mk_internal_function (f_labgen f) g |
---|
111 | (f_result f) (f_params f) (〈r,ty〉::(f_locals f)) |
---|
112 | (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉. |
---|
113 | |
---|
114 | axiom UnknownVariable : String. |
---|
115 | |
---|
116 | definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function ≝ |
---|
117 | λenv,ty,e,f. |
---|
118 | match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with |
---|
119 | [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉 |
---|
120 | | _ ⇒ λ_.fresh_reg f ty |
---|
121 | ]. |
---|
122 | |
---|
123 | let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ |
---|
124 | match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H. |
---|
125 | |
---|
126 | definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ]. |
---|
127 | |
---|
128 | definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). |
---|
129 | internal_function → All ? (exprtyp_present env) es → |
---|
130 | list register × internal_function ≝ |
---|
131 | λenv,es,f,Env. |
---|
132 | foldr_all (Σt:typ.expr t) ?? |
---|
133 | (λe,p,acc. let 〈rs,f〉 ≝ acc in |
---|
134 | let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in |
---|
135 | 〈r::rs,f'〉) 〈[ ], f〉 es Env. |
---|
136 | @p qed. |
---|
137 | |
---|
138 | lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. |
---|
139 | ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → |
---|
140 | ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. |
---|
141 | #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. |
---|
142 | |
---|
143 | |
---|
144 | lemma choose_regs_length : ∀env,es,f,p,rs,f'. |
---|
145 | choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|. |
---|
146 | #env #es #f elim es |
---|
147 | [ #p #rs #f normalize #E destruct @refl |
---|
148 | | * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E |
---|
149 | cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E; |
---|
150 | cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2; |
---|
151 | destruct (E4) skip (E1 E3) @eq_f @IH |
---|
152 | [ @(proj2 … p) |
---|
153 | | 3: @sym_eq @E1 |
---|
154 | | 2: skip |
---|
155 | ] |
---|
156 | ] qed. |
---|
157 | |
---|
158 | axiom BadCminorProgram : String. |
---|
159 | |
---|
160 | let rec add_expr (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function ≝ |
---|
161 | match e return λty,e.expr_vars ty e (present ?? env) → internal_function with |
---|
162 | [ Id _ i ⇒ λEnv. |
---|
163 | let r ≝ lookup' env i Env in |
---|
164 | match register_eq r dst with |
---|
165 | [ inl _ ⇒ f |
---|
166 | | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f |
---|
167 | ] |
---|
168 | | Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f |
---|
169 | | Op1 _ _ op e' ⇒ λEnv. |
---|
170 | let 〈r,f〉 ≝ choose_reg env ? e' f Env in |
---|
171 | let f ≝ add_fresh_to_graph (St_op1 op dst r) f in |
---|
172 | add_expr env ? e' Env r f |
---|
173 | | Op2 _ _ _ op e1 e2 ⇒ λEnv. |
---|
174 | let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in |
---|
175 | let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in |
---|
176 | let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in |
---|
177 | let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in |
---|
178 | add_expr env ? e1 (proj1 … Env) r1 f |
---|
179 | | Mem _ _ q e' ⇒ λEnv. |
---|
180 | let 〈r,f〉 ≝ choose_reg env ? e' f Env in |
---|
181 | let f ≝ add_fresh_to_graph (St_load q r dst) f in |
---|
182 | add_expr env ? e' Env r f |
---|
183 | | Cond _ _ _ e' e1 e2 ⇒ λEnv. |
---|
184 | let resume_at ≝ f_entry f in |
---|
185 | let f ≝ add_expr env ? e2 (proj2 … Env) dst f in |
---|
186 | let lfalse ≝ f_entry f in |
---|
187 | let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in |
---|
188 | let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in |
---|
189 | let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in |
---|
190 | let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in |
---|
191 | add_expr env ? e' (proj1 … (proj1 … Env)) r f |
---|
192 | | Ecost _ l e' ⇒ λEnv. |
---|
193 | let f ≝ add_expr env ? e' Env dst f in |
---|
194 | add_fresh_to_graph (St_cost l) f |
---|
195 | ] Env. |
---|
196 | |
---|
197 | let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) |
---|
198 | (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝ |
---|
199 | match es return λes.All ?? es → |es|=|dsts| → ? with |
---|
200 | [ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ] |
---|
201 | | cons e et ⇒ λEnv. |
---|
202 | match dsts return λx. ?=|x| → ? with |
---|
203 | [ nil ⇒ λpf.⊥ |
---|
204 | | cons r rt ⇒ λpf. |
---|
205 | let f ≝ add_exprs env et ? rt ? f in |
---|
206 | match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env) |
---|
207 | ] |
---|
208 | ] Env pf. |
---|
209 | [ 1,2,3: normalize in pf; destruct // |
---|
210 | | whd in Env @(proj2 … Env) |
---|
211 | | normalize in pf; destruct @e0 ] qed. |
---|
212 | |
---|
213 | axiom UnknownLabel : String. |
---|
214 | axiom ReturnMismatch : String. |
---|
215 | |
---|
216 | notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" |
---|
217 | with precedence 10 |
---|
218 | for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒ |
---|
219 | λ${ident E}.$s ] (refl ? $t) }. |
---|
220 | |
---|
221 | let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝ |
---|
222 | match s return λs.stmt_vars s (present ?? env) → res internal_function with |
---|
223 | [ St_skip ⇒ λ_. OK ? f |
---|
224 | | St_assign _ x e ⇒ λEnv. |
---|
225 | let dst ≝ lookup' env x (proj1 … Env) in |
---|
226 | OK ? (add_expr env ? e (proj2 … Env) dst f) |
---|
227 | | St_store _ _ q e1 e2 ⇒ λEnv. |
---|
228 | let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in |
---|
229 | let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in |
---|
230 | let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in |
---|
231 | let f ≝ add_expr env ? e1 (proj1 … Env) addr_reg f in |
---|
232 | OK ? (add_expr env ? e2 (proj2 … Env) val_reg f) |
---|
233 | | St_call return_opt_id e args ⇒ λEnv. |
---|
234 | let return_opt_reg ≝ |
---|
235 | match return_opt_id return λo. ? → ? with |
---|
236 | [ None ⇒ λ_. None ? |
---|
237 | | Some id ⇒ λEnv. Some ? (lookup' env id ?) |
---|
238 | ] Env in |
---|
239 | let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in |
---|
240 | let f ≝ |
---|
241 | match e with |
---|
242 | [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f |
---|
243 | | _ ⇒ |
---|
244 | let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in |
---|
245 | let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in |
---|
246 | add_expr env ? e (proj2 … (proj1 … Env)) fnr f |
---|
247 | ] in |
---|
248 | OK ? (add_exprs env args (proj2 … Env) args_regs ? f) |
---|
249 | | St_tailcall e args ⇒ λEnv. |
---|
250 | let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in |
---|
251 | let f ≝ |
---|
252 | match e with |
---|
253 | [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f |
---|
254 | | _ ⇒ |
---|
255 | let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in |
---|
256 | let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in |
---|
257 | add_expr env ? e (proj1 … Env) fnr f |
---|
258 | ] in |
---|
259 | OK ? (add_exprs env args (proj2 … Env) args_regs ? f) |
---|
260 | | St_seq s1 s2 ⇒ λEnv. |
---|
261 | do f ← add_stmt env label_env s2 (proj2 … Env) exits f; |
---|
262 | add_stmt env label_env s1 (proj1 … Env) exits f |
---|
263 | | St_ifthenelse _ _ e s1 s2 ⇒ λEnv. |
---|
264 | let l_next ≝ f_entry f in |
---|
265 | do f ← add_stmt env label_env s2 (proj2 … Env) exits f; |
---|
266 | let l2 ≝ f_entry f in |
---|
267 | let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in |
---|
268 | do f ← add_stmt env label_env s1 (proj2 … (proj1 … Env)) exits f; |
---|
269 | let 〈r,f〉 ≝ choose_reg env ? e f (proj1 … (proj1 … Env)) in |
---|
270 | let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in |
---|
271 | OK ? (add_expr env ? e (proj1 … (proj1 … Env)) r f) |
---|
272 | | St_loop s ⇒ λEnv. |
---|
273 | let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *) |
---|
274 | let l_loop ≝ f_entry f in |
---|
275 | do f ← add_stmt env label_env s Env exits f; |
---|
276 | OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f) |
---|
277 | | St_block s ⇒ λEnv. |
---|
278 | add_stmt env label_env s Env ((f_entry f)::exits) f |
---|
279 | | St_exit n ⇒ λEnv. |
---|
280 | do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
281 | OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f) |
---|
282 | | St_switch sz sg e tab n ⇒ λEnv. |
---|
283 | let 〈r,f〉 ≝ choose_reg env ? e f Env in |
---|
284 | do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
285 | let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in |
---|
286 | do f ← foldr ?? (λcs,f. |
---|
287 | do f ← f; |
---|
288 | let 〈i,n〉 ≝ cs in |
---|
289 | let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in |
---|
290 | let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in |
---|
291 | do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits); |
---|
292 | let f ≝ add_fresh_to_graph (St_cond br l_case) f in |
---|
293 | let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in |
---|
294 | OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab; |
---|
295 | OK ? (add_expr env ? e Env r f) |
---|
296 | | St_return opt_e ⇒ |
---|
297 | let f ≝ add_fresh_to_graph (λ_. St_return) f in |
---|
298 | match opt_e return λo. ? → ? with |
---|
299 | [ None ⇒ λEnv. OK ? f |
---|
300 | | Some e ⇒ |
---|
301 | match f_result f with |
---|
302 | [ None ⇒ λEnv. Error ? (msg ReturnMismatch) |
---|
303 | | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ] |
---|
304 | ] |
---|
305 | ] |
---|
306 | | St_label l s' ⇒ λEnv. |
---|
307 | do f ← add_stmt env label_env s' Env exits f; |
---|
308 | do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); |
---|
309 | OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f) |
---|
310 | | St_goto l ⇒ λEnv. |
---|
311 | do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l); |
---|
312 | OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f) |
---|
313 | | St_cost l s' ⇒ λEnv. |
---|
314 | do f ← add_stmt env label_env s' Env exits f; |
---|
315 | OK ? (add_fresh_to_graph (St_cost l) f) |
---|
316 | ] Env. |
---|
317 | [ -f @(choose_regs_length … (sym_eq … Eregs)) |
---|
318 | | whd in Env @(proj1 … (proj1 … Env)) |
---|
319 | | -f @(choose_regs_length … (sym_eq … Eregs)) |
---|
320 | | @(λ_. St_skip l_next) |
---|
321 | | @(St_skip (f_entry f)) |
---|
322 | | @St_skip |
---|
323 | | @(λ_. St_skip l) |
---|
324 | | @(λ_. St_skip l_default) |
---|
325 | | whd in Env @Env |
---|
326 | | @(St_skip (f_entry f)) |
---|
327 | | @(λ_.St_skip l') |
---|
328 | ] qed. |
---|
329 | |
---|
330 | (* Get labels from a Cminor statement. *) |
---|
331 | let rec labels_of (s:stmt) : list ident ≝ |
---|
332 | match s with |
---|
333 | [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
334 | | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) |
---|
335 | | St_loop s ⇒ labels_of s |
---|
336 | | St_block s ⇒ labels_of s |
---|
337 | | St_label l s ⇒ l::(labels_of s) |
---|
338 | | St_cost _ s ⇒ labels_of s |
---|
339 | | _ ⇒ [ ] |
---|
340 | ]. |
---|
341 | |
---|
342 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" |
---|
343 | with precedence 10 |
---|
344 | for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒ |
---|
345 | match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒ |
---|
346 | λ${ident E}.$s ] ] (refl ? $t) }. |
---|
347 | |
---|
348 | |
---|
349 | definition c2ra_function (*: internal_function → internal_function*) ≝ |
---|
350 | λf. |
---|
351 | let labgen0 ≝ new_universe LabelTag in |
---|
352 | let reggen0 ≝ new_universe RegisterTag in |
---|
353 | let cminor_labels ≝ labels_of (f_body f) in |
---|
354 | let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in |
---|
355 | let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in |
---|
356 | let 〈result, locals, reggen〉 ≝ |
---|
357 | match f_return f with |
---|
358 | [ None ⇒ 〈None ?, locals0, reggen2〉 |
---|
359 | | Some ty ⇒ |
---|
360 | let 〈r,gen〉 ≝ fresh … reggen2 in |
---|
361 | 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in |
---|
362 | let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in |
---|
363 | let 〈l,labgen〉 ≝ fresh … labgen1 in |
---|
364 | let emptyfn ≝ |
---|
365 | mk_internal_function |
---|
366 | labgen |
---|
367 | reggen |
---|
368 | result |
---|
369 | params |
---|
370 | locals |
---|
371 | (f_stacksize f) |
---|
372 | (add ?? (empty_map …) l St_return) |
---|
373 | l |
---|
374 | l in |
---|
375 | do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn; |
---|
376 | do u1 ← check_universe_ok ? (f_labgen f); |
---|
377 | do u2 ← check_universe_ok ? (f_reggen f); |
---|
378 | OK ? f |
---|
379 | . |
---|
380 | [ @(stmt_vars_mp … (f_bound f)) |
---|
381 | #i #H cases (Exists_append … H) |
---|
382 | [ #H1 @(populate_extends ?????? (sym_eq … E2)) |
---|
383 | @(populates_env … (sym_eq … E1)) @H1 |
---|
384 | | #H1 @(populates_env … (sym_eq … E2)) @H1 |
---|
385 | ] |
---|
386 | | *: >lookup_add_hit % #E destruct |
---|
387 | ] |
---|
388 | qed. |
---|
389 | |
---|
390 | definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
391 | transform_partial_program ??? |
---|
392 | (transf_partial_fundef ?? c2ra_function). |
---|
393 | |
---|
394 | include "Cminor/initialisation.ma". |
---|
395 | |
---|
396 | definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝ |
---|
397 | λp. let p' ≝ replace_init p in cminor_to_rtlabs p. |
---|