source: src/Cminor/toRTLabs.ma @ 2232

Last change on this file since 2232 was 2232, checked in by campbell, 7 years ago

Remove unused block structure in Cminor.

File size: 38.0 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 × typ).
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,ty〉, gen'〉) 〈[ ], en, gen〉.
15
16definition Env_has : env → ident → typ → Prop ≝
17λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
18
19lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
20#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
21[ * | * #r #t' #E % #E' destruct ]
22qed.
23
24lemma populates_env : ∀l,e,u,l',e',u'.
25  distinct_env ?? l →
26  populate_env e u l = 〈l',e',u'〉 →
27  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
28      Env_has e' i t.
29#l elim l
30[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
31| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
32  * [ #E1 destruct (E1)
33      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
34      whd in ⊢ (??%? → ?);
35      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
36      #r #gen' #E1 #E2
37      whd in E2:(??%?); destruct;
38      whd >lookup_add_hit %
39    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
40      lapply (refl ? (populate_env e u tl))
41      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
42      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
43      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
44      whd in ⊢ (??%? → ?); #E destruct
45      whd >lookup_add_miss
46      [ @(IH … E1 ?? H) @(proj2 … D)
47      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
48      ]
49    ]
50] qed.
51
52lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
53  distinct_env ?? (l@r) →
54  populate_env e u l = 〈l',e',u'〉 →
55  All ? (λit. fresh_for_map … (\fst it) e) r →
56  All ? (λit. fresh_for_map … (\fst it) e') r.
57#r #l elim l
58[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
59| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
60  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
61  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
62  * #x #y #z #E2 >E2 in E;
63  whd in ⊢ (??%? → ?);
64  elim (fresh ? z)
65  #rg #gen' #E
66  whd in E:(??%?); destruct
67  #F lapply (IH … E2 F)
68  [ @(proj2 … D)
69  | lapply (All_append_r … (proj1 … D))
70    elim r
71    [ //
72    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
73      [ @fresh_for_map_add /2/
74      | @IH //
75      ]
76    ]
77  ]
78] qed.
79
80lemma populate_extends : ∀l,e,u,l',e',u'.
81  All ? (λit. fresh_for_map ?? (\fst it) e) l →
82  populate_env e u l = 〈l',e',u'〉 →
83  ∀i,t. Env_has e i t → Env_has e' i t.
84#l elim l
85[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
86| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
87  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
88  lapply (refl ? (populate_env e u tl))
89  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
90  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
91  destruct
92  #i #t #H whd >lookup_add_miss
93  [ @(IH … E0) [ @(proj2 … F) | @H ]
94  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
95] qed.
96
97definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
98/2/ qed.
99
100lemma populate_env_list : ∀l,e,u,l',e',u'.
101  populate_env e u l = 〈l',e',u'〉 →
102  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
103    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
104#l elim l
105[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
106| * #id #ty #tl #IH #e #u #l' #e' #u' #E
107  whd in E:(??%?);
108  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
109  lapply (refl ? (populate_env e u tl))
110  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
111  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
112  destruct
113  #i #r #t cases (identifier_eq ? i id)
114  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
115    generalize in ⊢ (??(??? (?%))? → ?);
116    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
117    %2 %1 %
118  | #NE #H #L cases (IH … E0 i r t ??)
119    [ /2/
120    | #X %2 %2 @X
121    | whd in H ⊢ %; >lookup_add_miss in H; //
122    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
123      lapply L -L
124      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
125      generalize in ⊢ (? → ? → ??(????%)?);
126      >lookup_add_miss // #H0 #p
127      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
128      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
129      #p' #X @X
130    ]
131  ]
132] qed.
133
134definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
135λen,gen. foldr ??
136 (λid,engen.
137   let 〈en,gen〉 ≝ engen in
138   let 〈r,gen'〉 ≝ fresh … gen in
139     〈add ?? en id r, gen'〉) 〈en, gen〉.
140
141lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
142  populate_label_env lbls u ls = 〈lbls',u'〉 →
143  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
144#ls elim ls
145[ #lbls #u #lbls' #u' #E #l *
146| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
147  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
148  lapply (refl ? (populate_label_env lbls u t))
149  cases (populate_label_env lbls u t) in ⊢ (???% → %);
150  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
151  cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);
152  #E destruct
153  #l *
154  [ #El <El whd >lookup_add_hit % #Er destruct
155  | #H @lookup_add_oblivious @(IH … E1 ? H)
156  ]
157] qed.
158
159lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
160  populate_label_env lbls u ls = 〈lbls',u'〉 →
161  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
162#ls elim ls
163[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
164| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
165  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
166  lapply (refl ? (populate_label_env lbls u t))
167  cases (populate_label_env lbls u t) in ⊢ (???% → %);
168  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
169  cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);
170  #E destruct
171  #l #H cases (identifier_eq ? l h)
172  [ #El %1 %1 @El
173  | #NE cases (IH … E1 l ?)
174    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
175  ]
176] qed.
177
178definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
179
180(* Check that the domain of one graph is included in another, for monotonicity
181   properties.  Note that we don't say anything about the statements. *)
182definition graph_included : graph statement → graph statement → Prop ≝
183λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
184
185lemma graph_inc_trans : ∀g1,g2,g3.
186  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
187#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
188
189definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
190
191definition partially_closed : label_env → graph statement → Prop ≝
192 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
193
194(* I'd use a single parametrised definition along with internal_function, but
195   it's a pain without implicit parameters. *)
196record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
197{ pf_labgen    : universe LabelTag
198; pf_reggen    : universe RegisterTag
199; pf_params    : list (register × typ)
200; pf_locals    : list (register × typ)
201; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
202; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
203; pf_stacksize : nat
204; pf_graph     : graph statement
205; pf_closed    : partially_closed lenv pf_graph
206; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
207; pf_entry     : Σl:label. present ?? pf_graph l
208; pf_exit      : Σl:label. present ?? pf_graph l
209}.
210
211definition fn_env_has ≝
212  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
213
214record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
215{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
216; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
217}.
218
219lemma fn_con_trans : ∀le,env,f1,f2,f3.
220  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
221#le #env #f1 #f2 #f3 #H1 #H2 %
222[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
223| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
224] qed.
225
226lemma fn_con_refl : ∀label_env,env,f.
227  fn_contains label_env env f f.
228#le #env #f % #l // qed.
229
230lemma fn_con_sig : ∀label_env,env,f,f0.
231  ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
232  fn_contains label_env env f f0 →
233  fn_contains label_env env f f'.
234#le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
235qed.
236
237lemma add_statement_inv : ∀le,env,l,s.∀f.
238  labels_present (pf_graph le env f) s →
239  partially_closed le (add … (pf_graph … f) l s).
240#le #env #l #s #f #p
241#l' #s' #H cases (identifier_eq … l l')
242[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
243  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
244| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
245  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
246  | >lookup_add_miss in H; /2/
247  ]
248] qed.
249
250definition statement_typed_in ≝
251λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
252
253lemma forall_nodes_add : ∀A,P,l,a,g.
254  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
255#A #P #l #a #g #ALL #NEW
256#l' #a'
257cases (identifier_eq … l' l)
258[ #E destruct >lookup_add_hit #E destruct @NEW
259| #ne >lookup_add_miss /2/
260] qed.
261
262(* Add a statement to the graph, *without* updating the entry label. *)
263definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
264  labels_present (pf_graph … f) s →
265  statement_typed_in le env f s →
266  Σf':partial_fn le env. fn_contains … f f' ≝
267λle,env,l,s,f,p,tp.
268  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
269                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
270                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
271                «pf_entry … f, ?» «pf_exit … f, ?».
272[ @add_statement_inv @p
273| @forall_nodes_add //
274| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
275| % [ #l' @lookup_add_oblivious | // ]
276] qed.
277
278(* Add a statement to the graph, making it the entry label. *)
279definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
280  labels_present (pf_graph … f) s →
281  statement_typed_in … f s →
282  Σf':partial_fn le env. fn_contains … f f' ≝
283λle,env,l,s,f,p,tl.
284  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
285                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
286                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
287                «l, ?» «pf_exit … f, ?».
288[ @add_statement_inv @p
289| @forall_nodes_add //
290| whd >lookup_add_hit % #E destruct
291| @lookup_add_oblivious @(pi2 … (pf_exit … f))
292| % [ #l' @lookup_add_oblivious | // ]
293] qed.
294
295(* Add a statement with a fresh label to the start of the function.  The
296   statement is parametrised by the *next* instruction's label. *)
297definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
298  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
299  (∀l. statement_typed_in … f (s l)) →
300  Σf':partial_fn le env. fn_contains … f f' ≝
301λle,env,s,f,p,tp.
302  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
303  let s' ≝ s (pf_entry … f) in
304    (mk_partial_fn le env g (pf_reggen … f)
305                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
306                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
307                   «l, ?» «pf_exit … f, ?»).
308[ % [ #l' @lookup_add_oblivious | // ]
309| @add_statement_inv @p @(pi2 … (pf_entry …))
310| @forall_nodes_add //
311| whd >lookup_add_hit % #E destruct
312| @lookup_add_oblivious @(pi2 … (pf_exit …))
313] qed.
314
315(* Variants for labels which are (goto) labels *)
316
317lemma add_statement_inv' : ∀le,env,l,s.∀f.
318  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
319  partially_closed le (add … (pf_graph … f) l s).
320#le #env #l #s #f #p
321#l' #s' #H cases (identifier_eq … l l')
322[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
323  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
324| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
325  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
326  | >lookup_add_miss in H; /2/
327  ]
328] qed.
329
330definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
331  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
332  (∀l. statement_typed_in … f (s l)) →
333  Σf':partial_fn le env. fn_contains … f f' ≝
334λle,env,s,f,p,tp.
335  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
336  let s' ≝ s (pf_entry … f) in
337    (mk_partial_fn le env g (pf_reggen … f)
338                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
339                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
340                   «l, ?» «pf_exit … f, ?»).
341[ % [ #l' @lookup_add_oblivious | // ]
342| @add_statement_inv' @p @(pi2 … (pf_entry …))
343| @forall_nodes_add //
344| whd >lookup_add_hit % #E destruct
345| @lookup_add_oblivious @(pi2 … (pf_exit …))
346] qed.
347
348lemma extend_typ_env : ∀te,r,t,r',t'.
349  env_has te r t → env_has (〈r',t'〉::te) r t.
350#tw #r #t #r' #t' #H %2 @H
351qed.
352
353lemma stmt_extend_typ_env : ∀te,r,t,s.
354  statement_typed te s → statement_typed (〈r,t〉::te) s.
355#tw #r #t *
356[ 3: #t' #r #cst #l #H %2 @H
357| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
358| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
359| *: //
360] qed.
361
362(* A little more nesting in the result type than I'd like, but it keeps the
363   function closely paired with the proof that it contains f. *)
364definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
365  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
366λle,env,f,ty.
367  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
368  let f' ≝
369    «mk_partial_fn le env
370       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
371       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
372       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
373  in
374    ❬f' , ?(*«r, ?»*)❭.
375[ @(«r, ?») % @refl
376| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
377| #i #t #r1 #H #L %2 @(pf_envok … f … L)
378| %2 @(pi2 … rt)
379| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
380] qed.
381
382axiom UnknownVariable : String.
383
384definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
385  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
386λle,env,ty,e,f.
387  match e return λty,e. expr_vars ty e (Env_has env) → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) with
388  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
389  | _ ⇒ λ_.fresh_reg le env f ?
390  ].
391[ % //
392| @(pf_envok … Env) @refl
393] qed.
394 
395let 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 ≝ 
396 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.
397 
398let rec foldr_all' (A:Type[0]) (P:A → Prop) (B:list A → Type[0]) (f:∀a:A. P a → ∀l. B l → B (a::l)) (b:B [ ]) (l:list A) (H:All ? P l) on l :B l ≝ 
399 match l return λx.All ? P x → B x with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) l (foldr_all' A P B f b l (proj2 … H))] H.
400
401definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
402
403definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
404λA,P,x. match x with [ mk_DPair a _ ⇒ a].
405
406definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
407                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
408                         𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es) ≝
409λle,env,es,f,Env.
410  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs es))
411    (λe,p,tl,acc.
412      match acc return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
413        match e return λe.exprtyp_present env e → 𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
414          match choose_reg le env t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has le env f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
415            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
416          ]
417        ] p
418      ]) ❬«f, ?», «[ ], I»❭ es Env.
419[ @p
420| cases r #r' #Hr' cases rs #rs' #Hrs'
421  % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
422| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
423| @fn_con_refl
424]  qed.
425
426lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
427((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
428∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
429#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
430
431
432lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
433  choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
434#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
435qed.
436
437lemma present_included : ∀le,env,f,f',l.
438  fn_contains le env f f' →
439  present ?? (pf_graph … f) l →
440  present ?? (pf_graph … f') l.
441#le #env #f #f' #l * #H1 #H2 @H1 qed.
442
443(* Some definitions for the add_stmt function later, which we introduce now so
444   that we can build the whole fn_graph_included machinery at once. *)
445
446(* We need to show that the graph only grows, and that Cminor labels will end
447   up in the graph. *)
448definition Cminor_labels_added ≝ λle,env,s,f'.
449∀l. Exists ? (λl'.l=l') (labels_of s) →
450∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
451
452record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
453{ stmt_graph_con : fn_contains … f f'
454; stmt_labels_added : Cminor_labels_added … s f'
455}.
456
457(* Build some machinery to solve fn_contains goals. *)
458
459(* A datatype saying how we intend to prove a step. *)
460inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
461| fn_con_eq : ∀f. fn_con_because le env f
462| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
463    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
464| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
465    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
466.
467
468(* Extract the starting function for a step. *)
469let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env ≝
470  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
471
472(* Some unification hints to pick the right step to apply.  The dummy variable
473   is there to provide goal that the lemma can't apply to, which causes an error
474   and forces the "repeat" tactical to stop.  The first hint recognises that we
475   have reached the desired starting point. *)
476
477unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
478  f' ≟ f,
479  b  ≟ fn_con_eq le env f
480
481  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
482.
483
484unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, f3:(Σf3:partial_fn le env. fn_contains le env f2 f3);
485  b ≟ fn_con_sig le env f1 f2 H12 f3
486
487  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
488.
489
490unification hint 1 ≔ le:label_env, env:env, f1:partial_fn le env, f2:partial_fn le env, H12 : fn_contains le env f1 f2, s:stmt, f3:(Σf3:partial_fn le env. add_stmt_inv le env s f2 f3);
491  b ≟ fn_con_addinv le env f1 f2 H12 s f3
492
493  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
494.
495
496(* A lemma to perform a step of the proof.  We can repeat this to do the whole
497   proof. *) 
498lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
499#le #env #f *
500[ #f @fn_con_refl
501| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
502| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
503] qed.
504
505axiom BadCminorProgram : String.
506
507let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
508  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
509  (dst:Σdst. fn_env_has … f dst ty)
510  on e: Σf':partial_fn le env. fn_contains … f f' ≝
511match e return λty,e.expr_vars ty e (Env_has env) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn le env. fn_contains … f f' with
512[ Id t i ⇒ λEnv,dst.
513    let r ≝ lookup_reg env i t Env in
514    match register_eq r dst with
515    [ inl _ ⇒ «f, ?»
516    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
517    ]
518| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
519| Op1 t t' op e' ⇒ λEnv,dst.
520    let ❬f,r❭ ≝ choose_reg … e' f Env in
521    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
522    let f ≝ add_expr … env ? e' Env f «r, ?» in
523      «pi1 … f, ?»
524| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
525    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
526    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
527    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
528    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
529    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
530      «pi1 … f, ?»
531| Mem t e' ⇒ λEnv,dst.
532    let ❬f,r❭ ≝ choose_reg … e' f Env in
533    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
534    let f ≝ add_expr … env ? e' Env f «r,?» in
535      «pi1 … f, ?»
536| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
537    let resume_at ≝ pf_entry … f in
538    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
539    let lfalse ≝ pf_entry … f in
540    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
541    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
542    let ❬f,r❭ ≝ choose_reg … e' f ? in
543    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
544    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
545      «pi1 … f, ?»
546| Ecost _ l e' ⇒ λEnv,dst.
547    let f ≝ add_expr … env ? e' Env f dst in
548    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
549      «f, ?»
550] Env dst.
551(* For new labels, we need to step back through the definitions of f until we
552   hit the point that it was added. *)
553try (repeat @fn_contains_step @I)
554try (#l #H @H)
555try (#l @I)
556[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
557| #l @(pi2 … dst)
558| 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
559| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
560| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
561| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
562| #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
563| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
564| @(π1 (π1 Env))
565| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
566| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
567] qed.
568
569let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
570                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
571                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
572match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
573[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
574| cons e et ⇒ λEnv.
575    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
576    [ nil ⇒ λ_.λpf.⊥
577    | cons r rt ⇒ λHdsts,pf.
578        let f' ≝ add_exprs ? env et ? rt ? f ? in
579        match e return λe.exprtyp_present ? e → fn_env_has le env f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
580          let f'' ≝ add_expr ? env ty e ? f' r in
581            «pi1 … f'', ?»
582        ] (proj1 ?? Env) (π1 Hdsts)
583    ]
584] Env Hdsts pf.
585try (repeat @fn_contains_step @I)
586[ 1,2: normalize in pf; destruct
587| @Env
588| @(fn_con_env … Hr) repeat @fn_contains_step @I
589| @(proj2 … Env)
590| normalize in pf; destruct @e0
591| @(π2 Hdsts)
592] qed.
593
594axiom UnknownLabel : String.
595axiom ReturnMismatch : String.
596
597definition stmt_inv : env → label_env → stmt → Prop ≝
598λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
599
600(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
601definition expr_is_Id : ∀t. expr t → option ident ≝
602λt,e. match e with
603[ Id _ id ⇒ Some ? id
604| _ ⇒ None ?
605].
606
607(* XXX Work around odd disambiguation errors. *)
608alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
609(* If reenabling tailcalls, change 12 to 14. *)
610alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
611
612lemma lookup_label_rev : ∀lenv,l,l',p.
613  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
614#lenv #l #l' #p
615cut (∃lx. lookup ?? lenv l = Some ? lx)
616[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
617  [ * #H cases (H (refl ??))
618  | #lx #_ %{lx} @refl
619  ]
620| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
621] qed.
622
623lemma lookup_label_rev' : ∀lenv,l,p.
624  lookup ?? lenv l = Some ? (lookup_label lenv l p).
625#lenv #l #p @lookup_label_rev [ @p | @refl ]
626qed.
627
628lemma lookup_label_lpresent : ∀lenv,l,p.
629  lpresent lenv (lookup_label lenv l p).
630#le #l #p whd %{l} @lookup_label_rev'
631qed.
632
633lemma empty_Cminor_labels_added : ∀le,env,s,f'.
634  labels_of s = [ ] → Cminor_labels_added le env s f'.
635#le #env #s #f' #E whd >E #l *;
636qed.
637
638lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
639  labels_of s = labels_of s' → Cminor_labels_added … s' f →
640  Cminor_labels_added le env s f.
641#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
642qed.
643
644lemma Cminor_labels_con : ∀le,env,s,f,f'.
645  fn_contains le env f f' →
646  Cminor_labels_added … s f →
647  Cminor_labels_added … s f'.
648#le #env #s #f #f' #INC #ADDED
649#l #E cases (ADDED l E) #l' * #L #P
650%{l'} % [ @L | @(present_included … P) @INC ]
651qed.
652
653lemma Cminor_labels_inv : ∀le,env,s,s',f.
654  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
655  Cminor_labels_added le env s f →
656  Cminor_labels_added le env s f'.
657#le #env #s #s' #f * #f' * #H1 #H2 #H3
658#l #E cases (H3 l E) #l' * #L #P
659%{l'} % [ @L | @(present_included … P) @H1 ]
660qed.
661
662lemma Cminor_labels_sig : ∀le,env,s,f.
663  ∀f':Σf':partial_fn le env. fn_contains … f f'.
664  Cminor_labels_added … s f →
665  Cminor_labels_added … s f'.
666#le #env #s #f * #f' #H1 #H2
667#l #E cases (H2 l E) #l' * #L #P
668%{l'} % [ @L | @(present_included … P) @H1 ]
669qed.
670
671let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
672match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
673[ St_skip ⇒ λ_. OK ? «f, ?»
674| St_assign t x e ⇒ λEnv.
675    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
676    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
677| St_store t e1 e2 ⇒ λEnv.
678    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
679    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
680    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
681    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
682    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
683| St_call return_opt_id e args ⇒ λEnv.
684    let return_opt_reg ≝
685      match return_opt_id return λo. ? → ? with
686      [ None ⇒ λ_. None ?
687      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
688      ] Env in
689    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
690    let f ≝
691      match expr_is_Id ? e with
692      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
693      | None ⇒
694        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
695        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
696        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
697      ] in
698    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
699(*
700| St_tailcall e args ⇒ λEnv.
701    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
702    let f ≝
703      match expr_is_Id ? e with
704      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
705      | None ⇒
706        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
707        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
708        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
709      ] in
710    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
711*)
712| St_seq s1 s2 ⇒ λEnv.
713    do f2 ← add_stmt env label_env s2 ? f;
714    do f1 ← add_stmt env label_env s1 ? f2;
715      OK ? «pi1 … f1, ?»
716| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
717    let l_next ≝ pf_entry … f in
718    do f2 ← add_stmt env label_env s2 (π2 Env) f;
719    let l2 ≝ pf_entry … f2 in
720    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
721    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f;
722    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
723    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
724    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
725| St_return opt_e ⇒ let f0 ≝ f in
726    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
727    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return o) f0 f') with
728    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
729    | Some e ⇒
730        match pf_result … f with
731        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
732        | Some r ⇒
733            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env env.add_stmt_inv … (St_return (Some ? e)) f0 f') with
734            [ mk_DPair ty e ⇒ λEnv.
735                match typ_eq (\snd r) ty with
736                [ inl E ⇒ let f ≝ add_expr label_env env ty e ? f «\fst r, ? E (* XXX E goes missing if I don't use it! *)» in
737                          OK ? «pi1 … f, ?»
738                | inr _ ⇒ Error ? (msg ReturnMismatch)
739                ]
740            ]
741        ]
742    ]
743| St_label l s' ⇒ λEnv.
744    do f ← add_stmt env label_env s' (π2 Env) f;
745    let l' ≝ lookup_label label_env l ? in
746    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
747| St_goto l ⇒ λEnv.
748    let l' ≝ lookup_label label_env l ? in
749    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
750| St_cost l s' ⇒ λEnv.
751    do f ← add_stmt env label_env s' (π2 Env) f;
752    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
753] Env.
754try @(π1 Env)
755try @(π2 Env)
756try @(π1 (π1 Env))
757try @(π2 (π1 Env))
758try @mk_add_stmt_inv
759try (repeat @fn_contains_step @I)
760try (@empty_Cminor_labels_added @refl)
761try (#l #H @I)
762try (#l #H @H)
763try (#l @I)
764[ @(pf_envok … (π1 (π1 Env))) @refl
765| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
766| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
767| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
768| @sym_eq @(All2_length … (pi2 ?? args_regs))
769| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
770| @(π1 (π1 (π1 Env)))
771| #l #H cases (Exists_append … H)
772  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
773  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
774  ]
775| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
776| #l #H cases (Exists_append … H)
777  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
778  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
779  ]
780| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
781| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
782| #_ (* see above *) <E @(pi2 ?? r)
783| @(pi2 … (pf_entry …))
784| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
785        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
786        ]
787| #l1 #H whd %2 @lookup_label_lpresent
788| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
789] qed.
790
791definition c2ra_function (*: internal_function → internal_function*) ≝
792λf.
793let labgen0 ≝ new_universe LabelTag in
794let reggen0 ≝ new_universe RegisterTag in
795let cminor_labels ≝ labels_of (f_body f) in
796let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
797let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
798let ❬locals_reggen, result❭ as E3 ≝
799  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
800  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
801  | Some ty ⇒
802      let 〈r,gen〉 ≝ fresh … reggen2 in
803        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
804let locals ≝ \fst locals_reggen in
805let reggen ≝ \snd locals_reggen in
806let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
807let 〈l,labgen〉 ≝ fresh … labgen1 in
808let emptyfn ≝
809  mk_partial_fn
810    label_env
811    env
812    labgen
813    reggen
814    params
815    locals
816    result
817    ?
818    (f_stacksize f)
819    (add ?? (empty_map …) l St_return)
820    ?
821    ?
822    l
823    l in
824do f ← add_stmt env label_env (f_body f) ? emptyfn;
825OK ? (mk_internal_function
826    (pf_labgen … f)
827    (pf_reggen … f)
828    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
829    (pf_params … f)
830    (pf_locals … f)
831    (pf_stacksize … f)
832    (pf_graph … f)
833    ?
834    (pf_typed … f)
835    (pf_entry … f)
836    (pf_exit … f)
837  ).
838[ -emptyfn @(stmt_P_mp … (f_inv f))
839  #s * #V #L %
840  [ @(stmt_vars_mp … V)
841    #i #t #H cases (Exists_append … H)
842    [ #H1 @(populate_extends … (sym_eq … E2))
843      [ @(populates_env_distinct … (sym_eq … E1)) //
844        @All_alt //
845      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
846      ]
847    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
848    ]
849  | @(stmt_labels_mp … L)
850    #l #H @(populates_label_env … (sym_eq … El)) @H
851  ]
852| #l #s #E @(labels_P_mp … (pf_closed … f l s E))
853  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
854  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
855  #P' @P'
856  | cases (label_env_contents … (sym_eq ??? El) l ?)
857    [ #H @H
858    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
859    | whd >H % #E' destruct (E')
860    ]
861  ]
862  ]
863| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
864  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
865    [ * * | normalize @Exists_append_r ]
866  | cases (f_return f) in E3;
867    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
868      @Exists_append_l
869    | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
870      #H' @Exists_append_l %2 @H'
871    ]
872  ]
873| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
874  [ * #E1 #E2 >E2 @I
875  | whd in ⊢ (??%? → ?); #E' destruct (E')
876  ]
877| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
878  [ * #E1 #E2 >E2 @I
879  | whd in ⊢ (??%? → ?); #E' destruct (E')
880  ]
881| 6,7: whd >lookup_add_hit % #E destruct
882| % @refl
883]
884qed.
885
886definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
887λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).
888
889include "Cminor/initialisation.ma".
890
891definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
892λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.