Mercurial > cpdt > repo
comparison src/Extensional.v @ 224:4b73ea13574d
Port Extensional
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 16 Nov 2009 12:30:38 -0500 |
parents | 54e8ecb5ec88 |
children | 19902d0b6622 |
comparison
equal
deleted
inserted
replaced
223:2a34c4dc6a10 | 224:4b73ea13574d |
---|---|
88 match t with | 88 match t with |
89 | Nat => nat | 89 | Nat => nat |
90 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 90 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
91 end. | 91 end. |
92 | 92 |
93 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | 93 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
94 match e in (exp _ t) return (typeDenote t) with | 94 match e with |
95 | Var _ v => v | 95 | Var _ v => v |
96 | 96 |
97 | Const n => n | 97 | Const n => n |
98 | Plus e1 e2 => expDenote e1 + expDenote e2 | 98 | Plus e1 e2 => expDenote e1 + expDenote e2 |
99 | 99 |
105 | 105 |
106 (* begin thide *) | 106 (* begin thide *) |
107 Section exp_equiv. | 107 Section exp_equiv. |
108 Variables var1 var2 : type -> Type. | 108 Variables var1 var2 : type -> Type. |
109 | 109 |
110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := | 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type |
111 -> forall t, exp var1 t -> exp var2 t -> Prop := | |
111 | EqVar : forall G t (v1 : var1 t) v2, | 112 | EqVar : forall G t (v1 : var1 t) v2, |
112 In (existT _ t (v1, v2)) G | 113 In (existT _ t (v1, v2)) G |
113 -> exp_equiv G (#v1) (#v2) | 114 -> exp_equiv G (#v1) (#v2) |
114 | 115 |
115 | EqConst : forall G n, | 116 | EqConst : forall G n, |
235 | PHalt n => n | 236 | PHalt n => n |
236 | App _ f x => f x | 237 | App _ f x => f x |
237 | Bind _ p x => progDenote (x (primopDenote p)) | 238 | Bind _ p x => progDenote (x (primopDenote p)) |
238 end | 239 end |
239 | 240 |
240 with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t := | 241 with primopDenote t (p : primop typeDenote t) : typeDenote t := |
241 match p in (primop _ t) return (typeDenote t) with | 242 match p with |
242 | Var _ v => v | 243 | Var _ v => v |
243 | 244 |
244 | Const n => n | 245 | Const n => n |
245 | Plus n1 n2 => n1 + n2 | 246 | Plus n1 n2 => n1 + n2 |
246 | 247 |
272 Variable var : CPS.type -> Type. | 273 Variable var : CPS.type -> Type. |
273 | 274 |
274 Import Source. | 275 Import Source. |
275 Open Scope cps_scope. | 276 Open Scope cps_scope. |
276 | 277 |
277 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e} | 278 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) |
278 : (var (cpsType t) -> prog var) -> prog var := | 279 : (var (cpsType t) -> prog var) -> prog var := |
279 match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with | 280 match e with |
280 | Var _ v => fun k => k v | 281 | Var _ v => fun k => k v |
281 | 282 |
282 | Const n => fun k => | 283 | Const n => fun k => |
283 x <- ^n; | 284 x <- ^n; |
284 k x | 285 k x |
327 Eval compute in ProgDenote (CpsExp app_ident). | 328 Eval compute in ProgDenote (CpsExp app_ident). |
328 Eval compute in ProgDenote (CpsExp app_ident'). | 329 Eval compute in ProgDenote (CpsExp app_ident'). |
329 | 330 |
330 (* begin thide *) | 331 (* begin thide *) |
331 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := | 332 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := |
332 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with | 333 match t with |
333 | Nat => fun n1 n2 => n1 = n2 | 334 | Nat => fun n1 n2 => n1 = n2 |
334 | t1 --> t2 => fun f1 f2 => | 335 | t1 --> t2 => fun f1 f2 => |
335 forall x1 x2, lr _ x1 x2 | 336 forall x1 x2, lr _ x1 x2 |
336 -> forall k, exists r, | 337 -> forall k, exists r, |
337 f2 (x2, k) = k r | 338 f2 (x2, k) = k r |
495 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 496 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |
496 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type | 497 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type |
497 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type | 498 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type |
498 end. | 499 end. |
499 | 500 |
500 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) := | 501 Fixpoint patDenote t ts (p : pat t ts) |
501 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with | 502 : typeDenote t -> option (hlist typeDenote ts) := |
503 match p with | |
502 | PVar _ => fun v => Some (v ::: HNil) | 504 | PVar _ => fun v => Some (v ::: HNil) |
503 | PPair _ _ _ _ p1 p2 => fun v => | 505 | PPair _ _ _ _ p1 p2 => fun v => |
504 match patDenote p1 (fst v), patDenote p2 (snd v) with | 506 match patDenote p1 (fst v), patDenote p2 (snd v) with |
505 | Some tup1, Some tup2 => Some (happ tup1 tup2) | 507 | Some tup1, Some tup2 => Some (happ tup1 tup2) |
506 | _, _ => None | 508 | _, _ => None |
523 | 525 |
524 Fixpoint matchesDenote (tss : list (list type)) | 526 Fixpoint matchesDenote (tss : list (list type)) |
525 : (forall ts, member ts tss -> option (hlist typeDenote ts)) | 527 : (forall ts, member ts tss -> option (hlist typeDenote ts)) |
526 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) | 528 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) |
527 -> typeDenote t2 := | 529 -> typeDenote t2 := |
528 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts)) | 530 match tss with |
529 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) | |
530 -> _ with | |
531 | nil => fun _ _ => | 531 | nil => fun _ _ => |
532 default | 532 default |
533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts')) | 533 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') |
534 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) => | 534 -> option (hlist typeDenote ts')) |
535 (bodies : forall ts', member ts' (ts :: tss') | |
536 -> hlist typeDenote ts' -> typeDenote t2) => | |
535 match envs _ HFirst with | 537 match envs _ HFirst with |
536 | None => matchesDenote | 538 | None => matchesDenote |
537 (fun _ mem => envs _ (HNext mem)) | 539 (fun _ mem => envs _ (HNext mem)) |
538 (fun _ mem => bodies _ (HNext mem)) | 540 (fun _ mem => bodies _ (HNext mem)) |
539 | Some env => (bodies _ HFirst) env | 541 | Some env => (bodies _ HFirst) env |
541 end. | 543 end. |
542 End matchesDenote. | 544 End matchesDenote. |
543 | 545 |
544 Implicit Arguments matchesDenote [t2 tss]. | 546 Implicit Arguments matchesDenote [t2 tss]. |
545 | 547 |
546 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | 548 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
547 match e in (exp _ t) return (typeDenote t) with | 549 match e with |
548 | Var _ v => v | 550 | Var _ v => v |
549 | 551 |
550 | EUnit => tt | 552 | EUnit => tt |
551 | 553 |
552 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | 554 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) |
643 Bind Scope elab_scope with exp. | 645 Bind Scope elab_scope with exp. |
644 Delimit Scope elab_scope with elab. | 646 Delimit Scope elab_scope with elab. |
645 | 647 |
646 Open Scope elab_scope. | 648 Open Scope elab_scope. |
647 | 649 |
648 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | 650 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t := |
649 match e in (exp _ t) return (typeDenote t) with | 651 match e with |
650 | Var _ v => v | 652 | Var _ v => v |
651 | 653 |
652 | EUnit => tt | 654 | EUnit => tt |
653 | 655 |
654 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | 656 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) |
690 choice_tree var t1 result | 692 choice_tree var t1 result |
691 * choice_tree var t2 result | 693 * choice_tree var t2 result |
692 | t => exp var t -> result | 694 | t => exp var t -> result |
693 end%type. | 695 end%type. |
694 | 696 |
695 Fixpoint merge var t result {struct t} | 697 Fixpoint merge var t result |
696 : (result -> result -> result) | 698 : (result -> result -> result) |
697 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result := | 699 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result := |
698 match t return ((result -> result -> result) | 700 match t with |
699 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result) with | |
700 | _ ** _ => fun mr ct1 ct2 => | 701 | _ ** _ => fun mr ct1 ct2 => |
701 merge _ _ | 702 merge _ _ |
702 (merge _ _ mr) | 703 (merge _ _ mr) |
703 ct1 ct2 | 704 ct1 ct2 |
704 | 705 |
707 merge var _ mr (snd ct1) (snd ct2)) | 708 merge var _ mr (snd ct1) (snd ct2)) |
708 | 709 |
709 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e) | 710 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e) |
710 end. | 711 end. |
711 | 712 |
712 Fixpoint everywhere var t result {struct t} | 713 Fixpoint everywhere var t result |
713 : (exp var t -> result) -> choice_tree var t result := | 714 : (exp var t -> result) -> choice_tree var t result := |
714 match t return ((exp var t -> result) -> choice_tree var t result) with | 715 match t with |
715 | t1 ** t2 => fun r => | 716 | t1 ** t2 => fun r => |
716 everywhere (t := t1) (fun e1 => | 717 everywhere (t := t1) (fun e1 => |
717 everywhere (t := t2) (fun e2 => | 718 everywhere (t := t2) (fun e2 => |
718 r ([e1, e2])%elab)) | 719 r ([e1, e2])%elab)) |
719 | 720 |
728 Implicit Arguments merge [var t result]. | 729 Implicit Arguments merge [var t result]. |
729 | 730 |
730 Section elaborate. | 731 Section elaborate. |
731 Local Open Scope elab_scope. | 732 Local Open Scope elab_scope. |
732 | 733 |
733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : | 734 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) : |
734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := | 735 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := |
735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result) | 736 match p with |
736 -> result -> choice_tree var t1 result) with | |
737 | PVar _ => fun succ fail => | 737 | PVar _ => fun succ fail => |
738 everywhere (fun disc => succ (disc ::: HNil)) | 738 everywhere (fun disc => succ (disc ::: HNil)) |
739 | 739 |
740 | PPair _ _ _ _ p1 p2 => fun succ fail => | 740 | PPair _ _ _ _ p1 p2 => fun succ fail => |
741 elaboratePat p1 | 741 elaboratePat p1 |
754 elaboratePat p' succ fail) | 754 elaboratePat p' succ fail) |
755 end. | 755 end. |
756 | 756 |
757 Implicit Arguments elaboratePat [var t1 ts result]. | 757 Implicit Arguments elaboratePat [var t1 ts result]. |
758 | 758 |
759 Fixpoint letify var t ts {struct ts} : (hlist var ts -> exp var t) | 759 Fixpoint letify var t ts : (hlist var ts -> exp var t) |
760 -> hlist (exp var) ts -> exp var t := | 760 -> hlist (exp var) ts -> exp var t := |
761 match ts return ((hlist var ts -> exp var t) | 761 match ts with |
762 -> hlist (exp var) ts -> exp var t) with | |
763 | nil => fun f _ => f HNil | 762 | nil => fun f _ => f HNil |
764 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup) | 763 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup) |
765 end. | 764 end. |
766 | 765 |
767 Implicit Arguments letify [var t ts]. | 766 Implicit Arguments letify [var t ts]. |
768 | 767 |
769 Fixpoint expand var result t1 t2 | 768 Fixpoint expand var result t1 t2 |
770 (out : result -> exp var t2) {struct t1} | 769 (out : result -> exp var t2) |
771 : forall ct : choice_tree var t1 result, | 770 : forall ct : choice_tree var t1 result, |
772 exp var t1 | 771 exp var t1 |
773 -> exp var t2 := | 772 -> exp var t2 := |
774 match t1 return (forall ct : choice_tree var t1 result, exp var t1 | 773 match t1 with |
775 -> exp var t2) with | |
776 | (_ ** _)%source => fun ct disc => | 774 | (_ ** _)%source => fun ct disc => |
777 expand | 775 expand |
778 (fun ct' => expand out ct' (#2 disc)%source) | 776 (fun ct' => expand out ct' (#2 disc)%source) |
779 ct | 777 ct |
780 (#1 disc) | 778 (#1 disc) |
795 end. | 793 end. |
796 | 794 |
797 Import Source. | 795 Import Source. |
798 | 796 |
799 Fixpoint elaborateMatches var t1 t2 | 797 Fixpoint elaborateMatches var t1 t2 |
800 (tss : list (list type)) {struct tss} | 798 (tss : list (list type)) |
801 : (forall ts, member ts tss -> pat t1 ts) | 799 : (forall ts, member ts tss -> pat t1 ts) |
802 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) | 800 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) |
803 -> choice_tree var t1 (option (Elab.exp var t2)) := | 801 -> choice_tree var t1 (option (Elab.exp var t2)) := |
804 match tss return (forall ts, member ts tss -> pat t1 ts) | 802 match tss with |
805 -> (forall ts, member ts tss -> _) | |
806 -> _ with | |
807 | nil => fun _ _ => | 803 | nil => fun _ _ => |
808 everywhere (fun _ => None) | 804 everywhere (fun _ => None) |
809 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') | 805 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') |
810 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) => | 806 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) => |
811 merge (@mergeOpt _) | 807 merge (@mergeOpt _) |
821 | 817 |
822 Implicit Arguments elaborateMatches [var t1 t2 tss]. | 818 Implicit Arguments elaborateMatches [var t1 t2 tss]. |
823 | 819 |
824 Open Scope cps_scope. | 820 Open Scope cps_scope. |
825 | 821 |
826 Fixpoint elaborate var t (e : Source.exp var t) {struct e} : Elab.exp var t := | 822 Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t := |
827 match e in (Source.exp _ t) return (Elab.exp var t) with | 823 match e with |
828 | Var _ v => #v | 824 | Var _ v => #v |
829 | 825 |
830 | EUnit => () | 826 | EUnit => () |
831 | 827 |
832 | App _ _ e1 e2 => elaborate e1 @ elaborate e2 | 828 | App _ _ e1 e2 => elaborate e1 @ elaborate e2 |
849 | 845 |
850 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t := | 846 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t := |
851 fun _ => elaborate (E _). | 847 fun _ => elaborate (E _). |
852 | 848 |
853 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result := | 849 Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result := |
854 match t return (choice_tree typeDenote t result -> typeDenote t -> result) with | 850 match t with |
855 | t1 ** t2 => fun ct v => | 851 | t1 ** t2 => fun ct v => |
856 grab t2 _ (grab t1 _ ct (fst v)) (snd v) | 852 grab t2 _ (grab t1 _ ct (fst v)) (snd v) |
857 | t1 ++ t2 => fun ct v => | 853 | t1 ++ t2 => fun ct v => |
858 match v with | 854 match v with |
859 | inl v' => grab t1 _ (fst ct) v' | 855 | inl v' => grab t1 _ (fst ct) v' |
873 | 869 |
874 Lemma expand_grab : forall t2 t1 result | 870 Lemma expand_grab : forall t2 t1 result |
875 (out : result -> Elab.exp typeDenote t2) | 871 (out : result -> Elab.exp typeDenote t2) |
876 (ct : choice_tree typeDenote t1 result) | 872 (ct : choice_tree typeDenote t1 result) |
877 (disc : Elab.exp typeDenote t1), | 873 (disc : Elab.exp typeDenote t1), |
878 Elab.expDenote (expand out ct disc) = Elab.expDenote (out (grab ct (Elab.expDenote disc))). | 874 Elab.expDenote (expand out ct disc) |
875 = Elab.expDenote (out (grab ct (Elab.expDenote disc))). | |
879 induction t1; my_crush. | 876 induction t1; my_crush. |
880 Qed. | 877 Qed. |
881 | 878 |
882 Lemma recreate_pair : forall t1 t2 | 879 Lemma recreate_pair : forall t1 t2 |
883 (x : Elab.exp typeDenote t1) | 880 (x : Elab.exp typeDenote t1) |
933 induction p; crush; fold choice_tree; | 930 induction p; crush; fold choice_tree; |
934 repeat (match goal with | 931 repeat (match goal with |
935 | [ |- context[grab (everywhere ?succ) ?v] ] => | 932 | [ |- context[grab (everywhere ?succ) ?v] ] => |
936 generalize (everywhere_correct succ (#v)%elab) | 933 generalize (everywhere_correct succ (#v)%elab) |
937 | 934 |
938 | [ H : forall result succ fail, _ |- context[grab (elaboratePat _ ?S ?F) ?V] ] => | 935 | [ H : forall result succ fail, _ |
936 |- context[grab (elaboratePat _ ?S ?F) ?V] ] => | |
939 generalize (H _ S F V); clear H | 937 generalize (H _ S F V); clear H |
940 | [ H1 : context[match ?E with Some _ => _ | None => _ end], | 938 | [ H1 : context[match ?E with Some _ => _ | None => _ end], |
941 H2 : forall env, ?E = Some env -> _ |- _ ] => | 939 H2 : forall env, ?E = Some env -> _ |- _ ] => |
942 destruct E | 940 destruct E |
943 | [ H : forall env, Some ?E = Some env -> _ |- _ ] => | 941 | [ H : forall env, Some ?E = Some env -> _ |- _ ] => |
961 generalize (elaboratePat_correct P S F V); intros; | 959 generalize (elaboratePat_correct P S F V); intros; |
962 destruct (patDenote P V); try discriminate | 960 destruct (patDenote P V); try discriminate |
963 | [ H : forall env, Some _ = Some env -> _ |- _ ] => | 961 | [ H : forall env, Some _ = Some env -> _ |- _ ] => |
964 destruct (H _ (refl_equal _)); clear H; intuition | 962 destruct (H _ (refl_equal _)); clear H; intuition |
965 | [ H : _ |- _ ] => rewrite H; intuition | 963 | [ H : _ |- _ ] => rewrite H; intuition |
966 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto | 964 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => |
965 destruct v; auto | |
967 end. | 966 end. |
968 Qed. | 967 Qed. |
969 | 968 |
970 Implicit Arguments letify [var t ts]. | 969 Implicit Arguments letify [var t ts]. |
971 | 970 |