source: src/Cminor/toRTLabs.ma @ 2335

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

Deal with goto labels in RTLabs to Cminor by fixing up goto statements
after the main translation to avoid generating extra skips in awkward
locations.

File size: 39.3 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(* Add a statement with a fresh label to the start of the function.  The
290   statement is parametrised by the *next* instruction's label. *)
291definition add_fresh_to_graph : ∀fx. ∀s:(label → statement). ∀f:partial_fn fx.
292  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
293  (∀l. statement_typed_in … f (s l)) →
294  Σf':partial_fn fx. fn_contains … f f' ≝
295λfx,s,f,p,tp.
296  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
297  let s' ≝ s (pf_entry … f) in
298    (mk_partial_fn fx g (pf_reggen … f)
299                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
300                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ????
301                   «l, ?» «pf_exit … f, ?»).
302[ 4: cases (pf_labels … f) #m #PR %{m} #l1 #l2 #L @lookup_add_oblivious @(PR … L)
303| % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
304| @add_statement_inv @p @(pi2 … (pf_entry …))
305| cases (pf_gotos … f) #m #dom #img %
306  [ @m | #id #P @lookup_add_oblivious @dom @P | @img ]
307| @forall_nodes_add //
308| whd >lookup_add_hit % #E destruct
309| @lookup_add_oblivious @(pi2 … (pf_exit …))
310] qed.
311
312lemma extend_typ_env : ∀te,r,t,r',t'.
313  env_has te r t → env_has (〈r',t'〉::te) r t.
314#tw #r #t #r' #t' #H %2 @H
315qed.
316
317lemma stmt_extend_typ_env : ∀te,r,t,s.
318  statement_typed te s → statement_typed (〈r,t〉::te) s.
319#tw #r #t *
320[ 1,2: //
321| #t' #r #cst #l #H %2 @H
322| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
323| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
324| 6,7: #t' #r1 #r2 #l * /3/
325| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
326| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
327| #r' #l1 #l2 * #t' #E /3/
328| //
329] qed.
330
331(* A little more nesting in the result type than I'd like, but it keeps the
332   function closely paired with the proof that it contains f. *)
333definition fresh_reg : ∀fx. ∀f:partial_fn fx. ∀ty:typ.
334  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
335λfx,f,ty.
336  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
337  let f' ≝
338    «mk_partial_fn fx
339       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f)) ? ?
340       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) (pf_gotos … f) (pf_labels … f) ? (pf_entry … f) (pf_exit … f), ?»
341  in
342    ❬f' , ?(*«r, ?»*)❭.
343[ @(«r, ?») % @refl
344| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
345| #i #t #r1 #H #L %2 @(pf_envok … f … L)
346| lapply (pf_result fx f) cases (fx_rettyp fx) // #t * #r' #H %{r'} @extend_typ_env //
347| % [ #l // | #r' #ty' #H @extend_typ_env @H | // ]
348] qed.
349
350definition choose_reg : ∀fx.∀ty.∀e:expr ty. ∀f:partial_fn fx. expr_vars ty e (Env_has (fx_env fx)) →
351  𝚺f':(Σf':partial_fn fx. fn_contains … f f'). (Σr:register. fn_env_has … f' r ty) ≝
352λfx,ty,e,f.
353  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
354  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg (fx_env fx) i t Env, ?»❭
355  | _ ⇒ λ_.fresh_reg … f ?
356  ].
357[ % //
358| @(pf_envok … Env) @refl
359] qed.
360 
361let 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 ≝ 
362 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.
363 
364let 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 ≝ 
365 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.
366
367definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
368
369definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
370λA,P,x. match x with [ mk_DPair a _ ⇒ a].
371
372definition choose_regs : ∀fx. ∀es:list (𝚺t:typ.expr t).
373                         ∀f:partial_fn fx. All ? (exprtyp_present (fx_env fx)) es →
374                         𝚺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) ≝
375λfx,es,f,Env.
376  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))
377    (λe,p,tl,acc.
378      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 ⇒
379        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.
380          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 ⇒
381            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
382          ]
383        ] p
384      ]) ❬«f, ?», «[ ], I»❭ es Env.
385[ @p
386| cases r #r' #Hr' cases rs #rs' #Hrs'
387  % [ whd in ⊢ (??%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
388| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
389| @fn_con_refl
390]  qed.
391
392lemma choose_regs_length : ∀fx,es,f,p,f',rs.
393  choose_regs fx es f p = ❬f',rs❭ → |es| = length … rs.
394#fx #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
395qed.
396
397lemma present_included : ∀fx,f,f',l.
398  fn_contains fx f f' →
399  present ?? (pf_graph … f) l →
400  present ?? (pf_graph … f') l.
401#fx #f #f' #l * #H1 #H2 #H3 @H1 qed.
402
403(* Some definitions for the add_stmt function later, which we introduce now so
404   that we can build the whole fn_graph_included machinery at once. *)
405
406(* We need to show that the graph only grows, and that Cminor labels will end
407   up in the graph. *)
408definition Cminor_labels_added ≝ λfx,s,f'.
409∀l. Exists ? (λl'.l=l') (labels_of s) → present ?? (pf_labels fx f') l.
410
411record add_stmt_inv (fx:fixed) (s:stmt) (f:partial_fn fx) (f':partial_fn fx) : Prop ≝
412{ stmt_graph_con : fn_contains … f f'
413; stmt_labels_added : Cminor_labels_added … s f'
414}.
415
416(* Build some machinery to solve fn_contains goals. *)
417
418(* A datatype saying how we intend to prove a step. *)
419inductive fn_con_because (fx:fixed) : partial_fn fx → Type[0] ≝
420| fn_con_eq : ∀f. fn_con_because fx f
421| fn_con_sig : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
422    ∀f3:(Σf3:partial_fn fx.fn_contains … f2 f3). fn_con_because fx f3
423| fn_con_addinv : ∀f1,f2:partial_fn fx. fn_contains … f1 f2 →
424    ∀s.∀f3:(Σf3:partial_fn fx.add_stmt_inv … s f2 f3). fn_con_because fx f3
425.
426
427(* Extract the starting function for a step. *)
428let rec fn_con_because_left fx f0  (b:fn_con_because ? f0) on b : partial_fn fx ≝
429  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
430
431(* Some unification hints to pick the right step to apply.  The dummy variable
432   is there to provide goal that the lemma can't apply to, which causes an error
433   and forces the "repeat" tactical to stop.  The first hint recognises that we
434   have reached the desired starting point. *)
435
436unification hint 0 ≔ fx:fixed, f:partial_fn fx, dummy:True;
437  f' ≟ f,
438  b  ≟ fn_con_eq fx f
439
440  fn_contains fx f f' ≡ fn_contains fx (fn_con_because_left fx f' b) f'
441.
442
443unification 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);
444  b ≟ fn_con_sig fx f1 f2 H12 f3
445
446  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
447.
448
449unification 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);
450  b ≟ fn_con_addinv fx f1 f2 H12 s f3
451
452  fn_contains fx f1 f3 ≡ fn_contains fx (fn_con_because_left fx f3 b) f3
453.
454
455(* A lemma to perform a step of the proof.  We can repeat this to do the whole
456   proof. *) 
457lemma fn_contains_step : ∀fx,f. ∀b:fn_con_because fx f. fn_contains … (fn_con_because_left … f b) f.
458#fx #f *
459[ #f @fn_con_refl
460| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
461| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
462] qed.
463
464
465let rec add_expr (fx:fixed) (ty:typ) (e:expr ty)
466  (Env:expr_vars ty e (Env_has (fx_env fx))) (f:partial_fn fx)
467  (dst:Σdst. fn_env_has … f dst ty)
468  on e: Σf':partial_fn fx. fn_contains … f f' ≝
469match 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
470[ Id t i ⇒ λEnv,dst.
471    let r ≝ lookup_reg (fx_env fx) i t Env in
472    match register_eq r dst with
473    [ inl _ ⇒ «f, ?»
474    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
475    ]
476| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
477| Op1 t t' op e' ⇒ λEnv,dst.
478    let ❬f,r❭ ≝ choose_reg … e' f Env in
479    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
480    let f ≝ add_expr … ? e' Env f «r, ?» in
481      «pi1 … f, ?»
482| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
483    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
484    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
485    let f ≝ add_fresh_to_graph … (St_op2 ??? op dst r1 r2) f ?? in
486    let f ≝ add_expr … ? e2 (proj2 … Env) f «r2, ?» in
487    let f ≝ add_expr … ? e1 (proj1 … Env) f «r1, ?» in
488      «pi1 … f, ?»
489| Mem t e' ⇒ λEnv,dst.
490    let ❬f,r❭ ≝ choose_reg … e' f Env in
491    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
492    let f ≝ add_expr … ? e' Env f «r,?» in
493      «pi1 … f, ?»
494| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
495    let resume_at ≝ pf_entry … f in
496    let f ≝ add_expr … ? e2 (proj2 … Env) f dst in
497    let lfalse ≝ pf_entry … f in
498    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
499    let f ≝ add_expr … ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
500    let ❬f,r❭ ≝ choose_reg … e' f ? in
501    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
502    let f ≝ add_expr … ? e' (proj1 … (proj1 … Env)) f «r, ?» in
503      «pi1 … f, ?»
504| Ecost _ l e' ⇒ λEnv,dst.
505    let f ≝ add_expr … ? e' Env f dst in
506    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
507      «f, ?»
508] Env dst.
509(* For new labels, we need to step back through the definitions of f until we
510   hit the point that it was added. *)
511try (repeat @fn_contains_step @I)
512try (#l #H @H)
513try (#l @I)
514[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
515| #l @(pi2 … dst)
516| 3,8,10: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
517| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
518| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
519| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
520| #l % [ % [ @(fn_con_env … (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
521| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
522| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
523| #l % [2: @(pi2 ?? r) | skip ]
524| @(π1 (π1 Env))
525| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
526| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
527] qed.
528
529let rec add_exprs (fx:fixed) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present (fx_env fx)) es)
530                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn fx)
531                  (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' ≝
532match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
533[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn fx. fn_contains … f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
534| cons e et ⇒ λEnv.
535    match dsts return λx. All2 ?? (λr,e. fn_env_has … f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
536    [ nil ⇒ λ_.λpf.⊥
537    | cons r rt ⇒ λHdsts,pf.
538        let f' ≝ add_exprs … et ? rt ? f ? in
539        match e return λe.exprtyp_present ? e → fn_env_has … f r (eject' typ expr e) → ? with [ mk_DPair ty e ⇒ λEnv,Hr.
540          let f'' ≝ add_expr … ty e ? f' r in
541            «pi1 … f'', ?»
542        ] (proj1 ?? Env) (π1 Hdsts)
543    ]
544] Env Hdsts pf.
545try (repeat @fn_contains_step @I)
546[ 1,2: normalize in pf; destruct
547| @Env
548| @(fn_con_env … Hr) repeat @fn_contains_step @I
549| @(proj2 … Env)
550| normalize in pf; destruct @e0
551| @(π2 Hdsts)
552] qed.
553
554definition return_ok ≝
555λt,s. match s with [ St_return oe ⇒ rettyp_match t oe | _ ⇒ True ].
556
557(* Invariants about Cminor statements that we'll need *)
558
559record stmt_inv (fx:fixed) (s:stmt) : Prop ≝ {
560  si_vars : stmt_vars (Env_has (fx_env fx)) s;
561  si_labels : stmt_labels (present ?? (fx_gotos fx)) s;
562  si_return : return_ok (fx_rettyp fx) s
563}.
564
565definition stmts_inv : fixed → stmt → Prop ≝
566λfx. stmt_P (stmt_inv fx).
567
568(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
569definition expr_is_Id : ∀t. expr t → option ident ≝
570λt,e. match e with
571[ Id _ id ⇒ Some ? id
572| _ ⇒ None ?
573].
574
575(* XXX Work around odd disambiguation errors. *)
576alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
577(* If reenabling tailcalls, change 12 to 14. *)
578alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,11,0)".
579
580lemma empty_Cminor_labels_added : ∀fx,s,f'.
581  labels_of s = [ ] → Cminor_labels_added fx s f'.
582#fx #s #f' #E whd >E #l *;
583qed.
584
585lemma equal_Cminor_labels_added : ∀fx,s,s',f.
586  labels_of s = labels_of s' → Cminor_labels_added … s' f →
587  Cminor_labels_added fx s f.
588#fx #s #s' #f #E whd in ⊢ (% → %); > E #H @H
589qed.
590
591lemma Cminor_labels_con : ∀fx,s,f,f'.
592  fn_contains fx f f' →
593  Cminor_labels_added … s f →
594  Cminor_labels_added … s f'.
595#fx #s #f #f' #INC #ADDED
596#l #E
597@(fn_con_labels … INC l (ADDED l E))
598qed.
599
600lemma Cminor_labels_inv : ∀fx,s,s',f.
601  ∀f':Σf':partial_fn fx. add_stmt_inv fx s' f f'.
602  Cminor_labels_added fx s f →
603  Cminor_labels_added fx s f'.
604#fx #s #s' #f * #f' * #H1 #H2 #H3
605@(Cminor_labels_con … H1) assumption
606qed.
607
608lemma Cminor_labels_sig : ∀fx,s,f.
609  ∀f':Σf':partial_fn fx. fn_contains … f f'.
610  Cminor_labels_added … s f →
611  Cminor_labels_added … s f'.
612#fx #s #f * #f' #H1 @(Cminor_labels_con … H1)
613qed.
614
615discriminator option.
616discriminator DPair.
617
618(* Return statements need a little careful treatment to avoid errors using the
619   invariant about the return type. *)
620
621definition add_return : ∀fx,opt_e. ∀f:partial_fn fx. ∀Env:stmts_inv fx (St_return opt_e).
622  Σf':partial_fn fx. add_stmt_inv fx (St_return opt_e) f f' ≝
623λfx,opt_e,f.
624  let f0 ≝ f in
625  let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
626  match opt_e return λo. stmts_inv ? (St_return o) → Σf':partial_fn fx.add_stmt_inv … (St_return o) f0 f' with
627  [ None ⇒ λEnv. «pi1 … f, ?»
628  | Some et ⇒
629    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
630    [ mk_DPair ty e ⇒ λEnv.
631      match fx_rettyp fx return λX. rettyp_match X ? → match X with [ Some t ⇒ Σr:register. env_has ?? t | None ⇒ ? ] → ? with
632      [ None ⇒ λH. ⊥
633      | Some t ⇒ λH,R.
634        match R with
635        [ mk_Sig r Hr ⇒
636            let f ≝ add_expr fx ty e ? f «r, ?» in
637            «pi1 … f, ?»
638        ]
639      ] (si_return … (π1 Env)) (pf_result fx f)
640    ]
641  ].
642[ @mk_add_stmt_inv /2 by refl, empty_Cminor_labels_added, fn_con_sig/
643| inversion H #A #B #C destruct
644| @mk_add_stmt_inv
645  [ repeat @fn_contains_step @I
646  | @empty_Cminor_labels_added //
647  ]
648| @(si_vars … (π1 Env))
649| inversion H [ #E destruct ] #ty' #e' #E1 #E2 #_ destruct @Hr
650| #l #H @I
651| #l //
652] qed.
653
654(* Record the mapping for a Cminor goto label so that we can put it in the skips
655   for the goto statements later. *)
656
657definition record_goto_label : ∀fx. partial_fn fx → identifier Label → partial_fn fx ≝
658λfx,f,l. mk_partial_fn fx
659  (pf_labgen … f) (pf_reggen … f) (pf_params … f) (pf_locals … f)
660  (pf_result … f) (pf_envok … f) (pf_stacksize … f) (pf_graph … f)
661  (pf_closed … f) (pf_gotos …  f) «add … (pf_labels … f) l (pf_entry … f), ?»
662  (pf_typed … f) (pf_entry … f) (pf_exit … f).
663#l1 #l2 cases (identifier_eq … l2 (pf_entry … f))
664[ #E destruct #L @(pi2 … (pf_entry … f))
665| #NE cases (identifier_eq … l l1)
666  [ #E destruct >lookup_add_hit #E destruct /2/
667  | #NE' >lookup_add_miss [ @(pi2 … (pf_labels … f)) | /2/ ]
668  ]
669] qed.
670
671(* Add a dummy statement for each goto so that we can put the real destination
672   in at the end once we've recorded them all. *)
673
674definition add_goto_dummy : ∀fx. ∀f:partial_fn fx. ∀l. present … (fx_gotos fx) l → Σf':partial_fn fx. fn_contains … f f' ≝
675λfx,f,dest,PR.
676  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
677    (mk_partial_fn fx g (pf_reggen … f)
678                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
679                   (pf_stacksize … f) (add ?? (pf_graph … f) l St_return) ?
680                   (mk_goto_map … (add … (pf_gotos … f) l dest) ??)
681                   «pf_labels … f, ?» ?
682                   «l, ?» «pf_exit … f, ?»).
683[ % [ #l' @lookup_add_oblivious | // | cases (pf_labels fx f) /2/ ]
684| @add_statement_inv @I
685| #l1 #l2 cases (identifier_eq … l1 l)
686  [ #E destruct >lookup_add_hit #E destruct @PR
687  | #NE >lookup_add_miss [ @(gm_img … (pf_gotos … f)) | // ]
688  ]
689| #id cases (identifier_eq … id l)
690  [ #E destruct //
691  | #NE whd in ⊢ (% → %); >lookup_add_miss [ >lookup_add_miss [ @(gm_dom … (pf_gotos … f)) | // ] | // ]
692  ]
693| cases (pf_labels … f) #m #PR #l1 #l2 #L @lookup_add_oblivious @(PR … L)
694| @forall_nodes_add //
695| whd >lookup_add_hit % #E destruct
696| @lookup_add_oblivious @(pi2 … (pf_exit …))
697] qed.
698
699(* It's important for correctness that recursive calls to add_stmt happen in
700   reverse order.  This is because Cminor and Clight programs allow goto labels
701   to occur multiple times, but only use the first one to appear in the
702   function.  It would be nice to rule these programs out entirely, but that
703   means establishing and maintaining another invariant on Cminor programs,
704   which I'd like to avoid. *)
705
706let 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' ≝
707match s return λs.stmts_inv fx s → Σf':partial_fn fx. add_stmt_inv … s f f' with
708[ St_skip ⇒ λ_. «f, ?»
709| St_assign t x e ⇒ λEnv.
710    let dst ≝ lookup_reg (fx_env fx) x t (π1 (si_vars … (π1 Env))) in
711    «pi1 … (add_expr … e (π2 (si_vars … (π1 Env))) f dst), ?»
712| St_store t e1 e2 ⇒ λEnv.
713    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (si_vars … (π1 Env))) in
714    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (si_vars … (π1 Env))) in
715    let f ≝ add_fresh_to_graph … (St_store t addr_reg val_reg) f ?? in
716    let f ≝ add_expr … e1 (π1 (si_vars … (π1 Env))) f «addr_reg, ?» in
717    «pi1 … (add_expr … ? e2 (π2 (si_vars … (π1 Env))) f «val_reg, ?»), ?»
718| St_call return_opt_id e args ⇒ λEnv.
719    let return_opt_reg ≝
720      match return_opt_id return λo. ? → ? with
721      [ None ⇒ λ_. None ?
722      | Some idty ⇒ λEnv. Some ? (lookup_reg (fx_env fx) (\fst idty) (\snd idty) ?)
723      ] Env in
724    let ❬f, args_regs❭ ≝ choose_regs ? args f (π2 (si_vars ?? (π1 Env))) in
725    let f ≝
726      match expr_is_Id ? e with
727      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
728      | None ⇒
729        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (si_vars … (π1 Env)))) in
730        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
731        «pi1 … (add_expr … ? e (π2 (π1 (si_vars … (π1 Env)))) f «fnr, ?»), ?»
732      ] in
733    «pi1 … (add_exprs … args (π2 (si_vars … (π1 Env))) args_regs ? f ?), ?»
734| St_seq s1 s2 ⇒ λEnv.
735    let f2 ≝ add_stmt … s2 ? f in
736    let f1 ≝ add_stmt … s1 ? f2 in
737      «pi1 … f1, ?»
738| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
739    let l_next ≝ pf_entry … f in
740    let f2 ≝ add_stmt … s2 (π2 (π2 Env)) f in
741    let l2 ≝ pf_entry … f2 in
742    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
743    let f1 ≝ add_stmt … s1 (π1 (π2 Env)) f in
744    let ❬f,r❭ ≝ choose_reg … e f1 (si_vars … (π1 Env)) in
745    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
746    «pi1 … (add_expr … ? e (si_vars … (π1 Env)) f «r, ?»), ?»
747| St_return opt_e ⇒ λEnv. add_return fx opt_e f Env
748| St_label l s' ⇒ λEnv.
749    let f ≝ add_stmt … s' (π2 Env) f in
750    «record_goto_label … f l, ?»
751| St_goto l ⇒ λEnv.
752    «add_goto_dummy … f l ?, ?»
753| St_cost l s' ⇒ λEnv.
754    let f ≝ add_stmt … s' (π2 Env) f in
755    «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
756] Env.
757try @(π2 Env)
758try @(π1 (π2 Env))
759try @(π2 (π2 Env))
760try @mk_add_stmt_inv
761try (repeat @fn_contains_step @I)
762try (@empty_Cminor_labels_added @refl)
763try (#l #H @I)
764try (#l #H @H)
765try (#l @I)
766[ @(pf_envok … (π1 (si_vars … (π1 Env)))) @refl
767| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
768| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
769| #l % [ @(fn_con_env … (pi2 ?? val_reg)) | @(pi2 ?? addr_reg) ] repeat @fn_contains_step @I
770| @sym_eq @(All2_length … (pi2 ?? args_regs))
771| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
772| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
773| #l % try @conj
774  [ @(pi2 ?? fnr)
775  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
776  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
777    [ #Env @I
778    | * #retid #retty * #Env #moo %{retty} /2/
779    ]
780  ]
781| #l %
782  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
783  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
784    [ #Env @I
785    | * #retid #retty * #Env #moo %{retty} /2/
786    ]
787  ]
788| @(π1 (π1 (si_vars … (π1 Env))))
789| #l #H cases (Exists_append … H)
790  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
791  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (pi2 ?? f2))
792  ]
793| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
794| #l #H cases (Exists_append … H)
795  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f1))
796  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ?? f2))
797  ]
798| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
799| #l whd % [2: @(pi2 ?? r) | skip ]
800| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
801| cases (pi2 … f) * #INC #ENV #LBLE #LBLA %
802  [ @INC | @ENV | @(extends_dom_trans … LBLE) #l1 #PR whd in ⊢ (???%?); @lookup_add_oblivious @PR ]
803| #l1 * [ #E >E //
804        | @(Cminor_labels_con … (stmt_labels_added ???? (pi2 … f)))
805          % [ // | // | #x #PR @lookup_add_oblivious @PR ]
806        ]
807| @(si_labels … (π1 Env))
808| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 … f)) ]
809] qed.
810
811
812
813definition patch_gotos : ∀fx. ∀f:partial_fn fx.
814 (∀l,l'. lookup ?? (pf_gotos … f) l = Some ? l' → present ?? (pf_labels … f) l') →
815 Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l ≝
816λfx,f,PR.
817fold_inf ? (Σf':partial_fn fx. ∀l. present ?? (pf_labels … f) l → present ?? (pf_labels … f') l) ? (pf_gotos … f)
818  (λl,l',H,f'. «fill_in_statement fx l (St_skip (lookup_present ?? (pf_labels … f') l' ?)) f' ??, ?»)
819  «f, λx,H.H».
820[ #l #PR' @(pi2 … f') @PR'
821| @(pi2 … f') @(PR … H)
822| @(pi2 … (pf_labels … f')) [ @l' | @lookup_lookup_present ]
823| %
824] qed.
825
826definition c2ra_function (*: internal_function → internal_function*) ≝
827λf.
828let labgen0 ≝ new_universe LabelTag in
829let reggen0 ≝ new_universe RegisterTag in
830let cminor_labels ≝ labels_of (f_body f) in
831let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
832let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
833let ❬locals_reggen, result❭ as E3 ≝
834  match f_return f return λt.𝚺lr. resultok t ((\fst lr)@params) with
835  [ None ⇒ ❬〈locals0, reggen2〉, I❭
836  | Some ty ⇒
837      let 〈r,gen〉 ≝ fresh … reggen2 in
838        mk_DPair ? (λlr.Σr. env_has ((\fst lr)@params) r ty) 〈〈r,ty〉::locals0, gen〉 «r, ?» ] in
839let locals ≝ \fst locals_reggen in
840let reggen ≝ \snd locals_reggen in
841let 〈l,labgen〉 ≝ fresh … labgen0 in
842let fixed ≝ mk_fixed (set_of_list … (labels_of (f_body f))) env (f_return f) in
843let emptyfn ≝
844  mk_partial_fn fixed
845    labgen
846    reggen
847    params
848    locals
849    result
850    ?
851    (f_stacksize f)
852    (add ?? (empty_map …) l St_return)
853    ?
854    (mk_goto_map ?? (empty_map …) ??)
855    «empty_map …, ?»
856    ?
857    l
858    l in
859let f ≝ add_stmt fixed (f_body f) ? emptyfn in
860let f ≝ patch_gotos … f ? in
861  mk_internal_function
862    (pf_labgen … f)
863    (pf_reggen … f)
864    (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))
865    (pf_params … f)
866    (pf_locals … f)
867    (pf_stacksize … f)
868    (pf_graph … f)
869    (pf_closed … f)
870    (pf_typed … f)
871    (pf_entry … f)
872    (pf_exit … f)
873  .
874[ #l1 #l2 #L
875  lapply (gm_img … (pf_gotos … f) … L)
876  whd in match fixed;
877  #PR
878  lapply (in_set_of_list' … PR)
879  @(stmt_labels_added … (pi2 … f))
880| -emptyfn @(stmt_P_mp … (f_inv f))
881  #s * #V #L #R %
882  [ @(stmt_vars_mp … V)
883    #i #t #H cases (Exists_append … H)
884    [ #H1 @(populate_extends … (sym_eq … E2))
885      [ @(populates_env_distinct … (sym_eq … E1)) //
886        @All_alt //
887      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
888      ]
889    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
890    ]
891  | @(stmt_labels_mp … L)
892    #l #H whd in match fixed; @in_set_of_list assumption
893  | cases s in R ⊢ %; //
894  ]
895| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
896  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
897    [ * * | normalize @Exists_append_r ]
898  | (* gave up with     cases (f_return f) in result E3; *)
899    @(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)
900    [ whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
901      @Exists_append_l
902    | cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3' whd in match locals; destruct
903      #H' @Exists_append_l %2 @H'
904    ]
905  ]
906| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
907  [ * #E1 #E2 >E2 @I
908  | whd in ⊢ (??%? → ?); #E' destruct (E')
909  ]
910| #id #l #E normalize in E; destruct
911| #id normalize * #H cases (H (refl ??))
912| #l #l' normalize #E destruct
913| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
914  [ * #E1 #E2 >E2 @I
915  | whd in ⊢ (??%? → ?); #E' destruct (E')
916  ]
917| 9,10: whd >lookup_add_hit % #E destruct
918| % @refl
919]
920qed.
921
922definition cminor_noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝
923λp.transform_program … p (λ_. transf_fundef … c2ra_function).
924
925include "Cminor/initialisation.ma".
926
927definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
928λ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.