source: src/Cminor/toRTLabs.ma @ 2292

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

More RTLabs invariants.

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