--- a/src/Extensional.v	Wed Dec 09 13:59:01 2009 -0500
+++ b/src/Extensional.v	Wed Dec 09 14:12:33 2009 -0500
@@ -384,631 +384,6 @@
 End STLC.
 
 
-(** * A Pattern Compiler *)
-
-Module PatMatch.
-  Module Source.
-    Inductive type : Type :=
-    | Unit : type
-    | Arrow : type -> type -> type
-    | Prod : type -> type -> type
-    | Sum : type -> type -> type.
-
-    Infix "-->" := Arrow (right associativity, at level 61).
-    Infix "++" := Sum (right associativity, at level 60).
-    Infix "**" := Prod (right associativity, at level 59).
-
-    Inductive pat : type -> list type -> Type :=
-    | PVar : forall t,
-      pat t (t :: nil)
-    | PPair : forall t1 t2 ts1 ts2,
-      pat t1 ts1
-      -> pat t2 ts2
-      -> pat (t1 ** t2) (ts1 ++ ts2)
-    | PInl : forall t1 t2 ts,
-      pat t1 ts
-      -> pat (t1 ++ t2) ts
-    | PInr : forall t1 t2 ts,
-      pat t2 ts
-      -> pat (t1 ++ t2) ts.
-
-    Implicit Arguments PVar [t].
-    Implicit Arguments PInl [t1 t2 ts].
-    Implicit Arguments PInr [t1 t2 ts].
-
-    Notation "##" := PVar (at level 70) : pat_scope.
-    Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope.
-    Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope.
-    Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope.
-
-    Bind Scope pat_scope with pat.
-    Delimit Scope pat_scope with pat.
-
-    Section vars.
-      Variable var : type -> Type.
-
-      Inductive exp : type -> Type :=
-      | Var : forall t,
-        var t
-        -> exp t
-
-      | EUnit : exp Unit
-
-      | App : forall t1 t2,
-        exp (t1 --> t2)
-        -> exp t1
-        -> exp t2
-      | Abs : forall t1 t2,
-        (var t1 -> exp t2)
-        -> exp (t1 --> t2)
-
-      | Pair : forall t1 t2,
-        exp t1
-        -> exp t2
-        -> exp (t1 ** t2)
-
-      | EInl : forall t1 t2,
-        exp t1
-        -> exp (t1 ++ t2)
-      | EInr : forall t1 t2,
-        exp t2
-        -> exp (t1 ++ t2)
-
-      | Case : forall t1 t2 (tss : list (list type)),
-        exp t1
-        -> (forall ts, member ts tss -> pat t1 ts)
-        -> (forall ts, member ts tss -> hlist var ts -> exp t2)
-        -> exp t2
-        -> exp t2.
-    End vars.
-
-    Definition Exp t := forall var, exp var t.
-
-    Implicit Arguments Var [var t].
-    Implicit Arguments EUnit [var].
-    Implicit Arguments App [var t1 t2].
-    Implicit Arguments Abs [var t1 t2].
-    Implicit Arguments Pair [var t1 t2].
-    Implicit Arguments EInl [var t1 t2].
-    Implicit Arguments EInr [var t1 t2].
-    Implicit Arguments Case [var t1 t2].
-
-    Notation "# v" := (Var v) (at level 70) : source_scope.
-
-    Notation "()" := EUnit : source_scope.
-
-    Infix "@" := App (left associativity, at level 77) : source_scope.
-    Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
-
-    Notation "[ x , y ]" := (Pair x y) : source_scope.
-
-    Notation "'Inl' e" := (EInl e) (at level 71) : source_scope.
-    Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
-
-    Delimit Scope source_scope with source.
-    Bind Scope source_scope with exp.
-
-    Local Open Scope source_scope.
-
-    Fixpoint typeDenote (t : type) : Set :=
-      match t with
-        | Unit => unit
-        | t1 --> t2 => typeDenote t1 -> typeDenote t2
-        | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
-        | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type
-      end.
-
-    Fixpoint patDenote t ts (p : pat t ts)
-      : typeDenote t -> option (hlist typeDenote ts) :=
-      match p with
-        | PVar _ => fun v => Some (v ::: HNil)
-        | PPair _ _ _ _ p1 p2 => fun v =>
-          match patDenote p1 (fst v), patDenote p2 (snd v) with
-            | Some tup1, Some tup2 => Some (happ tup1 tup2)
-            | _, _ => None
-          end
-        | PInl _ _ _ p' => fun v =>
-          match v with
-            | inl v' => patDenote p' v'
-            | _ => None
-          end
-        | PInr _ _ _ p' => fun v =>
-          match v with
-            | inr v' => patDenote p' v'
-            | _ => None
-          end
-      end.
-
-    Section matchesDenote.
-      Variables t2 : type.
-      Variable default : typeDenote t2.
-
-      Fixpoint matchesDenote (tss : list (list type))
-        : (forall ts, member ts tss -> option (hlist typeDenote ts))
-        -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-        -> typeDenote t2 :=
-        match tss return (forall ts, member ts tss -> option (hlist typeDenote ts))
-          -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2)
-          -> _ with
-          | nil => fun _ _ =>
-            default
-          | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss')
-            -> option (hlist typeDenote ts'))
-            (bodies : forall ts', member ts' (ts :: tss')
-              -> hlist typeDenote ts' -> typeDenote t2) =>
-            match envs _ HFirst with
-              | None => matchesDenote
-                (fun _ mem => envs _ (HNext mem))
-                (fun _ mem => bodies _ (HNext mem))
-              | Some env => (bodies _ HFirst) env
-            end
-        end.
-    End matchesDenote.
-
-    Implicit Arguments matchesDenote [t2 tss].
-
-    Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
-      match e with
-        | Var _ v => v
-
-        | EUnit => tt
-
-        | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
-        | Abs _ _ e' => fun x => expDenote (e' x)
-
-        | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
-
-        | EInl _ _ e' => inl _ (expDenote e')
-        | EInr _ _ e' => inr _ (expDenote e')
-
-        | Case _ _ _ e ps es def =>
-          matchesDenote (expDenote def)
-          (fun _ mem => patDenote (ps _ mem) (expDenote e))
-          (fun _ mem env => expDenote (es _ mem env))
-      end.
-
-    Definition ExpDenote t (E : Exp t) := expDenote (E _).
-  End Source.
-
-  Import Source.
-
-  Module Elab.
-    Section vars.
-      Variable var : type -> Type.
-
-      Inductive exp : type -> Type :=
-      | Var : forall t,
-        var t
-        -> exp t
-
-      | EUnit : exp Unit
-
-      | App : forall t1 t2,
-        exp (t1 --> t2)
-        -> exp t1
-        -> exp t2
-      | Abs : forall t1 t2,
-        (var t1 -> exp t2)
-        -> exp (t1 --> t2)
-
-      | Pair : forall t1 t2,
-        exp t1
-        -> exp t2
-        -> exp (t1 ** t2)
-      | Fst : forall t1 t2,
-        exp (t1 ** t2)
-        -> exp t1
-      | Snd : forall t1 t2,
-        exp (t1 ** t2)
-        -> exp t2
-
-      | EInl : forall t1 t2,
-        exp t1
-        -> exp (t1 ++ t2)
-      | EInr : forall t1 t2,
-        exp t2
-        -> exp (t1 ++ t2)
-      | Case : forall t1 t2 t,
-        exp (t1 ++ t2)
-        -> (var t1 -> exp t)
-        -> (var t2 -> exp t)
-        -> exp t.
-    End vars.
-
-    Definition Exp t := forall var, exp var t.
-
-    Implicit Arguments Var [var t].
-    Implicit Arguments EUnit [var].
-    Implicit Arguments App [var t1 t2].
-    Implicit Arguments Abs [var t1 t2].
-    Implicit Arguments Pair [var t1 t2].
-    Implicit Arguments Fst [var t1 t2].
-    Implicit Arguments Snd [var t1 t2].
-    Implicit Arguments EInl [var t1 t2].
-    Implicit Arguments EInr [var t1 t2].
-    Implicit Arguments Case [var t1 t2 t].
-
-
-    Notation "# v" := (Var v) (at level 70) : elab_scope.
-
-    Notation "()" := EUnit : elab_scope.
-
-    Infix "@" := App (left associativity, at level 77) : elab_scope.
-    Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope.
-    Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope.
-
-    Notation "[ x , y ]" := (Pair x y) : elab_scope.
-    Notation "#1 e" := (Fst e) (at level 72) : elab_scope.
-    Notation "#2 e" := (Snd e) (at level 72) : elab_scope.
-
-    Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope.
-    Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope.
-
-    Bind Scope elab_scope with exp.
-    Delimit Scope elab_scope with elab.
-
-    Open Scope elab_scope.
-
-    Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
-      match e with
-        | Var _ v => v
-
-        | EUnit => tt
-
-        | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
-        | Abs _ _ e' => fun x => expDenote (e' x)
-
-        | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
-        | Fst _ _ e' => fst (expDenote e')
-        | Snd _ _ e' => snd (expDenote e')
-
-        | EInl _ _ e' => inl _ (expDenote e')
-        | EInr _ _ e' => inr _ (expDenote e')
-        | Case _ _ _ e' e1 e2 =>
-          match expDenote e' with
-            | inl v => expDenote (e1 v)
-            | inr v => expDenote (e2 v)
-          end
-      end.
-
-    Definition ExpDenote t (E : Exp t) := expDenote (E _).
-  End Elab.
-
-  Import Elab.
-
-  Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source
-    (right associativity, at level 76, e1 at next level) : source_scope.
-  Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab
-    (right associativity, at level 76, e1 at next level) : elab_scope.
-
-  Section choice_tree.
-    Open Scope source_scope.
-
-    Fixpoint choice_tree var (t : type) (result : Type) : Type :=
-      match t with
-        | t1 ** t2 =>
-          choice_tree var t1
-          (choice_tree var t2
-            result)
-        | t1 ++ t2 =>
-          choice_tree var t1 result
-          * choice_tree var t2 result
-        | t => exp var t -> result
-      end%type.
-
-    Fixpoint merge var t result
-      : (result -> result -> result)
-      -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result :=
-      match t with
-        | _ ** _ => fun mr ct1 ct2 =>
-          merge _ _
-          (merge _ _ mr)
-          ct1 ct2
-
-        | _ ++ _ => fun mr ct1 ct2 =>
-          (merge var _ mr (fst ct1) (fst ct2),
-            merge var _ mr (snd ct1) (snd ct2))
-
-        | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e)
-      end.
-
-    Fixpoint everywhere var t result
-      : (exp var t -> result) -> choice_tree var t result :=
-      match t with
-        | t1 ** t2 => fun r =>
-          everywhere (t := t1) (fun e1 =>
-            everywhere (t := t2) (fun e2 =>
-              r ([e1, e2])%elab))
-
-        | _ ++ _ => fun r =>
-          (everywhere (fun e => r (Inl e)%elab),
-            everywhere (fun e => r (Inr e)%elab))
-
-        | _ => fun r => r
-      end.
-  End choice_tree.
-
-  Implicit Arguments merge [var t result].
-
-  Section elaborate.
-    Local Open Scope elab_scope.
-
-    Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) :
-      (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
-      match p with
-        | PVar _ => fun succ fail =>
-          everywhere (fun disc => succ (disc ::: HNil))
-
-        | PPair _ _ _ _ p1 p2 => fun succ fail =>
-          elaboratePat p1
-          (fun tup1 =>
-            elaboratePat p2
-            (fun tup2 =>
-              succ (happ tup1 tup2))
-            fail)
-          (everywhere (fun _ => fail))
-
-        | PInl _ _ _ p' => fun succ fail =>
-          (elaboratePat p' succ fail,
-            everywhere (fun _ => fail))
-        | PInr _ _ _ p' => fun succ fail =>
-          (everywhere (fun _ => fail),
-            elaboratePat p' succ fail)
-      end.
-
-    Implicit Arguments elaboratePat [var t1 ts result].
-
-    Fixpoint letify var t ts : (hlist var ts -> exp var t)
-      -> hlist (exp var) ts -> exp var t :=
-      match ts with
-        | nil => fun f _ => f HNil
-        | _ :: _ => fun f tup => letify (fun tup' => x <- hhd tup; f (x ::: tup')) (htl tup)
-      end.
-
-    Implicit Arguments letify [var t ts].
-
-    Fixpoint expand var result t1 t2
-      (out : result -> exp var t2)
-      : forall ct : choice_tree var t1 result,
-        exp var t1
-        -> exp var t2 :=
-        match t1 with
-          | (_ ** _)%source => fun ct disc =>
-            expand
-            (fun ct' => expand out ct' (#2 disc)%source)
-            ct
-            (#1 disc)
-            
-          | (_ ++ _)%source => fun ct disc =>
-            Case disc
-            (fun x => expand out (fst ct) (#x))
-            (fun y => expand out (snd ct) (#y))
-                  
-          | _ => fun ct disc =>
-            x <- disc; out (ct (#x))
-        end.
-
-    Definition mergeOpt A (o1 o2 : option A) :=
-      match o1 with
-        | None => o2
-        | _ => o1
-      end.
-
-    Import Source.
-
-    Fixpoint elaborateMatches var t1 t2
-      (tss : list (list type))
-      : (forall ts, member ts tss -> pat t1 ts)
-      -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-      -> choice_tree var t1 (option (Elab.exp var t2)) :=
-      match tss return (forall ts, member ts tss -> pat t1 ts)
-        -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2)
-        -> _ with
-        | nil => fun _ _ =>
-          everywhere (fun _ => None)
-        | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts')
-          (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) =>
-          merge (@mergeOpt _)
-          (elaboratePat (ps _ HFirst)
-            (fun ts => Some (letify
-              (fun ts' => es _ HFirst ts')
-              ts))
-            None)
-          (elaborateMatches
-            (fun _ mem => ps _ (HNext mem))
-            (fun _ mem => es _ (HNext mem)))
-      end.
-
-    Implicit Arguments elaborateMatches [var t1 t2 tss].
-
-    Open Scope cps_scope.
-
-    Fixpoint elaborate var t (e : Source.exp var t) : Elab.exp var t :=
-      match e with
-        | Var _ v => #v
-
-        | EUnit => ()
-
-        | App _ _ e1 e2 => elaborate e1 @ elaborate e2
-        | Abs _ _ e' => \x, elaborate (e' x) 
-
-        | Pair _ _ e1 e2 => [elaborate e1, elaborate e2]
-        | EInl _ _ e' => Inl (elaborate e')
-        | EInr _ _ e' => Inr (elaborate e')
-
-        | Case _ _ _ e' ps es def =>
-          expand
-          (fun eo => match eo with
-                       | None => elaborate def
-                       | Some e => e
-                     end)
-          (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env)))
-          (elaborate e')
-      end.
-  End elaborate.
-
-  Definition Elaborate t (E : Source.Exp t) : Elab.Exp t :=
-    fun _ => elaborate (E _).
-
-  Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result :=
-    match t with
-      | t1 ** t2 => fun ct v =>
-        grab t2 _ (grab t1 _ ct (fst v)) (snd v)
-      | t1 ++ t2 => fun ct v =>
-        match v with
-          | inl v' => grab t1 _ (fst ct) v'
-          | inr v' => grab t2 _ (snd ct) v'
-        end
-      | t => fun ct v => ct (#v)%elab
-    end%source%type.
-
-  Implicit Arguments grab [t result].
-
-  Ltac my_crush :=
-    crush;
-    repeat (match goal with
-              | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] =>
-                destruct E
-            end; crush).
-
-  Lemma expand_grab : forall t2 t1 result
-    (out : result -> Elab.exp typeDenote t2)
-    (ct : choice_tree typeDenote t1 result)
-    (disc : Elab.exp typeDenote t1),
-    Elab.expDenote (expand out ct disc)
-    = Elab.expDenote (out (grab ct (Elab.expDenote disc))).
-    induction t1; my_crush.
-  Qed.
-
-  Lemma recreate_pair : forall t1 t2
-    (x : Elab.exp typeDenote t1)
-    (x0 : Elab.exp typeDenote t2)
-    (v : typeDenote (t1 ** t2)),
-    expDenote x = fst v
-    -> expDenote x0 = snd v
-    -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v.
-    destruct v; crush.
-  Qed.
-
-  Lemma everywhere_correct : forall t1 result
-    (succ : Elab.exp typeDenote t1 -> result) disc,
-    exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc'
-      /\ Elab.expDenote disc' = Elab.expDenote disc.
-    Hint Resolve recreate_pair.
-
-    induction t1; my_crush; eauto; fold choice_tree;
-      repeat (fold typeDenote in *; crush;
-        match goal with
-          | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] =>
-            generalize (IH _ S); clear IH
-          | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
-            generalize (IH (#1 e)); clear IH
-          | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
-            generalize (IH (#2 e)); clear IH
-          | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] =>
-            generalize (IH (#e)); clear IH
-        end; crush); eauto.
-  Qed.
-
-  Lemma merge_correct : forall t result
-    (ct1 ct2 : choice_tree typeDenote t result)
-    (mr : result -> result -> result) v,
-    grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v).
-    induction t; crush.
-  Qed.
-
-  Lemma everywhere_fail : forall t result
-    (fail : result) v,
-    grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail.
-    induction t; crush.
-  Qed.
-
-  Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts)
-    result (succ : hlist (Elab.exp typeDenote) ts -> result)
-    (fail : result) v env,
-    patDenote p v = Some env
-    -> exists env', grab (elaboratePat p succ fail) v = succ env'
-      /\ env = hmap Elab.expDenote env'.
-    Hint Resolve hmap_happ.
-
-    induction p; crush; fold choice_tree;
-      repeat (match goal with
-                | [ |- context[grab (everywhere ?succ) ?v] ] =>
-                  generalize (everywhere_correct succ (#v)%elab)
-
-                | [ H : forall result succ fail, _
-                    |- context[grab (elaboratePat _ ?S ?F) ?V] ] =>
-                  generalize (H _ S F V); clear H
-                | [ H1 : context[match ?E with Some _ => _ | None => _ end],
-                    H2 : forall env, ?E = Some env -> _ |- _ ] =>
-                  destruct E
-                | [ H : forall env, Some ?E = Some env -> _ |- _ ] =>
-                  generalize (H _ (refl_equal _)); clear H
-              end; crush); eauto.
-  Qed.
-
-  Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts)
-    result (succ : hlist (Elab.exp typeDenote) ts -> result)
-    (fail : result) v,
-    patDenote p v = None
-    -> grab (elaboratePat p succ fail) v = fail.
-    Hint Resolve everywhere_fail.
-
-    induction p; try solve [ crush ];
-      simpl; fold choice_tree; intuition; simpl in *;
-        repeat match goal with
-                 | [ IH : forall result succ fail v, patDenote ?P v = _ -> _
-                   |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
-                   generalize (IH _ S F V); clear IH; intro IH;
-                     generalize (elaboratePat_correct P S F V); intros;
-                       destruct (patDenote P V); try discriminate
-                 | [ H : forall env, Some _ = Some env -> _ |- _ ] =>
-                   destruct (H _ (refl_equal _)); clear H; intuition
-                 | [ H : _ |- _ ] => rewrite H; intuition
-                 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] =>
-                   destruct v; auto
-               end.
-  Qed.
-
-  Implicit Arguments letify [var t ts].
-
-  Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t)
-    (env : hlist (Elab.exp typeDenote) ts),
-    Elab.expDenote (letify f env)
-    = Elab.expDenote (f (hmap Elab.expDenote env)).
-    induction ts; crush; dep_destruct env; crush.
-  Qed.
-
-  Theorem elaborate_correct : forall t (e : Source.exp typeDenote t),
-    Elab.expDenote (elaborate e) = Source.expDenote e.
-    Hint Rewrite expand_grab merge_correct letify_correct : cpdt.
-    Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt.
-
-    induction e; crush; try (ext_eq; crush);
-      match goal with
-        | [ tss : list (list type) |- _ ] =>
-          induction tss; crush;
-            match goal with
-              | [ |- context[grab (elaboratePat ?P ?S ?F) ?V] ] =>
-                case_eq (patDenote P V); [intros env Heq;
-                  destruct (elaboratePat_correct P S F _ Heq); crush;
-                    match goal with
-                      | [ H : _ |- _ ] => rewrite <- H; crush
-                    end
-                  | crush ]
-            end
-      end.
-  Qed.
-
-  Theorem Elaborate_correct : forall t (E : Source.Exp t),
-    Elab.ExpDenote (Elaborate E) = Source.ExpDenote E.
-    unfold Elab.ExpDenote, Elaborate, Source.ExpDenote;
-      intros; apply elaborate_correct.
-  Qed.
-
-End PatMatch.
-
-
 (** * Exercises *)
 
 (** %\begin{enumerate}%#<ol>#