source: src/Cminor/toRTLabs.ma @ 1464

Last change on this file since 1464 was 1464, checked in by campbell, 9 years ago

Use unification hints to simplify the graph monotonicity proofs.

File size: 31.3 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_included : ∀le,f,f',l.
287  fn_graph_included le f f' →
288  present ?? (pf_graph le f) l →
289  present ?? (pf_graph le f') l.
290#le #f #f' #l * #H1 #H2 @H1 @H2 qed.
291
292(* Some definitions for the add_stmt function later, which we introduce now so
293   that we can build the whole fn_graph_included machinery at once. *)
294
295(* We need to show that the graph only grows, and that Cminor labels will end
296   up in the graph. *)
297definition Cminor_labels_added ≝ λle,s,f'.
298∀l. Exists ? (λl'.l=l') (labels_of s) →
299∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.
300
301record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝
302{ stmt_graph_inc : fn_graph_included ? f f'
303; stmt_labels_added : Cminor_labels_added le s f'
304}.
305
306(* Build some machinery to solve fn_graph_included goals. *)
307
308(* A datatype saying how we intend to prove a step. *)
309inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝
310| fn_inc_eq : ∀f. fn_inc_because le f
311| fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
312    ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3
313| fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 →
314    ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3
315.
316
317(* Extract the starting function for a step. *)
318let rec fn_inc_because_left le f0  (b:fn_inc_because le f0) on b : partial_fn le ≝
319  match b with [ fn_inc_eq f ⇒ f | fn_inc_sig f _ _ _ ⇒ f | fn_inc_addinv f _ _ _ _ ⇒ f ].
320
321(* Some unification hints to pick the right step to apply.  The dummy variable
322   is there to provide goal that the lemma can't apply to, which causes an error
323   and forces the "repeat" tactical to stop.  The first hint recognises that we
324   have reached the desired starting point. *)
325
326unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True;
327  f' ≟ f,
328  b  ≟ fn_inc_eq le f
329
330  fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f'
331.
332
333unification 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);
334  b ≟ fn_inc_sig le f1 f2 H12 f3
335
336  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
337.
338
339unification 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);
340  b ≟ fn_inc_addinv le f1 f2 H12 s f3
341
342  fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3
343.
344
345(* A lemma to perform a step of the proof.  We can repeat this to do the whole
346   proof. *) 
347lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f.
348#le #f *
349[ #f @fn_graph_included_refl
350| #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23)
351| #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23)
352] qed.
353
354
355axiom BadCminorProgram : String.
356
357let 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' ≝
358match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
359[ Id t i ⇒ λEnv.
360    let r ≝ lookup_reg env i Env in
361    match register_eq r dst with
362    [ inl _ ⇒ «f, ?»
363    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
364    ]
365| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
366| Op1 t t' op e' ⇒ λEnv.
367    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
368    let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
369    let f ≝ add_expr ? env ? e' Env r f in
370      «eject … f, ?»
371| Op2 _ _ _ op e1 e2 ⇒ λEnv.
372    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
373    let 〈r2,f〉 ≝ choose_reg ? env ? e2 f (proj2 … Env) in
374    let f ≝ add_fresh_to_graph ? (St_op2 op dst r1 r2) f ? in
375    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
376    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
377      «eject … f, ?»
378| Mem _ _ q e' ⇒ λEnv.
379    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
380    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
381    let f ≝ add_expr ? env ? e' Env r f in
382      «eject … f, ?»
383| Cond _ _ _ e' e1 e2 ⇒ λEnv.
384    let resume_at ≝ pf_entry ? f in
385    let f ≝ add_expr ? env ? e2 (proj2 … Env) dst f in
386    let lfalse ≝ pf_entry ? f in
387    let f ≝ add_fresh_to_graph ? (λ_.St_skip resume_at) f ? in
388    let f ≝ add_expr ? env ? e1 (proj2 … (proj1 … Env)) dst f in
389    let 〈r,f〉 as E ≝ choose_reg ? env ? e' f (proj1 … (proj1 … Env)) in
390    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
391    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
392      «eject … f, ?»
393| Ecost _ l e' ⇒ λEnv.
394    let f ≝ add_expr ? env ? e' Env dst f in
395    let f ≝ add_fresh_to_graph ? (St_cost l) f ? in
396      «f, ?»
397] Env.
398(* For new labels, we need to step back through the definitions of f until we
399   hit the point that it was added. *)
400try (repeat @fn_includes_step @I)
401try (#l #H @H)
402[ #l #H whd % [ @H | @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ]
403| #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_step @I
404] qed.
405
406let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
407                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f' ≝
408match es return λes.All ?? es → |es|=|dsts| → ? with
409[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
410| cons e et ⇒ λEnv.
411    match dsts return λx. ?=|x| → ? with
412    [ nil ⇒ λpf.⊥
413    | cons r rt ⇒ λpf.
414        let f ≝ add_exprs ? env et ? rt ? f in
415        match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
416          let f ≝ add_expr ? env ty e ? r f in
417            «eject … f, ?» ] (proj1 ?? Env)
418    ]
419] Env pf.
420try (repeat @fn_includes_step @I)
421[ 1,2: normalize in pf; destruct
422| @Env
423| @(proj2 … Env)
424| normalize in pf; destruct @e0
425] qed.
426
427axiom UnknownLabel : String.
428axiom ReturnMismatch : String.
429
430definition stmt_inv : env → label_env → stmt → Prop ≝
431λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
432
433(* Trick to avoid multiplying the proof obligations for the non-Id cases. *)
434definition expr_is_Id : ∀t. expr t → option ident ≝
435λt,e. match e with
436[ Id _ id ⇒ Some ? id
437| _ ⇒ None ?
438].
439
440(* XXX Work around odd disambiguation errors. *)
441alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
442alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
443
444definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
445λA,P,m,l,n.
446  match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
447  [ None ⇒ λ_. Error ? m
448  | Some a ⇒ λH'. OK ? «a, ?»
449  ] (All_nth A P n l (use_sig … l)).
450@H' @refl qed.
451
452lemma lookup_label_rev : ∀lenv,l,l',p.
453  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
454#lenv #l #l' #p
455cut (∃lx. lookup ?? lenv l = Some ? lx)
456[ whd in p; cases (lookup ?? lenv l) in p ⊢ %
457  [ * #H cases (H (refl ??))
458  | #lx #_ %{lx} @refl
459  ]
460| * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
461] qed.
462
463lemma lookup_label_rev' : ∀lenv,l,p.
464  lookup ?? lenv l = Some ? (lookup_label lenv l p).
465#lenv #l #p @lookup_label_rev [ @p | @refl ]
466qed.
467
468lemma lookup_label_lpresent : ∀lenv,l,p.
469  lpresent lenv (lookup_label lenv l p).
470#le #l #p whd %{l} @lookup_label_rev'
471qed.
472
473lemma empty_Cminor_labels_added : ∀le,s,f'.
474  labels_of s = [ ] → Cminor_labels_added le s f'.
475#le #s #f' #E whd >E #l *;
476qed.
477
478lemma equal_Cminor_labels_added : ∀le,s,s',f.
479  labels_of s = labels_of s' → Cminor_labels_added le s' f →
480  Cminor_labels_added le s f.
481#le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
482qed.
483
484lemma Cminor_labels_inc : ∀le,s,f,f'.
485  fn_graph_included le f f' →
486  Cminor_labels_added le s f →
487  Cminor_labels_added le s f'.
488#le #s #f #f' #INC #ADDED
489#l #E cases (ADDED l E) #l' * #L #P
490%{l'} % [ @L | @(present_included … P) @INC ]
491qed.
492
493lemma Cminor_labels_inv : ∀le,s,s',f.
494  ∀f':Σf':partial_fn le. add_stmt_inv le s' f f'.
495  Cminor_labels_added le s f →
496  Cminor_labels_added le s f'.
497#le #s #s' #f * #f' * #H1 #H2 #H3
498#l #E cases (H3 l E) #l' * #L #P
499%{l'} % [ @L | @(present_included … P) @H1 ]
500qed.
501
502lemma Cminor_labels_sig : ∀le,s,f.
503  ∀f':Σf':partial_fn le. fn_graph_included le f f'.
504  Cminor_labels_added le s f →
505  Cminor_labels_added le s f'.
506#le #s #f * #f' #H1 #H2
507#l #E cases (H2 l E) #l' * #L #P
508%{l'} % [ @L | @(present_included … P) @H1 ]
509qed.
510
511let 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') ≝
512match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
513[ St_skip ⇒ λ_. OK ? «f, ?»
514| St_assign _ x e ⇒ λEnv.
515    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
516    OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
517| St_store _ _ q e1 e2 ⇒ λEnv.
518    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
519    let 〈addr_reg, f〉 ≝ choose_reg ? env ? e1 f (π1 (π1 Env)) in
520    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
521    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
522    OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
523| St_call return_opt_id e args ⇒ λEnv.
524    let return_opt_reg ≝
525      match return_opt_id return λo. ? → ? with
526      [ None ⇒ λ_. None ?
527      | Some id ⇒ λEnv. Some ? (lookup_reg env id ?)
528      ] Env in
529    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
530    let f ≝
531      match expr_is_Id ? e with
532      [ Some id ⇒ add_fresh_to_graph ? (St_call_id id args_regs return_opt_reg) f ?
533      | None ⇒
534        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
535        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
536        «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
537      ] in
538    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
539| St_tailcall e args ⇒ λEnv.
540    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
541    let f ≝
542      match expr_is_Id ? e with
543      [ Some id ⇒ add_fresh_to_graph ? (λ_. St_tailcall_id id args_regs) f ?
544      | None ⇒
545        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
546        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
547        «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
548      ] in
549    OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
550| St_seq s1 s2 ⇒ λEnv.
551    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
552    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
553      OK ? «eject … f1, ?»
554| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
555    let l_next ≝ pf_entry ? f in
556    do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
557    let l2 ≝ pf_entry ? f2 in
558    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_next) f2 ? in
559    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
560    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
561    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
562    OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
563| St_loop s ⇒ λEnv.
564    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
565    let l_loop ≝ pf_entry ? f in
566    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
567    OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
568| St_block s ⇒ λEnv.
569    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
570    OK ? «eject … f, ?»
571| St_exit n ⇒ λEnv.
572    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
573    OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
574| St_switch sz sg e tab n ⇒ λEnv.
575    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
576    do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
577    let f ≝ add_fresh_to_graph ? (λ_. R_skip l_default) f ? in
578    do f ← foldr ? (res (Σf':partial_fn ?. ?)) (λcs,f.
579      do f ← f;
580      let 〈i,n〉 ≝ cs in
581      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
582      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
583      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
584      let f ≝ add_fresh_to_graph ? (St_cond br l_case) f ? in
585      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
586      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
587        OK ? «eject … f, ?») (OK ? f) tab;
588    OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
589| St_return opt_e ⇒ let f0 ≝ f in
590    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
591    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
592    [ None ⇒ λEnv. OK ? «eject … f, ?»
593    | Some e ⇒
594        match pf_result ? f with
595        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
596        | Some r ⇒
597            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
598            [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
599                              OK ? «eject … f, ?» ]
600        ]
601    ]
602| St_label l s' ⇒ λEnv.
603    do f ← add_stmt env label_env s' (π2 Env) f exits;
604    let l' ≝ lookup_label label_env l ? in
605    OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
606| St_goto l ⇒ λEnv.
607    let l' ≝ lookup_label label_env l ? in
608    OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
609| St_cost l s' ⇒ λEnv.
610    do f ← add_stmt env label_env s' (π2 Env) f exits;
611    OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?»
612] Env.
613try @(π1 Env)
614try @(π2 Env)
615try @(π1 (π1 Env))
616try @(π2 (π1 Env))
617try @mk_add_stmt_inv
618try (repeat @fn_includes_step @I)
619try (@empty_Cminor_labels_added @refl)
620try (@(All_mp … (use_sig ?? exits)))
621try (#l #H @I)
622try (#l #H @H)
623[ -f @(choose_regs_length … (sym_eq … Eregs))
624| whd in Env @(π1 (π1 (π1 Env)))
625| -f @(choose_regs_length … (sym_eq … Eregs))
626| #l #H cases (Exists_append … H)
627  [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
628  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (use_sig ?? f2)) ]
629  ]
630| #l #H @(present_included … H) repeat @fn_includes_step @I
631| #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I
632| #l #H cases (Exists_append … H)
633  [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I
634  | @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I
635  ]
636| #l #H % [ @H | @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ]
637| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
638| @(use_sig ?? (pf_entry ??))
639| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
640| % [ @use_sig | @(use_sig ?? exits) ]
641| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
642| #l #H @use_sig
643| #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I
644| #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I | @H ]
645| @use_sig
646| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
647        |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
648        ]
649| #l1 #H whd %2 @lookup_label_lpresent
650| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
651] qed.
652
653definition c2ra_function (*: internal_function → internal_function*) ≝
654λf.
655let labgen0 ≝ new_universe LabelTag in
656let reggen0 ≝ new_universe RegisterTag in
657let cminor_labels ≝ labels_of (f_body f) in
658let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
659let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
660let 〈result, locals, reggen〉 ≝
661  match f_return f with
662  [ None ⇒ 〈None ?, locals0, reggen2〉
663  | Some ty ⇒
664      let 〈r,gen〉 ≝ fresh … reggen2 in
665        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
666let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
667let 〈l,labgen〉 ≝ fresh … labgen1 in
668let emptyfn ≝
669  mk_partial_fn
670    label_env
671    labgen
672    reggen
673    result
674    params
675    locals
676    (f_stacksize f)
677    (add ?? (empty_map …) l St_return)
678    ?
679    l
680    l in
681do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
682do u1 ← check_universe_ok ? (pf_labgen ? f);
683do u2 ← check_universe_ok ? (pf_reggen ? f);
684OK ? (mk_internal_function
685    (pf_labgen ? f)
686    (pf_reggen ? f)
687    (pf_result ? f)
688    (pf_params ? f)
689    (pf_locals ? f)
690    (pf_stacksize ? f)
691    (pf_graph ? f)
692    ?
693    (pf_entry ? f)
694    (pf_exit ? f)
695  ).
696[ @I
697| -emptyfn @(stmt_P_mp … (f_inv f))
698  #s * #V #L %
699  [ @(stmt_vars_mp … V)
700    #i #H cases (Exists_append … H)
701    [ #H1 @(populate_extends ?????? (sym_eq … E2))
702          @(populates_env … (sym_eq … E1)) @H1
703    | #H1 @(populates_env … (sym_eq … E2)) @H1
704    ]
705  | @(stmt_labels_mp … L)
706    #l #H @(populates_label_env … (sym_eq … El)) @H
707  ]
708| #l #s #E @(labels_P_mp … (pf_closed ? f l s E))
709  #l' * [ // | * #l #H cases f #f' * #L #P cases (P l ?)
710  [ #lx >H * #Ex >(?:lx = l') [ 2: destruct (Ex) @refl ]
711  #P' @P'
712  | cases (label_env_contents … (sym_eq ??? El) l ?)
713    [ #H @H
714    | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
715    | whd >H % #E' destruct (E')
716    ]
717  ]
718  ]
719| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
720  [ * #E1 #E2 >E2 @I
721  | whd in ⊢ (??%? → ?) #E' destruct (E')
722  ]
723| *: whd >lookup_add_hit % #E destruct
724]
725qed.
726
727definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
728λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
729
730include "Cminor/initialisation.ma".
731
732definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
733λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracBrowser for help on using the repository browser.