source: src/Cminor/toRTLabs.ma @ 2260

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

Cminor to RTLabs is now a total function.

File size: 37.9 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(* Some data structures for the transformation that remain fixed throughout. *)
195record fixed : Type[0] ≝ {
196  fx_lenv   : label_env;
197  fx_env    : env;
198  fx_rettyp : option typ
199}.
200
201definition resultok : option typ → list (register × typ) → Type[0] ≝
202λty,env.
203  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
204
205(* I'd use a single parametrised definition along with internal_function, but
206   it's a pain without implicit parameters. *)
207record partial_fn (fx:fixed) : Type[0] ≝
208{ pf_labgen    : universe LabelTag
209; pf_reggen    : universe RegisterTag
210; pf_params    : list (register × typ)
211; pf_locals    : list (register × typ)
212; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
213; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
214; pf_stacksize : nat
215; pf_graph     : graph statement
216; pf_closed    : partially_closed (fx_lenv … fx) pf_graph
217; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
218; pf_entry     : Σl:label. present ?? pf_graph l
219; pf_exit      : Σl:label. present ?? pf_graph l
220}.
221
222definition fn_env_has ≝
223  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
224
225record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
226{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
227; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
228}.
229
230lemma fn_con_trans : ∀fx,f1,f2,f3.
231  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
232#fx #f1 #f2 #f3 #H1 #H2 %
233[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
234| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
235] qed.
236
237lemma fn_con_refl : ∀fx,f.
238  fn_contains fx f f.
239#fx #f % #l // qed.
240
241lemma fn_con_sig : ∀fx,f,f0.
242  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
243  fn_contains fx f f0 →
244  fn_contains fx f f'.
245#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
246qed.
247
248lemma add_statement_inv : ∀fx,l,s.∀f.
249  labels_present (pf_graph fx f) s →
250  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
251#fx #l #s #f #p
252#l' #s' #H cases (identifier_eq … l l')
253[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
254  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
255| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
256  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
257  | >lookup_add_miss in H; /2/
258  ]
259] qed.
260
261definition statement_typed_in ≝
262λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.
263
264lemma forall_nodes_add : ∀A,P,l,a,g.
265  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
266#A #P #l #a #g #ALL #NEW
267#l' #a'
268cases (identifier_eq … l' l)
269[ #E destruct >lookup_add_hit #E destruct @NEW
270| #ne >lookup_add_miss /2/
271] qed.
272
273(* Add a statement to the graph, *without* updating the entry label. *)
274definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
275  labels_present (pf_graph … f) s →
276  statement_typed_in … f s →
277  Σf':partial_fn fx. fn_contains … f f' ≝
278λfx,l,s,f,p,tp.
279  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
280                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
281                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
282                «pf_entry … f, ?» «pf_exit … f, ?».
283[ @add_statement_inv @p
284| @forall_nodes_add //
285| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
286| % [ #l' @lookup_add_oblivious | // ]
287] qed.
288
289(* Add a statement to the graph, making it the entry label. *)
290definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
291  labels_present (pf_graph … f) s →
292  statement_typed_in … f s →
293  Σf':partial_fn fx. fn_contains … f f' ≝
294λfx,l,s,f,p,tl.
295  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
296                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
297                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
298                «l, ?» «pf_exit … f, ?».
299[ @add_statement_inv @p
300| @forall_nodes_add //
301| whd >lookup_add_hit % #E destruct
302| @lookup_add_oblivious @(pi2 … (pf_exit … f))
303| % [ #l' @lookup_add_oblivious | // ]
304] qed.
305
306(* Add a statement with a fresh label to the start of the function.  The
307   statement is parametrised by the *next* instruction's label. *)
308definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
309  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
310  (∀l. statement_typed_in … f (s l)) →
311  Σf':partial_fn fx. fn_contains … f f' ≝
312λfx,s,f,p,tp.
313  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
314  let s' ≝ s (pf_entry … f) in
315    (mk_partial_fn fx g (pf_reggen … f)
316                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
317                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
318                   «l, ?» «pf_exit … f, ?»).
319[ % [ #l' @lookup_add_oblivious | // ]
320| @add_statement_inv @p @(pi2 … (pf_entry …))
321| @forall_nodes_add //
322| whd >lookup_add_hit % #E destruct
323| @lookup_add_oblivious @(pi2 … (pf_exit …))
324] qed.
325
326(* Variants for labels which are (goto) labels *)
327
328lemma add_statement_inv' : ∀fx,l,s.∀f.
329  labels_P (λl. present ?? (pf_graph fx f) l ∨ lpresent (fx_lenv … fx) l) s →
330  partially_closed (fx_lenv … fx) (add … (pf_graph … f) l s).
331#fx #l #s #f #p
332#l' #s' #H cases (identifier_eq … l l')
333[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
334  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
335| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
336  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
337  | >lookup_add_miss in H; /2/
338  ]
339] qed.
340
341definition add_fresh_to_graph' : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
342  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent (fx_lenv … fx) l) (s l)) →
343  (∀l. statement_typed_in … f (s l)) →
344  Σf':partial_fn fx. fn_contains … f f' ≝
345λfx,s,f,p,tp.
346  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
347  let s' ≝ s (pf_entry … f) in
348    (mk_partial_fn fx g (pf_reggen … f)
349                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
350                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
351                   «l, ?» «pf_exit … f, ?»).
352[ % [ #l' @lookup_add_oblivious | // ]
353| @add_statement_inv' @p @(pi2 … (pf_entry …))
354| @forall_nodes_add //
355| whd >lookup_add_hit % #E destruct
356| @lookup_add_oblivious @(pi2 … (pf_exit …))
357] qed.
358
359lemma extend_typ_env : ∀te,r,t,r',t'.
360  env_has te r t → env_has (〈r',t'〉::te) r t.
361#tw #r #t #r' #t' #H %2 @H
362qed.
363
364lemma stmt_extend_typ_env : ∀te,r,t,s.
365  statement_typed te s → statement_typed (〈r,t〉::te) s.
366#tw #r #t *
367[ 3: #t' #r #cst #l #H %2 @H
368| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
369| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
370| *: //
371] qed.
372
373(* A little more nesting in the result type than I'd like, but it keeps the
374   function closely paired with the proof that it contains f. *)
375definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
376  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
377λfx,f,ty.
378  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
379  let f' ≝
380    «mk_partial_fn fx
381       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
382       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
383  in
384    ❬f' , ?(*«r, ?»*)❭.
385[ @(«r, ?») % @refl
386| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
387| #i #t #r1 #H #L %2 @(pf_envok … f … L)
388| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
389| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
390] qed.
391
392definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
393  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
394λfx,ty,e,f.
395  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
396  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
397  | _ ⇒ λ_.fresh_reg … f ?
398  ].
399[ % //
400| @(pf_envok … Env) @refl
401] qed.
402 
403let 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 ≝ 
404 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.
405 
406let 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 ≝ 
407 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.
408
409definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
410
411definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
412λA,P,x. match x with [ mk_DPair a _ ⇒ a].
413
414definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
415                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
416                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
417λfx,es,f,Env.
418  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
419    (λe,p,tl,acc.
420      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
421        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
422          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
423            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
424          ]
425        ] p
426      ]) ❬«f, ?», «[ ], I»❭ es Env.
427[ @p
428| cases r #r' #Hr' cases rs #rs' #Hrs'
429  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
430| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
431| @fn_con_refl
432]  qed.
433
434lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
435((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
436∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
437#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
438
439
440lemma choose_regs_length : ∀fx,es,f,p,f',rs.
441  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
442#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
443qed.
444
445lemma present_included : ∀fx,f,f',l.
446  fn_contains fx f f' →
447  present ?? (pf_graph … f) l →
448  present ?? (pf_graph … f') l.
449#fx #f #f' #l * #H1 #H2 @H1 qed.
450
451(* Some definitions for the add_stmt function later, which we introduce now so
452   that we can build the whole fn_graph_included machinery at once. *)
453
454(* We need to show that the graph only grows, and that Cminor labels will end
455   up in the graph. *)
456definition Cminor_labels_added ≝ λfx,s,f'.
457∀l. Exists ? (λl'.l=l') (labels_of s) →
458∃l'. lookup ?? (fx_lenv fx) l = Some ? l' ∧ present ?? (pf_graph fx f') l'.
459
460record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
461{ stmt_graph_con : fn_contains … f f'
462; stmt_labels_added : Cminor_labels_added … s f'
463}.
464
465(* Build some machinery to solve fn_contains goals. *)
466
467(* A datatype saying how we intend to prove a step. *)
468inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
469| fn_con_eq : ∀f. fn_con_because fx f
470| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
471    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
472| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
473    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
474.
475
476(* Extract the starting function for a step. *)
477let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
478  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
479
480(* Some unification hints to pick the right step to apply.  The dummy variable
481   is there to provide goal that the lemma can't apply to, which causes an error
482   and forces the "repeat" tactical to stop.  The first hint recognises that we
483   have reached the desired starting point. *)
484
485unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
486  f' ≟ f,
487  b  ≟ fn_con_eq fx f
488
489  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
490.
491
492unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
493  b ≟ fn_con_sig fx f1 f2 H12 f3
494
495  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
496.
497
498unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
499  b ≟ fn_con_addinv fx f1 f2 H12 s f3
500
501  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
502.
503
504(* A lemma to perform a step of the proof.  We can repeat this to do the whole
505   proof. *) 
506lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
507#fx #f *
508[ #f @fn_con_refl
509| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
510| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
511] qed.
512
513
514let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
515  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
516  (dst:Σdst. fn_env_has … f dst ty)
517  on e: Σf':partial_fn fx. fn_contains … f f' ≝
518match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
519[ Id t i ⇒ λEnv,dst.
520    let r ≝ lookup_reg (fx_env fx) i t Env in
521    match register_eq r dst with
522    [ inl _ ⇒ «f, ?»
523    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
524    ]
525| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
526| Op1 t t' op e' ⇒ λEnv,dst.
527    let ❬f,r❭ ≝ choose_reg … e' f Env in
528    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
529    let f ≝ add_expr … ? e' Env f «r, ?» in
530      «pi1 … f, ?»
531| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
532    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
533    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
534    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
535    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
536    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
537      «pi1 … f, ?»
538| Mem t e' ⇒ λEnv,dst.
539    let ❬f,r❭ ≝ choose_reg … e' f Env in
540    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
541    let f ≝ add_expr … ? e' Env f «r,?» in
542      «pi1 … f, ?»
543| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
544    let resume_at ≝ pf_entry … f in
545    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
546    let lfalse ≝ pf_entry … f in
547    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
548    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
549    let ❬f,r❭ ≝ choose_reg … e' f ? in
550    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
551    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
552      «pi1 … f, ?»
553| Ecost _ l e' ⇒ λEnv,dst.
554    let f ≝ add_expr … ? e' Env f dst in
555    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
556      «f, ?»
557] Env dst.
558(* For new labels, we need to step back through the definitions of f until we
559   hit the point that it was added. *)
560try (repeat @fn_contains_step @I)
561try (#l #H @H)
562try (#l @I)
563[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
564| #l @(pi2 … dst)
565| 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
566| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
567| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
568| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
569| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
570| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
571| @(π1 (π1 Env))
572| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
573| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
574] qed.
575
576let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
577                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
578                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
579match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
580[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
581| cons e et ⇒ λEnv.
582    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
583    [ nil ⇒ λ_.λpf.⊥
584    | cons r rt ⇒ λHdsts,pf.
585        let f' ≝ add_exprs … et ? rt ? f ? in
586        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
587          let f'' ≝ add_expr … ty e ? f' r in
588            «pi1 … f'', ?»
589        ] (proj1 ?? Env) (π1 Hdsts)
590    ]
591] Env Hdsts pf.
592try (repeat @fn_contains_step @I)
593[ 1,2: normalize in pf; destruct
594| @Env
595| @(fn_con_env … Hr) repeat @fn_contains_step @I
596| @(proj2 … Env)
597| normalize in pf; destruct @e0
598| @(π2 Hdsts)
599] qed.
600
601definition return_ok ≝
602λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
603
604record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
605  si_vars : stmt_vars (Env_has (fx_env fx)) s;
606  si_labels : stmt_labels (present ?? (fx_lenv fx)) s;
607  si_return : return_ok (fx_rettyp fx) s
608}.
609
610definition stmts_inv : fixed → stmt → Prop ≝
611λfx. stmt_P (stmt_inv fx).
612
613(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
614definition expr_is_Id : ∀t. expr t → option ident ≝
615λt,e. match e with
616[ Id _ id ⇒ Some ? id
617| _ ⇒ None ?
618].
619
620(* XXX Work around odd disambiguation errors. *)
621alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
622(* If reenabling tailcalls, change 12 to 14. *)
623alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
624
625lemma lookup_label_rev : ∀lenv,l,l',p.
626  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
627#lenv #l #l' #p
628cut (∃lx. lookup ?? lenv l = Some ? lx)
629[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
630  [ * #H cases (H (refl ??))
631  | #lx #_ %{lx} @refl
632  ]
633| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
634] qed.
635
636lemma lookup_label_rev' : ∀lenv,l,p.
637  lookup ?? lenv l = Some ? (lookup_label lenv l p).
638#lenv #l #p @lookup_label_rev [ @p | @refl ]
639qed.
640
641lemma lookup_label_lpresent : ∀lenv,l,p.
642  lpresent lenv (lookup_label lenv l p).
643#le #l #p whd %{l} @lookup_label_rev'
644qed.
645
646lemma empty_Cminor_labels_added : ∀fx,s,f'.
647  labels_of s = [ ] → Cminor_labels_added fx s f'.
648#fx #s #f' #E whd >E #l *;
649qed.
650
651lemma equal_Cminor_labels_added : ∀fx,s,s',f.
652  labels_of s = labels_of s' → Cminor_labels_added … s' f →
653  Cminor_labels_added fx s f.
654#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
655qed.
656
657lemma Cminor_labels_con : ∀fx,s,f,f'.
658  fn_contains fx f f' →
659  Cminor_labels_added … s f →
660  Cminor_labels_added … s f'.
661#fx #s #f #f' #INC #ADDED
662#l #E cases (ADDED l E) #l' * #L #P
663%{l'} % [ @L | @(present_included … P) @INC ]
664qed.
665
666lemma Cminor_labels_inv : ∀fx,s,s',f.
667  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
668  Cminor_labels_added fx s f →
669  Cminor_labels_added fx s f'.
670#fx #s #s' #f * #f' * #H1 #H2 #H3
671#l #E cases (H3 l E) #l' * #L #P
672%{l'} % [ @L | @(present_included … P) @H1 ]
673qed.
674
675lemma Cminor_labels_sig : ∀fx,s,f.
676  ∀f':Σf':partial_fn fx. fn_contains … f f'.
677  Cminor_labels_added … s f →
678  Cminor_labels_added … s f'.
679#fx #s #f * #f' #H1 #H2
680#l #E cases (H2 l E) #l' * #L #P
681%{l'} % [ @L | @(present_included … P) @H1 ]
682qed.
683
684discriminator option.
685discriminator DPair.
686
687(* Return statements need a little careful treatment to avoid errors using the
688   invariant about the return type. *)
689
690definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
691  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
692λfx,opt_e,f.
693  let f0 ≝ f in
694  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
695  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
696  [ None ⇒ λEnv. «pi1 … f, ?»
697  | Some et ⇒
698    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
699    [ mk_DPair ty e ⇒ λEnv.
700      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
701      [ None ⇒ λH. ⊥
702      | Some t ⇒ λH,R.
703        match R with
704        [ mk_Sig r Hr ⇒
705            let f ≝ add_expr fx ty e ? f «r, ?» in
706            «pi1 … f, ?»
707        ]
708      ] (si_return … (π1 Env)) (pf_result fx f)
709    ]
710  ].
711[ @mk_add_stmt_inv /2/
712| inversion H #A #B #C destruct
713| @mk_add_stmt_inv
714  [ repeat @fn_contains_step @I
715  | @empty_Cminor_labels_added //
716  ]
717| @(si_vars … (π1 Env))
718| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
719| #l #H @I
720| #l //
721] qed.
722
723
724let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f' ≝
725match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
726[ St_skip ⇒ λ_. «f, ?»
727| St_assign t x e ⇒ λEnv.
728    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
729    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
730| St_store t e1 e2 ⇒ λEnv.
731    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
732    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
733    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
734    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
735    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
736| St_call return_opt_id e args ⇒ λEnv.
737    let return_opt_reg ≝
738      match return_opt_id return λo. ? → ? with
739      [ None ⇒ λ_. None ?
740      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
741      ] Env in
742    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
743    let f ≝
744      match expr_is_Id ? e with
745      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
746      | None ⇒
747        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
748        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
749        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
750      ] in
751    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
752| St_seq s1 s2 ⇒ λEnv.
753    let f2 ≝ add_stmt … s2 ? f in
754    let f1 ≝ add_stmt … s1 ? f2 in
755      «pi1 … f1, ?»
756| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
757    let l_next ≝ pf_entry … f in
758    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
759    let l2 ≝ pf_entry … f2 in
760    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
761    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
762    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
763    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
764    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
765| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
766| St_label l s' ⇒ λEnv.
767    let f ≝ add_stmt … s' (π2 Env) f in
768    let l' ≝ lookup_label (fx_lenv fx) l ? in
769    «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
770| St_goto l ⇒ λEnv.
771    let l' ≝ lookup_label (fx_lenv fx) l ? in
772    «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
773| St_cost l s' ⇒ λEnv.
774    let f ≝ add_stmt … s' (π2 Env) f in
775    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
776] Env.
777try @(π2 Env)
778try @(π1 (π2 Env))
779try @(π2 (π2 Env))
780try @mk_add_stmt_inv
781try (repeat @fn_contains_step @I)
782try (@empty_Cminor_labels_added @refl)
783try (#l #H @I)
784try (#l #H @H)
785try (#l @I)
786[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
787| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
788| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
789| @sym_eq @(All2_length … (pi2 ?? args_regs))
790| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
791| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
792| @(π1 (π1 (si_vars … (π1 Env))))
793| #l #H cases (Exists_append … H)
794  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
795  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
796  ]
797| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
798| #l #H cases (Exists_append … H)
799  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
800  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
801  ]
802| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
803| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
804| @(pi2 … (pf_entry …))
805| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
806        | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f))
807        ]
808| @(si_labels … (π1 Env))
809| #l1 #H whd %2 @lookup_label_lpresent
810| @(si_labels … (π1 Env))
811| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
812] qed.
813
814definition c2ra_function (*: internal_function → internal_function*) ≝
815λf.
816let labgen0 ≝ new_universe LabelTag in
817let reggen0 ≝ new_universe RegisterTag in
818let cminor_labels ≝ labels_of (f_body f) in
819let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
820let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
821let ❬locals_reggen, result❭ as E3 ≝
822  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
823  [ None ⇒ ❬〈locals0, reggen2〉, I❭
824  | Some ty ⇒
825      let 〈r,gen〉 ≝ fresh … reggen2 in
826        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
827let locals ≝ \fst locals_reggen in
828let reggen ≝ \snd locals_reggen in
829let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
830let 〈l,labgen〉 ≝ fresh … labgen1 in
831let fixed ≝ mk_fixed label_env env (f_return f) in
832let emptyfn ≝
833  mk_partial_fn fixed
834    labgen
835    reggen
836    params
837    locals
838    result
839    ?
840    (f_stacksize f)
841    (add ?? (empty_map …) l St_return)
842    ?
843    ?
844    l
845    l in
846let f ≝ add_stmt fixed (f_body f) ? emptyfn in
847  mk_internal_function
848    (pf_labgen … f)
849    (pf_reggen … f)
850    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
851    (pf_params … f)
852    (pf_locals … f)
853    (pf_stacksize … f)
854    (pf_graph … f)
855    ?
856    (pf_typed … f)
857    (pf_entry … f)
858    (pf_exit … f)
859  .
860[ #l #s #E @(labels_P_mp … (pf_closed … f l s E))
861  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
862  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
863  #P' @P'
864  | cases (label_env_contents … (sym_eq ??? El) l ?)
865    [ #H @H
866    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
867    | whd >H % #E' destruct (E')
868    ]
869  ]
870  ]
871| -emptyfn @(stmt_P_mp … (f_inv f))
872  #s * #V #L #R %
873  [ @(stmt_vars_mp … V)
874    #i #t #H cases (Exists_append … H)
875    [ #H1 @(populate_extends … (sym_eq … E2))
876      [ @(populates_env_distinct … (sym_eq … E1)) //
877        @All_alt //
878      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
879      ]
880    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
881    ]
882  | @(stmt_labels_mp … L)
883    #l #H @(populates_label_env … (sym_eq … El)) @H
884  | cases s in R ⊢ %; //
885  ]
886| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
887  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
888    [ * * | normalize @Exists_append_r ]
889  | (* gave up with     cases (f_return f) in result E3; *)
890    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
891    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
892      @Exists_append_l
893    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
894      #H' @Exists_append_l %2 @H'
895    ]
896  ]
897| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
898  [ * #E1 #E2 >E2 @I
899  | whd in ⊢ (??%? → ?); #E' destruct (E')
900  ]
901| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
902  [ * #E1 #E2 >E2 @I
903  | whd in ⊢ (??%? → ?); #E' destruct (E')
904  ]
905| 6,7: whd >lookup_add_hit % #E destruct
906| % @refl
907]
908qed.
909
910definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
911λp.transform_program … p (λ_. transf_fundef … c2ra_function).
912
913include "Cminor/initialisation.ma".
914
915definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
916λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.