source: src/Cminor/toRTLabs.ma @ 1611

Last change on this file since 1611 was 1611, checked in by sacerdot, 8 years ago

All of Cminor now compiles with the latest lib of Matita.

File size: 30.7 KB
Line 
1include "basics/lists/list.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag register.
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, 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 lookup_reg : ∀e:env. ∀id. present ?? e id → register ≝ lookup_present ??.
95definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
96
97(* Check that the domain of one graph is included in another, for monotonicity
98   properties.  Note that we don't say anything about the statements. *)
99definition graph_included : graph statement → graph statement → Prop ≝
100λg1,g2. ∀l. present ?? g1 l → present ?? g2 l.
101
102lemma graph_inc_trans : ∀g1,g2,g3.
103  graph_included g1 g2 → graph_included g2 g3 → graph_included g1 g3.
104#g1 #g2 #g3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed.
105
106definition lpresent ≝ λlbls:label_env. λl. ∃l'. lookup ?? lbls l' = Some ? l.
107
108definition partially_closed : label_env → graph statement → Prop ≝
109 λe,g. ∀l,s. lookup ?? g l = Some ? s → labels_P (λl. present ?? g l ∨ lpresent e l) s.
110
111(* I'd use a single parametrised definition along with internal_function, but
112   it's a pain without implicit parameters. *)
113record partial_fn (lenv:label_env) : Type[0] ≝
114{ pf_labgen    : universe LabelTag
115; pf_reggen    : universe RegisterTag
116; pf_result    : option (register × typ)
117; pf_params    : list (register × typ)
118; pf_locals    : list (register × typ)
119; pf_stacksize : nat
120; pf_graph     : graph statement
121; pf_closed    : partially_closed lenv pf_graph
122; pf_entry     : Σl:label. present ?? pf_graph l
123; pf_exit      : Σl:label. present ?? pf_graph l
124}.
125
126inductive fn_graph_included (le:label_env) (f1:partial_fn le) (f2:partial_fn le) : Prop ≝
127| fn_graph_inc : graph_included (pf_graph ? f1) (pf_graph ? f2) → fn_graph_included le f1 f2.
128
129lemma fn_graph_inc_trans : ∀le,f1,f2,f3.
130  fn_graph_included le f1 f2 → fn_graph_included le f2 f3 → fn_graph_included le f1 f3.
131#le #f1 #f2 #f3 * #H1 * #H2 % @(graph_inc_trans … H1 H2) qed.
132
133lemma fn_graph_included_refl : ∀label_env,f.
134  fn_graph_included label_env f f.
135#le #f % #l #H @H qed.
136
137lemma fn_graph_included_sig : ∀label_env,f,f0.
138  ∀f':Σf':partial_fn label_env. fn_graph_included ? f0 f'.
139  fn_graph_included label_env f f0 →
140  fn_graph_included label_env f f'.
141#le #f #f0 * #f' #H1 #H2 @(fn_graph_inc_trans … H2 H1)
142qed.
143
144lemma add_statement_inv : ∀le,l,s.∀f.
145  labels_present (pf_graph le f) s →
146  partially_closed le (add … (pf_graph ? f) l s).
147#le #l #s #f #p
148#l' #s' #H cases (identifier_eq … l l')
149[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
150  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
151| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
152  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
153  | >lookup_add_miss in H; /2/
154  ]
155] qed.
156
157(* Add a statement to the graph, *without* updating the entry label. *)
158definition fill_in_statement : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
159λle,l,s,f,p.
160  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
161                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
162                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
163                «pf_entry ? f, ?» «pf_exit ? f, ?».
164[ @add_statement_inv @p
165| 2,3: @lookup_add_oblivious [ @(pi2 … (pf_entry le f)) | @(pi2 … (pf_exit le f)) ]
166| % #l' @lookup_add_oblivious
167] qed.
168
169(* Add a statement to the graph, making it the entry label. *)
170definition add_to_graph : ∀le. label → ∀s:statement. ∀f:partial_fn le. labels_present (pf_graph ? f) s → Σf':partial_fn le. fn_graph_included le f f' ≝
171λle,l,s,f,p.
172  mk_partial_fn le (pf_labgen ? f) (pf_reggen ? f)
173                (pf_result ? f) (pf_params ? f) (pf_locals ? f)
174                (pf_stacksize ? f) (add ?? (pf_graph ? f) l s) ?
175                «l, ?» «pf_exit ? f, ?».
176[ @add_statement_inv @p
177| whd >lookup_add_hit % #E destruct
178| @lookup_add_oblivious @(pi2 … (pf_exit le f))
179| % #l' @lookup_add_oblivious
180] qed.
181
182(* Add a statement with a fresh label to the start of the function.  The
183   statement is parametrised by the *next* instruction's label. *)
184definition add_fresh_to_graph : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_present (pf_graph ? f) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
185λle,s,f,p.
186  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
187  let s' ≝ s (pf_entry ? f) in
188    (mk_partial_fn le g (pf_reggen ? f)
189                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
190                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
191                   «l, ?» «pf_exit ? f, ?»).
192[ % #l' @lookup_add_oblivious
193| @add_statement_inv @p @(pi2 … (pf_entry …))
194| whd >lookup_add_hit % #E destruct
195| @lookup_add_oblivious @(pi2 … (pf_exit …))
196] qed.
197
198(* Variants for labels which are (goto) labels *)
199
200lemma add_statement_inv' : ∀le,l,s.∀f.
201  labels_P (λl. present ?? (pf_graph le f) l ∨ lpresent le l) s →
202  partially_closed le (add … (pf_graph ? f) l s).
203#le #l #s #f #p
204#l' #s' #H cases (identifier_eq … l l')
205[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
206  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
207| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
208  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
209  | >lookup_add_miss in H; /2/
210  ]
211] qed.
212
213definition add_fresh_to_graph' : ∀le. ∀s:(label → statement). ∀f:partial_fn le. (∀l. present ?? (pf_graph ? f) l → labels_P (λl.present ?? (pf_graph ? f) l ∨ lpresent le l) (s l)) → Σf':partial_fn le. fn_graph_included le f f' ≝
214λle,s,f,p.
215  let 〈l,g〉 ≝ fresh … (pf_labgen ? f) in
216  let s' ≝ s (pf_entry ? f) in
217    (mk_partial_fn le g (pf_reggen ? f)
218                   (pf_result ? f) (pf_params ? f) (pf_locals ? f)
219                   (pf_stacksize ? f) (add ?? (pf_graph ? f) l s') ?
220                   «l, ?» «pf_exit ? f, ?»).
221[ % #l' @lookup_add_oblivious
222| @add_statement_inv' @p @(pi2 … (pf_entry …))
223| whd >lookup_add_hit % #E destruct
224| @lookup_add_oblivious @(pi2 … (pf_exit …))
225] qed.
226
227definition fresh_reg : ∀le. ∀f:partial_fn le. typ → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
228λle,f,ty.
229  let 〈r,g〉 ≝ fresh … (pf_reggen ? f) in
230    〈r, «mk_partial_fn le (pf_labgen ? f) g
231                       (pf_result ? f) (pf_params ? f) (〈r,ty〉::(pf_locals ? f))
232                       (pf_stacksize ? f) (pf_graph ? f) (pf_closed ? f) (pf_entry ? f) (pf_exit ? f), ?»〉.
233% #l // qed.
234
235axiom UnknownVariable : String.
236
237definition choose_reg : ∀le. ∀env:env.∀ty.∀e:expr ty. ∀f:partial_fn le. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') ≝
238λle,env,ty,e,f.
239  match e return λty,e. expr_vars ty e (present ?? env) → register × (Σf':partial_fn le. fn_graph_included le f f') with
240  [ Id _ i ⇒ λEnv. 〈lookup_reg env i Env, «f, ?»〉
241  | _ ⇒ λ_.fresh_reg le f ty
242  ].
243% // qed.
244 
245let 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 ≝ 
246 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.
247
248definition exprtyp_present ≝ λenv:env.λe:𝚺t:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
249
250definition choose_regs : ∀le. ∀env:env. ∀es:list (𝚺t:typ.expr t).
251                         ∀f:partial_fn le. All ? (exprtyp_present env) es →
252                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
253λle,env,es,f,Env.
254  foldr_all (𝚺t:typ.expr t) ??
255    (λe,p,acc. let 〈rs,f〉 ≝ acc in
256             let 〈r,f'〉 ≝ match e return λe.? → ? with [ mk_DPair t e ⇒ λp.choose_reg le env t e (pi1 ?? f) ? ] p in
257             〈r::rs,«pi1 ?? f', ?»〉) 〈[ ], «f, ?»〉 es Env.
258[ @p
259| @fn_graph_inc_trans [ 3: @(pi2 ?? f') | skip | @(pi2 ?? f) ]
260| % //
261]  qed.
262
263lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
264((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
265∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
266#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
267
268
269lemma choose_regs_length : ∀le,env,es,f,p,rs,f'.
270  choose_regs le env es f p = 〈rs,f'〉 → |es| = |rs|.
271#le #env #es #f elim es
272[ #p #rs #f normalize #E destruct @refl
273| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E
274  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
275  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
276  destruct (E4) skip (E1 E3) @eq_f @IH
277  [ @(proj2 … p)
278  | 3: @sym_eq @E1
279  | 2: skip
280  ]
281] qed.
282
283lemma present_included : ∀le,f,f',l.
284  fn_graph_included le f f' →
285  present ?? (pf_graph le f) l →
286  present ?? (pf_graph le f') l.
287#le #f #f' #l * #H1 #H2 @H1 @H2 qed.
288
289(* Some definitions for the add_stmt function later, which we introduce now so
290   that we can build the whole fn_graph_included machinery at once. *)
291
292(* We need to show that the graph only grows, and that Cminor labels will end
293   up in the graph. *)
294definition Cminor_labels_added ≝ λle,s,f'.
295∀l. Exists ? (λl'.l=l') (labels_of s) →
296∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
297
298record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
299{ stmt_graph_inc : fn_graph_included ? f f'
300; stmt_labels_added : Cminor_labels_added le s f'
301}.
302
303(* Build some machinery to solve fn_graph_included goals. *)
304
305(* A datatype saying how we intend to prove a step. *)
306inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
307| fn_inc_eq : ∀f. fn_inc_because le f
308| fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
309    ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
310| fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
311    ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
312.
313
314(* Extract the starting function for a step. *)
315let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le ≝
316  match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
317
318(* Some unification hints to pick the right step to apply.  The dummy variable
319   is there to provide goal that the lemma can't apply to, which causes an error
320   and forces the "repeat" tactical to stop.  The first hint recognises that we
321   have reached the desired starting point. *)
322
323unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
324  f' ≟ f,
325  b  ≟ fn_inc_eq le f
326
327  fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
328.
329
330unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3);
331  b ≟ fn_inc_sig le f1 f2 H12 f3
332
333  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
334.
335
336unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3);
337  b ≟ fn_inc_addinv le f1 f2 H12 s f3
338
339  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
340.
341
342(* A lemma to perform a step of the proof.  We can repeat this to do the whole
343   proof. *) 
344lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
345#le #f *
346[ #f @fn_graph_included_refl
347| #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
348| #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
349] qed.
350
351
352axiom BadCminorProgram : String.
353
354let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
355match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
356[ Id t i ⇒ λEnv.
357    let r ≝ lookup_reg env i Env in
358    match register_eq r dst with
359    [ inl _ ⇒ «f, ?»
360    | inr _ ⇒ «pi1 … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
361    ]
362| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
363| Op1 t t' op e' ⇒ λEnv.
364    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
365    let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
366    let f ≝ add_expr ? env ? e' Env r f in
367      «pi1 … f, ?»
368| Op2 _ _ _ op e1 e2 ⇒ λEnv.
369    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
370    let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
371    let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
372    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
373    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
374      «pi1 … f, ?»
375| Mem _ _ q e' ⇒ λEnv.
376    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
377    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
378    let f ≝ add_expr ? env ? e' Env r f in
379      «pi1 … f, ?»
380| Cond _ _ _ e' e1 e2 ⇒ λEnv.
381    let resume_at ≝ pf_entry ? f in
382    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
383    let lfalse ≝ pf_entry ? f in
384    let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
385    let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
386    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
387    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
388    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
389      «pi1 … f, ?»
390| Ecost _ l e' ⇒ λEnv.
391    let f ≝ add_expr ? env ? e' Env dst f in
392    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
393      «f, ?»
394] Env.
395(* For new labels, we need to step back through the definitions of f until we
396   hit the point that it was added. *)
397try (repeat @fn_includes_step @I)
398try (#l #H @H)
399[ #l #H whd % [ @H | @(present_included … (pi2 … lfalse)) repeat @fn_includes_step @I ]
400| #l #H @(present_included … (pi2 ?? resume_at)) repeat @fn_includes_step @I
401] qed.
402
403let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
404                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
405match es return λes.All ?? es → |es|=|dsts| → ? with
406[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
407| cons e et ⇒ λEnv.
408    match dsts return λx. ?=|x| → ? with
409    [ nil ⇒ λpf.⊥
410    | cons r rt ⇒ λpf.
411        let f ≝ add_exprs ? env et ? rt ? f in
412        match e return λe.exprtyp_present ? e → ? with [ mk_DPair ty e ⇒ λEnv.
413          let f ≝ add_expr ? env ty e ? r f in
414            «pi1 … f, ?» ] (proj1 ?? Env)
415    ]
416] Env pf.
417try (repeat @fn_includes_step @I)
418[ 1,2: normalize in pf; destruct
419| @Env
420| @(proj2 … Env)
421| normalize in pf; destruct @e0
422] qed.
423
424axiom UnknownLabel : String.
425axiom ReturnMismatch : String.
426
427definition stmt_inv : env → label_env → stmt → Prop ≝
428λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
429
430(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
431definition expr_is_Id : ∀t. expr t → option ident ≝
432λt,e. match e with
433[ Id _ id ⇒ Some ? id
434| _ ⇒ None ?
435].
436
437(* XXX Work around odd disambiguation errors. *)
438alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
439alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
440
441definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
442λA,P,m,l,n.
443  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
444  [ None ⇒ λ_. Error ? m
445  | Some a ⇒ λH'. OK ? «a, ?»
446  ] (All_nth A P n l (pi2 … l)).
447@H' @refl qed.
448
449lemma lookup_label_rev : ∀lenv,l,l',p.
450  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
451#lenv #l #l' #p
452cut (∃lx. lookup ?? lenv l = Some ? lx)
453[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
454  [ * #H cases (H (refl ??))
455  | #lx #_ %{lx} @refl
456  ]
457| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
458] qed.
459
460lemma lookup_label_rev' : ∀lenv,l,p.
461  lookup ?? lenv l = Some ? (lookup_label lenv l p).
462#lenv #l #p @lookup_label_rev [ @p | @refl ]
463qed.
464
465lemma lookup_label_lpresent : ∀lenv,l,p.
466  lpresent lenv (lookup_label lenv l p).
467#le #l #p whd %{l} @lookup_label_rev'
468qed.
469
470lemma empty_Cminor_labels_added : ∀le,s,f'.
471  labels_of s = [ ] → Cminor_labels_added le s f'.
472#le #s #f' #E whd >E #l *;
473qed.
474
475lemma equal_Cminor_labels_added : ∀le,s,s',f.
476  labels_of s = labels_of s' → Cminor_labels_added le s' f →
477  Cminor_labels_added le s f.
478#le #s #s' #f #E whd in ⊢ (% → %); > E #H @H
479qed.
480
481lemma Cminor_labels_inc : ∀le,s,f,f'.
482  fn_graph_included le f f' →
483  Cminor_labels_added le s f →
484  Cminor_labels_added le s f'.
485#le #s #f #f' #INC #ADDED
486#l #E cases (ADDED l E) #l' * #L #P
487%{l'} % [ @L | @(present_included … P) @INC ]
488qed.
489
490lemma Cminor_labels_inv : ∀le,s,s',f.
491  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
492  Cminor_labels_added le s f →
493  Cminor_labels_added le s f'.
494#le #s #s' #f * #f' * #H1 #H2 #H3
495#l #E cases (H3 l E) #l' * #L #P
496%{l'} % [ @L | @(present_included … P) @H1 ]
497qed.
498
499lemma Cminor_labels_sig : ∀le,s,f.
500  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
501  Cminor_labels_added le s f →
502  Cminor_labels_added le s f'.
503#le #s #f * #f' #H1 #H2
504#l #E cases (H2 l E) #l' * #L #P
505%{l'} % [ @L | @(present_included … P) @H1 ]
506qed.
507
508let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
509match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
510[ St_skip ⇒ λ_. OK ? «f, ?»
511| St_assign _ x e ⇒ λEnv.
512    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
513    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
514| St_store _ _ q e1 e2 ⇒ λEnv.
515    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
516    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
517    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
518    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
519    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
520| St_call return_opt_id e args ⇒ λEnv.
521    let return_opt_reg ≝
522      match return_opt_id return λo. ? → ? with
523      [ None ⇒ λ_. None ?
524      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
525      ] Env in
526    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
527    let f ≝
528      match expr_is_Id ? e with
529      [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
530      | None ⇒
531        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
532        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
533        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
534      ] in
535    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
536| St_tailcall e args ⇒ λEnv.
537    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
538    let f ≝
539      match expr_is_Id ? e with
540      [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
541      | None ⇒
542        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
543        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
544        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
545      ] in
546    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
547| St_seq s1 s2 ⇒ λEnv.
548    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
549    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
550      OK ? «pi1 … f1, ?»
551| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
552    let l_next ≝ pf_entry ? f in
553    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
554    let l2 ≝ pf_entry ? f2 in
555    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
556    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
557    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
558    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
559    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
560| St_loop s ⇒ λEnv.
561    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
562    let l_loop ≝ pf_entry ? f in
563    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
564    OK ? «pi1 … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
565| St_block s ⇒ λEnv.
566    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
567    OK ? «pi1 … f, ?»
568| St_exit n ⇒ λEnv.
569    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
570    OK ? «pi1 … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
571| St_switch sz sg e tab n ⇒ λEnv.
572    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
573    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
574    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
575    do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
576      do f ← f;
577      let 〈i,n〉 ≝ cs in
578      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
579      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
580      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
581      let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
582      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
583      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
584        OK ? «pi1 … f, ?») (OK ? f) tab;
585    OK ? «pi1 … (add_expr ? env ? e (π1 Env) r f), ?»
586| St_return opt_e ⇒ let f0 ≝ f in
587    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
588    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
589    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
590    | Some e ⇒
591        match pf_result ? f with
592        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
593        | Some r ⇒
594            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
595            [ mk_DPair ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
596                              OK ? «pi1 … f, ?» ]
597        ]
598    ]
599| St_label l s' ⇒ λEnv.
600    do f ← add_stmt env label_env s' (π2 Env) f exits;
601    let l' ≝ lookup_label label_env l ? in
602    OK ? «pi1 … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
603| St_goto l ⇒ λEnv.
604    let l' ≝ lookup_label label_env l ? in
605    OK ? «pi1 … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
606| St_cost l s' ⇒ λEnv.
607    do f ← add_stmt env label_env s' (π2 Env) f exits;
608    OK ? «pi1 … (add_fresh_to_graph ? (St_cost l) f ?), ?»
609] Env.
610try @(π1 Env)
611try @(π2 Env)
612try @(π1 (π1 Env))
613try @(π2 (π1 Env))
614try @mk_add_stmt_inv
615try (repeat @fn_includes_step @I)
616try (@empty_Cminor_labels_added @refl)
617try (@(All_mp … (pi2 ?? exits)))
618try (#l #H @I)
619try (#l #H @H)
620[ -f @(choose_regs_length … (sym_eq … Eregs))
621| whd in Env; @(π1 (π1 (π1 Env)))
622| -f @(choose_regs_length … (sym_eq … Eregs))
623| #l #H cases (Exists_append … H)
624  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
625  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (pi2 ?? f2)) ]
626  ]
627| #l #H @(present_included … H) repeat @fn_includes_step @I
628| #l #H @(present_included … (pi2 ?? l_next)) repeat @fn_includes_step @I
629| #l #H cases (Exists_append … H)
630  [ @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f1))) repeat @fn_includes_step @I
631  | @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f2))) repeat @fn_includes_step @I
632  ]
633| #l #H % [ @H | @(present_included … (pi2 ?? l2)) repeat @fn_includes_step @I ]
634| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
635| @(pi2 ?? (pf_entry ??))
636| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
637| % [ @pi2 | @(pi2 ?? exits) ]
638| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
639| #l' #H @(pi2 ?? l)
640| #l #H @(present_included … (pi2 ?? l_default)) repeat @fn_includes_step @I
641| #l #H % [ @(present_included … (pi2 ?? l_case)) repeat @fn_includes_step @I | @H ]
642| @(pi2 … (pf_entry …))
643| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
644        |@Cminor_labels_sig @(stmt_labels_added … (pi2 … f))
645        ]
646| #l1 #H whd %2 @lookup_label_lpresent
647| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added … (pi2 … f)) ]
648] qed.
649
650definition c2ra_function (*: internal_function → internal_function*) ≝
651λf.
652let labgen0 ≝ new_universe LabelTag in
653let reggen0 ≝ new_universe RegisterTag in
654let cminor_labels ≝ labels_of (f_body f) in
655let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
656let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
657let 〈result, locals, reggen〉 ≝
658  match f_return f with
659  [ None ⇒ 〈None ?, locals0, reggen2〉
660  | Some ty ⇒
661      let 〈r,gen〉 ≝ fresh … reggen2 in
662        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
663let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
664let 〈l,labgen〉 ≝ fresh … labgen1 in
665let emptyfn ≝
666  mk_partial_fn
667    label_env
668    labgen
669    reggen
670    result
671    params
672    locals
673    (f_stacksize f)
674    (add ?? (empty_map …) l St_return)
675    ?
676    l
677    l in
678do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
679OK ? (mk_internal_function
680    (pf_labgen ? f)
681    (pf_reggen ? f)
682    (pf_result ? f)
683    (pf_params ? f)
684    (pf_locals ? f)
685    (pf_stacksize ? f)
686    (pf_graph ? f)
687    ?
688    (pf_entry ? f)
689    (pf_exit ? f)
690  ).
691[ @I
692| -emptyfn @(stmt_P_mp … (f_inv f))
693  #s * #V #L %
694  [ @(stmt_vars_mp … V)
695    #i #H cases (Exists_append … H)
696    [ #H1 @(populate_extends ?????? (sym_eq … E2))
697          @(populates_env … (sym_eq … E1)) @H1
698    | #H1 @(populates_env … (sym_eq … E2)) @H1
699    ]
700  | @(stmt_labels_mp … L)
701    #l #H @(populates_label_env … (sym_eq … El)) @H
702  ]
703| #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
704  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
705  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
706  #P' @P'
707  | cases (label_env_contents … (sym_eq ??? El) l ?)
708    [ #H @H
709    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
710    | whd >H % #E' destruct (E')
711    ]
712  ]
713  ]
714| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
715  [ * #E1 #E2 >E2 @I
716  | whd in ⊢ (??%? → ?); #E' destruct (E')
717  ]
718| *: whd >lookup_add_hit % #E destruct
719]
720qed.
721
722definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
723λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
724
725include "Cminor/initialisation.ma".
726
727definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
728λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.