source: src/Cminor/toRTLabs.ma @ 1599

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

Start of merging of stuff into the standard library of Matita.

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