source: src/Cminor/toRTLabs.ma @ 1410

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

Remove a few old workarounds.

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