source: src/Cminor/toRTLabs.ma @ 2178

Last change on this file since 2178 was 2178, checked in by campbell, 7 years ago

Shift some notation into utilities.

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