Mercurial > cpdt > repo

comparison src/Extensional.v @ 216:d1464997078d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents cbf2f74a5130
children 54e8ecb5ec88
comparison
equal deleted inserted replaced
215:f8bcd33bdd91 216:d1464997078d
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2009, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
497 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type 497 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
498 end. 498 end.
499 499
500 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) := 500 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) :=
501 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with 501 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with
502 | PVar _ => fun v => Some (v, tt) 502 | PVar _ => fun v => Some (v ::: HNil)
503 | PPair _ _ _ _ p1 p2 => fun v => 503 | PPair _ _ _ _ p1 p2 => fun v =>
504 match patDenote p1 (fst v), patDenote p2 (snd v) with 504 match patDenote p1 (fst v), patDenote p2 (snd v) with
505 | Some tup1, Some tup2 => Some (happ tup1 tup2) 505 | Some tup1, Some tup2 => Some (happ tup1 tup2)
506 | _, _ => None 506 | _, _ => None
507 end 507 end
523 523
524 Fixpoint matchesDenote (tss : list (list type)) 524 Fixpoint matchesDenote (tss : list (list type))
525 : (forall ts, member ts tss -> option (hlist typeDenote ts)) 525 : (forall ts, member ts tss -> option (hlist typeDenote ts))
526 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) 526 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
527 -> typeDenote t2 := 527 -> typeDenote t2 :=
528 match tss return (forall ts, member ts tss -> _) 528 match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
529 -> (forall ts, member ts tss -> _) 529 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
530 -> _ with 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') -> option (hlist typeDenote ts'))
534 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) => 534 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) =>
535 match envs _ (hfirst (refl_equal _)) with 535 match envs _ HFirst with
536 | None => matchesDenote tss' 536 | None => matchesDenote
537 (fun _ mem => envs _ (hnext mem)) 537 (fun _ mem => envs _ (HNext mem))
538 (fun _ mem => bodies _ (hnext mem)) 538 (fun _ mem => bodies _ (HNext mem))
539 | Some env => (bodies _ (hfirst (refl_equal _))) env 539 | Some env => (bodies _ HFirst) env
540 end 540 end
541 end. 541 end.
542 End matchesDenote. 542 End matchesDenote.
543 543
544 Implicit Arguments matchesDenote [t2 tss]. 544 Implicit Arguments matchesDenote [t2 tss].
733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : 733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := 734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result) 735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result)
736 -> result -> choice_tree var t1 result) 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, tt)) 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
742 (fun tup1 => 742 (fun tup1 =>
743 elaboratePat _ p2 743 elaboratePat p2
744 (fun tup2 => 744 (fun tup2 =>
745 succ (happ tup1 tup2)) 745 succ (happ tup1 tup2))
746 fail) 746 fail)
747 (everywhere (fun _ => fail)) 747 (everywhere (fun _ => fail))
748 748
749 | PInl _ _ _ p' => fun succ fail => 749 | PInl _ _ _ p' => fun succ fail =>
750 (elaboratePat _ p' succ fail, 750 (elaboratePat p' succ fail,
751 everywhere (fun _ => fail)) 751 everywhere (fun _ => fail))
752 | PInr _ _ _ p' => fun succ fail => 752 | PInr _ _ _ p' => fun succ fail =>
753 (everywhere (fun _ => fail), 753 (everywhere (fun _ => fail),
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 {struct 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 return ((hlist var ts -> exp var t)
762 -> hlist (exp var) ts -> exp var t) with 762 -> hlist (exp var) ts -> exp var t) with
763 | nil => fun f _ => f tt 763 | nil => fun f _ => f HNil
764 | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd tup) 764 | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
765 end. 765 end.
766 766
767 Implicit Arguments letify [var t ts]. 767 Implicit Arguments letify [var t ts].
768 768
769 Fixpoint expand var result t1 t2 769 Fixpoint expand var result t1 t2
807 | nil => fun _ _ => 807 | nil => fun _ _ =>
808 everywhere (fun _ => None) 808 everywhere (fun _ => None)
809 | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') 809 | 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) => 810 (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
811 merge (@mergeOpt _) 811 merge (@mergeOpt _)
812 (elaboratePat (ps _ (hfirst (refl_equal _))) 812 (elaboratePat (ps _ HFirst)
813 (fun ts => Some (letify 813 (fun ts => Some (letify
814 (fun ts' => es _ (hfirst (refl_equal _)) ts') 814 (fun ts' => es _ HFirst ts')
815 ts)) 815 ts))
816 None) 816 None)
817 (elaborateMatches tss' 817 (elaborateMatches
818 (fun _ mem => ps _ (hnext mem)) 818 (fun _ mem => ps _ (HNext mem))
819 (fun _ mem => es _ (hnext mem))) 819 (fun _ mem => es _ (HNext mem)))
820 end. 820 end.
821 821
822 Implicit Arguments elaborateMatches [var t1 t2 tss]. 822 Implicit Arguments elaborateMatches [var t1 t2 tss].
823 823
824 Open Scope cps_scope. 824 Open Scope cps_scope.
924 924
925 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts) 925 Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
926 result (succ : hlist (Elab.exp typeDenote) ts -> result) 926 result (succ : hlist (Elab.exp typeDenote) ts -> result)
927 (fail : result) v env, 927 (fail : result) v env,
928 patDenote p v = Some env 928 patDenote p v = Some env
929 -> exists env', grab (elaboratePat typeDenote p succ fail) v = succ env' 929 -> exists env', grab (elaboratePat p succ fail) v = succ env'
930 /\ env = hmap Elab.expDenote env'. 930 /\ env = hmap Elab.expDenote env'.
931 Hint Resolve hmap_happ. 931 Hint Resolve hmap_happ.
932 932
933 induction p; crush; fold choice_tree; 933 induction p; crush; fold choice_tree;
934 repeat (match goal with 934 repeat (match goal with
935 | [ |- context[grab (everywhere ?succ) ?v] ] => 935 | [ |- context[grab (everywhere ?succ) ?v] ] =>
936 generalize (everywhere_correct succ (#v)%elab) 936 generalize (everywhere_correct succ (#v)%elab)
937 937
938 | [ H : forall result sudc fail, _ |- context[grab (elaboratePat _ _ ?S ?F) ?V] ] => 938 | [ H : forall result succ fail, _ |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
939 generalize (H _ S F V); clear H 939 generalize (H _ S F V); clear H
940 | [ H1 : context[match ?E with Some _ => _ | None => _ end], 940 | [ H1 : context[match ?E with Some _ => _ | None => _ end],
941 H2 : forall env, ?E = Some env -> _ |- _ ] => 941 H2 : forall env, ?E = Some env -> _ |- _ ] =>
942 destruct E 942 destruct E
943 | [ H : forall env, Some ?E = Some env -> _ |- _ ] => 943 | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
944 generalize (H _ (refl_equal _)); clear H 944 generalize (H _ (refl_equal _)); clear H
945 end; crush); eauto. 945 end; crush); eauto.
946 Qed. 946 Qed.
947 947
948 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts) 948 Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
949 result (succ : hlist (Elab.exp typeDenote) ts -> result) 949 result (succ : hlist (Elab.exp typeDenote) ts -> result)
950 (fail : result) v, 950 (fail : result) v,
951 patDenote p v = None 951 patDenote p v = None
952 -> grab (elaboratePat typeDenote p succ fail) v = fail. 952 -> grab (elaboratePat p succ fail) v = fail.
953 Hint Resolve everywhere_fail. 953 Hint Resolve everywhere_fail.
954 954
955 induction p; try solve [ crush ]; 955 induction p; try solve [ crush ];
956 simpl; fold choice_tree; intuition; simpl in *; 956 simpl; fold choice_tree; intuition; simpl in *;
957 repeat match goal with 957 repeat match goal with
958 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _ 958 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
959 |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] => 959 |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
960 generalize (IH _ S F V); clear IH; intro IH; 960 generalize (IH _ S F V); clear IH; intro IH;
961 generalize (elaboratePat_correct P S F V); intros; 961 generalize (elaboratePat_correct P S F V); intros;
962 destruct (patDenote P V); try discriminate 962 destruct (patDenote P V); try discriminate
963 | [ H : forall env, Some _ = Some env -> _ |- _ ] => 963 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
964 destruct (H _ (refl_equal _)); clear H; intuition 964 destruct (H _ (refl_equal _)); clear H; intuition
971 971
972 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t) 972 Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
973 (env : hlist (Elab.exp typeDenote) ts), 973 (env : hlist (Elab.exp typeDenote) ts),
974 Elab.expDenote (letify f env) 974 Elab.expDenote (letify f env)
975 = Elab.expDenote (f (hmap Elab.expDenote env)). 975 = Elab.expDenote (f (hmap Elab.expDenote env)).
976 induction ts; crush. 976 induction ts; crush; dep_destruct env; crush.
977 Qed. 977 Qed.
978 978
979 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t), 979 Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
980 Elab.expDenote (elaborate e) = Source.expDenote e. 980 Elab.expDenote (elaborate e) = Source.expDenote e.
981 Hint Rewrite expand_grab merge_correct letify_correct : cpdt. 981 Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
984 induction e; crush; try (ext_eq; crush); 984 induction e; crush; try (ext_eq; crush);
985 match goal with 985 match goal with
986 | [ tss : list (list type) |- _ ] => 986 | [ tss : list (list type) |- _ ] =>
987 induction tss; crush; 987 induction tss; crush;
988 match goal with 988 match goal with
989 | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] => 989 | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
990 case_eq (patDenote P V); [intros env Heq; 990 case_eq (patDenote P V); [intros env Heq;
991 destruct (elaboratePat_correct P S F _ Heq); crush; 991 destruct (elaboratePat_correct P S F _ Heq); crush;
992 match goal with 992 match goal with
993 | [ H : _ |- _ ] => rewrite <- H; crush 993 | [ H : _ |- _ ] => rewrite <- H; crush
994 end 994 end