source: src/Cminor/toRTLabs.ma @ 1515

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

Add type of maps on positive binary numbers, and use them for identifers.

Also:

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