adamc@182: (* Copyright (c) 2008, Adam Chlipala
adamc@182:  * 
adamc@182:  * This work is licensed under a
adamc@182:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@182:  * Unported License.
adamc@182:  * The license text is available at:
adamc@182:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@182:  *)
adamc@182: 
adamc@182: (* begin hide *)
adamc@184: Require Import Arith Bool String List Eqdep JMeq.
adamc@182: 
adamc@182: Require Import Axioms Tactics DepList.
adamc@182: 
adamc@182: Set Implicit Arguments.
adamc@184: 
adamc@184: Infix "==" := JMeq (at level 70, no associativity).
adamc@182: (* end hide *)
adamc@182: 
adamc@182: 
adamc@184: 
adamc@184: 
adamc@182: (** %\chapter{Intensional Transformations}% *)
adamc@182: 
adamc@182: (** TODO: Prose for this chapter *)
adamc@182: 
adamc@182: 
adamc@182: (** * Closure Conversion *)
adamc@182: 
adamc@182: Module Source.
adamc@182:   Inductive type : Type :=
adamc@182:   | TNat : type
adamc@182:   | Arrow : type -> type -> type.
adamc@182: 
adamc@182:   Notation "'Nat'" := TNat : source_scope.
adamc@182:   Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@182: 
adamc@182:   Open Scope source_scope.
adamc@182:   Bind Scope source_scope with type.
adamc@182:   Delimit Scope source_scope with source.
adamc@182: 
adamc@182:   Section vars.
adamc@182:     Variable var : type -> Type.
adamc@182: 
adamc@182:     Inductive exp : type -> Type :=
adamc@182:     | Var : forall t,
adamc@182:       var t
adamc@182:       -> exp t
adamc@182: 
adamc@182:     | Const : nat -> exp Nat
adamc@182:     | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182: 
adamc@182:     | App : forall t1 t2,
adamc@182:       exp (t1 --> t2)
adamc@182:       -> exp t1
adamc@182:       -> exp t2
adamc@182:     | Abs : forall t1 t2,
adamc@182:       (var t1 -> exp t2)
adamc@182:       -> exp (t1 --> t2).
adamc@182:   End vars.
adamc@182: 
adamc@182:   Definition Exp t := forall var, exp var t.
adamc@182: 
adamc@182:   Implicit Arguments Var [var t].
adamc@182:   Implicit Arguments Const [var].
adamc@182:   Implicit Arguments Plus [var].
adamc@182:   Implicit Arguments App [var t1 t2].
adamc@182:   Implicit Arguments Abs [var t1 t2].
adamc@182: 
adamc@182:   Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@182: 
adamc@182:   Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@182:   Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@182: 
adamc@182:   Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@182:   Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@182:   Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@182: 
adamc@182:   Bind Scope source_scope with exp.
adamc@182: 
adamc@182:   Definition zero : Exp Nat := fun _ => ^0.
adamc@182:   Definition one : Exp Nat := fun _ => ^1.
adamc@182:   Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@182:   Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@182:   Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@182:   Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@182:     \f, \x, #f @ #x.
adamc@182:   Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@182: 
adamc@182:   Fixpoint typeDenote (t : type) : Set :=
adamc@182:     match t with
adamc@182:       | Nat => nat
adamc@182:       | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@182:     end.
adamc@182: 
adamc@182:   Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182:     match e in (exp _ t) return (typeDenote t) with
adamc@182:       | Var _ v => v
adamc@182:         
adamc@182:       | Const n => n
adamc@182:       | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182:         
adamc@182:       | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@182:       | Abs _ _ e' => fun x => expDenote (e' x)
adamc@182:     end.
adamc@182: 
adamc@182:   Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@182: 
adamc@182:   Section exp_equiv.
adamc@182:     Variables var1 var2 : type -> Type.
adamc@182: 
adamc@182:     Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@182:     | EqVar : forall G t (v1 : var1 t) v2,
adamc@182:       In (existT _ t (v1, v2)) G
adamc@182:       -> exp_equiv G (#v1) (#v2)
adamc@182: 
adamc@182:     | EqConst : forall G n,
adamc@182:       exp_equiv G (^n) (^n)
adamc@182:     | EqPlus : forall G x1 y1 x2 y2,
adamc@182:       exp_equiv G x1 x2
adamc@182:       -> exp_equiv G y1 y2
adamc@182:       -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@182: 
adamc@182:     | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@182:       exp_equiv G f1 f2
adamc@182:       -> exp_equiv G x1 x2
adamc@182:       -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@182:     | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@182:       (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@182:       -> exp_equiv G (Abs f1) (Abs f2).
adamc@182:   End exp_equiv.
adamc@182: 
adamc@182:   Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@182:     exp_equiv nil (E var1) (E var2).
adamc@182: End Source.
adamc@182: 
adamc@183: Module Closed.
adamc@182:   Inductive type : Type :=
adamc@182:   | TNat : type
adamc@182:   | Arrow : type -> type -> type
adamc@182:   | Code : type -> type -> type -> type
adamc@182:   | Prod : type -> type -> type
adamc@182:   | TUnit : type.
adamc@182: 
adamc@182:   Notation "'Nat'" := TNat : cc_scope.
adamc@182:   Notation "'Unit'" := TUnit : cc_scope.
adamc@182:   Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
adamc@182:   Infix "**" := Prod (right associativity, at level 59) : cc_scope.
adamc@182:   Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
adamc@182: 
adamc@182:   Bind Scope cc_scope with type.
adamc@182:   Delimit Scope cc_scope with cc.
adamc@182: 
adamc@182:   Open Local Scope cc_scope.
adamc@182: 
adamc@182:   Section vars.
adamc@182:     Variable var : type -> Set.
adamc@182: 
adamc@182:     Inductive exp : type -> Type :=
adamc@182:     | Var : forall t,
adamc@182:       var t
adamc@182:       -> exp t
adamc@182: 
adamc@182:     | Const : nat -> exp Nat
adamc@182:     | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182: 
adamc@182:     | App : forall dom ran,
adamc@182:       exp (dom --> ran)
adamc@182:       -> exp dom
adamc@182:       -> exp ran
adamc@182: 
adamc@182:     | Pack : forall env dom ran,
adamc@182:       exp (env @@ dom ---> ran)
adamc@182:       -> exp env
adamc@182:       -> exp (dom --> ran)
adamc@182: 
adamc@182:     | EUnit : exp Unit
adamc@182: 
adamc@182:     | Pair : forall t1 t2,
adamc@182:       exp t1
adamc@182:       -> exp t2
adamc@182:       -> exp (t1 ** t2)
adamc@182:     | Fst : forall t1 t2,
adamc@182:       exp (t1 ** t2)
adamc@182:       -> exp t1
adamc@182:     | Snd : forall t1 t2,
adamc@182:       exp (t1 ** t2)
adamc@183:       -> exp t2
adamc@183: 
adamc@183:     | Let : forall t1 t2,
adamc@183:       exp t1
adamc@183:       -> (var t1 -> exp t2)
adamc@182:       -> exp t2.
adamc@182: 
adamc@182:     Section funcs.
adamc@182:       Variable T : Type.
adamc@182: 
adamc@182:       Inductive funcs : Type :=
adamc@182:       | Main : T -> funcs
adamc@182:       | Abs : forall env dom ran,
adamc@182:         (var env -> var dom -> exp ran)
adamc@182:         -> (var (env @@ dom ---> ran) -> funcs)
adamc@182:         -> funcs.
adamc@182:     End funcs.
adamc@182: 
adamc@182:     Definition prog t := funcs (exp t).
adamc@182:   End vars.
adamc@182: 
adamc@182:   Implicit Arguments Var [var t].
adamc@182:   Implicit Arguments Const [var].
adamc@182:   Implicit Arguments EUnit [var].
adamc@182:   Implicit Arguments Fst [var t1 t2].
adamc@182:   Implicit Arguments Snd [var t1 t2].
adamc@182: 
adamc@182:   Implicit Arguments Main [var T].
adamc@182:   Implicit Arguments Abs [var T env dom ran].
adamc@182: 
adamc@182:   Notation "# v" := (Var v) (at level 70) : cc_scope.
adamc@182: 
adamc@182:   Notation "^ n" := (Const n) (at level 70) : cc_scope.
adamc@182:   Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
adamc@182: 
adamc@183:   Infix "@" := App (left associativity, at level 77) : cc_scope.
adamc@182:   Infix "##" := Pack (no associativity, at level 71) : cc_scope.
adamc@182: 
adamc@182:   Notation "()" := EUnit : cc_scope.
adamc@182: 
adamc@182:   Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
adamc@182:   Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
adamc@182:   Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
adamc@182: 
adamc@183:   Notation "f <== \\ x , y , e ; fs" :=
adamc@182:     (Abs (fun x y => e) (fun f => fs))
adamc@182:     (right associativity, at level 80, e at next level) : cc_scope.
adamc@182: 
adamc@183:   Notation "x <- e1 ; e2" := (Let e1 (fun x => e2))
adamc@183:     (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183: 
adamc@182:   Bind Scope cc_scope with exp funcs prog.
adamc@182: 
adamc@182:   Fixpoint typeDenote (t : type) : Set :=
adamc@182:     match t with
adamc@182:       | Nat => nat
adamc@182:       | Unit => unit
adamc@182:       | dom --> ran => typeDenote dom -> typeDenote ran
adamc@182:       | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@182:       | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
adamc@182:     end%type.
adamc@182: 
adamc@182:   Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182:     match e in (exp _ t) return (typeDenote t) with
adamc@182:       | Var _ v => v
adamc@182: 
adamc@182:       | Const n => n
adamc@182:       | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182: 
adamc@182:       | App _ _ f x => (expDenote f) (expDenote x)
adamc@182:       | Pack _ _ _ f env => (expDenote f) (expDenote env)
adamc@182: 
adamc@182:       | EUnit => tt
adamc@182: 
adamc@182:       | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@182:       | Fst _ _ e' => fst (expDenote e')
adamc@182:       | Snd _ _ e' => snd (expDenote e')
adamc@183: 
adamc@183:       | Let _ _ e1 e2 => expDenote (e2 (expDenote e1))
adamc@182:     end.
adamc@182: 
adamc@182:   Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
adamc@182:     match fs with
adamc@182:       | Main v => v
adamc@182:       | Abs _ _ _ e fs =>
adamc@182:         funcsDenote (fs (fun env arg => expDenote (e env arg)))
adamc@182:     end.
adamc@182: 
adamc@182:   Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
adamc@182:     expDenote (funcsDenote p).
adamc@182: 
adamc@182:   Definition Exp t := forall var, exp var t.
adamc@182:   Definition Prog t := forall var, prog var t.
adamc@182: 
adamc@182:   Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@182:   Definition ProgDenote t (P : Prog t) := progDenote (P _).
adamc@182: End Closed.
adamc@182: 
adamc@183: Import Source Closed.
adamc@183: 
adamc@183: Section splice.
adamc@183:   Open Local Scope cc_scope.
adamc@183: 
adamc@183:   Fixpoint spliceFuncs var T1 (fs : funcs var T1)
adamc@183:     T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 :=
adamc@183:     match fs with
adamc@183:       | Main v => f v
adamc@183:       | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f)
adamc@183:     end.
adamc@183: End splice.
adamc@183: 
adamc@183: Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2))
adamc@183:   (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183: 
adamc@183: Definition natvar (_ : Source.type) := nat.
adamc@183: Definition isfree := hlist (fun (_ : Source.type) => bool).
adamc@183: 
adamc@183: Ltac maybe_destruct E :=
adamc@183:   match goal with
adamc@183:     | [ x : _ |- _ ] =>
adamc@183:       match E with
adamc@183:         | x => idtac
adamc@183:       end
adamc@183:     | _ =>
adamc@183:       match E with
adamc@183:         | eq_nat_dec _ _ => idtac
adamc@183:       end
adamc@183:   end; destruct E.
adamc@183: 
adamc@183: Ltac my_crush :=
adamc@183:   crush; repeat (match goal with
adamc@183:                    | [ x : (_ * _)%type |- _ ] => destruct x
adamc@183:                    | [ |- context[if ?B then _ else _] ] => maybe_destruct B
adamc@183:                    | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B
adamc@183:                  end; crush).
adamc@183: 
adamc@183: Section isfree.
adamc@183:   Import Source.
adamc@183:   Open Local Scope source_scope.
adamc@183: 
adamc@183:   Hint Extern 3 False => omega.
adamc@183: 
adamc@183:   Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT}
adamc@183:     : isfree envT -> option Source.type :=
adamc@183:     match envT return (isfree envT -> _) with
adamc@183:       | nil => fun _ => None
adamc@183:       | first :: rest => fun fvs =>
adamc@183:         if eq_nat_dec n (length rest)
adamc@183:           then match fvs with
adamc@183:                  | (true, _) => Some first
adamc@183:                  | (false, _) => None
adamc@183:                end
adamc@183:           else lookup_type rest n (snd fvs)
adamc@183:     end.
adamc@183:   
adamc@183:   Implicit Arguments lookup_type [envT].
adamc@183: 
adamc@183:   Notation ok := (fun (envT : list Source.type) (fvs : isfree envT)
adamc@183:     (n : nat) (t : Source.type)
adamc@183:     => lookup_type n fvs = Some t).
adamc@183: 
adamc@183:   Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT)
adamc@183:     t (e : Source.exp natvar t) {struct e} : Prop :=
adamc@183:     match e with
adamc@183:       | Var t v => ok envT fvs v t
adamc@183: 
adamc@183:       | Const _ => True
adamc@183:       | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183: 
adamc@183:       | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183:       | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT))
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments wfExp [envT t].
adamc@183: 
adamc@183:   Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT),
adamc@183:     wfExp fvs e
adamc@183:     -> (forall n t, ok _ fvs n t -> ok _ fvs' n t)
adamc@183:     -> wfExp fvs' e.
adamc@183:     Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) =>
adamc@183:       simpl in *; my_crush.
adamc@183: 
adamc@183:     induction e; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Fixpoint isfree_none (envT : list Source.type) : isfree envT :=
adamc@183:     match envT return (isfree envT) with
adamc@183:       | nil => tt
adamc@183:       | _ :: _ => (false, isfree_none _)
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments isfree_none [envT].
adamc@183: 
adamc@183:   Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT :=
adamc@183:     match envT return (isfree envT) with
adamc@183:       | nil => tt
adamc@183:       | _ :: rest =>
adamc@183:         if eq_nat_dec n (length rest)
adamc@183:           then (true, isfree_none)
adamc@183:           else (false, isfree_one _ n)
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments isfree_one [envT].
adamc@183: 
adamc@183:   Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT :=
adamc@183:     match envT return (isfree envT -> isfree envT -> isfree envT) with
adamc@183:       | nil => fun _ _ => tt
adamc@183:       | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2))
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments isfree_merge [envT].
adamc@183: 
adamc@183:   Fixpoint fvsExp t (e : exp natvar t)
adamc@183:     (envT : list Source.type) {struct e} : isfree envT :=
adamc@183:     match e with
adamc@183:       | Var _ n => isfree_one n
adamc@183: 
adamc@183:       | Const _ => isfree_none
adamc@183:       | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183: 
adamc@183:       | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183:       | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT))
adamc@183:     end.
adamc@183: 
adamc@183:   Lemma isfree_one_correct : forall t (v : natvar t) envT fvs,
adamc@183:     ok envT fvs v t
adamc@183:     -> ok envT (isfree_one (envT:=envT) v) v t.
adamc@183:     induction envT; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183:     ok envT fvs1 v t
adamc@183:     -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183:     induction envT; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Rewrite orb_true_r : cpdt.
adamc@183: 
adamc@183:   Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183:     ok envT fvs2 v t
adamc@183:     -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183:     induction envT; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2.
adamc@183:   
adamc@183:   Lemma fvsExp_correct : forall t (e : exp natvar t)
adamc@183:     envT (fvs : isfree envT), wfExp fvs e
adamc@183:     -> forall (fvs' : isfree envT),
adamc@183:       (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t)
adamc@183:       -> wfExp fvs' e.
adamc@183:     Hint Extern 1 (_ = _) =>
adamc@183:       match goal with
adamc@183:         | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183:           destruct (fvsExp X Y); my_crush
adamc@183:       end.
adamc@183: 
adamc@183:     induction e; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT),
adamc@183:     lookup_type v fvs1 = Some t1
adamc@183:     -> lookup_type v fvs2 = Some t2
adamc@183:     -> t1 = t2.
adamc@183:     induction envT; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2].
adamc@183: 
adamc@183:   Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183:     match goal with
adamc@183:       | [ H1 : lookup_type ?v _ = Some _,
adamc@183:         H2 : lookup_type ?v _ = Some _ |- _ ] =>
adamc@183:       (generalize (lookup_type_unique H1 H2); intro; subst)
adamc@183:       || rewrite <- (lookup_type_unique H1 H2)
adamc@183:     end.
adamc@183: 
adamc@183:   Lemma lookup_none : forall v t envT,
adamc@183:     lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t
adamc@183:     -> False.
adamc@183:     induction envT; my_crush.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption.
adamc@183: 
adamc@183:   Lemma lookup_one : forall v' v t envT,
adamc@183:     lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t
adamc@183:     -> v' = v.
adamc@183:     induction envT; my_crush.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Implicit Arguments lookup_one [v' v t envT].
adamc@183: 
adamc@183:   Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183:     match goal with
adamc@183:       | [ H : lookup_type _ _ = Some _ |- _ ] =>
adamc@183:         generalize (lookup_one H); intro; subst
adamc@183:     end.
adamc@183: 
adamc@183:   Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT),
adamc@183:     lookup_type v (isfree_merge fvs1 fvs2) = Some t
adamc@183:     -> lookup_type v fvs1 = Some t
adamc@183:     \/ lookup_type v fvs2 = Some t.
adamc@183:     induction envT; my_crush.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Implicit Arguments lookup_merge [v t envT fvs1 fvs2].
adamc@183: 
adamc@183:   Lemma lookup_bound : forall v t envT (fvs : isfree envT),
adamc@183:     lookup_type v fvs = Some t
adamc@183:     -> v < length envT.
adamc@183:     Hint Resolve lt_S.
adamc@183:     induction envT; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Resolve lookup_bound.
adamc@183: 
adamc@183:   Lemma lookup_bound_contra : forall t envT (fvs : isfree envT),
adamc@183:     lookup_type (length envT) fvs = Some t
adamc@183:     -> False.
adamc@183:     intros; assert (length envT < length envT); eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Resolve lookup_bound_contra.
adamc@183: 
adamc@183:   Hint Extern 3 (_ = _) => elimtype False; omega.
adamc@183: 
adamc@183:   Lemma lookup_push_drop : forall v t t' envT fvs,
adamc@183:     v < length envT
adamc@183:     -> lookup_type (envT := t :: envT) v (true, fvs) = Some t'
adamc@183:     -> lookup_type (envT := envT) v fvs = Some t'.
adamc@183:     my_crush.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Lemma lookup_push_add : forall v t t' envT fvs,
adamc@183:     lookup_type (envT := envT) v (snd fvs) = Some t'
adamc@183:     -> lookup_type (envT := t :: envT) v fvs = Some t'.
adamc@183:     my_crush; elimtype False; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Resolve lookup_bound lookup_push_drop lookup_push_add.
adamc@183: 
adamc@183:   Theorem fvsExp_minimal : forall t (e : exp natvar t)
adamc@183:     envT (fvs : isfree envT), wfExp fvs e
adamc@183:     -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t).
adamc@183:     Hint Extern 1 (_ = _) =>
adamc@183:       match goal with
adamc@183:         | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] =>
adamc@183:           destruct (lookup_merge H); clear H; eauto
adamc@183:       end.
adamc@183: 
adamc@183:     induction e; my_crush; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Fixpoint ccType (t : Source.type) : Closed.type :=
adamc@183:     match t with
adamc@183:       | Nat%source => Nat
adamc@183:       | (dom --> ran)%source => ccType dom --> ccType ran
adamc@183:     end%cc.
adamc@183: 
adamc@183:   Open Local Scope cc_scope.
adamc@183: 
adamc@183:   Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type :=
adamc@183:     match envT return (isfree envT -> _) with
adamc@183:       | nil => fun _ => Unit
adamc@183:       | t :: _ => fun tup =>
adamc@183:         if fst tup
adamc@183:           then ccType t ** envType _ (snd tup)
adamc@183:           else envType _ (snd tup)
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments envType [envT].
adamc@183: 
adamc@183:   Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183:     : isfree envT -> Set :=
adamc@183:     match envT return (isfree envT -> _) with
adamc@183:       | nil => fun _ => unit
adamc@183:       | first :: rest => fun fvs =>
adamc@183:         match fvs with
adamc@183:           | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type
adamc@183:           | (false, fvs') => envOf var rest fvs'
adamc@183:         end
adamc@183:     end.
adamc@183: 
adamc@183:   Implicit Arguments envOf [envT].
adamc@183: 
adamc@183:   Notation "var <| to" := (match to with
adamc@183:                              | None => unit
adamc@183:                              | Some t => var (ccType t)
adamc@183:                            end) (no associativity, at level 70).
adamc@183: 
adamc@183:   Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) :
adamc@183:     forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs :=
adamc@183:       match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs
adamc@183:         -> var <| lookup_type n fvs) with
adamc@183:         | nil => fun _ _ _ => tt
adamc@183:         | first :: rest => fun n fvs =>
adamc@183:           match (eq_nat_dec n (length rest)) as Heq return
adamc@183:             (envOf var (envT := first :: rest) fvs
adamc@183:               -> var <| (if Heq
adamc@183:                 then match fvs with
adamc@183:                        | (true, _) => Some first
adamc@183:                        | (false, _) => None
adamc@183:                      end
adamc@183:                 else lookup_type n (snd fvs))) with
adamc@183:             | left _ =>
adamc@183:               match fvs return (envOf var (envT := first :: rest) fvs
adamc@183:                 -> var <| (match fvs with
adamc@183:                              | (true, _) => Some first
adamc@183:                              | (false, _) => None
adamc@183:                            end)) with
adamc@183:                 | (true, _) => fun env => fst env
adamc@183:                 | (false, _) => fun _ => tt
adamc@183:               end
adamc@183:             | right _ =>
adamc@183:               match fvs return (envOf var (envT := first :: rest) fvs
adamc@183:                 -> var <| (lookup_type n (snd fvs))) with
adamc@183:                 | (true, fvs') => fun env => lookup var rest n fvs' (snd env)
adamc@183:                 | (false, fvs') => fun env => lookup var rest n fvs' env
adamc@183:               end
adamc@183:           end
adamc@183:       end.
adamc@183: 
adamc@183:   Theorem lok : forall var n t envT (fvs : isfree envT),
adamc@183:     lookup_type n fvs = Some t
adamc@183:     -> var <| lookup_type n fvs = var (ccType t).
adamc@183:     crush.
adamc@183:   Defined.
adamc@183: End isfree.
adamc@183: 
adamc@183: Implicit Arguments lookup_type [envT].
adamc@183: Implicit Arguments lookup [envT fvs].
adamc@183: Implicit Arguments wfExp [t envT].
adamc@183: Implicit Arguments envType [envT].
adamc@183: Implicit Arguments envOf [envT].
adamc@183: Implicit Arguments lok [var n t envT fvs].
adamc@183: 
adamc@183: Section lookup_hints.
adamc@183:   Hint Resolve lookup_bound_contra.
adamc@183: 
adamc@183:   (*Ltac my_chooser T k :=
adamc@183:     match T with
adamc@183:       | ptype =>
adamc@183:         match goal with
adamc@183:           | [ H : lookup _ _ = Some ?t |- _ ] => k t
adamc@183:         end
adamc@183:       | _ => default_chooser T k
adamc@183:     end.
adamc@183: 
adamc@183:   Ltac my_matching := matching equation my_chooser.*)
adamc@183: 
adamc@183:   Hint Resolve lookup_bound_contra.
adamc@183: 
adamc@183:   Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2,
adamc@183:     (forall (n : nat) (t : Source.type),
adamc@183:       lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t ->
adamc@183:       lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t)
adamc@183:     -> (forall (n : nat) (t : Source.type),
adamc@183:       lookup_type n fvs1 = Some t ->
adamc@183:       lookup_type n fvs2 = Some t).
adamc@183:     intros until b2; intro H; intros n t;
adamc@183:       generalize (H n t); my_crush; elimtype False; eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT),
adamc@183:     (forall (n : nat) (t : Source.type),
adamc@183:       lookup_type (envT := t' :: envT) n (true, fvs1) = Some t ->
adamc@183:       lookup_type (envT := t' :: envT) n (false, fvs2) = Some t)
adamc@183:     -> False.
adamc@183:     intros until fvs2; intro H; generalize (H (length envT) t'); my_crush.
adamc@183:   Defined.
adamc@183: End lookup_hints.
adamc@183: 
adamc@183: Section packing.
adamc@183:   Open Local Scope cc_scope.
adamc@183: 
adamc@183:   Hint Resolve lookup_type_push lookup_type_push_contra.
adamc@183: 
adamc@183:   Definition packExp (var : Closed.type -> Set) (envT : list Source.type)
adamc@183:     (fvs1 fvs2 : isfree envT)
adamc@183:     : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183:     -> envOf var fvs2 -> exp var (envType fvs1).
adamc@183:     refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183:       : forall fvs1 fvs2 : isfree envT,
adamc@183:         (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183:         -> envOf var fvs2 -> exp var (envType fvs1) :=
adamc@183:         match envT return (forall fvs1 fvs2 : isfree envT,
adamc@183:           (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183:           -> envOf var fvs2
adamc@183:           -> exp var (envType fvs1)) with
adamc@183:           | nil => fun _ _ _ _ => ()
adamc@183:           | first :: rest => fun fvs1 =>
adamc@183:             match fvs1 return (forall fvs2 : isfree (first :: rest),
adamc@183:               (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t
adamc@183:                 -> lookup_type n fvs2 = Some t)
adamc@183:               -> envOf var fvs2
adamc@183:               -> exp var (envType (envT := first :: rest) fvs1)) with
adamc@183:               | (false, fvs1') => fun fvs2 =>
adamc@183:                 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t
adamc@183:                   -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183:                 -> envOf (envT := first :: rest) var fvs2
adamc@183:                 -> exp var (envType (envT := first :: rest) (false, fvs1'))) with
adamc@183:                   | (false, fvs2') => fun Hmin env =>
adamc@183:                     packExp var _  fvs1' fvs2' _ env
adamc@183:                   | (true, fvs2') => fun Hmin env =>
adamc@183:                     packExp var _  fvs1' fvs2' _ (snd env)
adamc@183:                 end
adamc@183:               | (true, fvs1') => fun fvs2 =>
adamc@183:                 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t
adamc@183:                   -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183:                 -> envOf (envT := first :: rest) var fvs2
adamc@183:                 -> exp var (envType (envT := first :: rest) (true, fvs1'))) with
adamc@183:                   | (false, fvs2') => fun Hmin env =>
adamc@183:                     False_rect _ _
adamc@183:                   | (true, fvs2') => fun Hmin env =>
adamc@183:                     [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)]
adamc@183:                 end
adamc@183:             end
adamc@183:         end); eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Hint Resolve fvsExp_correct fvsExp_minimal.
adamc@183:   Hint Resolve lookup_push_drop lookup_bound lookup_push_add.
adamc@183: 
adamc@183:   Implicit Arguments packExp [var envT].
adamc@183: 
adamc@183:   Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT}
adamc@183:     : forall fvs : isfree envT,
adamc@183:       exp var (envType fvs)
adamc@183:       -> (envOf var fvs -> exp var t) -> exp var t :=
adamc@183:       match envT return (forall fvs : isfree envT,
adamc@183:         exp var (envType fvs)
adamc@183:         -> (envOf var fvs -> exp var t) -> exp var t) with
adamc@183:         | nil => fun _ _ f => f tt
adamc@183:         | first :: rest => fun fvs =>
adamc@183:           match fvs return (exp var (envType (envT := first :: rest) fvs)
adamc@183:             -> (envOf var (envT := first :: rest) fvs -> exp var t)
adamc@183:             -> exp var t) with
adamc@183:             | (false, fvs') => fun p f =>
adamc@183:               unpackExp rest fvs' p f
adamc@183:             | (true, fvs') => fun p f =>
adamc@183:               x <- #1 p;
adamc@183:               unpackExp rest fvs' (#2 p)
adamc@183:               (fun env => f (x, env))
adamc@183:           end
adamc@183:       end.
adamc@183:   
adamc@183:   Implicit Arguments unpackExp [var t envT fvs].
adamc@183: 
adamc@183:   Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t),
adamc@183:     wfExp (envT := t' :: envT) (true, fvs) e
adamc@183:     -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e.
adamc@183:     Hint Extern 1 (_ = _) =>
adamc@183:       match goal with
adamc@183:         | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183:           destruct (fvsExp X Y); my_crush
adamc@183:       end.
adamc@183:     eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Implicit Arguments wfExp_lax [t t' envT fvs e].
adamc@183: 
adamc@183:   Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t),
adamc@183:     wfExp (envT := t' :: envT) (true, fvs) e
adamc@183:     -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t
adamc@183:       -> lookup_type n fvs = Some t).
adamc@183:     eauto.
adamc@183:   Defined.
adamc@183: 
adamc@183:   Implicit Arguments inclusion [t t' envT fvs e].
adamc@183: 
adamc@183:   Definition env_prog var t envT (fvs : isfree envT) :=
adamc@183:     funcs var (envOf var fvs -> Closed.exp var t).
adamc@183: 
adamc@183:   Implicit Arguments env_prog [envT].
adamc@183: 
adamc@183:   Axiom cheat : forall T, T.
adamc@183: 
adamc@183:   Import Source.
adamc@183:   Open Local Scope cc_scope.
adamc@183: 
adamc@183:   Fixpoint ccExp var t (e : Source.exp natvar t)
adamc@183:     (envT : list Source.type) (fvs : isfree envT)
adamc@183:     {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs :=
adamc@183:     match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with
adamc@183:       | Const n => fun _ => Main (fun _ => ^n)
adamc@183:       | Plus e1 e2 => fun wf =>
adamc@183:         n1 <-- ccExp var e1 _ fvs (proj1 wf);
adamc@183:         n2 <-- ccExp var e2 _ fvs (proj2 wf);
adamc@183:         Main (fun env => n1 env +^ n2 env)
adamc@183: 
adamc@183:       | Var _ n => fun wf =>
adamc@183:         Main (fun env => #(match lok wf in _ = T return T with
adamc@183:                              | refl_equal => lookup var n env
adamc@183:                            end))
adamc@183: 
adamc@183:       | App _ _ f x => fun wf =>
adamc@183:         f' <-- ccExp var f _ fvs (proj1 wf);
adamc@183:         x' <-- ccExp var x _ fvs (proj2 wf);
adamc@183:         Main (fun env => f' env @ x' env)
adamc@183: 
adamc@183:       | Abs dom _ b => fun wf =>
adamc@183:         b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf);
adamc@183:         f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env));
adamc@183:         Main (fun env => #f ##
adamc@183:           packExp
adamc@183:           (snd (fvsExp (b (length envT)) (dom :: envT)))
adamc@183:           fvs (inclusion wf) env)
adamc@183:     end.
adamc@183: End packing.
adamc@183: 
adamc@183: Implicit Arguments packExp [var envT].
adamc@183: Implicit Arguments unpackExp [var t envT fvs].
adamc@183: 
adamc@183: Implicit Arguments ccExp [var t envT].
adamc@183: 
adamc@184: Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
adamc@184:   : funcs var T2 :=
adamc@183:   match fs with
adamc@184:     | Main v => Main (f v)
adamc@184:     | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
adamc@183:   end.
adamc@183: 
adamc@186: Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
adamc@184:   fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
adamc@183: 
adamc@183: 
adamc@183: (** * Correctness *)
adamc@183: 
adamc@184: Section spliceFuncs_correct.
adamc@184:   Variables T1 T2 : Type.
adamc@184:   Variable f : T1 -> funcs typeDenote T2.
adamc@183: 
adamc@184:   Theorem spliceFuncs_correct : forall fs,
adamc@184:     funcsDenote (spliceFuncs fs f)
adamc@184:     = funcsDenote (f (funcsDenote fs)).
adamc@184:     induction fs; crush.
adamc@183:   Qed.
adamc@183: End spliceFuncs_correct.
adamc@183: 
adamc@183: 
adamc@185: Notation "var <| to" := (match to return Set with
adamc@183:                            | None => unit
adamc@184:                            | Some t => var (ccType t)
adamc@183:                          end) (no associativity, at level 70).
adamc@183: 
adamc@183: Section packing_correct.
adamc@184:   Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
adamc@184:     Closed.typeDenote (envType fvs)
adamc@184:     -> envOf Closed.typeDenote fvs :=
adamc@183:     match envT return (forall (fvs : isfree envT),
adamc@184:       Closed.typeDenote (envType fvs)
adamc@184:       -> envOf Closed.typeDenote fvs) with
adamc@183:       | nil => fun _ _ => tt
adamc@183:       | first :: rest => fun fvs =>
adamc@184:         match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
adamc@184:           -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
adamc@183:           | (false, fvs') => fun env => makeEnv rest fvs' env
adamc@183:           | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
adamc@183:         end
adamc@183:     end.
adamc@183: 
adamc@184:   Implicit Arguments makeEnv [envT fvs].
adamc@184: 
adamc@184:   Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
adamc@184:     (e1 : Closed.exp Closed.typeDenote (envType fvs))
adamc@184:     (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
adamc@184:     Closed.expDenote (unpackExp e1 e2)
adamc@184:     = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
adamc@184:     induction envT; my_crush.
adamc@183:   Qed.
adamc@183: 
adamc@183:   Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
adamc@183:     (v2 = length envT -> False)
adamc@183:     -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
adamc@183:     -> lookup_type v2 fvs = v.
adamc@184:     my_crush.
adamc@183:   Qed.
adamc@183: 
adamc@183:   Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
adamc@183:     (v2 = length envT -> False)
adamc@183:     -> lookup_type v2 (snd fvs) = v
adamc@183:     -> lookup_type v2 (envT := t :: envT) fvs = v.
adamc@184:     my_crush.
adamc@183:   Qed.
adamc@183: 
adamc@184:   Hint Resolve lookup_bound_contra.
adamc@184: 
adamc@183:   Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
adamc@183:     lookup_type v fvs = Some t
adamc@183:     -> v = length envT
adamc@183:     -> False.
adamc@184:     my_crush; elimtype False; eauto.
adamc@184:   Qed.
adamc@183: 
adamc@184:   Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
adamc@184:     wfExp (envT := t' :: envT) (true, fvs) e
adamc@184:     -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
adamc@184:     -> lookup_type v fvs = Some t''.
adamc@184:     Hint Resolve lookup_bound_contra_eq fvsExp_minimal
adamc@183:       lookup_type_more lookup_type_less.
adamc@184:     Hint Extern 2 (Some _ = Some _) => elimtype False.
adamc@183: 
adamc@183:     eauto 6.
adamc@183:   Qed.
adamc@183: 
adamc@183:   Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
adamc@184:     match H1 in _ = T return T with
adamc@184:       | refl_equal => x
adamc@184:     end
adamc@184:     = match H2 in _ = T return T with
adamc@184:         | refl_equal => x
adamc@184:       end.
adamc@184:     intros; generalize H1; crush;
adamc@184:       repeat match goal with
adamc@184:                | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@184:                  rewrite (UIP_refl _ _ pf)
adamc@184:              end;
adamc@184:       reflexivity.
adamc@183:   Qed.
adamc@183: 
adamc@183:   Hint Immediate cast_irrel.
adamc@183: 
adamc@184:   Hint Extern 3 (_ == _) =>
adamc@183:     match goal with
adamc@183:       | [ |- context[False_rect _ ?H] ] =>
adamc@183:         apply False_rect; exact H
adamc@183:     end.
adamc@183: 
adamc@184:   Theorem packExp_correct : forall v envT (fvs1 fvs2 : isfree envT)
adamc@183:     Hincl env,
adamc@184:     lookup_type v fvs1 <> None
adamc@184:     -> lookup Closed.typeDenote v env
adamc@184:     == lookup Closed.typeDenote v
adamc@184:     (makeEnv (Closed.expDenote
adamc@184:       (packExp fvs1 fvs2 Hincl env))).
adamc@184:     induction envT; my_crush.
adamc@183:   Qed.
adamc@183: End packing_correct.
adamc@183: 
adamc@185: About packExp_correct.
adamc@185: Implicit Arguments packExp_correct [v envT fvs1].
adamc@185: 
adamc@185: Implicit Arguments lookup_type_more [v2 envT fvs t b v].
adamc@184: 
adamc@184: Lemma typeDenote_same : forall t,
adamc@184:   Source.typeDenote t = Closed.typeDenote (ccType t).
adamc@184:   induction t; crush.
adamc@184: Qed.
adamc@184: 
adamc@184: Hint Resolve typeDenote_same.
adamc@184: 
adamc@183: Lemma look : forall envT n (fvs : isfree envT) t,
adamc@183:   lookup_type n fvs = Some t
adamc@184:   -> Closed.typeDenote <| lookup_type n fvs = Source.typeDenote t.
adamc@184:   crush.
adamc@183: Qed.
adamc@183: 
adamc@183: Implicit Arguments look [envT n fvs t].
adamc@183: 
adamc@185: Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
adamc@185:   match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
adamc@185:     | Nat => @eq nat
adamc@185:     | dom --> ran => fun f1 f2 =>
adamc@185:       forall x1 x2, lr dom x1 x2
adamc@185:         -> lr ran (f1 x1) (f2 x2)
adamc@185:   end.
adamc@184: 
adamc@186: Theorem ccExp_correct : forall t G
adamc@184:   (e1 : Source.exp Source.typeDenote t)
adamc@184:   (e2 : Source.exp natvar t),
adamc@184:   exp_equiv G e1 e2
adamc@184:   -> forall (envT : list Source.type) (fvs : isfree envT)
adamc@184:     (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
adamc@184:     (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184:       In (existT _ _ (v1, v2)) G
adamc@183:       -> v2 < length envT)
adamc@184:     -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184:       In (existT _ _ (v1, v2)) G
adamc@185:       -> forall pf,
adamc@185:         lr t v1 (match lok pf in _ = T return T with
adamc@185:                    | refl_equal => lookup Closed.typeDenote v2 env
adamc@185:                  end))
adamc@185:       (*-> forall pf : lookup_type v2 fvs = Some t,
adamc@185:         lr t v1 (match pf in _ = T return Closed.typeDenote <| T with
adamc@185:                    | refl_equal => lookup Closed.typeDenote v2 env
adamc@185:                  end))*)
adamc@185:     -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
adamc@183: 
adamc@184:   Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
adamc@183:   Hint Resolve packExp_correct lookup_type_inner.
adamc@183: 
adamc@184:   induction 1.
adamc@183: 
adamc@184:   crush.
adamc@184:   crush.
adamc@184:   crush.
adamc@184:   crush.
adamc@183: 
adamc@185:   crush.
adamc@185:   apply (H0 x1 (length envT) (t1 :: envT) (true, snd (fvsExp (f2 (length envT)) (t1 :: envT)))).
adamc@185:   clear H0.
adamc@185:   crush.
adamc@185:   eauto.
adamc@185:   generalize (H1 _ _ _ H4).
adamc@185:   crush.
adamc@183: 
adamc@185:   crush.
adamc@185:   generalize H3; clear_all.
adamc@185:   match goal with
adamc@185:     | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185:   end.
adamc@184:   simpl.
adamc@185:   destruct (eq_nat_dec (length envT) (length envT)); crush.
adamc@185:   rewrite (UIP_refl _ _ e0); assumption.
adamc@185: 
adamc@185:   match goal with
adamc@185:     | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185:   end; simpl.
adamc@185:   destruct (eq_nat_dec v2 (length envT)); crush.
adamc@185:   generalize (H1 _ _ _ H5).
adamc@185:   crush.
adamc@185:   generalize (H2 _ _ _ H5).
adamc@185:   clear H2; intro H2.
adamc@185:   generalize (H2 (lookup_type_inner _ _ _ _ _ wf pf)).
adamc@185:   clear H2; intro H2.
adamc@185:   generalize H2; clear_all.
adamc@185:   repeat match goal with
adamc@185:            | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@185:          end; simpl.
adamc@185: 
adamc@185:   match type of pf with
adamc@185:     | ?X = _ => assert (X <> None)
adamc@185:   end.
adamc@185:   congruence.
adamc@185:   assert (forall (n : nat) (t0 : Source.type),
adamc@185:     lookup_type (envT:=envT) n (snd (fvsExp (f2 (length envT)) (t1 :: envT))) = Some t0 ->
adamc@185:     lookup_type (envT:=envT) n fvs = Some t0).
adamc@185:   eauto.
adamc@185:   generalize (packExp_correct fvs (inclusion t1 envT fvs (f2 (length envT)) wf) env H).
adamc@185:   simpl.
adamc@185:   match goal with
adamc@185:     | [ |- ?X == ?Y -> _ ] =>
adamc@185:       generalize X Y
adamc@185:   end.
adamc@185:   rewrite pf.
adamc@185:   rewrite (lookup_type_inner _ _ _ _ _ wf pf).
adamc@185:   crush.
adamc@185:   rewrite (UIP_refl _ _ e0).
adamc@185:   rewrite (UIP_refl _ _ e1) in H2.
adamc@185:   crush.
adamc@185:   rewrite <- H1.
adamc@185:   assumption.
adamc@183: Qed.
adamc@183: 
adamc@183: 
adamc@183: (** * Parametric version *)
adamc@183: 
adamc@183: Section wf.
adamc@186:   Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t),
adamc@186:     exp_equiv G e1 e2
adamc@186:     -> forall envT (fvs : isfree envT),
adamc@186:       (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
adamc@186:         -> lookup_type v1 fvs = Some t)
adamc@186:       -> wfExp fvs e1.
adamc@186:     Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
adamc@183: 
adamc@186:     induction 1; crush.
adamc@186:     eapply H0.
adamc@186:     eauto.
adamc@183: 
adamc@186:     apply H0 with (length envT).
adamc@186:     my_crush.
adamc@186:     eauto.
adamc@183:   Qed.
adamc@183: 
adamc@186:   Theorem Exp_wf : forall t (E : Source.Exp t),
adamc@186:     wfExp (envT := nil) tt (E _).
adamc@186:     intros; eapply Exp_wf';
adamc@186:       [apply Exp_equiv
adamc@186:         | crush].
adamc@183:   Qed.
adamc@183: End wf.
adamc@183: 
adamc@186: Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
adamc@186:   CcExp' E (Exp_wf E).
adamc@183: 
adamc@186: Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1),
adamc@186:   funcsDenote (map_funcs f fs) = f (funcsDenote fs).
adamc@186:   induction fs; crush.
adamc@183: Qed.
adamc@183: 
adamc@186: Theorem CcExp_correct : forall (E : Source.Exp Nat),
adamc@186:   Source.ExpDenote E
adamc@186:   = ProgDenote (CcExp E).
adamc@186:   Hint Rewrite map_funcs_correct : cpdt.
adamc@183: 
adamc@186:   unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush;
adamc@186:     apply (ccExp_correct
adamc@183:       (G := nil)
adamc@183:       (e1 := E _)
adamc@183:       (e2 := E _)
adamc@186:       (Exp_equiv _ _ _)
adamc@183:       nil
adamc@183:       tt
adamc@186:       tt); crush.
adamc@183: Qed.