source: src/Cminor/toRTLabs.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 6 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 41.0 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag (register × typ).
7definition label_env ≝ identifier_map Label label.
8definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
9λen,gen. foldr ??
10 (λidt,rsengen.
11   let 〈id,ty〉 ≝ idt in
12   let 〈rs,en,gen〉 ≝ rsengen in
13   let 〈r,gen'〉 ≝ fresh … gen in
14     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
15
16definition Env_has : env → ident → typ → Prop ≝
17λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
18
19lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
20#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
21[ * | * #r #t' #E % #E' destruct ]
22qed.
23
24lemma populates_env : ∀l,e,u,l',e',u'.
25  distinct_env ?? l →
26  populate_env e u l = 〈l',e',u'〉 →
27  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
28      Env_has e' i t.
29#l elim l
30[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
31| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
32  * [ #E1 destruct (E1)
33      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
34      whd in ⊢ (??%? → ?);
35      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
36      #r #gen' #E1 #E2
37      whd in E2:(??%?); destruct;
38      whd >lookup_add_hit %
39    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
40      lapply (refl ? (populate_env e u tl))
41      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
42      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
43      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
44      whd in ⊢ (??%? → ?); #E destruct
45      whd >lookup_add_miss
46      [ @(IH … E1 ?? H) @(proj2 … D)
47      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
48      ]
49    ]
50] qed.
51
52lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
53  distinct_env ?? (l@r) →
54  populate_env e u l = 〈l',e',u'〉 →
55  All ? (λit. fresh_for_map … (\fst it) e) r →
56  All ? (λit. fresh_for_map … (\fst it) e') r.
57#r #l elim l
58[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
59| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
60  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
61  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
62  * #x #y #z #E2 >E2 in E;
63  whd in ⊢ (??%? → ?);
64  elim (fresh ? z)
65  #rg #gen' #E
66  whd in E:(??%?); destruct
67  #F lapply (IH … E2 F)
68  [ @(proj2 … D)
69  | lapply (All_append_r … (proj1 … D))
70    elim r
71    [ //
72    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
73      [ @fresh_for_map_add /2/
74      | @IH //
75      ]
76    ]
77  ]
78] qed.
79
80lemma populate_extends : ∀l,e,u,l',e',u'.
81  All ? (λit. fresh_for_map ?? (\fst it) e) l →
82  populate_env e u l = 〈l',e',u'〉 →
83  ∀i,t. Env_has e i t → Env_has e' i t.
84#l elim l
85[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
86| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
87  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
88  lapply (refl ? (populate_env e u tl))
89  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
90  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
91  destruct
92  #i #t #H whd >lookup_add_miss
93  [ @(IH … E0) [ @(proj2 … F) | @H ]
94  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
95] qed.
96
97definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
98/2/ qed.
99
100lemma populate_env_list : ∀l,e,u,l',e',u'.
101  populate_env e u l = 〈l',e',u'〉 →
102  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
103    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
104#l elim l
105[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
106| * #id #ty #tl #IH #e #u #l' #e' #u' #E
107  whd in E:(??%?);
108  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
109  lapply (refl ? (populate_env e u tl))
110  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
111  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
112  destruct
113  #i #r #t cases (identifier_eq ? i id)
114  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
115    generalize in ⊢ (??(??? (?%))? → ?);
116    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
117    %2 %1 %
118  | #NE #H #L cases (IH … E0 i r t ??)
119    [ /2/
120    | #X %2 %2 @X
121    | whd in H ⊢ %; >lookup_add_miss in H; //
122    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
123      lapply L -L
124      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
125      generalize in ⊢ (? → ? → ??(????%)?);
126      >lookup_add_miss // #H0 #p
127      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
128      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
129      #p' #X @X
130    ]
131  ]
132] qed.
133
134definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
135λen,gen. foldr ??
136 (λid,engen.
137   let 〈en,gen〉 ≝ engen in
138   let 〈r,gen'〉 ≝ fresh … gen in
139     〈add ?? en id r, gen'〉) 〈en, gen〉.
140
141lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
142  populate_label_env lbls u ls = 〈lbls',u'〉 →
143  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
144#ls elim ls
145[ #lbls #u #lbls' #u' #E #l *
146| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
147  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
148  lapply (refl ? (populate_label_env lbls u t))
149  cases (populate_label_env lbls u t) in ⊢ (???% → %);
150  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
151  cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);
152  #E destruct
153  #l *
154  [ #El <El whd >lookup_add_hit % #Er destruct
155  | #H @lookup_add_oblivious @(IH … E1 ? H)
156  ]
157] qed.
158
159lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
160  populate_label_env lbls u ls = 〈lbls',u'〉 →
161  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
162#ls elim ls
163[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
164| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
165  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
166  lapply (refl ? (populate_label_env lbls u t))
167  cases (populate_label_env lbls u t) in ⊢ (???% → %);
168  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
169  cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);
170  #E destruct
171  #l #H cases (identifier_eq ? l h)
172  [ #El %1 %1 @El
173  | #NE cases (IH … E1 l ?)
174    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
175  ]
176] qed.
177
178definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
179
180(* Check that the domain of one graph is included in another, for monotonicity
181   properties.  Note that we don't say anything about the statements. *)
182definition graph_included : graph statement → graph statement → Prop ≝
183λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
184
185lemma graph_inc_trans : ∀g1,g2,g3.
186  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
187#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
188
189definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
190
191definition partially_closed : label_env → graph statement → Prop ≝
192 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
193
194(* 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
505notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
506  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
507
508axiom BadCminorProgram : String.
509
510let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
511  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
512  (dst:Σdst. fn_env_has … f dst ty)
513  on e: Σf':partial_fn le env. fn_contains … f f' ≝
514match 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
515[ Id t i ⇒ λEnv,dst.
516    let r ≝ lookup_reg env i t Env in
517    match register_eq r dst with
518    [ inl _ ⇒ «f, ?»
519    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
520    ]
521| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
522| Op1 t t' op e' ⇒ λEnv,dst.
523    let ❬f,r❭ ≝ choose_reg … e' f Env in
524    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
525    let f ≝ add_expr … env ? e' Env f «r, ?» in
526      «pi1 … f, ?»
527| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
528    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
529    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
530    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
531    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
532    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
533      «pi1 … f, ?»
534| Mem t e' ⇒ λEnv,dst.
535    let ❬f,r❭ ≝ choose_reg … e' f Env in
536    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
537    let f ≝ add_expr … env ? e' Env f «r,?» in
538      «pi1 … f, ?»
539| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
540    let resume_at ≝ pf_entry … f in
541    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
542    let lfalse ≝ pf_entry … f in
543    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
544    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
545    let ❬f,r❭ ≝ choose_reg … e' f ? in
546    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
547    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
548      «pi1 … f, ?»
549| Ecost _ l e' ⇒ λEnv,dst.
550    let f ≝ add_expr … env ? e' Env f dst in
551    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
552      «f, ?»
553] Env dst.
554(* For new labels, we need to step back through the definitions of f until we
555   hit the point that it was added. *)
556try (repeat @fn_contains_step @I)
557try (#l #H @H)
558try (#l @I)
559[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
560| #l @(pi2 … dst)
561| 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
562| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
563| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
564| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
565| #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
566| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
567| @(π1 (π1 Env))
568| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
569| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
570] qed.
571
572let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
573                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
574                  (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' ≝
575match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
576[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
577| cons e et ⇒ λEnv.
578    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
579    [ nil ⇒ λ_.λpf.⊥
580    | cons r rt ⇒ λHdsts,pf.
581        let f' ≝ add_exprs ? env et ? rt ? f ? in
582        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.
583          let f'' ≝ add_expr ? env ty e ? f' r in
584            «pi1 … f'', ?»
585        ] (proj1 ?? Env) (π1 Hdsts)
586    ]
587] Env Hdsts pf.
588try (repeat @fn_contains_step @I)
589[ 1,2: normalize in pf; destruct
590| @Env
591| @(fn_con_env … Hr) repeat @fn_contains_step @I
592| @(proj2 … Env)
593| normalize in pf; destruct @e0
594| @(π2 Hdsts)
595] qed.
596
597axiom UnknownLabel : String.
598axiom ReturnMismatch : String.
599
600definition stmt_inv : env → label_env → stmt → Prop ≝
601λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
602
603(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
604definition expr_is_Id : ∀t. expr t → option ident ≝
605λt,e. match e with
606[ Id _ id ⇒ Some ? id
607| _ ⇒ None ?
608].
609
610(* XXX Work around odd disambiguation errors. *)
611alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
612(* If reenabling tailcalls, change 12 to 14. *)
613alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
614
615definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
616λA,P,m,l,n.
617  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
618  [ None ⇒ λ_. Error ? m
619  | Some a ⇒ λH'. OK ? «a, ?»
620  ] (All_nth A P n l (pi2 … l)).
621@H' @refl qed.
622
623lemma lookup_label_rev : ∀lenv,l,l',p.
624  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
625#lenv #l #l' #p
626cut (∃lx. lookup ?? lenv l = Some ? lx)
627[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
628  [ * #H cases (H (refl ??))
629  | #lx #_ %{lx} @refl
630  ]
631| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
632] qed.
633
634lemma lookup_label_rev' : ∀lenv,l,p.
635  lookup ?? lenv l = Some ? (lookup_label lenv l p).
636#lenv #l #p @lookup_label_rev [ @p | @refl ]
637qed.
638
639lemma lookup_label_lpresent : ∀lenv,l,p.
640  lpresent lenv (lookup_label lenv l p).
641#le #l #p whd %{l} @lookup_label_rev'
642qed.
643
644lemma empty_Cminor_labels_added : ∀le,env,s,f'.
645  labels_of s = [ ] → Cminor_labels_added le env s f'.
646#le #env #s #f' #E whd >E #l *;
647qed.
648
649lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
650  labels_of s = labels_of s' → Cminor_labels_added … s' f →
651  Cminor_labels_added le env s f.
652#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
653qed.
654
655lemma Cminor_labels_con : ∀le,env,s,f,f'.
656  fn_contains le env f f' →
657  Cminor_labels_added … s f →
658  Cminor_labels_added … s f'.
659#le #env #s #f #f' #INC #ADDED
660#l #E cases (ADDED l E) #l' * #L #P
661%{l'} % [ @L | @(present_included … P) @INC ]
662qed.
663
664lemma Cminor_labels_inv : ∀le,env,s,s',f.
665  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
666  Cminor_labels_added le env s f →
667  Cminor_labels_added le env s f'.
668#le #env #s #s' #f * #f' * #H1 #H2 #H3
669#l #E cases (H3 l E) #l' * #L #P
670%{l'} % [ @L | @(present_included … P) @H1 ]
671qed.
672
673lemma Cminor_labels_sig : ∀le,env,s,f.
674  ∀f':Σf':partial_fn le env. fn_contains … f f'.
675  Cminor_labels_added … s f →
676  Cminor_labels_added … s f'.
677#le #env #s #f * #f' #H1 #H2
678#l #E cases (H2 l E) #l' * #L #P
679%{l'} % [ @L | @(present_included … P) @H1 ]
680qed.
681
682let 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') ≝
683match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
684[ St_skip ⇒ λ_. OK ? «f, ?»
685| St_assign t x e ⇒ λEnv.
686    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
687    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
688| St_store t e1 e2 ⇒ λEnv.
689    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
690    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
691    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
692    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
693    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
694| St_call return_opt_id e args ⇒ λEnv.
695    let return_opt_reg ≝
696      match return_opt_id return λo. ? → ? with
697      [ None ⇒ λ_. None ?
698      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
699      ] Env in
700    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
701    let f ≝
702      match expr_is_Id ? e with
703      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
704      | None ⇒
705        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
706        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
707        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
708      ] in
709    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
710(*
711| St_tailcall e args ⇒ λEnv.
712    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
713    let f ≝
714      match expr_is_Id ? e with
715      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
716      | None ⇒
717        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
718        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
719        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
720      ] in
721    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
722*)
723| St_seq s1 s2 ⇒ λEnv.
724    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
725    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
726      OK ? «pi1 … f1, ?»
727| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
728    let l_next ≝ pf_entry … f in
729    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
730    let l2 ≝ pf_entry … f2 in
731    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
732    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
733    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
734    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
735    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
736| St_loop s ⇒ λEnv.
737    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
738    let l_loop ≝ pf_entry … f in
739    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
740    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
741| St_block s ⇒ λEnv.
742    do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
743    OK ? «pi1 … f, ?»
744| St_exit n ⇒ λEnv.
745    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
746    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
747| St_switch sz sg e tab n ⇒ λEnv.
748    let ❬f,r❭ ≝ choose_reg … e f ? in
749    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
750    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
751    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
752      do f ← f;
753      let 〈i,n〉 ≝ cs in
754      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
755      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
756      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
757      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
758      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
759      let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
760        OK ? «pi1 … f, ?») (OK ? f) tab;
761    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
762| St_return opt_e ⇒ let f0 ≝ f in
763    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
764    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
765    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
766    | Some e ⇒
767        match pf_result … f with
768        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
769        | Some r ⇒
770            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
771            [ mk_DPair ty e ⇒ λEnv.
772                match typ_eq (\snd r) ty with
773                [ 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
774                          OK ? «pi1 … f, ?»
775                | inr _ ⇒ Error ? (msg ReturnMismatch)
776                ]
777            ]
778        ]
779    ]
780| St_label l s' ⇒ λEnv.
781    do f ← add_stmt env label_env s' (π2 Env) f exits;
782    let l' ≝ lookup_label label_env l ? in
783    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
784| St_goto l ⇒ λEnv.
785    let l' ≝ lookup_label label_env l ? in
786    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
787| St_cost l s' ⇒ λEnv.
788    do f ← add_stmt env label_env s' (π2 Env) f exits;
789    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
790] Env.
791try @(π1 Env)
792try @(π2 Env)
793try @(π1 (π1 Env))
794try @(π2 (π1 Env))
795try @mk_add_stmt_inv
796try (repeat @fn_contains_step @I)
797try (@empty_Cminor_labels_added @refl)
798try (#l #H @I)
799try (#l #H @H)
800try (#l @I)
801[ @(pf_envok … (π1 (π1 Env))) @refl
802| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
803| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
804| (*4,8:*) @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
805| (*5,9:*) @sym_eq @(All2_length … (pi2 ?? args_regs))
806| (*6,10:*) @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
807| @(π1 (π1 (π1 Env)))
808| 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
809| #l #H cases (Exists_append … H)
810  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
811  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
812  ]
813| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
814| #l #H cases (Exists_append … H)
815  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
816  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
817  ]
818| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
819| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
820| @(pi2 … (pf_entry …))
821| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
822| % [ @pi2 | @(pi2 ?? exits) ]
823| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
824| #l' #H @(pi2 … l)
825| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
826| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
827| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
828| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
829| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
830| #_ (* see above *) <E @(pi2 ?? r)
831| @(pi2 … (pf_entry …))
832| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
833        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
834        ]
835| #l1 #H whd %2 @lookup_label_lpresent
836| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
837] qed.
838
839notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
840 with precedence 10
841for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
842        λ${ident E}.$s ] (refl ? $t) }.
843
844definition c2ra_function (*: internal_function → internal_function*) ≝
845λf.
846let labgen0 ≝ new_universe LabelTag in
847let reggen0 ≝ new_universe RegisterTag in
848let cminor_labels ≝ labels_of (f_body f) in
849let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
850let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
851let ❬locals_reggen, result❭ as E3 ≝
852  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
853  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
854  | Some ty ⇒
855      let 〈r,gen〉 ≝ fresh … reggen2 in
856        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
857let locals ≝ \fst locals_reggen in
858let reggen ≝ \snd locals_reggen in
859let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
860let 〈l,labgen〉 ≝ fresh … labgen1 in
861let emptyfn ≝
862  mk_partial_fn
863    label_env
864    env
865    labgen
866    reggen
867    params
868    locals
869    result
870    ?
871    (f_stacksize f)
872    (add ?? (empty_map …) l St_return)
873    ?
874    ?
875    l
876    l in
877do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
878OK ? (mk_internal_function
879    (pf_labgen … f)
880    (pf_reggen … f)
881    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
882    (pf_params … f)
883    (pf_locals … f)
884    (pf_stacksize … f)
885    (pf_graph … f)
886    ?
887    (pf_typed … f)
888    (pf_entry … f)
889    (pf_exit … f)
890  ).
891[ @I
892| -emptyfn @(stmt_P_mp … (f_inv f))
893  #s * #V #L %
894  [ @(stmt_vars_mp … V)
895    #i #t #H cases (Exists_append … H)
896    [ #H1 @(populate_extends … (sym_eq … E2))
897      [ @(populates_env_distinct … (sym_eq … E1)) //
898        @All_alt //
899      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
900      ]
901    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
902    ]
903  | @(stmt_labels_mp … L)
904    #l #H @(populates_label_env … (sym_eq … El)) @H
905  ]
906| #l #s #E @(labels_P_mp … (pf_closed … f l s E))
907  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
908  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
909  #P' @P'
910  | cases (label_env_contents … (sym_eq ??? El) l ?)
911    [ #H @H
912    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
913    | whd >H % #E' destruct (E')
914    ]
915  ]
916  ]
917| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
918  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
919    [ * * | normalize @Exists_append_r ]
920  | cases (f_return f) in E3;
921    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
922      @Exists_append_l
923    | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
924      #H' @Exists_append_l %2 @H'
925    ]
926  ]
927| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
928  [ * #E1 #E2 >E2 @I
929  | whd in ⊢ (??%? → ?); #E' destruct (E')
930  ]
931| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
932  [ * #E1 #E2 >E2 @I
933  | whd in ⊢ (??%? → ?); #E' destruct (E')
934  ]
935| 7,8: whd >lookup_add_hit % #E destruct
936| % @refl
937]
938qed.
939
940definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
941λp.transform_partial_program … p (λ_. transf_partial_fundef … c2ra_function).
942
943include "Cminor/initialisation.ma".
944
945definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
946λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.