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@187: Notation "f <== \\ ! , y , e ; fs" := adamc@187: (Abs (fun _ y => e) (fun f => fs)) adamc@187: (right associativity, at level 80, e at next level) : cc_scope. adamc@187: Notation "f <== \\ x , ! , e ; fs" := adamc@187: (Abs (fun x _ => e) (fun f => fs)) adamc@187: (right associativity, at level 80, e at next level) : cc_scope. adamc@187: Notation "f <== \\ ! , ! , e ; fs" := adamc@187: (Abs (fun _ _ => e) (fun f => fs)) adamc@187: (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: 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@187: intros; assert (length envT < length envT); eauto; crush. adamc@183: Defined. adamc@183: adamc@183: Hint Resolve lookup_bound_contra. 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: 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: Import Source. adamc@183: Open Local Scope cc_scope. adamc@183: adamc@187: Definition proj1 A B (pf : A /\ B) : A := adamc@187: let (x, _) := pf in x. adamc@187: Definition proj2 A B (pf : A /\ B) : B := adamc@187: let (_, y) := pf in y. adamc@187: 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@187: (** ** Examples *) adamc@187: adamc@187: Open Local Scope source_scope. adamc@187: adamc@187: Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x. adamc@187: Theorem ident_ok : wfExp (envT := nil) tt (ident _). adamc@187: crush. adamc@187: Defined. adamc@187: Eval compute in CcExp' ident ident_ok. adamc@187: Eval compute in ProgDenote (CcExp' ident ident_ok). adamc@187: adamc@187: Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0. adamc@187: Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _). adamc@187: crush. adamc@187: Defined. adamc@187: Eval compute in CcExp' app_ident app_ident_ok. adamc@187: Eval compute in ProgDenote (CcExp' app_ident app_ident_ok). adamc@187: adamc@187: Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ => adamc@187: \x, \y, #x. adamc@187: Theorem first_ok : wfExp (envT := nil) tt (first _). adamc@187: crush. adamc@187: Defined. adamc@187: Eval compute in CcExp' first first_ok. adamc@187: Eval compute in ProgDenote (CcExp' first first_ok). adamc@187: adamc@187: Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0. adamc@187: Theorem app_first_ok : wfExp (envT := nil) tt (app_first _). adamc@187: crush. adamc@187: Defined. adamc@187: Eval compute in CcExp' app_first app_first_ok. adamc@187: Eval compute in ProgDenote (CcExp' app_first app_first_ok). adamc@187: adamc@187: adamc@187: (** ** 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@187: Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT) adamc@183: Hincl env, adamc@187: lookup_type v fvs1 = Some t 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: Implicit Arguments packExp_correct [v envT fvs1]. adamc@187: Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e]. adamc@187: Implicit Arguments inclusion [t t' envT fvs e]. 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@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: -> 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@188: induction 1; crush; adamc@188: match goal with adamc@188: | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] => adamc@188: apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV)))) adamc@188: end; crush; adamc@188: match goal with adamc@188: | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] => adamc@188: solve [ generalize (Hlt _ _ _ Hin); crush ] adamc@188: | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf adamc@188: end; simpl; adamc@188: match goal with adamc@188: | [ |- context[if ?E then _ else _] ] => destruct E adamc@188: end; intuition; subst; adamc@188: match goal with adamc@188: | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption adamc@188: | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] => adamc@188: generalize (Hlt _ _ _ Hin); crush adamc@188: | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _, adamc@188: fvs : isfree _, env : envOf _ _ |- _ ] => adamc@188: generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all; adamc@188: repeat match goal with adamc@188: | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf adamc@188: end; simpl; adamc@188: generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl; adamc@188: match goal with adamc@188: | [ |- ?X == ?Y -> _ ] => adamc@188: generalize X Y adamc@188: end; adamc@188: rewrite pf; rewrite (lookup_type_inner wf pf); adamc@188: intros lhs rhs Heq; intros; adamc@188: repeat match goal with adamc@188: | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in * adamc@188: end; adamc@188: rewrite <- Heq; assumption adamc@188: end. 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@189: induction 1; crush; eauto; adamc@189: match goal with adamc@189: | [ H : _, envT : list Source.type |- _ ] => adamc@189: apply H with (length envT); my_crush; eauto adamc@189: end. adamc@183: Qed. adamc@183: adamc@186: Theorem Exp_wf : forall t (E : Source.Exp t), adamc@186: wfExp (envT := nil) tt (E _). adamc@189: Hint Resolve Exp_equiv. adamc@189: adamc@189: intros; eapply Exp_wf'; 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.