source: src/Cminor/toRTLabs.ma @ 2287

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

RTLabs typing for loads and stores.

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