Mercurial > cpdt > repo

comparison src/Intensional.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents 0198181d1b64
children 2a34c4dc6a10
comparison
equal deleted inserted replaced
203:71ade09024ac 204:cbf2f74a5130
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *)
11 Require Import Arith Bool String List Eqdep JMeq.
12
13 Require Import Axioms Tactics DepList.
14
15 Set Implicit Arguments.
16
17 Infix "==" := JMeq (at level 70, no associativity).
18 (* end hide *)
19
20
21
22 10
23 (** %\chapter{Intensional Transformations}% *) 11 (** %\chapter{Intensional Transformations}% *)
24 12
25 (** TODO: Prose for this chapter *) 13 (** TODO: This chapter! (Old version was too complicated) *)
26
27
28 (** * Closure Conversion *)
29
30 Module Source.
31 Inductive type : Type :=
32 | TNat : type
33 | Arrow : type -> type -> type.
34
35 Notation "'Nat'" := TNat : source_scope.
36 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
37
38 Open Scope source_scope.
39 Bind Scope source_scope with type.
40 Delimit Scope source_scope with source.
41
42 Section vars.
43 Variable var : type -> Type.
44
45 Inductive exp : type -> Type :=
46 | Var : forall t,
47 var t
48 -> exp t
49
50 | Const : nat -> exp Nat
51 | Plus : exp Nat -> exp Nat -> exp Nat
52
53 | App : forall t1 t2,
54 exp (t1 --> t2)
55 -> exp t1
56 -> exp t2
57 | Abs : forall t1 t2,
58 (var t1 -> exp t2)
59 -> exp (t1 --> t2).
60 End vars.
61
62 Definition Exp t := forall var, exp var t.
63
64 Implicit Arguments Var [var t].
65 Implicit Arguments Const [var].
66 Implicit Arguments Plus [var].
67 Implicit Arguments App [var t1 t2].
68 Implicit Arguments Abs [var t1 t2].
69
70 Notation "# v" := (Var v) (at level 70) : source_scope.
71
72 Notation "^ n" := (Const n) (at level 70) : source_scope.
73 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
74
75 Infix "@" := App (left associativity, at level 77) : source_scope.
76 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
77 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
78
79 Bind Scope source_scope with exp.
80
81 Definition zero : Exp Nat := fun _ => ^0.
82 Definition one : Exp Nat := fun _ => ^1.
83 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
84 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
85 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
86 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
87 \f, \x, #f @ #x.
88 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
89
90 Fixpoint typeDenote (t : type) : Set :=
91 match t with
92 | Nat => nat
93 | t1 --> t2 => typeDenote t1 -> typeDenote t2
94 end.
95
96 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
97 match e in (exp _ t) return (typeDenote t) with
98 | Var _ v => v
99
100 | Const n => n
101 | Plus e1 e2 => expDenote e1 + expDenote e2
102
103 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
104 | Abs _ _ e' => fun x => expDenote (e' x)
105 end.
106
107 Definition ExpDenote t (e : Exp t) := expDenote (e _).
108
109 Section exp_equiv.
110 Variables var1 var2 : type -> Type.
111
112 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
113 | EqVar : forall G t (v1 : var1 t) v2,
114 In (existT _ t (v1, v2)) G
115 -> exp_equiv G (#v1) (#v2)
116
117 | EqConst : forall G n,
118 exp_equiv G (^n) (^n)
119 | EqPlus : forall G x1 y1 x2 y2,
120 exp_equiv G x1 x2
121 -> exp_equiv G y1 y2
122 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
123
124 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
125 exp_equiv G f1 f2
126 -> exp_equiv G x1 x2
127 -> exp_equiv G (f1 @ x1) (f2 @ x2)
128 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
129 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
130 -> exp_equiv G (Abs f1) (Abs f2).
131 End exp_equiv.
132
133 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
134 exp_equiv nil (E var1) (E var2).
135 End Source.
136
137 Module Closed.
138 Inductive type : Type :=
139 | TNat : type
140 | Arrow : type -> type -> type
141 | Code : type -> type -> type -> type
142 | Prod : type -> type -> type
143 | TUnit : type.
144
145 Notation "'Nat'" := TNat : cc_scope.
146 Notation "'Unit'" := TUnit : cc_scope.
147 Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
148 Infix "**" := Prod (right associativity, at level 59) : cc_scope.
149 Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
150
151 Bind Scope cc_scope with type.
152 Delimit Scope cc_scope with cc.
153
154 Open Local Scope cc_scope.
155
156 Section vars.
157 Variable var : type -> Set.
158
159 Inductive exp : type -> Type :=
160 | Var : forall t,
161 var t
162 -> exp t
163
164 | Const : nat -> exp Nat
165 | Plus : exp Nat -> exp Nat -> exp Nat
166
167 | App : forall dom ran,
168 exp (dom --> ran)
169 -> exp dom
170 -> exp ran
171
172 | Pack : forall env dom ran,
173 exp (env @@ dom ---> ran)
174 -> exp env
175 -> exp (dom --> ran)
176
177 | EUnit : exp Unit
178
179 | Pair : forall t1 t2,
180 exp t1
181 -> exp t2
182 -> exp (t1 ** t2)
183 | Fst : forall t1 t2,
184 exp (t1 ** t2)
185 -> exp t1
186 | Snd : forall t1 t2,
187 exp (t1 ** t2)
188 -> exp t2
189
190 | Let : forall t1 t2,
191 exp t1
192 -> (var t1 -> exp t2)
193 -> exp t2.
194
195 Section funcs.
196 Variable T : Type.
197
198 Inductive funcs : Type :=
199 | Main : T -> funcs
200 | Abs : forall env dom ran,
201 (var env -> var dom -> exp ran)
202 -> (var (env @@ dom ---> ran) -> funcs)
203 -> funcs.
204 End funcs.
205
206 Definition prog t := funcs (exp t).
207 End vars.
208
209 Implicit Arguments Var [var t].
210 Implicit Arguments Const [var].
211 Implicit Arguments EUnit [var].
212 Implicit Arguments Fst [var t1 t2].
213 Implicit Arguments Snd [var t1 t2].
214
215 Implicit Arguments Main [var T].
216 Implicit Arguments Abs [var T env dom ran].
217
218 Notation "# v" := (Var v) (at level 70) : cc_scope.
219
220 Notation "^ n" := (Const n) (at level 70) : cc_scope.
221 Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
222
223 Infix "@" := App (left associativity, at level 77) : cc_scope.
224 Infix "##" := Pack (no associativity, at level 71) : cc_scope.
225
226 Notation "()" := EUnit : cc_scope.
227
228 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
231
232 Notation "f <== \\ x , y , e ; fs" :=
233 (Abs (fun x y => e) (fun f => fs))
234 (right associativity, at level 80, e at next level) : cc_scope.
235 Notation "f <== \\ ! , y , e ; fs" :=
236 (Abs (fun _ y => e) (fun f => fs))
237 (right associativity, at level 80, e at next level) : cc_scope.
238 Notation "f <== \\ x , ! , e ; fs" :=
239 (Abs (fun x _ => e) (fun f => fs))
240 (right associativity, at level 80, e at next level) : cc_scope.
241 Notation "f <== \\ ! , ! , e ; fs" :=
242 (Abs (fun _ _ => e) (fun f => fs))
243 (right associativity, at level 80, e at next level) : cc_scope.
244
245 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2))
246 (right associativity, at level 80, e1 at next level) : cc_scope.
247
248 Bind Scope cc_scope with exp funcs prog.
249
250 Fixpoint typeDenote (t : type) : Set :=
251 match t with
252 | Nat => nat
253 | Unit => unit
254 | dom --> ran => typeDenote dom -> typeDenote ran
255 | t1 ** t2 => typeDenote t1 * typeDenote t2
256 | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
257 end%type.
258
259 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
260 match e in (exp _ t) return (typeDenote t) with
261 | Var _ v => v
262
263 | Const n => n
264 | Plus e1 e2 => expDenote e1 + expDenote e2
265
266 | App _ _ f x => (expDenote f) (expDenote x)
267 | Pack _ _ _ f env => (expDenote f) (expDenote env)
268
269 | EUnit => tt
270
271 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
272 | Fst _ _ e' => fst (expDenote e')
273 | Snd _ _ e' => snd (expDenote e')
274
275 | Let _ _ e1 e2 => expDenote (e2 (expDenote e1))
276 end.
277
278 Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
279 match fs with
280 | Main v => v
281 | Abs _ _ _ e fs =>
282 funcsDenote (fs (fun env arg => expDenote (e env arg)))
283 end.
284
285 Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
286 expDenote (funcsDenote p).
287
288 Definition Exp t := forall var, exp var t.
289 Definition Prog t := forall var, prog var t.
290
291 Definition ExpDenote t (E : Exp t) := expDenote (E _).
292 Definition ProgDenote t (P : Prog t) := progDenote (P _).
293 End Closed.
294
295 Import Source Closed.
296
297 Section splice.
298 Open Local Scope cc_scope.
299
300 Fixpoint spliceFuncs var T1 (fs : funcs var T1)
301 T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 :=
302 match fs with
303 | Main v => f v
304 | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f)
305 end.
306 End splice.
307
308 Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2))
309 (right associativity, at level 80, e1 at next level) : cc_scope.
310
311 Definition natvar (_ : Source.type) := nat.
312 Definition isfree := hlist (fun (_ : Source.type) => bool).
313
314 Ltac maybe_destruct E :=
315 match goal with
316 | [ x : _ |- _ ] =>
317 match E with
318 | x => idtac
319 end
320 | _ =>
321 match E with
322 | eq_nat_dec _ _ => idtac
323 end
324 end; destruct E.
325
326 Ltac my_crush :=
327 crush; repeat (match goal with
328 | [ x : (_ * _)%type |- _ ] => destruct x
329 | [ |- context[if ?B then _ else _] ] => maybe_destruct B
330 | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B
331 end; crush).
332
333 Section isfree.
334 Import Source.
335 Open Local Scope source_scope.
336
337 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT}
338 : isfree envT -> option Source.type :=
339 match envT return (isfree envT -> _) with
340 | nil => fun _ => None
341 | first :: rest => fun fvs =>
342 if eq_nat_dec n (length rest)
343 then match fvs with
344 | (true, _) => Some first
345 | (false, _) => None
346 end
347 else lookup_type rest n (snd fvs)
348 end.
349
350 Implicit Arguments lookup_type [envT].
351
352 Notation ok := (fun (envT : list Source.type) (fvs : isfree envT)
353 (n : nat) (t : Source.type)
354 => lookup_type n fvs = Some t).
355
356 Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT)
357 t (e : Source.exp natvar t) {struct e} : Prop :=
358 match e with
359 | Var t v => ok envT fvs v t
360
361 | Const _ => True
362 | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
363
364 | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
365 | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT))
366 end.
367
368 Implicit Arguments wfExp [envT t].
369
370 Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT),
371 wfExp fvs e
372 -> (forall n t, ok _ fvs n t -> ok _ fvs' n t)
373 -> wfExp fvs' e.
374 Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) =>
375 simpl in *; my_crush.
376
377 induction e; my_crush; eauto.
378 Defined.
379
380 Fixpoint isfree_none (envT : list Source.type) : isfree envT :=
381 match envT return (isfree envT) with
382 | nil => tt
383 | _ :: _ => (false, isfree_none _)
384 end.
385
386 Implicit Arguments isfree_none [envT].
387
388 Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT :=
389 match envT return (isfree envT) with
390 | nil => tt
391 | _ :: rest =>
392 if eq_nat_dec n (length rest)
393 then (true, isfree_none)
394 else (false, isfree_one _ n)
395 end.
396
397 Implicit Arguments isfree_one [envT].
398
399 Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT :=
400 match envT return (isfree envT -> isfree envT -> isfree envT) with
401 | nil => fun _ _ => tt
402 | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2))
403 end.
404
405 Implicit Arguments isfree_merge [envT].
406
407 Fixpoint fvsExp t (e : exp natvar t)
408 (envT : list Source.type) {struct e} : isfree envT :=
409 match e with
410 | Var _ n => isfree_one n
411
412 | Const _ => isfree_none
413 | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
414
415 | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
416 | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT))
417 end.
418
419 Lemma isfree_one_correct : forall t (v : natvar t) envT fvs,
420 ok envT fvs v t
421 -> ok envT (isfree_one (envT:=envT) v) v t.
422 induction envT; my_crush; eauto.
423 Defined.
424
425 Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2,
426 ok envT fvs1 v t
427 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
428 induction envT; my_crush; eauto.
429 Defined.
430
431 Hint Rewrite orb_true_r : cpdt.
432
433 Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2,
434 ok envT fvs2 v t
435 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
436 induction envT; my_crush; eauto.
437 Defined.
438
439 Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2.
440
441 Lemma fvsExp_correct : forall t (e : exp natvar t)
442 envT (fvs : isfree envT), wfExp fvs e
443 -> forall (fvs' : isfree envT),
444 (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t)
445 -> wfExp fvs' e.
446 Hint Extern 1 (_ = _) =>
447 match goal with
448 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
449 destruct (fvsExp X Y); my_crush
450 end.
451
452 induction e; my_crush; eauto.
453 Defined.
454
455 Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT),
456 lookup_type v fvs1 = Some t1
457 -> lookup_type v fvs2 = Some t2
458 -> t1 = t2.
459 induction envT; my_crush; eauto.
460 Defined.
461
462 Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2].
463
464 Hint Extern 2 (lookup_type _ _ = Some _) =>
465 match goal with
466 | [ H1 : lookup_type ?v _ = Some _,
467 H2 : lookup_type ?v _ = Some _ |- _ ] =>
468 (generalize (lookup_type_unique H1 H2); intro; subst)
469 || rewrite <- (lookup_type_unique H1 H2)
470 end.
471
472 Lemma lookup_none : forall v t envT,
473 lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t
474 -> False.
475 induction envT; my_crush.
476 Defined.
477
478 Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption.
479
480 Lemma lookup_one : forall v' v t envT,
481 lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t
482 -> v' = v.
483 induction envT; my_crush.
484 Defined.
485
486 Implicit Arguments lookup_one [v' v t envT].
487
488 Hint Extern 2 (lookup_type _ _ = Some _) =>
489 match goal with
490 | [ H : lookup_type _ _ = Some _ |- _ ] =>
491 generalize (lookup_one H); intro; subst
492 end.
493
494 Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT),
495 lookup_type v (isfree_merge fvs1 fvs2) = Some t
496 -> lookup_type v fvs1 = Some t
497 \/ lookup_type v fvs2 = Some t.
498 induction envT; my_crush.
499 Defined.
500
501 Implicit Arguments lookup_merge [v t envT fvs1 fvs2].
502
503 Lemma lookup_bound : forall v t envT (fvs : isfree envT),
504 lookup_type v fvs = Some t
505 -> v < length envT.
506 Hint Resolve lt_S.
507 induction envT; my_crush; eauto.
508 Defined.
509
510 Hint Resolve lookup_bound.
511
512 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT),
513 lookup_type (length envT) fvs = Some t
514 -> False.
515 intros; assert (length envT < length envT); eauto; crush.
516 Defined.
517
518 Hint Resolve lookup_bound_contra.
519
520 Lemma lookup_push_drop : forall v t t' envT fvs,
521 v < length envT
522 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t'
523 -> lookup_type (envT := envT) v fvs = Some t'.
524 my_crush.
525 Defined.
526
527 Lemma lookup_push_add : forall v t t' envT fvs,
528 lookup_type (envT := envT) v (snd fvs) = Some t'
529 -> lookup_type (envT := t :: envT) v fvs = Some t'.
530 my_crush; elimtype False; eauto.
531 Defined.
532
533 Hint Resolve lookup_bound lookup_push_drop lookup_push_add.
534
535 Theorem fvsExp_minimal : forall t (e : exp natvar t)
536 envT (fvs : isfree envT), wfExp fvs e
537 -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t).
538 Hint Extern 1 (_ = _) =>
539 match goal with
540 | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] =>
541 destruct (lookup_merge H); clear H; eauto
542 end.
543
544 induction e; my_crush; eauto.
545 Defined.
546
547 Fixpoint ccType (t : Source.type) : Closed.type :=
548 match t with
549 | Nat%source => Nat
550 | (dom --> ran)%source => ccType dom --> ccType ran
551 end%cc.
552
553 Open Local Scope cc_scope.
554
555 Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type :=
556 match envT return (isfree envT -> _) with
557 | nil => fun _ => Unit
558 | t :: _ => fun tup =>
559 if fst tup
560 then ccType t ** envType _ (snd tup)
561 else envType _ (snd tup)
562 end.
563
564 Implicit Arguments envType [envT].
565
566 Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
567 : isfree envT -> Set :=
568 match envT return (isfree envT -> _) with
569 | nil => fun _ => unit
570 | first :: rest => fun fvs =>
571 match fvs with
572 | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type
573 | (false, fvs') => envOf var rest fvs'
574 end
575 end.
576
577 Implicit Arguments envOf [envT].
578
579 Notation "var <| to" := (match to with
580 | None => unit
581 | Some t => var (ccType t)
582 end) (no associativity, at level 70).
583
584 Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) :
585 forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs :=
586 match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs
587 -> var <| lookup_type n fvs) with
588 | nil => fun _ _ _ => tt
589 | first :: rest => fun n fvs =>
590 match (eq_nat_dec n (length rest)) as Heq return
591 (envOf var (envT := first :: rest) fvs
592 -> var <| (if Heq
593 then match fvs with
594 | (true, _) => Some first
595 | (false, _) => None
596 end
597 else lookup_type n (snd fvs))) with
598 | left _ =>
599 match fvs return (envOf var (envT := first :: rest) fvs
600 -> var <| (match fvs with
601 | (true, _) => Some first
602 | (false, _) => None
603 end)) with
604 | (true, _) => fun env => fst env
605 | (false, _) => fun _ => tt
606 end
607 | right _ =>
608 match fvs return (envOf var (envT := first :: rest) fvs
609 -> var <| (lookup_type n (snd fvs))) with
610 | (true, fvs') => fun env => lookup var rest n fvs' (snd env)
611 | (false, fvs') => fun env => lookup var rest n fvs' env
612 end
613 end
614 end.
615
616 Theorem lok : forall var n t envT (fvs : isfree envT),
617 lookup_type n fvs = Some t
618 -> var <| lookup_type n fvs = var (ccType t).
619 crush.
620 Defined.
621 End isfree.
622
623 Implicit Arguments lookup_type [envT].
624 Implicit Arguments lookup [envT fvs].
625 Implicit Arguments wfExp [t envT].
626 Implicit Arguments envType [envT].
627 Implicit Arguments envOf [envT].
628 Implicit Arguments lok [var n t envT fvs].
629
630 Section lookup_hints.
631 Hint Resolve lookup_bound_contra.
632
633 Hint Resolve lookup_bound_contra.
634
635 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2,
636 (forall (n : nat) (t : Source.type),
637 lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t ->
638 lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t)
639 -> (forall (n : nat) (t : Source.type),
640 lookup_type n fvs1 = Some t ->
641 lookup_type n fvs2 = Some t).
642 intros until b2; intro H; intros n t;
643 generalize (H n t); my_crush; elimtype False; eauto.
644 Defined.
645
646 Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT),
647 (forall (n : nat) (t : Source.type),
648 lookup_type (envT := t' :: envT) n (true, fvs1) = Some t ->
649 lookup_type (envT := t' :: envT) n (false, fvs2) = Some t)
650 -> False.
651 intros until fvs2; intro H; generalize (H (length envT) t'); my_crush.
652 Defined.
653 End lookup_hints.
654
655 Section packing.
656 Open Local Scope cc_scope.
657
658 Hint Resolve lookup_type_push lookup_type_push_contra.
659
660 Definition packExp (var : Closed.type -> Set) (envT : list Source.type)
661 (fvs1 fvs2 : isfree envT)
662 : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
663 -> envOf var fvs2 -> exp var (envType fvs1).
664 refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
665 : forall fvs1 fvs2 : isfree envT,
666 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
667 -> envOf var fvs2 -> exp var (envType fvs1) :=
668 match envT return (forall fvs1 fvs2 : isfree envT,
669 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
670 -> envOf var fvs2
671 -> exp var (envType fvs1)) with
672 | nil => fun _ _ _ _ => ()
673 | first :: rest => fun fvs1 =>
674 match fvs1 return (forall fvs2 : isfree (first :: rest),
675 (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t
676 -> lookup_type n fvs2 = Some t)
677 -> envOf var fvs2
678 -> exp var (envType (envT := first :: rest) fvs1)) with
679 | (false, fvs1') => fun fvs2 =>
680 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t
681 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
682 -> envOf (envT := first :: rest) var fvs2
683 -> exp var (envType (envT := first :: rest) (false, fvs1'))) with
684 | (false, fvs2') => fun Hmin env =>
685 packExp var _ fvs1' fvs2' _ env
686 | (true, fvs2') => fun Hmin env =>
687 packExp var _ fvs1' fvs2' _ (snd env)
688 end
689 | (true, fvs1') => fun fvs2 =>
690 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t
691 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
692 -> envOf (envT := first :: rest) var fvs2
693 -> exp var (envType (envT := first :: rest) (true, fvs1'))) with
694 | (false, fvs2') => fun Hmin env =>
695 False_rect _ _
696 | (true, fvs2') => fun Hmin env =>
697 [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)]
698 end
699 end
700 end); eauto.
701 Defined.
702
703 Hint Resolve fvsExp_correct fvsExp_minimal.
704 Hint Resolve lookup_push_drop lookup_bound lookup_push_add.
705
706 Implicit Arguments packExp [var envT].
707
708 Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT}
709 : forall fvs : isfree envT,
710 exp var (envType fvs)
711 -> (envOf var fvs -> exp var t) -> exp var t :=
712 match envT return (forall fvs : isfree envT,
713 exp var (envType fvs)
714 -> (envOf var fvs -> exp var t) -> exp var t) with
715 | nil => fun _ _ f => f tt
716 | first :: rest => fun fvs =>
717 match fvs return (exp var (envType (envT := first :: rest) fvs)
718 -> (envOf var (envT := first :: rest) fvs -> exp var t)
719 -> exp var t) with
720 | (false, fvs') => fun p f =>
721 unpackExp rest fvs' p f
722 | (true, fvs') => fun p f =>
723 x <- #1 p;
724 unpackExp rest fvs' (#2 p)
725 (fun env => f (x, env))
726 end
727 end.
728
729 Implicit Arguments unpackExp [var t envT fvs].
730
731 Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t),
732 wfExp (envT := t' :: envT) (true, fvs) e
733 -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e.
734 Hint Extern 1 (_ = _) =>
735 match goal with
736 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
737 destruct (fvsExp X Y); my_crush
738 end.
739 eauto.
740 Defined.
741
742 Implicit Arguments wfExp_lax [t t' envT fvs e].
743
744 Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t),
745 wfExp (envT := t' :: envT) (true, fvs) e
746 -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t
747 -> lookup_type n fvs = Some t).
748 eauto.
749 Defined.
750
751 Implicit Arguments inclusion [t t' envT fvs e].
752
753 Definition env_prog var t envT (fvs : isfree envT) :=
754 funcs var (envOf var fvs -> Closed.exp var t).
755
756 Implicit Arguments env_prog [envT].
757
758 Import Source.
759 Open Local Scope cc_scope.
760
761 Definition proj1 A B (pf : A /\ B) : A :=
762 let (x, _) := pf in x.
763 Definition proj2 A B (pf : A /\ B) : B :=
764 let (_, y) := pf in y.
765
766 Fixpoint ccExp var t (e : Source.exp natvar t)
767 (envT : list Source.type) (fvs : isfree envT)
768 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs :=
769 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with
770 | Const n => fun _ => Main (fun _ => ^n)
771 | Plus e1 e2 => fun wf =>
772 n1 <-- ccExp var e1 _ fvs (proj1 wf);
773 n2 <-- ccExp var e2 _ fvs (proj2 wf);
774 Main (fun env => n1 env +^ n2 env)
775
776 | Var _ n => fun wf =>
777 Main (fun env => #(match lok wf in _ = T return T with
778 | refl_equal => lookup var n env
779 end))
780
781 | App _ _ f x => fun wf =>
782 f' <-- ccExp var f _ fvs (proj1 wf);
783 x' <-- ccExp var x _ fvs (proj2 wf);
784 Main (fun env => f' env @ x' env)
785
786 | Abs dom _ b => fun wf =>
787 b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf);
788 f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env));
789 Main (fun env => #f ##
790 packExp
791 (snd (fvsExp (b (length envT)) (dom :: envT)))
792 fvs (inclusion wf) env)
793 end.
794 End packing.
795
796 Implicit Arguments packExp [var envT].
797 Implicit Arguments unpackExp [var t envT fvs].
798
799 Implicit Arguments ccExp [var t envT].
800
801 Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
802 : funcs var T2 :=
803 match fs with
804 | Main v => Main (f v)
805 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
806 end.
807
808 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
809 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
810
811
812 (** ** Examples *)
813
814 Open Local Scope source_scope.
815
816 Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x.
817 Theorem ident_ok : wfExp (envT := nil) tt (ident _).
818 crush.
819 Defined.
820 Eval compute in CcExp' ident ident_ok.
821 Eval compute in ProgDenote (CcExp' ident ident_ok).
822
823 Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0.
824 Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _).
825 crush.
826 Defined.
827 Eval compute in CcExp' app_ident app_ident_ok.
828 Eval compute in ProgDenote (CcExp' app_ident app_ident_ok).
829
830 Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ =>
831 \x, \y, #x.
832 Theorem first_ok : wfExp (envT := nil) tt (first _).
833 crush.
834 Defined.
835 Eval compute in CcExp' first first_ok.
836 Eval compute in ProgDenote (CcExp' first first_ok).
837
838 Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0.
839 Theorem app_first_ok : wfExp (envT := nil) tt (app_first _).
840 crush.
841 Defined.
842 Eval compute in CcExp' app_first app_first_ok.
843 Eval compute in ProgDenote (CcExp' app_first app_first_ok).
844
845
846 (** ** Correctness *)
847
848 Section spliceFuncs_correct.
849 Variables T1 T2 : Type.
850 Variable f : T1 -> funcs typeDenote T2.
851
852 Theorem spliceFuncs_correct : forall fs,
853 funcsDenote (spliceFuncs fs f)
854 = funcsDenote (f (funcsDenote fs)).
855 induction fs; crush.
856 Qed.
857 End spliceFuncs_correct.
858
859
860 Notation "var <| to" := (match to return Set with
861 | None => unit
862 | Some t => var (ccType t)
863 end) (no associativity, at level 70).
864
865 Section packing_correct.
866 Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
867 Closed.typeDenote (envType fvs)
868 -> envOf Closed.typeDenote fvs :=
869 match envT return (forall (fvs : isfree envT),
870 Closed.typeDenote (envType fvs)
871 -> envOf Closed.typeDenote fvs) with
872 | nil => fun _ _ => tt
873 | first :: rest => fun fvs =>
874 match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
875 -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
876 | (false, fvs') => fun env => makeEnv rest fvs' env
877 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
878 end
879 end.
880
881 Implicit Arguments makeEnv [envT fvs].
882
883 Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
884 (e1 : Closed.exp Closed.typeDenote (envType fvs))
885 (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
886 Closed.expDenote (unpackExp e1 e2)
887 = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
888 induction envT; my_crush.
889 Qed.
890
891 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
892 (v2 = length envT -> False)
893 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
894 -> lookup_type v2 fvs = v.
895 my_crush.
896 Qed.
897
898 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
899 (v2 = length envT -> False)
900 -> lookup_type v2 (snd fvs) = v
901 -> lookup_type v2 (envT := t :: envT) fvs = v.
902 my_crush.
903 Qed.
904
905 Hint Resolve lookup_bound_contra.
906
907 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
908 lookup_type v fvs = Some t
909 -> v = length envT
910 -> False.
911 my_crush; elimtype False; eauto.
912 Qed.
913
914 Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
915 wfExp (envT := t' :: envT) (true, fvs) e
916 -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
917 -> lookup_type v fvs = Some t''.
918 Hint Resolve lookup_bound_contra_eq fvsExp_minimal
919 lookup_type_more lookup_type_less.
920 Hint Extern 2 (Some _ = Some _) => elimtype False.
921
922 eauto 6.
923 Qed.
924
925 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
926 match H1 in _ = T return T with
927 | refl_equal => x
928 end
929 = match H2 in _ = T return T with
930 | refl_equal => x
931 end.
932 intros; generalize H1; crush;
933 repeat match goal with
934 | [ |- context[match ?pf with refl_equal => _ end] ] =>
935 rewrite (UIP_refl _ _ pf)
936 end;
937 reflexivity.
938 Qed.
939
940 Hint Immediate cast_irrel.
941
942 Hint Extern 3 (_ == _) =>
943 match goal with
944 | [ |- context[False_rect _ ?H] ] =>
945 apply False_rect; exact H
946 end.
947
948 Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT)
949 Hincl env,
950 lookup_type v fvs1 = Some t
951 -> lookup Closed.typeDenote v env
952 == lookup Closed.typeDenote v
953 (makeEnv (Closed.expDenote
954 (packExp fvs1 fvs2 Hincl env))).
955 induction envT; my_crush.
956 Qed.
957 End packing_correct.
958
959 Implicit Arguments packExp_correct [v envT fvs1].
960 Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e].
961 Implicit Arguments inclusion [t t' envT fvs e].
962
963 Lemma typeDenote_same : forall t,
964 Source.typeDenote t = Closed.typeDenote (ccType t).
965 induction t; crush.
966 Qed.
967
968 Hint Resolve typeDenote_same.
969
970 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
971 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
972 | Nat => @eq nat
973 | dom --> ran => fun f1 f2 =>
974 forall x1 x2, lr dom x1 x2
975 -> lr ran (f1 x1) (f2 x2)
976 end.
977
978 Theorem ccExp_correct : forall t G
979 (e1 : Source.exp Source.typeDenote t)
980 (e2 : Source.exp natvar t),
981 exp_equiv G e1 e2
982 -> forall (envT : list Source.type) (fvs : isfree envT)
983 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
984 (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
985 In (existT _ _ (v1, v2)) G
986 -> v2 < length envT)
987 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
988 In (existT _ _ (v1, v2)) G
989 -> forall pf,
990 lr t v1 (match lok pf in _ = T return T with
991 | refl_equal => lookup Closed.typeDenote v2 env
992 end))
993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
994
995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
996 Hint Resolve packExp_correct lookup_type_inner.
997
998 induction 1; crush;
999 match goal with
1000 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] =>
1001 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV))))
1002 end; crush;
1003 match goal with
1004 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] =>
1005 solve [ generalize (Hlt _ _ _ Hin); crush ]
1006 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1007 end; simpl;
1008 match goal with
1009 | [ |- context[if ?E then _ else _] ] => destruct E
1010 end; intuition; subst;
1011 match goal with
1012 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption
1013 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] =>
1014 generalize (Hlt _ _ _ Hin); crush
1015 | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _,
1016 fvs : isfree _, env : envOf _ _ |- _ ] =>
1017 generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all;
1018 repeat match goal with
1019 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1020 end; simpl;
1021 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl;
1022 match goal with
1023 | [ |- ?X == ?Y -> _ ] =>
1024 generalize X Y
1025 end;
1026 rewrite pf; rewrite (lookup_type_inner wf pf);
1027 intros lhs rhs Heq; intros;
1028 repeat match goal with
1029 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in *
1030 end;
1031 rewrite <- Heq; assumption
1032 end.
1033 Qed.
1034
1035
1036 (** * Parametric version *)
1037
1038 Section wf.
1039 Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t),
1040 exp_equiv G e1 e2
1041 -> forall envT (fvs : isfree envT),
1042 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
1043 -> lookup_type v1 fvs = Some t)
1044 -> wfExp fvs e1.
1045 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
1046
1047 induction 1; crush; eauto;
1048 match goal with
1049 | [ H : _, envT : list Source.type |- _ ] =>
1050 apply H with (length envT); my_crush; eauto
1051 end.
1052 Qed.
1053
1054 Theorem Exp_wf : forall t (E : Source.Exp t),
1055 wfExp (envT := nil) tt (E _).
1056 Hint Resolve Exp_equiv.
1057
1058 intros; eapply Exp_wf'; crush.
1059 Qed.
1060 End wf.
1061
1062 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
1063 CcExp' E (Exp_wf E).
1064
1065 Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1),
1066 funcsDenote (map_funcs f fs) = f (funcsDenote fs).
1067 induction fs; crush.
1068 Qed.
1069
1070 Theorem CcExp_correct : forall (E : Source.Exp Nat),
1071 Source.ExpDenote E
1072 = ProgDenote (CcExp E).
1073 Hint Rewrite map_funcs_correct : cpdt.
1074
1075 unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush;
1076 apply (ccExp_correct
1077 (G := nil)
1078 (e1 := E _)
1079 (e2 := E _)
1080 (Exp_equiv _ _ _)
1081 nil
1082 tt
1083 tt); crush.
1084 Qed.