source: src/Cminor/toRTLabs.ma @ 2390

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

Tidy up a corner case when generating RTLabs so that we generate
less skips.

File size: 39.9 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 populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
8λen,gen. foldr ??
9 (λidt,rsengen.
10   let 〈id,ty〉 ≝ idt in
11   let 〈rs,en,gen〉 ≝ rsengen in
12   let 〈r,gen'〉 ≝ fresh … gen in
13     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
14
15definition Env_has : env → ident → typ → Prop ≝
16λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
17
18lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
19#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
20[ * | * #r #t' #E % #E' destruct ]
21qed.
22
23lemma populates_env : ∀l,e,u,l',e',u'.
24  distinct_env ?? l →
25  populate_env e u l = 〈l',e',u'〉 →
26  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
27      Env_has e' i t.
28#l elim l
29[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
30| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
31  * [ #E1 destruct (E1)
32      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
33      whd in ⊢ (??%? → ?);
34      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
35      #r #gen' #E1 #E2
36      whd in E2:(??%?); destruct;
37      whd >lookup_add_hit %
38    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
39      lapply (refl ? (populate_env e u tl))
40      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
41      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
42      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
43      whd in ⊢ (??%? → ?); #E destruct
44      whd >lookup_add_miss
45      [ @(IH … E1 ?? H) @(proj2 … D)
46      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
47      ]
48    ]
49] qed.
50
51lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
52  distinct_env ?? (l@r) →
53  populate_env e u l = 〈l',e',u'〉 →
54  All ? (λit. fresh_for_map … (\fst it) e) r →
55  All ? (λit. fresh_for_map … (\fst it) e') r.
56#r #l elim l
57[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
58| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
59  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
60  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
61  * #x #y #z #E2 >E2 in E;
62  whd in ⊢ (??%? → ?);
63  elim (fresh ? z)
64  #rg #gen' #E
65  whd in E:(??%?); destruct
66  #F lapply (IH … E2 F)
67  [ @(proj2 … D)
68  | lapply (All_append_r … (proj1 … D))
69    elim r
70    [ //
71    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
72      [ @fresh_for_map_add /2/
73      | @IH //
74      ]
75    ]
76  ]
77] qed.
78
79lemma populate_extends : ∀l,e,u,l',e',u'.
80  All ? (λit. fresh_for_map ?? (\fst it) e) l →
81  populate_env e u l = 〈l',e',u'〉 →
82  ∀i,t. Env_has e i t → Env_has e' i t.
83#l elim l
84[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
85| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
86  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
87  lapply (refl ? (populate_env e u tl))
88  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
89  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
90  destruct
91  #i #t #H whd >lookup_add_miss
92  [ @(IH … E0) [ @(proj2 … F) | @H ]
93  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
94] qed.
95
96definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
97/2/ qed.
98
99lemma populate_env_list : ∀l,e,u,l',e',u'.
100  populate_env e u l = 〈l',e',u'〉 →
101  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
102    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
103#l elim l
104[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
105| * #id #ty #tl #IH #e #u #l' #e' #u' #E
106  whd in E:(??%?);
107  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
108  lapply (refl ? (populate_env e u tl))
109  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
110  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
111  destruct
112  #i #r #t cases (identifier_eq ? i id)
113  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
114    generalize in ⊢ (??(??? (?%))? → ?);
115    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
116    %2 %1 %
117  | #NE #H #L cases (IH … E0 i r t ??)
118    [ /2/
119    | #X %2 %2 @X
120    | whd in H ⊢ %; >lookup_add_miss in H; //
121    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
122      lapply L -L
123      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
124      generalize in ⊢ (? → ? → ??(????%)?);
125      >lookup_add_miss // #H0 #p
126      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
127      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
128      #p' #X @X
129    ]
130  ]
131] qed.
132
133(* Check that the domain of one graph is included in another, for monotonicity
134   properties.  Note that we don't say anything about the statements. *)
135definition graph_included : graph statement → graph statement → Prop ≝
136extends_domain ??.
137
138lemma graph_inc_trans : ∀g1,g2,g3.
139  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
140@extends_dom_trans
141qed.
142
143
144(* Some data structures for the transformation that remain fixed throughout. *)
145record fixed : Type[0] ≝ {
146  fx_gotos  : identifier_set Label;
147  fx_env    : env;
148  fx_rettyp : option typ
149}.
150
151definition resultok : option typ → list (register × typ) → Type[0] ≝
152λty,env.
153  match ty with [ Some t ⇒ Σr:register. env_has env r t | _ ⇒ True ].
154
155(* We put in dummy statements for gotos, then change them afterwards once we
156   know their true destinations.  So first we need a mapping between the dummy
157   CFG nodes and the Cminor destination.  (We'll also keep a mapping of goto
158   labels to their RTLabs statements.) *)
159
160record goto_map (fx:fixed) (g:graph statement) : Type[0] ≝ {
161  gm_map :> identifier_map LabelTag (identifier Label);
162  gm_dom : ∀id. present ?? gm_map id → present ?? g id;
163  gm_img : ∀id,l. lookup … gm_map id = Some ? l → present ?? (fx_gotos fx) l
164}.
165
166(* I'd use a single parametrised definition along with internal_function, but
167   it's a pain without implicit parameters. *)
168record partial_fn (fx:fixed) : Type[0] ≝
169{ pf_labgen    : universe LabelTag
170; pf_reggen    : universe RegisterTag
171; pf_params    : list (register × typ)
172; pf_locals    : list (register × typ)
173; pf_result    : resultok (fx_rettyp … fx) (pf_locals @ pf_params)
174; pf_envok     : ∀id,ty,r,H. lookup_reg (fx_env … fx) id ty H = r → env_has (pf_locals @ pf_params) r ty
175; pf_stacksize : nat
176; pf_graph     : graph statement
177; pf_closed    : graph_closed pf_graph
178; pf_gotos     : goto_map fx pf_graph
179; pf_labels    : Σm:identifier_map Label (identifier LabelTag). ∀l,l'. lookup … m l = Some ? l' → present ?? pf_graph l'
180; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
181; pf_entry     : Σl:label. present ?? pf_graph l
182; pf_exit      : Σl:label. present ?? pf_graph l
183}.
184
185definition fn_env_has ≝
186  λfx,f. env_has (pf_locals fx f @ pf_params fx f).
187
188(* TODO: move or use another definition if there's already one *)
189definition map_extends : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝
190λtag,A,m1,m2. ∀id,a. lookup tag A m1 id = Some A a → lookup tag A m2 id = Some A a.
191
192lemma map_extends_trans : ∀tag,A,m1,m2,m3.
193  map_extends tag A m1 m2 →
194  map_extends tag A m2 m3 →
195  map_extends tag A m1 m3.
196/3/
197qed.
198
199record fn_contains (fx:fixed) (f1:partial_fn fx) (f2:partial_fn fx) : Prop ≝
200{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
201; fn_con_env : ∀r,ty. fn_env_has … f1 r ty → fn_env_has … f2 r ty
202; fn_con_labels : extends_domain … (pf_labels … f1) (pf_labels … f2)
203}.
204
205lemma fn_con_trans : ∀fx,f1,f2,f3.
206  fn_contains fx f1 f2 → fn_contains … f2 f3 → fn_contains … f1 f3.
207#fx #f1 #f2 #f3 #H1 #H2 %
208[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
209| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
210| @(extends_dom_trans … (fn_con_labels … H1) (fn_con_labels … H2))
211] qed.
212
213lemma fn_con_refl : ∀fx,f.
214  fn_contains fx f f.
215#fx #f % #l // qed.
216
217lemma fn_con_sig : ∀fx,f,f0.
218  ∀f':Σf':partial_fn fx. fn_contains … f0 f'.
219  fn_contains fx f f0 →
220  fn_contains fx f f'.
221#fx #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
222qed.
223
224lemma add_statement_inv : ∀fx,l,s.∀f.
225  labels_present (pf_graph fx f) s →
226  graph_closed (add … (pf_graph … f) l s).
227#fx #l #s #f #p
228#l' #s' #H cases (identifier_eq … l l')
229[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
230  @(labels_P_mp … p) #l0 #H @lookup_add_oblivious @H
231| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
232  [ #lx #H @lookup_add_oblivious @H
233  | >lookup_add_miss in H; /2/
234  ]
235] qed.
236
237definition statement_typed_in ≝
238λfx,f,s. statement_typed (pf_locals fx f @ pf_params fx f) s.
239
240lemma forall_nodes_add : ∀A,P,l,a,g.
241  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
242#A #P #l #a #g #ALL #NEW
243#l' #a'
244cases (identifier_eq … l' l)
245[ #E destruct >lookup_add_hit #E destruct @NEW
246| #ne >lookup_add_miss /2/
247] qed.
248
249(* Add a statement to the graph, *without* updating the entry label. *)
250definition fill_in_statement : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
251  labels_present (pf_graph … f) s →
252  statement_typed_in … f s →
253  Σf':partial_fn fx. fn_contains … f f' ≝
254λfx,l,s,f,p,tp.
255  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
256                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
257                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ?
258                (mk_goto_map … (pf_gotos … f) ??) «pf_labels … f, ?» ?
259                «pf_entry … f, ?» «pf_exit … f, ?».
260[ @add_statement_inv @p
261| @gm_img
262| #id #PR @lookup_add_oblivious @(gm_dom … PR)
263| #l1 #l2 #L @lookup_add_oblivious @(pi2 … (pf_labels … f) … L)
264| @forall_nodes_add //
265| 6,7: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
266| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
267] qed.
268
269(* Add a statement to the graph, making it the entry label. *)
270definition add_to_graph : ∀fx. label → ∀s:statement. ∀f:partial_fn fx.
271  labels_present (pf_graph … f) s →
272  statement_typed_in … f s →
273  Σf':partial_fn fx. fn_contains … f f' ≝
274λfx,l,s,f,p,tl.
275  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
276                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
277                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ????
278                «l, ?» «pf_exit … f, ?».
279[ @add_statement_inv @p
280| cases (pf_gotos … f) #m #dom #img %
281  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
282| cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
283| @forall_nodes_add //
284| whd >lookup_add_hit % #E destruct
285| @lookup_add_oblivious @(pi2 … (pf_exit … f))
286| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
287] qed.
288
289(* Change the entry point to the function (i.e., the successor for any new
290   instructions that we add). *)
291definition change_entry : ∀fx. ∀f:partial_fn fx.
292  ∀l. present ?? (pf_graph … f) l →
293  Σf':partial_fn fx. fn_contains … f f' ≝
294λfx,f,l,PR.
295  mk_partial_fn fx (pf_labgen … f) (pf_reggen … f)
296                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
297                (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f)
298                (pf_labels … f) (pf_typed … f)
299                «l, PR» (pf_exit … f).
300% //
301qed.
302
303(* Add a statement with a fresh label to the start of the function.  The
304   statement is parametrised by the *next* instruction's label. *)
305definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
306  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
307  (∀l. statement_typed_in … f (s l)) →
308  Σf':partial_fn fx. fn_contains … f f' ≝
309λfx,s,f,p,tp.
310  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
311  let s' ≝ s (pf_entry … f) in
312    (mk_partial_fn fx g (pf_reggen … f)
313                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
314                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
315                   «l, ?» «pf_exit … f, ?»).
316[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
317| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
318| @add_statement_inv @p @(pi2 … (pf_entry …))
319| cases (pf_gotos … f) #m #dom #img %
320  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
321| @forall_nodes_add //
322| whd >lookup_add_hit % #E destruct
323| @lookup_add_oblivious @(pi2 … (pf_exit …))
324] qed.
325
326lemma extend_typ_env : ∀te,r,t,r',t'.
327  env_has te r t → env_has (〈r',t'〉::te) r t.
328#tw #r #t #r' #t' #H %2 @H
329qed.
330
331lemma stmt_extend_typ_env : ∀te,r,t,s.
332  statement_typed te s → statement_typed (〈r,t〉::te) s.
333#tw #r #t *
334[ 1,2: //
335| #t' #r #cst #l #H %2 @H
336| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
337| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
338| 6,7: #t' #r1 #r2 #l * /3/
339| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
340| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
341| #r' #l1 #l2 * #t' #E /3/
342| //
343] qed.
344
345(* A little more nesting in the result type than I'd like, but it keeps the
346   function closely paired with the proof that it contains f. *)
347definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
348  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
349λfx,f,ty.
350  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
351  let f' ≝
352    «mk_partial_fn fx
353       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
354       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
355  in
356    ❬f' , ?(*«r, ?»*)❭.
357[ @(«r, ?») % @refl
358| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
359| #i #t #r1 #H #L %2 @(pf_envok … f … L)
360| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
361| % [ #l // | #r' #ty' #H @extend_typ_env @H | // ]
362] qed.
363
364definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
365  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
366λfx,ty,e,f.
367  match e return λty,e. expr_vars ty e (Env_has (fx_env fx)) → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) with
368  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
369  | _ ⇒ λ_.fresh_reg … f ?
370  ].
371[ % //
372| @(pf_envok … Env) @refl
373] qed.
374 
375let 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 ≝ 
376 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.
377 
378let 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 ≝ 
379 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.
380
381definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
382
383definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
384λA,P,x. match x with [ mk_DPair a _ ⇒ a].
385
386definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
387                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
388                         𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es) ≝
389λfx,es,f,Env.
390  foldr_all' (𝚺t:typ.expr t) ? (λes. 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs es))
391    (λe,p,tl,acc.
392      match acc return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair f1 rs ⇒
393        match e return λe.exprtyp_present (fx_env fx) e → 𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (e::tl)) with [ mk_DPair t e ⇒ λp.
394          match choose_reg fx t e (pi1 … f1) ? return λ_.𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σrs:list register. All2 ?? (λr,e. fn_env_has … f' r (eject' typ expr e)) rs (❬t,e❭::tl)) with [ mk_DPair f' r ⇒
395            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
396          ]
397        ] p
398      ]) ❬«f, ?», «[ ], I»❭ es Env.
399[ @p
400| cases r #r' #Hr' cases rs #rs' #Hrs'
401  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
402| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
403| @fn_con_refl
404]  qed.
405
406lemma choose_regs_length : ∀fx,es,f,p,f',rs.
407  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
408#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
409qed.
410
411lemma present_included : ∀fx,f,f',l.
412  fn_contains fx f f' →
413  present ?? (pf_graph … f) l →
414  present ?? (pf_graph … f') l.
415#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.
416
417(* Some definitions for the add_stmt function later, which we introduce now so
418   that we can build the whole fn_graph_included machinery at once. *)
419
420(* We need to show that the graph only grows, and that Cminor labels will end
421   up in the graph. *)
422definition Cminor_labels_added ≝ λfx,s,f'.
423∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l.
424
425record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
426{ stmt_graph_con : fn_contains … f f'
427; stmt_labels_added : Cminor_labels_added … s f'
428}.
429
430(* Build some machinery to solve fn_contains goals. *)
431
432(* A datatype saying how we intend to prove a step. *)
433inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
434| fn_con_eq : ∀f. fn_con_because fx f
435| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
436    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
437| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
438    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
439.
440
441(* Extract the starting function for a step. *)
442let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
443  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
444
445(* Some unification hints to pick the right step to apply.  The dummy variable
446   is there to provide goal that the lemma can't apply to, which causes an error
447   and forces the "repeat" tactical to stop.  The first hint recognises that we
448   have reached the desired starting point. *)
449
450unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
451  f' ≟ f,
452  b  ≟ fn_con_eq fx f
453
454  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
455.
456
457unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, f3:(Σf3:partial_fn fx. fn_contains fx f2 f3);
458  b ≟ fn_con_sig fx f1 f2 H12 f3
459
460  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
461.
462
463unification hint 1 ≔ fx:fixed, f1:partial_fn fx, f2:partial_fn fx, H12 : fn_contains fx f1 f2, s:stmt, f3:(Σf3:partial_fn fx. add_stmt_inv fx s f2 f3);
464  b ≟ fn_con_addinv fx f1 f2 H12 s f3
465
466  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
467.
468
469(* A lemma to perform a step of the proof.  We can repeat this to do the whole
470   proof. *) 
471lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
472#fx #f *
473[ #f @fn_con_refl
474| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
475| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
476] qed.
477
478
479let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
480  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
481  (dst:Σdst. fn_env_has … f dst ty)
482  on e: Σf':partial_fn fx. fn_contains … f f' ≝
483match e return λty,e.expr_vars ty e (Env_has ?) → (Σdst. fn_env_has … f dst ty) → Σf':partial_fn fx. fn_contains … f f' with
484[ Id t i ⇒ λEnv,dst.
485    let r ≝ lookup_reg (fx_env fx) i t Env in
486    match register_eq r dst with
487    [ inl _ ⇒ «f, ?»
488    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
489    ]
490| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
491| Op1 t t' op e' ⇒ λEnv,dst.
492    let ❬f,r❭ ≝ choose_reg … e' f Env in
493    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
494    let f ≝ add_expr … ? e' Env f «r, ?» in
495      «pi1 … f, ?»
496| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
497    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
498    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
499    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
500    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
501    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
502      «pi1 … f, ?»
503| Mem t e' ⇒ λEnv,dst.
504    let ❬f,r❭ ≝ choose_reg … e' f Env in
505    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
506    let f ≝ add_expr … ? e' Env f «r,?» in
507      «pi1 … f, ?»
508| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
509    let resume_at ≝ pf_entry … f in
510    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
511    let lfalse ≝ pf_entry … f in
512    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
513    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
514    let ❬f,r❭ ≝ choose_reg … e' f ? in
515    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
516    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
517      «pi1 … f, ?»
518| Ecost _ l e' ⇒ λEnv,dst.
519    let f ≝ add_expr … ? e' Env f dst in
520    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
521      «f, ?»
522] Env dst.
523(* For new labels, we need to step back through the definitions of f until we
524   hit the point that it was added. *)
525try (repeat @fn_contains_step @I)
526try (#l #H @H)
527try (#l @I)
528[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
529| #l @(pi2 … dst)
530| 3,8,10: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
531| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
532| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
533| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
534| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
535| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
536| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
537| #l % [2: @(pi2 ?? r) | skip ]
538| @(π1 (π1 Env))
539| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
540| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
541] qed.
542
543let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
544                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
545                  (Hdsts:All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn fx. fn_contains … f f' ≝
546match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
547[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
548| cons e et ⇒ λEnv.
549    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
550    [ nil ⇒ λ_.λpf.⊥
551    | cons r rt ⇒ λHdsts,pf.
552        let f' ≝ add_exprs … et ? rt ? f ? in
553        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
554          let f'' ≝ add_expr … ty e ? f' r in
555            «pi1 … f'', ?»
556        ] (proj1 ?? Env) (π1 Hdsts)
557    ]
558] Env Hdsts pf.
559try (repeat @fn_contains_step @I)
560[ 1,2: normalize in pf; destruct
561| @Env
562| @(fn_con_env … Hr) repeat @fn_contains_step @I
563| @(proj2 … Env)
564| normalize in pf; destruct @e0
565| @(π2 Hdsts)
566] qed.
567
568definition return_ok ≝
569λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
570
571(* Invariants about Cminor statements that we'll need *)
572
573record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
574  si_vars : stmt_vars (Env_has (fx_env fx)) s;
575  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
576  si_return : return_ok (fx_rettyp fx) s
577}.
578
579definition stmts_inv : fixed → stmt → Prop ≝
580λfx. stmt_P (stmt_inv fx).
581
582(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
583definition expr_is_Id : ∀t. expr t → option ident ≝
584λt,e. match e with
585[ Id _ id ⇒ Some ? id
586| _ ⇒ None ?
587].
588
589(* XXX Work around odd disambiguation errors. *)
590alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
591(* If reenabling tailcalls, change 12 to 14. *)
592alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)".
593
594lemma empty_Cminor_labels_added : ∀fx,s,f'.
595  labels_of s = [ ] → Cminor_labels_added fx s f'.
596#fx #s #f' #E whd >E #l *;
597qed.
598
599lemma equal_Cminor_labels_added : ∀fx,s,s',f.
600  labels_of s = labels_of s' → Cminor_labels_added … s' f →
601  Cminor_labels_added fx s f.
602#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
603qed.
604
605lemma Cminor_labels_con : ∀fx,s,f,f'.
606  fn_contains fx f f' →
607  Cminor_labels_added … s f →
608  Cminor_labels_added … s f'.
609#fx #s #f #f' #INC #ADDED
610#l #E
611@(fn_con_labels … INC l (ADDED l E))
612qed.
613
614lemma Cminor_labels_inv : ∀fx,s,s',f.
615  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
616  Cminor_labels_added fx s f →
617  Cminor_labels_added fx s f'.
618#fx #s #s' #f * #f' * #H1 #H2 #H3
619@(Cminor_labels_con … H1) assumption
620qed.
621
622lemma Cminor_labels_sig : ∀fx,s,f.
623  ∀f':Σf':partial_fn fx. fn_contains … f f'.
624  Cminor_labels_added … s f →
625  Cminor_labels_added … s f'.
626#fx #s #f * #f' #H1 @(Cminor_labels_con … H1)
627qed.
628
629discriminator option.
630discriminator DPair.
631
632(* Return statements need a little careful treatment to avoid errors using the
633   invariant about the return type. *)
634
635definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
636  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
637λfx,opt_e,f.
638  let f0 ≝ f in
639  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
640  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
641  [ None ⇒ λEnv. «pi1 … f, ?»
642  | Some et ⇒
643    match et return λe.stmts_inv fx (St_return (Some ? e)) → Σf':partial_fn fx.add_stmt_inv … (St_return (Some ? e)) f0 f' with
644    [ mk_DPair ty e ⇒ λEnv.
645      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
646      [ None ⇒ λH. ⊥
647      | Some t ⇒ λH,R.
648        match R with
649        [ mk_Sig r Hr ⇒
650            let f ≝ add_expr fx ty e ? f «r, ?» in
651            «pi1 … f, ?»
652        ]
653      ] (si_return … (π1 Env)) (pf_result fx f)
654    ]
655  ].
656[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
657| inversion H #A #B #C destruct
658| @mk_add_stmt_inv
659  [ repeat @fn_contains_step @I
660  | @empty_Cminor_labels_added //
661  ]
662| @(si_vars … (π1 Env))
663| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
664| #l #H @I
665| #l //
666] qed.
667
668(* Record the mapping for a Cminor goto label so that we can put it in the skips
669   for the goto statements later. *)
670
671definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝
672λfx,f,l. mk_partial_fn fx
673  (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f)
674  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
675  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
676  (pf_typed … f) (pf_entry … f) (pf_exit … f).
677#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
678[ #E destruct #L @(pi2 … (pf_entry … f))
679| #NE cases (identifier_eq … l l1)
680  [ #E destruct >lookup_add_hit #E destruct /2/
681  | #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f)) | /2/ ]
682  ]
683] qed.
684
685(* Add a dummy statement for each goto so that we can put the real destination
686   in at the end once we've recorded them all. *)
687
688definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝
689λfx,f,dest,PR.
690  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
691    (mk_partial_fn fx g (pf_reggen … f)
692                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
693                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
694                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
695                   «pf_labels … f, ?» ?
696                   «l, ?» «pf_exit … f, ?»).
697[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
698| @add_statement_inv @I
699| #l1 #l2 cases (identifier_eq … l1 l)
700  [ #E destruct >lookup_add_hit #E destruct @PR
701  | #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f)) | // ]
702  ]
703| #id cases (identifier_eq … id l)
704  [ #E destruct //
705  | #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f)) | // ] | // ]
706  ]
707| cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L)
708| @forall_nodes_add //
709| whd >lookup_add_hit % #E destruct
710| @lookup_add_oblivious @(pi2 … (pf_exit …))
711] qed.
712
713(* It's important for correctness that recursive calls to add_stmt happen in
714   reverse order.  This is because Cminor and Clight programs allow goto labels
715   to occur multiple times, but only use the first one to appear in the
716   function.  It would be nice to rule these programs out entirely, but that
717   means establishing and maintaining another invariant on Cminor programs,
718   which I'd like to avoid. *)
719
720let rec add_stmt (fx:fixed) (s:stmt) (Env:stmts_inv fx s) (f:partial_fn fx) on s : Σf':partial_fn fx. add_stmt_inv fx s f f' ≝
721match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
722[ St_skip ⇒ λ_. «f, ?»
723| St_assign t x e ⇒ λEnv.
724    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
725    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
726| St_store t e1 e2 ⇒ λEnv.
727    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
728    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
729    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
730    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
731    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
732| St_call return_opt_id e args ⇒ λEnv.
733    let return_opt_reg ≝
734      match return_opt_id return λo. ? → ? with
735      [ None ⇒ λ_. None ?
736      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
737      ] Env in
738    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
739    let f ≝
740      match expr_is_Id ? e with
741      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
742      | None ⇒
743        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
744        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
745        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
746      ] in
747    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
748| St_seq s1 s2 ⇒ λEnv.
749    let f2 ≝ add_stmt … s2 ? f in
750    let f1 ≝ add_stmt … s1 ? f2 in
751      «pi1 … f1, ?»
752| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
753    let l_next ≝ pf_entry … f in
754    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
755    let l2 ≝ pf_entry … f2 in
756    let f ≝ change_entry … f2 l_next ? in
757    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
758    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
759    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
760    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
761| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
762| St_label l s' ⇒ λEnv.
763    let f ≝ add_stmt … s' (π2 Env) f in
764    «record_goto_label … f l, ?»
765| St_goto l ⇒ λEnv.
766    «add_goto_dummy … f l ?, ?»
767| St_cost l s' ⇒ λEnv.
768    let f ≝ add_stmt … s' (π2 Env) f in
769    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
770] Env.
771try @(π2 Env)
772try @(π1 (π2 Env))
773try @(π2 (π2 Env))
774try @mk_add_stmt_inv
775try (repeat @fn_contains_step @I)
776try (@empty_Cminor_labels_added @refl)
777try (#l #H @I)
778try (#l #H @H)
779try (#l @I)
780[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
781| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
782| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
783| #l % [ @(fn_con_env … (pi2 ?? val_reg)) | @(pi2 ?? addr_reg) ] repeat @fn_contains_step @I
784| @sym_eq @(All2_length … (pi2 ?? args_regs))
785| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
786| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
787| #l % try @conj
788  [ @(pi2 ?? fnr)
789  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
790  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
791    [ #Env @I
792    | * #retid #retty * #Env #moo %{retty} /2/
793    ]
794  ]
795| #l %
796  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
797  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
798    [ #Env @I
799    | * #retid #retty * #Env #moo %{retty} /2/
800    ]
801  ]
802| @(π1 (π1 (si_vars … (π1 Env))))
803| #l #H cases (Exists_append … H)
804  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
805  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
806  ]
807| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
808| #l #H cases (Exists_append … H)
809  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
810  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
811  ]
812| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
813| #l whd % [2: @(pi2 ?? r) | skip ]
814| @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
815| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
816  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
817| #l1 * [ #E >E //
818        | @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f)))
819          % [ // | // | #x #PR @lookup_add_oblivious @PR ]
820        ]
821| @(si_labels … (π1 Env))
822| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
823] qed.
824
825
826
827definition patch_gotos : ∀fx. ∀f:partial_fn fx.
828 (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') →
829 Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝
830λfx,f,PR.
831fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
832  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
833  «f, λx,H.H».
834[ #l #PR' @(pi2 … f') @PR'
835| @(pi2 … f') @(PR … H)
836| @(pi2 … (pf_labels … f')) [ @l' | @lookup_lookup_present ]
837| %
838] qed.
839
840definition c2ra_function (*: internal_function → internal_function*) ≝
841λf.
842let labgen0 ≝ new_universe LabelTag in
843let reggen0 ≝ new_universe RegisterTag in
844let cminor_labels ≝ labels_of (f_body f) in
845let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
846let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
847let ❬locals_reggen, result❭ as E3 ≝
848  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
849  [ None ⇒ ❬〈locals0, reggen2〉, I❭
850  | Some ty ⇒
851      let 〈r,gen〉 ≝ fresh … reggen2 in
852        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
853let locals ≝ \fst locals_reggen in
854let reggen ≝ \snd locals_reggen in
855let 〈l,labgen〉 ≝ fresh … labgen0 in
856let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
857let emptyfn ≝
858  mk_partial_fn fixed
859    labgen
860    reggen
861    params
862    locals
863    result
864    ?
865    (f_stacksize f)
866    (add ?? (empty_map …) l St_return)
867    ?
868    (mk_goto_map ?? (empty_map …) ??)
869    «empty_map …, ?»
870    ?
871    l
872    l in
873let f ≝ add_stmt fixed (f_body f) ? emptyfn in
874let f ≝ patch_gotos … f ? in
875  mk_internal_function
876    (pf_labgen … f)
877    (pf_reggen … f)
878    (match fx_rettyp fixed return λt. match t with [ Some t ⇒ Σr:register. env_has ? r t | _ ⇒ True ] → ? with [ None ⇒ λ_. None ? | Some t ⇒ λR. Some ? 〈(pi1 … R),t〉 ] (pf_result … f))
879    (pf_params … f)
880    (pf_locals … f)
881    (pf_stacksize … f)
882    (pf_graph … f)
883    (pf_closed … f)
884    (pf_typed … f)
885    (pf_entry … f)
886    (pf_exit … f)
887  .
888[ #l1 #l2 #L
889  lapply (gm_img … (pf_gotos … f) … L)
890  whd in match fixed;
891  #PR
892  lapply (in_set_of_list' … PR)
893  @(stmt_labels_added … (pi2 … f))
894| -emptyfn @(stmt_P_mp … (f_inv f))
895  #s * #V #L #R %
896  [ @(stmt_vars_mp … V)
897    #i #t #H cases (Exists_append … H)
898    [ #H1 @(populate_extends … (sym_eq … E2))
899      [ @(populates_env_distinct … (sym_eq … E1)) //
900        @All_alt //
901      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
902      ]
903    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
904    ]
905  | @(stmt_labels_mp … L)
906    #l #H whd in match fixed; @in_set_of_list assumption
907  | cases s in R ⊢ %; //
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  | (* gave up with     cases (f_return f) in result E3; *)
913    @(match f_return f return λx.∀R:resultok x ((\fst locals_reggen)@params). ❬locals_reggen,R❭ = match x with [None ⇒ ?|Some _ ⇒ ?] → ? with [ None ⇒ λres1.? | Some rty ⇒ λres1.?] result E3)
914    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
915      @Exists_append_l
916    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
917      #H' @Exists_append_l %2 @H'
918    ]
919  ]
920| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
921  [ * #E1 #E2 >E2 @I
922  | whd in ⊢ (??%? → ?); #E' destruct (E')
923  ]
924| #id #l #E normalize in E; destruct
925| #id normalize * #H cases (H (refl ??))
926| #l #l' normalize #E destruct
927| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
928  [ * #E1 #E2 >E2 @I
929  | whd in ⊢ (??%? → ?); #E' destruct (E')
930  ]
931| 9,10: whd >lookup_add_hit % #E destruct
932| % @refl
933]
934qed.
935
936definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
937λp.transform_program … p (λ_. transf_fundef … c2ra_function).
938
939include "Cminor/initialisation.ma".
940
941definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
942λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.