Mercurial > cpdt > repo
comparison src/Extensional.v @ 178:f41d4e43fd30
PatMatch Elaborate
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 10 Nov 2008 12:19:47 -0500 |
parents | cee290647641 |
children | 8f3fc56b90d4 |
comparison
equal
deleted
inserted
replaced
177:cee290647641 | 178:f41d4e43fd30 |
---|---|
476 Notation "[ x , y ]" := (Pair x y) (at level 72) : source_scope. | 476 Notation "[ x , y ]" := (Pair x y) (at level 72) : source_scope. |
477 | 477 |
478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope. | 478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope. |
479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. | 479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. |
480 | 480 |
481 Delimit Scope source_scope with source. | |
481 Bind Scope source_scope with exp. | 482 Bind Scope source_scope with exp. |
482 | 483 |
483 Open Local Scope source_scope. | 484 Open Local Scope source_scope. |
484 | 485 |
485 Fixpoint typeDenote (t : type) : Set := | 486 Fixpoint typeDenote (t : type) : Set := |
559 Definition ExpDenote t (E : Exp t) := expDenote (E _). | 560 Definition ExpDenote t (E : Exp t) := expDenote (E _). |
560 End Source. | 561 End Source. |
561 | 562 |
562 Import Source. | 563 Import Source. |
563 | 564 |
564 Section Elab. | 565 Module Elab. |
565 Section vars. | 566 Section vars. |
566 Variable var : type -> Type. | 567 Variable var : type -> Type. |
567 | 568 |
568 Inductive exp : type -> Type := | 569 Inductive exp : type -> Type := |
569 | Var : forall t, | 570 | Var : forall t, |
661 end. | 662 end. |
662 | 663 |
663 Definition ExpDenote t (E : Exp t) := expDenote (E _). | 664 Definition ExpDenote t (E : Exp t) := expDenote (E _). |
664 End Elab. | 665 End Elab. |
665 | 666 |
667 Import Elab. | |
668 | |
669 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source | |
670 (right associativity, at level 76, e1 at next level) : source_scope. | |
671 Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab | |
672 (right associativity, at level 76, e1 at next level) : elab_scope. | |
673 | |
674 Section choice_tree. | |
675 Open Scope source_scope. | |
676 | |
677 Fixpoint choice_tree var (t : type) (result : Type) : Type := | |
678 match t with | |
679 | t1 ** t2 => | |
680 choice_tree var t1 | |
681 (choice_tree var t2 | |
682 result) | |
683 | t1 ++ t2 => | |
684 choice_tree var t1 result | |
685 * choice_tree var t2 result | |
686 | t => exp var t -> result | |
687 end%type. | |
688 | |
689 Fixpoint merge var t result {struct t} | |
690 : (result -> result -> result) | |
691 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result := | |
692 match t return ((result -> result -> result) | |
693 -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result) with | |
694 | _ ** _ => fun mr ct1 ct2 => | |
695 merge _ _ | |
696 (merge _ _ mr) | |
697 ct1 ct2 | |
698 | |
699 | _ ++ _ => fun mr ct1 ct2 => | |
700 (merge var _ mr (fst ct1) (fst ct2), | |
701 merge var _ mr (snd ct1) (snd ct2)) | |
702 | |
703 | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e) | |
704 end. | |
705 | |
706 Fixpoint everywhere var t result {struct t} | |
707 : (exp var t -> result) -> choice_tree var t result := | |
708 match t return ((exp var t -> result) -> choice_tree var t result) with | |
709 | t1 ** t2 => fun r => | |
710 everywhere (t := t1) (fun e1 => | |
711 everywhere (t := t2) (fun e2 => | |
712 r ([e1, e2])%elab)) | |
713 | |
714 | _ ++ _ => fun r => | |
715 (everywhere (fun e => r (Inl e)%elab), | |
716 everywhere (fun e => r (Inr e)%elab)) | |
717 | |
718 | _ => fun r => r | |
719 end. | |
720 End choice_tree. | |
721 | |
722 Implicit Arguments merge [var t result]. | |
723 | |
724 Section elaborate. | |
725 Open Local Scope elab_scope. | |
726 | |
727 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : | |
728 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := | |
729 match p in (pat t1 ts) return ((hlist (exp var) ts -> result) | |
730 -> result -> choice_tree var t1 result) with | |
731 | PVar _ => fun succ fail => | |
732 everywhere (fun disc => succ (disc, tt)) | |
733 | |
734 | PPair _ _ _ _ p1 p2 => fun succ fail => | |
735 elaboratePat _ p1 | |
736 (fun tup1 => | |
737 elaboratePat _ p2 | |
738 (fun tup2 => | |
739 succ (happ tup1 tup2)) | |
740 fail) | |
741 (everywhere (fun _ => fail)) | |
742 | |
743 | PInl _ _ _ p' => fun succ fail => | |
744 (elaboratePat _ p' succ fail, | |
745 everywhere (fun _ => fail)) | |
746 | PInr _ _ _ p' => fun succ fail => | |
747 (everywhere (fun _ => fail), | |
748 elaboratePat _ p' succ fail) | |
749 end. | |
750 | |
751 Implicit Arguments elaboratePat [var t1 ts result]. | |
752 | |
753 Fixpoint letify var t ts {struct ts} : (hlist var ts -> exp var t) | |
754 -> hlist (exp var) ts -> exp var t := | |
755 match ts return ((hlist var ts -> exp var t) | |
756 -> hlist (exp var) ts -> exp var t) with | |
757 | nil => fun f _ => f tt | |
758 | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd tup) | |
759 end. | |
760 | |
761 Implicit Arguments letify [var t ts]. | |
762 | |
763 Fixpoint expand var result t1 t2 | |
764 (out : result -> exp var t2) {struct t1} | |
765 : forall ct : choice_tree var t1 result, | |
766 exp var t1 | |
767 -> exp var t2 := | |
768 match t1 return (forall ct : choice_tree var t1 result, exp var t1 | |
769 -> exp var t2) with | |
770 | (_ ** _)%source => fun ct disc => | |
771 expand | |
772 (fun ct' => expand out ct' (#2 disc)%source) | |
773 ct | |
774 (#1 disc) | |
775 | |
776 | (_ ++ _)%source => fun ct disc => | |
777 Case disc | |
778 (fun x => expand out (fst ct) (#x)) | |
779 (fun y => expand out (snd ct) (#y)) | |
780 | |
781 | _ => fun ct disc => | |
782 x <- disc; out (ct (#x)) | |
783 end. | |
784 | |
785 Definition mergeOpt A (o1 o2 : option A) := | |
786 match o1 with | |
787 | None => o2 | |
788 | _ => o1 | |
789 end. | |
790 | |
791 Import Source. | |
792 | |
793 Fixpoint elaborateMatches var t1 t2 | |
794 (tss : list (list type)) {struct tss} | |
795 : (forall ts, member ts tss -> pat t1 ts) | |
796 -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) | |
797 -> choice_tree var t1 (option (Elab.exp var t2)) := | |
798 match tss return (forall ts, member ts tss -> pat t1 ts) | |
799 -> (forall ts, member ts tss -> _) | |
800 -> _ with | |
801 | nil => fun _ _ => | |
802 everywhere (fun _ => None) | |
803 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') | |
804 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) => | |
805 merge (@mergeOpt _) | |
806 (elaboratePat (ps _ (hfirst (refl_equal _))) | |
807 (fun ts => Some (letify | |
808 (fun ts' => es _ (hfirst (refl_equal _)) ts') | |
809 ts)) | |
810 None) | |
811 (elaborateMatches tss' | |
812 (fun _ mem => ps _ (hnext mem)) | |
813 (fun _ mem => es _ (hnext mem))) | |
814 end. | |
815 | |
816 Implicit Arguments elaborateMatches [var t1 t2 tss]. | |
817 | |
818 Open Scope cps_scope. | |
819 | |
820 Fixpoint elaborate var t (e : Source.exp var t) {struct e} : Elab.exp var t := | |
821 match e in (Source.exp _ t) return (Elab.exp var t) with | |
822 | Var _ v => #v | |
823 | |
824 | EUnit => () | |
825 | |
826 | App _ _ e1 e2 => elaborate e1 @ elaborate e2 | |
827 | Abs _ _ e' => \x, elaborate (e' x) | |
828 | |
829 | Pair _ _ e1 e2 => [elaborate e1, elaborate e2] | |
830 | EInl _ _ e' => Inl (elaborate e') | |
831 | EInr _ _ e' => Inr (elaborate e') | |
832 | |
833 | Case _ _ _ e' ps es def => | |
834 expand | |
835 (fun eo => match eo with | |
836 | None => elaborate def | |
837 | Some e => e | |
838 end) | |
839 (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env))) | |
840 (elaborate e') | |
841 end. | |
842 End elaborate. | |
843 | |
844 Definition Elaborate t (E : Source.Exp t) : Elab.Exp t := | |
845 fun _ => elaborate (E _). | |
846 | |
666 End PatMatch. | 847 End PatMatch. |