source: src/Cminor/toRTLabs.ma @ 1626

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

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File size: 37.0 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag (register × typ).
7definition label_env ≝ identifier_map Label label.
8definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
9λen,gen. foldr ??
10 (λidt,rsengen.
11   let 〈id,ty〉 ≝ idt in
12   let 〈rs,en,gen〉 ≝ rsengen in
13   let 〈r,gen'〉 ≝ fresh … gen in
14     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
15(*
16lemma populates_env : ∀l,e,u,l',e',u'.
17  populate_env e u l = 〈l',e',u'〉 →
18  ∀i. Exists ? (λx.\fst x = i) l →
19      present ?? e' i.
20#l elim l
21[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
22| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
23  * [ whd in ⊢ (??%? → ?); #E1 <E1
24      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
25      whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E
26      whd in E:(??%?); destruct;
27      whd >lookup_add_hit % #A destruct
28    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
29      lapply (refl ? (populate_env e u tl))
30      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
31      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u''
32      whd in ⊢ (??%? → ?); #E destruct
33      @lookup_add_oblivious
34      @(IH … E1 ? H)
35    ]
36] qed.
37
38lemma populate_extends : ∀l,e,u,l',e',u'.
39  populate_env e u l = 〈l',e',u'〉 →
40  ∀i. present ?? e i → present ?? e' i.
41#l elim l
42[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
43| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
44  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
45  lapply (refl ? (populate_env e u tl))
46  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
47  >E0 in E; whd in ⊢ (??%? → ?); #E
48  destruct
49  #i #H @lookup_add_oblivious @(IH … E0) @H
50] qed.
51*)
52definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
53λen,gen. foldr ??
54 (λid,engen.
55   let 〈en,gen〉 ≝ engen in
56   let 〈r,gen'〉 ≝ fresh … gen in
57     〈add ?? en id r, gen'〉) 〈en, gen〉.
58
59lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
60  populate_label_env lbls u ls = 〈lbls',u'〉 →
61  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
62#ls elim ls
63[ #lbls #u #lbls' #u' #E #l *
64| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
65  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
66  lapply (refl ? (populate_label_env lbls u t))
67  cases (populate_label_env lbls u t) in ⊢ (???% → %);
68  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
69  #E destruct
70  #l *
71  [ #El <El whd >lookup_add_hit % #Er destruct
72  | #H @lookup_add_oblivious @(IH … E1 ? H)
73  ]
74] qed.
75
76lemma label_env_contents : ∀ls,lbls,u,lbls',u'.
77  populate_label_env lbls u ls = 〈lbls',u'〉 →
78  ∀l. present ?? lbls' l → Exists ? (λl'.l = l') ls ∨ present ?? lbls l.
79#ls elim ls
80[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
81| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
82  change with (populate_label_env ???) in ⊢ (??match % with [ _ ⇒ ? ]? → ?);
83  lapply (refl ? (populate_label_env lbls u t))
84  cases (populate_label_env lbls u t) in ⊢ (???% → %);
85  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
86  #E destruct
87  #l #H cases (identifier_eq ? l h)
88  [ #El %1 %1 @El
89  | #NE cases (IH … E1 l ?)
90    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
91  ]
92] qed.
93
94definition Env_has : env → ident → typ → Prop ≝
95λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
96
97lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
98#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
99[ * | * #r #t' #E % #E' destruct ]
100qed.
101
102definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
103/2/ qed.
104definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
105
106(* Check that the domain of one graph is included in another, for monotonicity
107   properties.  Note that we don't say anything about the statements. *)
108definition graph_included : graph statement → graph statement → Prop ≝
109λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
110
111lemma graph_inc_trans : ∀g1,g2,g3.
112  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
113#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
114
115definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
116
117definition partially_closed : label_env → graph statement → Prop ≝
118 λe,g. forall_nodes ? (labels_P (λl. present ?? g l ∨ lpresent e l)) g.
119
120(* I'd use a single parametrised definition along with internal_function, but
121   it's a pain without implicit parameters. *)
122record partial_fn (lenv:label_env) (env:env) : Type[0] ≝
123{ pf_labgen    : universe LabelTag
124; pf_reggen    : universe RegisterTag
125; pf_params    : list (register × typ)
126; pf_locals    : list (register × typ)
127; pf_result    : option (Σrt:register × typ. env_has (pf_locals @ pf_params) (\fst rt) (\snd rt))
128; pf_envok     : ∀id,ty,r,H. lookup_reg env id ty H = r → env_has (pf_locals @ pf_params) r ty
129; pf_stacksize : nat
130; pf_graph     : graph statement
131; pf_closed    : partially_closed lenv pf_graph
132; pf_typed     : graph_typed (pf_locals @ pf_params) pf_graph
133; pf_entry     : Σl:label. present ?? pf_graph l
134; pf_exit      : Σl:label. present ?? pf_graph l
135}.
136
137definition fn_env_has ≝
138  λle,env,f. env_has (pf_locals le env f @ pf_params le env f).
139
140record fn_contains (le:label_env) (env:env) (f1:partial_fn le env) (f2:partial_fn le env) : Prop ≝
141{ fn_con_graph : graph_included (pf_graph … f1) (pf_graph … f2)
142; fn_con_env : ∀r,ty. fn_env_has le env f1 r ty → fn_env_has le env f2 r ty
143}.
144
145lemma fn_con_trans : ∀le,env,f1,f2,f3.
146  fn_contains le env f1 f2 → fn_contains le env f2 f3 → fn_contains le env f1 f3.
147#le #env #f1 #f2 #f3 #H1 #H2 %
148[ @(graph_inc_trans … (fn_con_graph … H1) (fn_con_graph … H2))
149| #r #ty #H @(fn_con_env … H2) @(fn_con_env … H1) @H
150] qed.
151
152lemma fn_con_refl : ∀label_env,env,f.
153  fn_contains label_env env f f.
154#le #env #f % #l // qed.
155
156lemma fn_con_sig : ∀label_env,env,f,f0.
157  ∀f':Σf':partial_fn label_env env. fn_contains … f0 f'.
158  fn_contains label_env env f f0 →
159  fn_contains label_env env f f'.
160#le #env #f #f0 * #f' #H1 #H2 @(fn_con_trans … H2 H1)
161qed.
162
163lemma add_statement_inv : ∀le,env,l,s.∀f.
164  labels_present (pf_graph le env f) s →
165  partially_closed le (add … (pf_graph … f) l s).
166#le #env #l #s #f #p
167#l' #s' #H cases (identifier_eq … l l')
168[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
169  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
170| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
171  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
172  | >lookup_add_miss in H; /2/
173  ]
174] qed.
175
176definition statement_typed_in ≝
177λle,env,f,s. statement_typed (pf_locals le env f @ pf_params le env f) s.
178
179lemma forall_nodes_add : ∀A,P,l,a,g.
180  forall_nodes A P g → P a → forall_nodes A P (add ?? g l a).
181#A #P #l #a #g #ALL #NEW
182#l' #a'
183cases (identifier_eq … l' l)
184[ #E destruct >lookup_add_hit #E destruct @NEW
185| #ne >lookup_add_miss /2/
186] qed.
187
188(* Add a statement to the graph, *without* updating the entry label. *)
189definition fill_in_statement : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
190  labels_present (pf_graph … f) s →
191  statement_typed_in le env f s →
192  Σf':partial_fn le env. fn_contains … f f' ≝
193λle,env,l,s,f,p,tp.
194  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
195                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
196                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
197                «pf_entry … f, ?» «pf_exit … f, ?».
198[ @add_statement_inv @p
199| @forall_nodes_add //
200| 3,4: @lookup_add_oblivious [ @(pi2 … (pf_entry … f)) | @(pi2 … (pf_exit … f)) ]
201| % [ #l' @lookup_add_oblivious | // ]
202] qed.
203
204(* Add a statement to the graph, making it the entry label. *)
205definition add_to_graph : ∀le,env. label → ∀s:statement. ∀f:partial_fn le env.
206  labels_present (pf_graph … f) s →
207  statement_typed_in … f s →
208  Σf':partial_fn le env. fn_contains … f f' ≝
209λle,env,l,s,f,p,tl.
210  mk_partial_fn le env (pf_labgen … f) (pf_reggen … f)
211                (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
212                (pf_stacksize … f) (add ?? (pf_graph … f) l s) ? ?
213                «l, ?» «pf_exit … f, ?».
214[ @add_statement_inv @p
215| @forall_nodes_add //
216| whd >lookup_add_hit % #E destruct
217| @lookup_add_oblivious @(pi2 … (pf_exit … f))
218| % [ #l' @lookup_add_oblivious | // ]
219] qed.
220
221(* Add a statement with a fresh label to the start of the function.  The
222   statement is parametrised by the *next* instruction's label. *)
223definition add_fresh_to_graph : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
224  (∀l. present ?? (pf_graph … f) l → labels_present (pf_graph … f) (s l)) →
225  (∀l. statement_typed_in … f (s l)) →
226  Σf':partial_fn le env. fn_contains … f f' ≝
227λle,env,s,f,p,tp.
228  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
229  let s' ≝ s (pf_entry … f) in
230    (mk_partial_fn le env g (pf_reggen … f)
231                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
232                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
233                   «l, ?» «pf_exit … f, ?»).
234[ % [ #l' @lookup_add_oblivious | // ]
235| @add_statement_inv @p @(pi2 … (pf_entry …))
236| @forall_nodes_add //
237| whd >lookup_add_hit % #E destruct
238| @lookup_add_oblivious @(pi2 … (pf_exit …))
239] qed.
240
241(* Variants for labels which are (goto) labels *)
242
243lemma add_statement_inv' : ∀le,env,l,s.∀f.
244  labels_P (λl. present ?? (pf_graph le env f) l ∨ lpresent le l) s →
245  partially_closed le (add … (pf_graph … f) l s).
246#le #env #l #s #f #p
247#l' #s' #H cases (identifier_eq … l l')
248[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
249  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
250| #NE @(labels_P_mp … (pf_closed … f l' s' ?))
251  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
252  | >lookup_add_miss in H; /2/
253  ]
254] qed.
255
256definition add_fresh_to_graph' : ∀le,env. ∀s:(label → statement). ∀f:partial_fn le env.
257  (∀l. present ?? (pf_graph … f) l → labels_P (λl.present ?? (pf_graph … f) l ∨ lpresent le l) (s l)) →
258  (∀l. statement_typed_in … f (s l)) →
259  Σf':partial_fn le env. fn_contains … f f' ≝
260λle,env,s,f,p,tp.
261  let 〈l,g〉 ≝ fresh … (pf_labgen … f) in
262  let s' ≝ s (pf_entry … f) in
263    (mk_partial_fn le env g (pf_reggen … f)
264                   (pf_params … f) (pf_locals … f) (pf_result … f) (pf_envok … f)
265                   (pf_stacksize … f) (add ?? (pf_graph … f) l s') ? ?
266                   «l, ?» «pf_exit … f, ?»).
267[ % [ #l' @lookup_add_oblivious | // ]
268| @add_statement_inv' @p @(pi2 … (pf_entry …))
269| @forall_nodes_add //
270| whd >lookup_add_hit % #E destruct
271| @lookup_add_oblivious @(pi2 … (pf_exit …))
272] qed.
273
274lemma extend_typ_env : ∀te,r,t,r',t'.
275  env_has te r t → env_has (〈r',t'〉::te) r t.
276#tw #r #t #r' #t' #H %2 @H
277qed.
278
279lemma stmt_extend_typ_env : ∀te,r,t,s.
280  statement_typed te s → statement_typed (〈r,t〉::te) s.
281#tw #r #t *
282[ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
283| *: //
284] qed.
285
286(* A little more nesting in the result type than I'd like, but it keeps the
287   function closely paired with the proof that it contains f. *)
288definition fresh_reg : ∀le,env. ∀f:partial_fn le env. ∀ty:typ.
289  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
290λle,env,f,ty.
291  let 〈r,g〉 ≝ fresh … (pf_reggen … f) in
292  let f' ≝
293    «mk_partial_fn le env
294       (pf_labgen … f) g (pf_params … f) (〈r,ty〉::(pf_locals … f))
295       (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? «pi1 … rt, ?»]) ?
296       (pf_stacksize … f) (pf_graph … f) (pf_closed … f) ? (pf_entry … f) (pf_exit … f), ?»
297  in
298    ❬f' , ?(*«r, ?»*)❭.
299[ @(«r, ?») % @refl
300| #l #s #L @stmt_extend_typ_env @(pf_typed … L)
301| #i #t #r1 #H #L %2 @(pf_envok … f … L)
302| %2 @(pi2 … rt)
303| % [ #l // | #r' #ty' #H @extend_typ_env @H ]
304] qed.
305
306axiom UnknownVariable : String.
307
308definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le env. expr_vars ty e (Env_has env) →
309  𝚺f':(Σf':partial_fn le env. fn_contains … f f'). (Σr:register. fn_env_has le env f' r ty) ≝
310λle,env,ty,e,f.
311  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
312  [ Id t i ⇒ λEnv. ❬«f, ?», «lookup_reg env i t Env, ?»❭
313  | _ ⇒ λ_.fresh_reg le env f ?
314  ].
315[ % //
316| @(pf_envok … Env) @refl
317] qed.
318 
319let 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 ≝ 
320 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.
321 
322let 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 ≝ 
323 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.
324
325definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (Env_has env) ].
326
327definition eject' : ∀A. ∀P:A → Type[0]. (𝚺a.P a) → A ≝
328λA,P,x. match x with [ mk_DPair a _ ⇒ a].
329
330definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
331                         ∀f:partial_fn le env. All ? (exprtyp_present env) es →
332                         𝚺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) ≝
333λle,env,es,f,Env.
334  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))
335    (λe,p,tl,acc.
336      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 ⇒
337        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.
338          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 ⇒
339            ❬«pi1 … f', ?»,«(pi1 … r)::(pi1 … rs), ?»❭
340          ]
341        ] p
342      ]) ❬«f, ?», «[ ], I»❭ es Env.
343[ @p
344| cases r #r' #Hr' cases rs #rs' #Hrs'
345  % [ whd in ⊢ (???%%%); @Hr' | @(All2_mp … Hrs') #r1 * #t1 #e1 #H1 @(fn_con_env … f1) [ @(pi2 … f') | @H1 ] ]
346| @fn_con_trans [ 3: @(pi2 … f') | skip | @(pi2 … f1) ]
347| @fn_con_refl
348]  qed.
349
350lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
351((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
352∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
353#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
354
355
356lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
357  choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|.
358#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
359qed.
360
361lemma present_included : ∀le,env,f,f',l.
362  fn_contains le env f f' →
363  present ?? (pf_graph … f) l →
364  present ?? (pf_graph … f') l.
365#le #env #f #f' #l * #H1 #H2 @H1 qed.
366
367(* Some definitions for the add_stmt function later, which we introduce now so
368   that we can build the whole fn_graph_included machinery at once. *)
369
370(* We need to show that the graph only grows, and that Cminor labels will end
371   up in the graph. *)
372definition Cminor_labels_added ≝ λle,env,s,f'.
373∀l. Exists ? (λl'.l=l') (labels_of s) →
374∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le env f') l'.
375
376record add_stmt_inv (le:label_env) (env:env) (s:stmt) (f:partial_fn le env) (f':partial_fn le env) : Prop ≝
377{ stmt_graph_con : fn_contains … f f'
378; stmt_labels_added : Cminor_labels_added … s f'
379}.
380
381(* Build some machinery to solve fn_contains goals. *)
382
383(* A datatype saying how we intend to prove a step. *)
384inductive fn_con_because (le:label_env) (env:env) : partial_fn le env → Type[0] ≝
385| fn_con_eq : ∀f. fn_con_because le env f
386| fn_con_sig : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
387    ∀f3:(Σf3:partial_fn le env.fn_contains … f2 f3). fn_con_because le env f3
388| fn_con_addinv : ∀f1,f2:partial_fn le env. fn_contains … f1 f2 →
389    ∀s.∀f3:(Σf3:partial_fn le env.add_stmt_inv … s f2 f3). fn_con_because le env f3
390.
391
392(* Extract the starting function for a step. *)
393let rec fn_con_because_left le env f0  (b:fn_con_because ?? f0) on b : partial_fn le env ≝
394  match b with [ fn_con_eq f ⇒ f | fn_con_sig f _ _ _ ⇒ f | fn_con_addinv f _ _ _ _ ⇒ f ].
395
396(* Some unification hints to pick the right step to apply.  The dummy variable
397   is there to provide goal that the lemma can't apply to, which causes an error
398   and forces the "repeat" tactical to stop.  The first hint recognises that we
399   have reached the desired starting point. *)
400
401unification hint 0 ≔ le:label_env, env:env, f:partial_fn le env, dummy:True;
402  f' ≟ f,
403  b  ≟ fn_con_eq le env f
404
405  fn_contains le env f f' ≡ fn_contains le env (fn_con_because_left le env f' b) f'
406.
407
408unification 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);
409  b ≟ fn_con_sig le env f1 f2 H12 f3
410
411  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
412.
413
414unification 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);
415  b ≟ fn_con_addinv le env f1 f2 H12 s f3
416
417  fn_contains le env f1 f3 ≡ fn_contains le env (fn_con_because_left le env f3 b) f3
418.
419
420(* A lemma to perform a step of the proof.  We can repeat this to do the whole
421   proof. *) 
422lemma fn_contains_step : ∀le,env,f. ∀b:fn_con_because le env f. fn_contains … (fn_con_because_left … f b) f.
423#le #env #f *
424[ #f @fn_con_refl
425| #f1 #f2 #H12 * #f3 #H23 @(fn_con_trans … H12 H23)
426| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
427] qed.
428
429notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
430  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
431
432axiom BadCminorProgram : String.
433
434let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty)
435  (Env:expr_vars ty e (Env_has env)) (f:partial_fn le env)
436  (dst:Σdst. fn_env_has … f dst ty)
437  on e: Σf':partial_fn le env. fn_contains … f f' ≝
438match 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
439[ Id t i ⇒ λEnv,dst.
440    let r ≝ lookup_reg env i t Env in
441    match register_eq r dst with
442    [ inl _ ⇒ «f, ?»
443    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
444    ]
445| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?»
446| Op1 t t' op e' ⇒ λEnv,dst.
447    let ❬f,r❭ ≝ choose_reg … e' f Env in
448    let f ≝ add_fresh_to_graph … (St_op1 t' t op dst r) f ?? in
449    let f ≝ add_expr … env ? e' Env f «r, ?» in
450      «pi1 … f, ?»
451| Op2 _ _ _ op e1 e2 ⇒ λEnv,dst.
452    let ❬f,r1❭ ≝ choose_reg … e1 f (proj1 … Env) in
453    let ❬f,r2❭ ≝ choose_reg … e2 f (proj2 … Env) in
454    let f ≝ add_fresh_to_graph … (St_op2 op dst r1 r2) f ?? in
455    let f ≝ add_expr … env ? e2 (proj2 … Env) f «r2, ?» in
456    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
457      «pi1 … f, ?»
458| Mem _ _ q e' ⇒ λEnv,dst.
459    let ❬f,r❭ ≝ choose_reg … e' f Env in
460    let f ≝ add_fresh_to_graph … (St_load q r dst) f ?? in
461    let f ≝ add_expr … env ? e' Env f «r,?» in
462      «pi1 … f, ?»
463| Cond _ _ _ e' e1 e2 ⇒ λEnv,dst.
464    let resume_at ≝ pf_entry … f in
465    let f ≝ add_expr … env ? e2 (proj2 … Env) f dst in
466    let lfalse ≝ pf_entry … f in
467    let f ≝ add_fresh_to_graph … (λ_.St_skip resume_at) f ?? in
468    let f ≝ add_expr … env ? e1 (proj2 … (proj1 … Env)) f «dst, ?» in
469    let ❬f,r❭ ≝ choose_reg … e' f ? in
470    let f ≝ add_fresh_to_graph … (λltrue. St_cond r ltrue lfalse) f ?? in
471    let f ≝ add_expr … env ? e' (proj1 … (proj1 … Env)) f «r, ?» in
472      «pi1 … f, ?»
473| Ecost _ l e' ⇒ λEnv,dst.
474    let f ≝ add_expr … env ? e' Env f dst in
475    let f ≝ add_fresh_to_graph … (St_cost l) f ?? in
476      «f, ?»
477] Env dst.
478(* For new labels, we need to step back through the definitions of f until we
479   hit the point that it was added. *)
480try (repeat @fn_contains_step @I)
481try (#l #H @H)
482try (#l @I)
483[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
484| 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
485| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
486| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
487| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
488| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
489| @(π1 (π1 Env))
490| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
491| #l #H @(fn_con_graph … (pi2 ?? resume_at)) repeat @fn_contains_step @I
492] qed.
493
494let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
495                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env)
496                  (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' ≝
497match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
498[ nil ⇒ λ_.λ_. match dsts return λx. ?=|x| → Σf':partial_fn le env. fn_contains le env f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
499| cons e et ⇒ λEnv.
500    match dsts return λx. All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) x (e::et) → ?=|x| → ? with
501    [ nil ⇒ λ_.λpf.⊥
502    | cons r rt ⇒ λHdsts,pf.
503        let f' ≝ add_exprs ? env et ? rt ? f ? in
504        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.
505          let f'' ≝ add_expr ? env ty e ? f' r in
506            «pi1 … f'', ?»
507        ] (proj1 ?? Env) (π1 Hdsts)
508    ]
509] Env Hdsts pf.
510try (repeat @fn_contains_step @I)
511[ 1,2: normalize in pf; destruct
512| @Env
513| @(fn_con_env … Hr) repeat @fn_contains_step @I
514| @(proj2 … Env)
515| normalize in pf; destruct @e0
516| @(π2 Hdsts)
517] qed.
518
519axiom UnknownLabel : String.
520axiom ReturnMismatch : String.
521
522definition stmt_inv : env → label_env → stmt → Prop ≝
523λenv,lenv. stmt_P (λs. stmt_vars (Env_has env) s ∧ stmt_labels (present ?? lenv) s).
524
525(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
526definition expr_is_Id : ∀t. expr t → option ident ≝
527λt,e. match e with
528[ Id _ id ⇒ Some ? id
529| _ ⇒ None ?
530].
531
532(* XXX Work around odd disambiguation errors. *)
533alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
534alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
535
536definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
537λA,P,m,l,n.
538  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
539  [ None ⇒ λ_. Error ? m
540  | Some a ⇒ λH'. OK ? «a, ?»
541  ] (All_nth A P n l (pi2 … l)).
542@H' @refl qed.
543
544lemma lookup_label_rev : ∀lenv,l,l',p.
545  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
546#lenv #l #l' #p
547cut (∃lx. lookup ?? lenv l = Some ? lx)
548[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
549  [ * #H cases (H (refl ??))
550  | #lx #_ %{lx} @refl
551  ]
552| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
553] qed.
554
555lemma lookup_label_rev' : ∀lenv,l,p.
556  lookup ?? lenv l = Some ? (lookup_label lenv l p).
557#lenv #l #p @lookup_label_rev [ @p | @refl ]
558qed.
559
560lemma lookup_label_lpresent : ∀lenv,l,p.
561  lpresent lenv (lookup_label lenv l p).
562#le #l #p whd %{l} @lookup_label_rev'
563qed.
564
565lemma empty_Cminor_labels_added : ∀le,env,s,f'.
566  labels_of s = [ ] → Cminor_labels_added le env s f'.
567#le #env #s #f' #E whd >E #l *;
568qed.
569
570lemma equal_Cminor_labels_added : ∀le,env,s,s',f.
571  labels_of s = labels_of s' → Cminor_labels_added … s' f →
572  Cminor_labels_added le env s f.
573#le #env #s #s' #f #E whd in ⊢ (% → %); > E #H @H
574qed.
575
576lemma Cminor_labels_con : ∀le,env,s,f,f'.
577  fn_contains le env f f' →
578  Cminor_labels_added … s f →
579  Cminor_labels_added … s f'.
580#le #env #s #f #f' #INC #ADDED
581#l #E cases (ADDED l E) #l' * #L #P
582%{l'} % [ @L | @(present_included … P) @INC ]
583qed.
584
585lemma Cminor_labels_inv : ∀le,env,s,s',f.
586  ∀f':Σf':partial_fn le env. add_stmt_inv le env s' f f'.
587  Cminor_labels_added le env s f →
588  Cminor_labels_added le env s f'.
589#le #env #s #s' #f * #f' * #H1 #H2 #H3
590#l #E cases (H3 l E) #l' * #L #P
591%{l'} % [ @L | @(present_included … P) @H1 ]
592qed.
593
594lemma Cminor_labels_sig : ∀le,env,s,f.
595  ∀f':Σf':partial_fn le env. fn_contains … f f'.
596  Cminor_labels_added … s f →
597  Cminor_labels_added … s f'.
598#le #env #s #f * #f' #H1 #H2
599#l #E cases (H2 l E) #l' * #L #P
600%{l'} % [ @L | @(present_included … P) @H1 ]
601qed.
602
603let 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') ≝
604match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
605[ St_skip ⇒ λ_. OK ? «f, ?»
606| St_assign t x e ⇒ λEnv.
607    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
608    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
609| St_store _ _ q e1 e2 ⇒ λEnv.
610    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
611    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
612    let f ≝ add_fresh_to_graph … (St_store q addr_reg val_reg) f ?? in
613    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) f «addr_reg, ?» in
614    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) f «val_reg, ?»), ?»
615| St_call return_opt_id e args ⇒ λEnv.
616    let return_opt_reg ≝
617      match return_opt_id return λo. ? → ? with
618      [ None ⇒ λ_. None ?
619      | Some idty ⇒ λEnv. Some ? (lookup_reg env (\fst idty) (\snd idty) ?)
620      ] Env in
621    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
622    let f ≝
623      match expr_is_Id ? e with
624      [ Some id ⇒ add_fresh_to_graph … (St_call_id id args_regs return_opt_reg) f ??
625      | None ⇒
626        let ❬f, fnr❭ ≝ choose_reg … e f (π2 (π1 (π1 Env))) in
627        let f ≝ add_fresh_to_graph … (St_call_ptr fnr args_regs return_opt_reg) f ?? in
628        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) f «fnr, ?»), ?»
629      ] in
630    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
631| St_tailcall e args ⇒ λEnv.
632    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
633    let f ≝
634      match expr_is_Id ? e with
635      [ Some id ⇒ add_fresh_to_graph … (λ_. St_tailcall_id id args_regs) f ??
636      | None ⇒
637        let ❬f,fnr❭ ≝ choose_reg … e f (π1 (π1 Env)) in
638        let f ≝ add_fresh_to_graph … (λ_. St_tailcall_ptr fnr args_regs) f ?? in
639        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) f «fnr, ?»), ?»
640      ] in
641    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
642| St_seq s1 s2 ⇒ λEnv.
643    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
644    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
645      OK ? «pi1 … f1, ?»
646| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
647    let l_next ≝ pf_entry … f in
648    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
649    let l2 ≝ pf_entry … f2 in
650    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
651    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
652    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
653    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
654    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
655| St_loop s ⇒ λEnv.
656    let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
657    let l_loop ≝ pf_entry … f in
658    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
659    OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
660| St_block s ⇒ λEnv.
661    do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
662    OK ? «pi1 … f, ?»
663| St_exit n ⇒ λEnv.
664    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
665    OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
666| St_switch sz sg e tab n ⇒ λEnv.
667    let ❬f,r❭ ≝ choose_reg … e f ? in
668    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
669    let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
670    do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
671      do f ← f;
672      let 〈i,n〉 ≝ cs in
673      let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
674      let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
675      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
676      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
677      let f ≝ add_fresh_to_graph … (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ?? in
678      let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
679        OK ? «pi1 … f, ?») (OK ? f) tab;
680    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
681| St_return opt_e ⇒ let f0 ≝ f in
682    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
683    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
684    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
685    | Some e ⇒
686        match pf_result … f with
687        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
688        | Some r ⇒
689            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
690            [ mk_DPair ty e ⇒ λEnv.
691                match typ_eq (\snd r) ty with
692                [ 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
693                          OK ? «pi1 … f, ?»
694                | inr _ ⇒ Error ? (msg ReturnMismatch)
695                ]
696            ]
697        ]
698    ]
699| St_label l s' ⇒ λEnv.
700    do f ← add_stmt env label_env s' (π2 Env) f exits;
701    let l' ≝ lookup_label label_env l ? in
702    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
703| St_goto l ⇒ λEnv.
704    let l' ≝ lookup_label label_env l ? in
705    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
706| St_cost l s' ⇒ λEnv.
707    do f ← add_stmt env label_env s' (π2 Env) f exits;
708    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
709] Env.
710try @(π1 Env)
711try @(π2 Env)
712try @(π1 (π1 Env))
713try @(π2 (π1 Env))
714try @mk_add_stmt_inv
715try (repeat @fn_contains_step @I)
716try (@empty_Cminor_labels_added @refl)
717try (#l #H @I)
718try (#l #H @H)
719try (#l @I)
720[ @(pf_envok … (π1 (π1 Env))) @refl
721| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
722| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
723| 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
724| 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs))
725| 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
726| @(π1 (π1 (π1 Env)))
727| 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
728| #l #H cases (Exists_append … H)
729  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
730  | #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ????? (pi2 ?? f2))
731  ]
732| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
733| #l #H cases (Exists_append … H)
734  [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f1))
735  | #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ????? (pi2 ?? f2))
736  ]
737| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
738| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
739| @(pi2 … (pf_entry …))
740| @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
741| % [ @pi2 | @(pi2 ?? exits) ]
742| @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
743| #l' #H @(pi2 … l)
744| #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
745| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
746| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
747| #_ (* see above *) <E @(pi2 ?? r)
748| @(pi2 … (pf_entry …))
749| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
750        | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f))
751        ]
752| #l1 #H whd %2 @lookup_label_lpresent
753| @(equal_Cminor_labels_added ??? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ????? (pi2 … f)) ]
754] qed.
755
756
757definition c2ra_function (*: internal_function → internal_function*) ≝
758λf.
759let labgen0 ≝ new_universe LabelTag in
760let reggen0 ≝ new_universe RegisterTag in
761let cminor_labels ≝ labels_of (f_body f) in
762let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
763let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
764let ❬locals_reggen, result❭ ≝
765  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
766  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
767  | Some ty ⇒
768      let 〈r,gen〉 ≝ fresh … reggen2 in
769        mk_DPair ? (λlr.option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt))) 〈〈r,ty〉::locals0, gen〉 (Some ? «〈r,ty〉, ?») ] in
770let locals ≝ \fst locals_reggen in
771let reggen ≝ \snd locals_reggen in
772let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
773let 〈l,labgen〉 ≝ fresh … labgen1 in
774let emptyfn ≝
775  mk_partial_fn
776    label_env
777    env
778    labgen
779    reggen
780    params
781    locals
782    result
783    ?
784    (f_stacksize f)
785    (add ?? (empty_map …) l St_return)
786    ?
787    ?
788    l
789    l in
790do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
791OK ? (mk_internal_function
792    (pf_labgen … f)
793    (pf_reggen … f)
794    (match pf_result … f with [ None ⇒ None ? | Some rt ⇒ Some ? (pi1 … rt) ])
795    (pf_params … f)
796    (pf_locals … f)
797    (pf_stacksize … f)
798    (pf_graph … f)
799    ?
800    (pf_typed … f)
801    (pf_entry … f)
802    (pf_exit … f)
803  ).
804[ @I
805| -emptyfn @(stmt_P_mp … (f_inv f))
806  #s * #V #L %
807  [ @(stmt_vars_mp … V)
808    #i #t #H cases (Exists_append … H)
809    cases daemon (* XXX needs populates_env
810    [ #H1 @(populate_extends ?????? (sym_eq … E2))
811          @(populates_env … (sym_eq … E1)) @H1
812    | #H1 @(populates_env … (sym_eq … E2)) @H1
813    ]*)
814  | @(stmt_labels_mp … L)
815    #l #H @(populates_label_env … (sym_eq … El)) @H
816  ]
817| #l #s #E @(labels_P_mp … (pf_closed … f l s E))
818  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
819  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
820  #P' @P'
821  | cases (label_env_contents … (sym_eq ??? El) l ?)
822    [ #H @H
823    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
824    | whd >H % #E' destruct (E')
825    ]
826  ]
827  ]
828| cases daemon (* XXX need information about env *)
829| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
830  [ * #E1 #E2 >E2 @I
831  | whd in ⊢ (??%? → ?); #E' destruct (E')
832  ]
833| #l #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
834  [ * #E1 #E2 >E2 @I
835  | whd in ⊢ (??%? → ?); #E' destruct (E')
836  ]
837| 7,8: whd >lookup_add_hit % #E destruct
838| % @refl
839]
840qed.
841
842definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
843λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
844
845include "Cminor/initialisation.ma".
846
847definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
848λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.