Mercurial > cpdt > repo

comparison src/Extensional.v @ 224:4b73ea13574d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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