source: src/Cminor/toRTLabs.ma @ 2252

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

Use the return statement invariant. Restructure the invariants for Cminor
a bit to make them more understandable.

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