source: Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma @ 1101

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

Label preservation in Cminor initialisation and RTLabs translation
on branch.

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