source: src/Cminor/toRTLabs.ma @ 1680

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

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

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