source: src/Cminor/toRTLabs.ma @ 1631

Last change on this file since 1631 was 1631, checked in by campbell, 9 years ago

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

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)".
608alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
609
610definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
611λA,P,m,l,n.
612  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
613  [ None ⇒ λ_. Error ? m
614  | Some a ⇒ λH'. OK ? «a, ?»
615  ] (All_nth A P n l (pi2 … l)).
616@H' @refl qed.
617
618lemma lookup_label_rev : ∀lenv,l,l',p.
619  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
620#lenv #l #l' #p
621cut (∃lx. lookup ?? lenv l = Some ? lx)
622[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
623  [ * #H cases (H (refl ??))
624  | #lx #_ %{lx} @refl
625  ]
626| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
627] qed.
628
629lemma lookup_label_rev' : ∀lenv,l,p.
630  lookup ?? lenv l = Some ? (lookup_label lenv l p).
631#lenv #l #p @lookup_label_rev [ @p | @refl ]
632qed.
633
634lemma lookup_label_lpresent : ∀lenv,l,p.
635  lpresent lenv (lookup_label lenv l p).
636#le #l #p whd %{l} @lookup_label_rev'
637qed.
638
639lemma empty_Cminor_labels_added : ∀le,env,s,f'.
640  labels_of s = [ ] → Cminor_labels_added le env s f'.
641#le #env #s #f' #E whd >E #l *;
642qed.
643
644lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
645  labels_of s = labels_of s' → Cminor_labels_added … s' f →
646  Cminor_labels_added le env s f.
647#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
648qed.
649
650lemma Cminor_labels_con : ∀le,env,s,f,f'.
651  fn_contains le env f f' →
652  Cminor_labels_added … s f →
653  Cminor_labels_added … s f'.
654#le #env #s #f #f' #INC #ADDED
655#l #E cases (ADDED l E) #l' * #L #P
656%{l'} % [ @L | @(present_included … P) @INC ]
657qed.
658
659lemma Cminor_labels_inv : ∀le,env,s,s',f.
660  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
661  Cminor_labels_added le env s f →
662  Cminor_labels_added le env s f'.
663#le #env #s #s' #f * #f' * #H1 #H2 #H3
664#l #E cases (H3 l E) #l' * #L #P
665%{l'} % [ @L | @(present_included … P) @H1 ]
666qed.
667
668lemma Cminor_labels_sig : ∀le,env,s,f.
669  ∀f':Σf':partial_fn le env. fn_contains … f f'.
670  Cminor_labels_added … s f →
671  Cminor_labels_added … s f'.
672#le #env #s #f * #f' #H1 #H2
673#l #E cases (H2 l E) #l' * #L #P
674%{l'} % [ @L | @(present_included … P) @H1 ]
675qed.
676
677let 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') ≝
678match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
679[ St_skip ⇒ λ_. OK ? «f, ?»
680| St_assign t x e ⇒ λEnv.
681    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
682    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
683| St_store _ _ q e1 e2 ⇒ λEnv.
684    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
685    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
686    let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
687    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
688    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
689| St_call return_opt_id e args ⇒ λEnv.
690    let return_opt_reg ≝
691      match return_opt_id return λo. ? → ? with
692      [ None ⇒ λ_. None ?
693      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
694      ] Env in
695    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
696    let f ≝
697      match expr_is_Id ? e with
698      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
699      | None ⇒
700        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
701        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
702        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
703      ] in
704    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
705| St_tailcall e args ⇒ λEnv.
706    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
707    let f ≝
708      match expr_is_Id ? e with
709      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
710      | None ⇒
711        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
712        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
713        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
714      ] in
715    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
716| St_seq s1 s2 ⇒ λEnv.
717    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
718    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
719      OK ? «pi1 … f1, ?»
720| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
721    let l_next ≝ pf_entry … f in
722    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
723    let l2 ≝ pf_entry … f2 in
724    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
725    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
726    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
727    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
728    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
729| St_loop s ⇒ λEnv.
730    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
731    let l_loop ≝ pf_entry … f in
732    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
733    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
734| St_block s ⇒ λEnv.
735    do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
736    OK ? «pi1 … f, ?»
737| St_exit n ⇒ λEnv.
738    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
739    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
740| St_switch sz sg e tab n ⇒ λEnv.
741    let ❬f,r❭ ≝ choose_reg … e f ? in
742    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
743    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
744    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
745      do f ← f;
746      let 〈i,n〉 ≝ cs in
747      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
748      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
749      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
750      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
751      let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
752      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
753        OK ? «pi1 … f, ?») (OK ? f) tab;
754    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
755| St_return opt_e ⇒ let f0 ≝ f in
756    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
757    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
758    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
759    | Some e ⇒
760        match pf_result … f with
761        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
762        | Some r ⇒
763            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
764            [ mk_DPair ty e ⇒ λEnv.
765                match typ_eq (\snd r) ty with
766                [ 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
767                          OK ? «pi1 … f, ?»
768                | inr _ ⇒ Error ? (msg ReturnMismatch)
769                ]
770            ]
771        ]
772    ]
773| St_label l s' ⇒ λEnv.
774    do f ← add_stmt env label_env s' (π2 Env) f exits;
775    let l' ≝ lookup_label label_env l ? in
776    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
777| St_goto l ⇒ λEnv.
778    let l' ≝ lookup_label label_env l ? in
779    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
780| St_cost l s' ⇒ λEnv.
781    do f ← add_stmt env label_env s' (π2 Env) f exits;
782    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
783] Env.
784try @(π1 Env)
785try @(π2 Env)
786try @(π1 (π1 Env))
787try @(π2 (π1 Env))
788try @mk_add_stmt_inv
789try (repeat @fn_contains_step @I)
790try (@empty_Cminor_labels_added @refl)
791try (#l #H @I)
792try (#l #H @H)
793try (#l @I)
794[ @(pf_envok … (π1 (π1 Env))) @refl
795| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
796| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
797| 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
798| 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs))
799| 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
800| @(π1 (π1 (π1 Env)))
801| 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
802| #l #H cases (Exists_append … H)
803  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
804  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
805  ]
806| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
807| #l #H cases (Exists_append … H)
808  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
809  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
810  ]
811| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
812| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
813| @(pi2 … (pf_entry …))
814| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
815| % [ @pi2 | @(pi2 ?? exits) ]
816| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
817| #l' #H @(pi2 … l)
818| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
819| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
820| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
821| #_ (* see above *) <E @(pi2 ?? r)
822| @(pi2 … (pf_entry …))
823| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
824        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
825        ]
826| #l1 #H whd %2 @lookup_label_lpresent
827| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
828] qed.
829
830notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
831 with precedence 10
832for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
833        λ${ident E}.$s ] (refl ? $t) }.
834
835definition c2ra_function (*: internal_function → internal_function*) ≝
836λf.
837let labgen0 ≝ new_universe LabelTag in
838let reggen0 ≝ new_universe RegisterTag in
839let cminor_labels ≝ labels_of (f_body f) in
840let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
841let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
842let ❬locals_reggen, result❭ as E3 ≝
843  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
844  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
845  | Some ty ⇒
846      let 〈r,gen〉 ≝ fresh … reggen2 in
847        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
848let locals ≝ \fst locals_reggen in
849let reggen ≝ \snd locals_reggen in
850let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
851let 〈l,labgen〉 ≝ fresh … labgen1 in
852let emptyfn ≝
853  mk_partial_fn
854    label_env
855    env
856    labgen
857    reggen
858    params
859    locals
860    result
861    ?
862    (f_stacksize f)
863    (add ?? (empty_map …) l St_return)
864    ?
865    ?
866    l
867    l in
868do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
869OK ? (mk_internal_function
870    (pf_labgen … f)
871    (pf_reggen … f)
872    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
873    (pf_params … f)
874    (pf_locals … f)
875    (pf_stacksize … f)
876    (pf_graph … f)
877    ?
878    (pf_typed … f)
879    (pf_entry … f)
880    (pf_exit … f)
881  ).
882[ @I
883| -emptyfn @(stmt_P_mp … (f_inv f))
884  #s * #V #L %
885  [ @(stmt_vars_mp … V)
886    #i #t #H cases (Exists_append … H)
887    [ #H1 @(populate_extends … (sym_eq … E2))
888      [ @(populates_env_distinct … (sym_eq … E1)) //
889        @All_alt //
890      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
891      ]
892    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
893    ]
894  | @(stmt_labels_mp … L)
895    #l #H @(populates_label_env … (sym_eq … El)) @H
896  ]
897| #l #s #E @(labels_P_mp … (pf_closed … f l s E))
898  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
899  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
900  #P' @P'
901  | cases (label_env_contents … (sym_eq ??? El) l ?)
902    [ #H @H
903    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
904    | whd >H % #E' destruct (E')
905    ]
906  ]
907  ]
908| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
909  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
910    [ * * | normalize @Exists_append_r ]
911  | cases (f_return f) in E3;
912    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
913      @Exists_append_l
914    | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
915      #H' @Exists_append_l %2 @H'
916    ]
917  ]
918| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
919  [ * #E1 #E2 >E2 @I
920  | whd in ⊢ (??%? → ?); #E' destruct (E')
921  ]
922| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
923  [ * #E1 #E2 >E2 @I
924  | whd in ⊢ (??%? → ?); #E' destruct (E')
925  ]
926| 7,8: whd >lookup_add_hit % #E destruct
927| % @refl
928]
929qed.
930
931definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
932λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
933
934include "Cminor/initialisation.ma".
935
936definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
937λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.