adamc@175: (* Copyright (c) 2008, Adam Chlipala adamc@175: * adamc@175: * This work is licensed under a adamc@175: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@175: * Unported License. adamc@175: * The license text is available at: adamc@175: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@175: *) adamc@175: adamc@175: (* begin hide *) adamc@175: Require Import String List. adamc@175: adamc@177: Require Import AxiomsImpred Tactics DepList. adamc@175: adamc@175: Set Implicit Arguments. adamc@175: (* end hide *) adamc@175: adamc@175: adamc@175: (** %\chapter{Certifying Extensional Transformations}% *) adamc@175: adamc@175: (** TODO: Prose for this chapter *) adamc@175: adamc@175: adamc@175: (** * Simply-Typed Lambda Calculus *) adamc@175: adamc@175: Module STLC. adamc@175: Module Source. adamc@175: Inductive type : Type := adamc@175: | TNat : type adamc@175: | Arrow : type -> type -> type. adamc@175: adamc@175: Notation "'Nat'" := TNat : source_scope. adamc@175: Infix "-->" := Arrow (right associativity, at level 60) : source_scope. adamc@175: adamc@175: Open Scope source_scope. adamc@175: Bind Scope source_scope with type. adamc@175: Delimit Scope source_scope with source. adamc@175: adamc@175: Section vars. adamc@175: Variable var : type -> Type. adamc@175: adamc@175: Inductive exp : type -> Type := adamc@175: | Var : forall t, adamc@175: var t adamc@175: -> exp t adamc@175: adamc@175: | Const : nat -> exp Nat adamc@175: | Plus : exp Nat -> exp Nat -> exp Nat adamc@175: adamc@175: | App : forall t1 t2, adamc@175: exp (t1 --> t2) adamc@175: -> exp t1 adamc@175: -> exp t2 adamc@175: | Abs : forall t1 t2, adamc@175: (var t1 -> exp t2) adamc@175: -> exp (t1 --> t2). adamc@175: End vars. adamc@175: adamc@175: Definition Exp t := forall var, exp var t. adamc@175: adamc@175: Implicit Arguments Var [var t]. adamc@175: Implicit Arguments Const [var]. adamc@175: Implicit Arguments Plus [var]. adamc@175: Implicit Arguments App [var t1 t2]. adamc@175: Implicit Arguments Abs [var t1 t2]. adamc@175: adamc@175: Notation "# v" := (Var v) (at level 70) : source_scope. adamc@175: adamc@175: Notation "^ n" := (Const n) (at level 70) : source_scope. adamc@175: Infix "+^" := Plus (left associativity, at level 79) : source_scope. adamc@175: adamc@175: Infix "@" := App (left associativity, at level 77) : source_scope. adamc@175: Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. adamc@175: Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. adamc@175: adamc@175: Bind Scope source_scope with exp. adamc@175: adamc@175: Definition zero : Exp Nat := fun _ => ^0. adamc@175: Definition one : Exp Nat := fun _ => ^1. adamc@175: Definition zpo : Exp Nat := fun _ => zero _ +^ one _. adamc@175: Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. adamc@175: Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. adamc@175: Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => adamc@175: \f, \x, #f @ #x. adamc@175: Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. adamc@175: adamc@175: Fixpoint typeDenote (t : type) : Set := adamc@175: match t with adamc@175: | Nat => nat adamc@175: | t1 --> t2 => typeDenote t1 -> typeDenote t2 adamc@175: end. adamc@175: adamc@175: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@175: match e in (exp _ t) return (typeDenote t) with adamc@175: | Var _ v => v adamc@175: adamc@175: | Const n => n adamc@175: | Plus e1 e2 => expDenote e1 + expDenote e2 adamc@175: adamc@175: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@175: | Abs _ _ e' => fun x => expDenote (e' x) adamc@175: end. adamc@175: adamc@175: Definition ExpDenote t (e : Exp t) := expDenote (e _). adamc@176: adamc@180: (* begin thide *) adamc@176: Section exp_equiv. adamc@176: Variables var1 var2 : type -> Type. adamc@176: adamc@176: Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := adamc@176: | EqEVar : forall G t (v1 : var1 t) v2, adamc@176: In (existT _ t (v1, v2)) G adamc@176: -> exp_equiv G (#v1) (#v2) adamc@176: adamc@176: | EqEConst : forall G n, adamc@176: exp_equiv G (^n) (^n) adamc@176: | EqEPlus : forall G x1 y1 x2 y2, adamc@176: exp_equiv G x1 x2 adamc@176: -> exp_equiv G y1 y2 adamc@176: -> exp_equiv G (x1 +^ y1) (x2 +^ y2) adamc@176: adamc@176: | EqEApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2, adamc@176: exp_equiv G f1 f2 adamc@176: -> exp_equiv G x1 x2 adamc@176: -> exp_equiv G (f1 @ x1) (f2 @ x2) adamc@176: | EqEAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, adamc@176: (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) adamc@176: -> exp_equiv G (Abs f1) (Abs f2). adamc@176: End exp_equiv. adamc@176: adamc@176: Axiom Exp_equiv : forall t (E : Exp t) var1 var2, adamc@176: exp_equiv nil (E var1) (E var2). adamc@180: (* end thide *) adamc@175: End Source. adamc@175: adamc@175: Module CPS. adamc@175: Inductive type : Type := adamc@175: | TNat : type adamc@175: | Cont : type -> type adamc@175: | TUnit : type adamc@175: | Prod : type -> type -> type. adamc@175: adamc@175: Notation "'Nat'" := TNat : cps_scope. adamc@175: Notation "'Unit'" := TUnit : cps_scope. adamc@175: Notation "t --->" := (Cont t) (at level 61) : cps_scope. adamc@175: Infix "**" := Prod (right associativity, at level 60) : cps_scope. adamc@175: adamc@175: Bind Scope cps_scope with type. adamc@175: Delimit Scope cps_scope with cps. adamc@175: adamc@175: Section vars. adamc@175: Variable var : type -> Type. adamc@175: adamc@175: Inductive prog : Type := adamc@175: | PHalt : adamc@175: var Nat adamc@175: -> prog adamc@175: | App : forall t, adamc@175: var (t --->) adamc@175: -> var t adamc@175: -> prog adamc@175: | Bind : forall t, adamc@175: primop t adamc@175: -> (var t -> prog) adamc@175: -> prog adamc@175: adamc@175: with primop : type -> Type := adamc@175: | Var : forall t, adamc@175: var t adamc@175: -> primop t adamc@175: adamc@175: | Const : nat -> primop Nat adamc@175: | Plus : var Nat -> var Nat -> primop Nat adamc@175: adamc@175: | Abs : forall t, adamc@175: (var t -> prog) adamc@175: -> primop (t --->) adamc@175: adamc@175: | Pair : forall t1 t2, adamc@175: var t1 adamc@175: -> var t2 adamc@175: -> primop (t1 ** t2) adamc@175: | Fst : forall t1 t2, adamc@175: var (t1 ** t2) adamc@175: -> primop t1 adamc@175: | Snd : forall t1 t2, adamc@175: var (t1 ** t2) adamc@175: -> primop t2. adamc@175: End vars. adamc@175: adamc@175: Implicit Arguments PHalt [var]. adamc@175: Implicit Arguments App [var t]. adamc@175: adamc@175: Implicit Arguments Var [var t]. adamc@175: Implicit Arguments Const [var]. adamc@175: Implicit Arguments Plus [var]. adamc@175: Implicit Arguments Abs [var t]. adamc@175: Implicit Arguments Pair [var t1 t2]. adamc@175: Implicit Arguments Fst [var t1 t2]. adamc@175: Implicit Arguments Snd [var t1 t2]. adamc@175: adamc@175: Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope. adamc@175: Infix "@@" := App (no associativity, at level 75) : cps_scope. adamc@175: Notation "x <- p ; e" := (Bind p (fun x => e)) adamc@175: (right associativity, at level 76, p at next level) : cps_scope. adamc@175: Notation "! <- p ; e" := (Bind p (fun _ => e)) adamc@175: (right associativity, at level 76, p at next level) : cps_scope. adamc@175: adamc@175: Notation "# v" := (Var v) (at level 70) : cps_scope. adamc@175: adamc@175: Notation "^ n" := (Const n) (at level 70) : cps_scope. adamc@175: Infix "+^" := Plus (left associativity, at level 79) : cps_scope. adamc@175: adamc@175: Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope. adamc@175: Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope. adamc@175: adamc@179: Notation "[ x1 , x2 ]" := (Pair x1 x2) : cps_scope. adamc@175: Notation "#1 x" := (Fst x) (at level 72) : cps_scope. adamc@175: Notation "#2 x" := (Snd x) (at level 72) : cps_scope. adamc@175: adamc@175: Bind Scope cps_scope with prog primop. adamc@175: adamc@175: Open Scope cps_scope. adamc@175: adamc@175: Fixpoint typeDenote (t : type) : Set := adamc@175: match t with adamc@175: | Nat => nat adamc@175: | t' ---> => typeDenote t' -> nat adamc@175: | Unit => unit adamc@175: | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type adamc@175: end. adamc@175: adamc@175: Fixpoint progDenote (e : prog typeDenote) : nat := adamc@175: match e with adamc@175: | PHalt n => n adamc@175: | App _ f x => f x adamc@175: | Bind _ p x => progDenote (x (primopDenote p)) adamc@175: end adamc@175: adamc@175: with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t := adamc@175: match p in (primop _ t) return (typeDenote t) with adamc@175: | Var _ v => v adamc@175: adamc@175: | Const n => n adamc@175: | Plus n1 n2 => n1 + n2 adamc@175: adamc@175: | Abs _ e => fun x => progDenote (e x) adamc@175: adamc@175: | Pair _ _ v1 v2 => (v1, v2) adamc@175: | Fst _ _ v => fst v adamc@175: | Snd _ _ v => snd v adamc@175: end. adamc@175: adamc@175: Definition Prog := forall var, prog var. adamc@175: Definition Primop t := forall var, primop var t. adamc@175: Definition ProgDenote (E : Prog) := progDenote (E _). adamc@175: Definition PrimopDenote t (P : Primop t) := primopDenote (P _). adamc@175: End CPS. adamc@175: adamc@175: Import Source CPS. adamc@175: adamc@180: (* begin thide *) adamc@175: Fixpoint cpsType (t : Source.type) : CPS.type := adamc@175: match t with adamc@175: | Nat => Nat%cps adamc@175: | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps adamc@175: end%source. adamc@175: adamc@175: Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). adamc@175: adamc@175: Section cpsExp. adamc@175: Variable var : CPS.type -> Type. adamc@175: adamc@175: Import Source. adamc@175: Open Scope cps_scope. adamc@175: adamc@175: Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e} adamc@175: : (var (cpsType t) -> prog var) -> prog var := adamc@175: match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with adamc@175: | Var _ v => fun k => k v adamc@175: adamc@175: | Const n => fun k => adamc@175: x <- ^n; adamc@175: k x adamc@175: | Plus e1 e2 => fun k => adamc@175: x1 <-- e1; adamc@175: x2 <-- e2; adamc@175: x <- x1 +^ x2; adamc@175: k x adamc@175: adamc@175: | App _ _ e1 e2 => fun k => adamc@175: f <-- e1; adamc@175: x <-- e2; adamc@175: kf <- \r, k r; adamc@175: p <- [x, kf]; adamc@175: f @@ p adamc@175: | Abs _ _ e' => fun k => adamc@175: f <- CPS.Abs (var := var) (fun p => adamc@175: x <- #1 p; adamc@175: kf <- #2 p; adamc@175: r <-- e' x; adamc@175: kf @@ r); adamc@175: k f adamc@175: end adamc@175: adamc@175: where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)). adamc@175: End cpsExp. adamc@175: adamc@175: Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope. adamc@175: Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2)) adamc@175: (right associativity, at level 76, e1 at next level) : cps_scope. adamc@175: adamc@175: Implicit Arguments cpsExp [var t]. adamc@175: Definition CpsExp (E : Exp Nat) : Prog := adamc@175: fun var => cpsExp (E _) (PHalt (var := _)). adamc@180: (* end thide *) adamc@175: adamc@175: Eval compute in CpsExp zero. adamc@175: Eval compute in CpsExp one. adamc@175: Eval compute in CpsExp zpo. adamc@175: Eval compute in CpsExp app_ident. adamc@175: Eval compute in CpsExp app_ident'. adamc@175: adamc@175: Eval compute in ProgDenote (CpsExp zero). adamc@175: Eval compute in ProgDenote (CpsExp one). adamc@175: Eval compute in ProgDenote (CpsExp zpo). adamc@175: Eval compute in ProgDenote (CpsExp app_ident). adamc@175: Eval compute in ProgDenote (CpsExp app_ident'). adamc@175: adamc@180: (* begin thide *) adamc@176: Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := adamc@176: match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with adamc@176: | Nat => fun n1 n2 => n1 = n2 adamc@176: | t1 --> t2 => fun f1 f2 => adamc@176: forall x1 x2, lr _ x1 x2 adamc@176: -> forall k, exists r, adamc@176: f2 (x2, k) = k r adamc@176: /\ lr _ (f1 x1) r adamc@176: end%source. adamc@176: adamc@176: Lemma cpsExp_correct : forall G t (e1 : exp _ t) (e2 : exp _ t), adamc@176: exp_equiv G e1 e2 adamc@176: -> (forall t v1 v2, In (existT _ t (v1, v2)) G -> lr t v1 v2) adamc@176: -> forall k, exists r, adamc@176: progDenote (cpsExp e2 k) = progDenote (k r) adamc@176: /\ lr t (expDenote e1) r. adamc@176: induction 1; crush; fold typeDenote in *; adamc@176: repeat (match goal with adamc@176: | [ H : forall k, exists r, progDenote (cpsExp ?E k) = _ /\ _ adamc@176: |- context[cpsExp ?E ?K] ] => adamc@176: generalize (H K); clear H adamc@176: | [ |- exists r, progDenote (_ ?R) = progDenote (_ r) /\ _ ] => adamc@176: exists R adamc@176: | [ t1 : Source.type |- _ ] => adamc@176: match goal with adamc@176: | [ Hlr : lr t1 ?X1 ?X2, IH : forall v1 v2, _ |- _ ] => adamc@176: generalize (IH X1 X2); clear IH; intro IH; adamc@176: match type of IH with adamc@176: | ?P -> _ => assert P adamc@176: end adamc@176: end adamc@176: end; crush); eauto. adamc@176: Qed. adamc@176: adamc@176: Lemma vars_easy : forall (t : Source.type) (v1 : Source.typeDenote t) adamc@176: (v2 : typeDenote (cpsType t)), adamc@176: In adamc@176: (existT adamc@176: (fun t0 : Source.type => adamc@176: (Source.typeDenote t0 * typeDenote (cpsType t0))%type) t adamc@176: (v1, v2)) nil -> lr t v1 v2. adamc@176: crush. adamc@176: Qed. adamc@176: adamc@176: Theorem CpsExp_correct : forall (E : Exp Nat), adamc@176: ProgDenote (CpsExp E) = ExpDenote E. adamc@176: unfold ProgDenote, CpsExp, ExpDenote; intros; adamc@176: generalize (cpsExp_correct (e1 := E _) (e2 := E _) adamc@176: (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. adamc@176: Qed. adamc@180: (* end thide *) adamc@176: adamc@175: End STLC. adamc@177: adamc@177: adamc@177: (** * A Pattern Compiler *) adamc@177: adamc@177: Module PatMatch. adamc@177: Module Source. adamc@177: Inductive type : Type := adamc@177: | Unit : type adamc@177: | Arrow : type -> type -> type adamc@177: | Prod : type -> type -> type adamc@177: | Sum : type -> type -> type. adamc@177: adamc@177: Infix "-->" := Arrow (right associativity, at level 61). adamc@177: Infix "++" := Sum (right associativity, at level 60). adamc@177: Infix "**" := Prod (right associativity, at level 59). adamc@177: adamc@177: Inductive pat : type -> list type -> Type := adamc@177: | PVar : forall t, adamc@177: pat t (t :: nil) adamc@177: | PPair : forall t1 t2 ts1 ts2, adamc@177: pat t1 ts1 adamc@177: -> pat t2 ts2 adamc@177: -> pat (t1 ** t2) (ts1 ++ ts2) adamc@177: | PInl : forall t1 t2 ts, adamc@177: pat t1 ts adamc@177: -> pat (t1 ++ t2) ts adamc@177: | PInr : forall t1 t2 ts, adamc@177: pat t2 ts adamc@177: -> pat (t1 ++ t2) ts. adamc@177: adamc@177: Implicit Arguments PVar [t]. adamc@177: Implicit Arguments PInl [t1 t2 ts]. adamc@177: Implicit Arguments PInr [t1 t2 ts]. adamc@177: adamc@177: Notation "##" := PVar (at level 70) : pat_scope. adamc@179: Notation "[ p1 , p2 ]" := (PPair p1 p2) : pat_scope. adamc@177: Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope. adamc@177: Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope. adamc@177: adamc@177: Bind Scope pat_scope with pat. adamc@177: Delimit Scope pat_scope with pat. adamc@177: adamc@177: Section vars. adamc@177: Variable var : type -> Type. adamc@177: adamc@177: Inductive exp : type -> Type := adamc@177: | Var : forall t, adamc@177: var t adamc@177: -> exp t adamc@177: adamc@177: | EUnit : exp Unit adamc@177: adamc@177: | App : forall t1 t2, adamc@177: exp (t1 --> t2) adamc@177: -> exp t1 adamc@177: -> exp t2 adamc@177: | Abs : forall t1 t2, adamc@177: (var t1 -> exp t2) adamc@177: -> exp (t1 --> t2) adamc@177: adamc@177: | Pair : forall t1 t2, adamc@177: exp t1 adamc@177: -> exp t2 adamc@177: -> exp (t1 ** t2) adamc@177: adamc@177: | EInl : forall t1 t2, adamc@177: exp t1 adamc@177: -> exp (t1 ++ t2) adamc@177: | EInr : forall t1 t2, adamc@177: exp t2 adamc@177: -> exp (t1 ++ t2) adamc@177: adamc@177: | Case : forall t1 t2 (tss : list (list type)), adamc@177: exp t1 adamc@177: -> (forall ts, member ts tss -> pat t1 ts) adamc@177: -> (forall ts, member ts tss -> hlist var ts -> exp t2) adamc@177: -> exp t2 adamc@177: -> exp t2. adamc@177: End vars. adamc@177: adamc@177: Definition Exp t := forall var, exp var t. adamc@177: adamc@177: Implicit Arguments Var [var t]. adamc@177: Implicit Arguments EUnit [var]. adamc@177: Implicit Arguments App [var t1 t2]. adamc@177: Implicit Arguments Abs [var t1 t2]. adamc@177: Implicit Arguments Pair [var t1 t2]. adamc@177: Implicit Arguments EInl [var t1 t2]. adamc@177: Implicit Arguments EInr [var t1 t2]. adamc@177: Implicit Arguments Case [var t1 t2]. adamc@177: adamc@177: Notation "# v" := (Var v) (at level 70) : source_scope. adamc@177: adamc@177: Notation "()" := EUnit : source_scope. adamc@177: adamc@177: Infix "@" := App (left associativity, at level 77) : source_scope. adamc@177: Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. adamc@177: adamc@179: Notation "[ x , y ]" := (Pair x y) : source_scope. adamc@177: adamc@177: Notation "'Inl' e" := (EInl e) (at level 71) : source_scope. adamc@177: Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. adamc@177: adamc@178: Delimit Scope source_scope with source. adamc@177: Bind Scope source_scope with exp. adamc@177: adamc@177: Open Local Scope source_scope. adamc@177: adamc@177: Fixpoint typeDenote (t : type) : Set := adamc@177: match t with adamc@177: | Unit => unit adamc@177: | t1 --> t2 => typeDenote t1 -> typeDenote t2 adamc@177: | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type adamc@177: | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type adamc@177: end. adamc@177: adamc@177: Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) := adamc@177: match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with adamc@177: | PVar _ => fun v => Some (v, tt) adamc@177: | PPair _ _ _ _ p1 p2 => fun v => adamc@177: match patDenote p1 (fst v), patDenote p2 (snd v) with adamc@177: | Some tup1, Some tup2 => Some (happ tup1 tup2) adamc@177: | _, _ => None adamc@177: end adamc@177: | PInl _ _ _ p' => fun v => adamc@177: match v with adamc@177: | inl v' => patDenote p' v' adamc@177: | _ => None adamc@177: end adamc@177: | PInr _ _ _ p' => fun v => adamc@177: match v with adamc@177: | inr v' => patDenote p' v' adamc@177: | _ => None adamc@177: end adamc@177: end. adamc@177: adamc@177: Section matchesDenote. adamc@177: Variables t2 : type. adamc@177: Variable default : typeDenote t2. adamc@177: adamc@177: Fixpoint matchesDenote (tss : list (list type)) adamc@177: : (forall ts, member ts tss -> option (hlist typeDenote ts)) adamc@177: -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) adamc@177: -> typeDenote t2 := adamc@177: match tss return (forall ts, member ts tss -> _) adamc@177: -> (forall ts, member ts tss -> _) adamc@177: -> _ with adamc@177: | nil => fun _ _ => adamc@177: default adamc@177: | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts')) adamc@177: (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) => adamc@177: match envs _ (hfirst (refl_equal _)) with adamc@177: | None => matchesDenote tss' adamc@177: (fun _ mem => envs _ (hnext mem)) adamc@177: (fun _ mem => bodies _ (hnext mem)) adamc@177: | Some env => (bodies _ (hfirst (refl_equal _))) env adamc@177: end adamc@177: end. adamc@177: End matchesDenote. adamc@177: adamc@177: Implicit Arguments matchesDenote [t2 tss]. adamc@177: adamc@177: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@177: match e in (exp _ t) return (typeDenote t) with adamc@177: | Var _ v => v adamc@177: adamc@177: | EUnit => tt adamc@177: adamc@177: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@177: | Abs _ _ e' => fun x => expDenote (e' x) adamc@177: adamc@177: | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) adamc@177: adamc@177: | EInl _ _ e' => inl _ (expDenote e') adamc@177: | EInr _ _ e' => inr _ (expDenote e') adamc@177: adamc@177: | Case _ _ _ e ps es def => adamc@177: matchesDenote (expDenote def) adamc@177: (fun _ mem => patDenote (ps _ mem) (expDenote e)) adamc@177: (fun _ mem env => expDenote (es _ mem env)) adamc@177: end. adamc@177: adamc@177: Definition ExpDenote t (E : Exp t) := expDenote (E _). adamc@177: End Source. adamc@177: adamc@177: Import Source. adamc@177: adamc@178: Module Elab. adamc@177: Section vars. adamc@177: Variable var : type -> Type. adamc@177: adamc@177: Inductive exp : type -> Type := adamc@177: | Var : forall t, adamc@177: var t adamc@177: -> exp t adamc@177: adamc@177: | EUnit : exp Unit adamc@177: adamc@177: | App : forall t1 t2, adamc@177: exp (t1 --> t2) adamc@177: -> exp t1 adamc@177: -> exp t2 adamc@177: | Abs : forall t1 t2, adamc@177: (var t1 -> exp t2) adamc@177: -> exp (t1 --> t2) adamc@177: adamc@177: | Pair : forall t1 t2, adamc@177: exp t1 adamc@177: -> exp t2 adamc@177: -> exp (t1 ** t2) adamc@177: | Fst : forall t1 t2, adamc@177: exp (t1 ** t2) adamc@177: -> exp t1 adamc@177: | Snd : forall t1 t2, adamc@177: exp (t1 ** t2) adamc@177: -> exp t2 adamc@177: adamc@177: | EInl : forall t1 t2, adamc@177: exp t1 adamc@177: -> exp (t1 ++ t2) adamc@177: | EInr : forall t1 t2, adamc@177: exp t2 adamc@177: -> exp (t1 ++ t2) adamc@177: | Case : forall t1 t2 t, adamc@177: exp (t1 ++ t2) adamc@177: -> (var t1 -> exp t) adamc@177: -> (var t2 -> exp t) adamc@177: -> exp t. adamc@177: End vars. adamc@177: adamc@177: Definition Exp t := forall var, exp var t. adamc@177: adamc@177: Implicit Arguments Var [var t]. adamc@177: Implicit Arguments EUnit [var]. adamc@177: Implicit Arguments App [var t1 t2]. adamc@177: Implicit Arguments Abs [var t1 t2]. adamc@177: Implicit Arguments Pair [var t1 t2]. adamc@177: Implicit Arguments Fst [var t1 t2]. adamc@177: Implicit Arguments Snd [var t1 t2]. adamc@177: Implicit Arguments EInl [var t1 t2]. adamc@177: Implicit Arguments EInr [var t1 t2]. adamc@177: Implicit Arguments Case [var t1 t2 t]. adamc@177: adamc@177: adamc@177: Notation "# v" := (Var v) (at level 70) : elab_scope. adamc@177: adamc@177: Notation "()" := EUnit : elab_scope. adamc@177: adamc@177: Infix "@" := App (left associativity, at level 77) : elab_scope. adamc@177: Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope. adamc@177: Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope. adamc@177: adamc@179: Notation "[ x , y ]" := (Pair x y) : elab_scope. adamc@177: Notation "#1 e" := (Fst e) (at level 72) : elab_scope. adamc@177: Notation "#2 e" := (Snd e) (at level 72) : elab_scope. adamc@177: adamc@177: Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope. adamc@177: Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope. adamc@177: adamc@177: Bind Scope elab_scope with exp. adamc@177: Delimit Scope elab_scope with elab. adamc@177: adamc@177: Open Scope elab_scope. adamc@177: adamc@177: Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := adamc@177: match e in (exp _ t) return (typeDenote t) with adamc@177: | Var _ v => v adamc@177: adamc@177: | EUnit => tt adamc@177: adamc@177: | App _ _ e1 e2 => (expDenote e1) (expDenote e2) adamc@177: | Abs _ _ e' => fun x => expDenote (e' x) adamc@177: adamc@177: | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) adamc@177: | Fst _ _ e' => fst (expDenote e') adamc@177: | Snd _ _ e' => snd (expDenote e') adamc@177: adamc@177: | EInl _ _ e' => inl _ (expDenote e') adamc@177: | EInr _ _ e' => inr _ (expDenote e') adamc@177: | Case _ _ _ e' e1 e2 => adamc@177: match expDenote e' with adamc@177: | inl v => expDenote (e1 v) adamc@177: | inr v => expDenote (e2 v) adamc@177: end adamc@177: end. adamc@177: adamc@177: Definition ExpDenote t (E : Exp t) := expDenote (E _). adamc@177: End Elab. adamc@177: adamc@178: Import Elab. adamc@178: adamc@178: Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%source adamc@178: (right associativity, at level 76, e1 at next level) : source_scope. adamc@178: Notation "x <- e1 ; e2" := ((\x, e2) @ e1)%elab adamc@178: (right associativity, at level 76, e1 at next level) : elab_scope. adamc@178: adamc@178: Section choice_tree. adamc@178: Open Scope source_scope. adamc@178: adamc@178: Fixpoint choice_tree var (t : type) (result : Type) : Type := adamc@178: match t with adamc@178: | t1 ** t2 => adamc@178: choice_tree var t1 adamc@178: (choice_tree var t2 adamc@178: result) adamc@178: | t1 ++ t2 => adamc@178: choice_tree var t1 result adamc@178: * choice_tree var t2 result adamc@178: | t => exp var t -> result adamc@178: end%type. adamc@178: adamc@178: Fixpoint merge var t result {struct t} adamc@178: : (result -> result -> result) adamc@178: -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result := adamc@178: match t return ((result -> result -> result) adamc@178: -> choice_tree var t result -> choice_tree var t result -> choice_tree var t result) with adamc@178: | _ ** _ => fun mr ct1 ct2 => adamc@178: merge _ _ adamc@178: (merge _ _ mr) adamc@178: ct1 ct2 adamc@178: adamc@178: | _ ++ _ => fun mr ct1 ct2 => adamc@178: (merge var _ mr (fst ct1) (fst ct2), adamc@178: merge var _ mr (snd ct1) (snd ct2)) adamc@178: adamc@178: | _ => fun mr ct1 ct2 e => mr (ct1 e) (ct2 e) adamc@178: end. adamc@178: adamc@178: Fixpoint everywhere var t result {struct t} adamc@178: : (exp var t -> result) -> choice_tree var t result := adamc@178: match t return ((exp var t -> result) -> choice_tree var t result) with adamc@178: | t1 ** t2 => fun r => adamc@178: everywhere (t := t1) (fun e1 => adamc@178: everywhere (t := t2) (fun e2 => adamc@178: r ([e1, e2])%elab)) adamc@178: adamc@178: | _ ++ _ => fun r => adamc@178: (everywhere (fun e => r (Inl e)%elab), adamc@178: everywhere (fun e => r (Inr e)%elab)) adamc@178: adamc@178: | _ => fun r => r adamc@178: end. adamc@178: End choice_tree. adamc@178: adamc@178: Implicit Arguments merge [var t result]. adamc@178: adamc@178: Section elaborate. adamc@178: Open Local Scope elab_scope. adamc@178: adamc@178: Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : adamc@178: (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := adamc@178: match p in (pat t1 ts) return ((hlist (exp var) ts -> result) adamc@178: -> result -> choice_tree var t1 result) with adamc@178: | PVar _ => fun succ fail => adamc@178: everywhere (fun disc => succ (disc, tt)) adamc@178: adamc@178: | PPair _ _ _ _ p1 p2 => fun succ fail => adamc@178: elaboratePat _ p1 adamc@178: (fun tup1 => adamc@178: elaboratePat _ p2 adamc@178: (fun tup2 => adamc@178: succ (happ tup1 tup2)) adamc@178: fail) adamc@178: (everywhere (fun _ => fail)) adamc@178: adamc@178: | PInl _ _ _ p' => fun succ fail => adamc@178: (elaboratePat _ p' succ fail, adamc@178: everywhere (fun _ => fail)) adamc@178: | PInr _ _ _ p' => fun succ fail => adamc@178: (everywhere (fun _ => fail), adamc@178: elaboratePat _ p' succ fail) adamc@178: end. adamc@178: adamc@178: Implicit Arguments elaboratePat [var t1 ts result]. adamc@178: adamc@178: Fixpoint letify var t ts {struct ts} : (hlist var ts -> exp var t) adamc@178: -> hlist (exp var) ts -> exp var t := adamc@178: match ts return ((hlist var ts -> exp var t) adamc@178: -> hlist (exp var) ts -> exp var t) with adamc@178: | nil => fun f _ => f tt adamc@178: | _ :: _ => fun f tup => letify _ (fun tup' => x <- fst tup; f (x, tup')) (snd tup) adamc@178: end. adamc@178: adamc@178: Implicit Arguments letify [var t ts]. adamc@178: adamc@178: Fixpoint expand var result t1 t2 adamc@178: (out : result -> exp var t2) {struct t1} adamc@178: : forall ct : choice_tree var t1 result, adamc@178: exp var t1 adamc@178: -> exp var t2 := adamc@178: match t1 return (forall ct : choice_tree var t1 result, exp var t1 adamc@178: -> exp var t2) with adamc@178: | (_ ** _)%source => fun ct disc => adamc@178: expand adamc@178: (fun ct' => expand out ct' (#2 disc)%source) adamc@178: ct adamc@178: (#1 disc) adamc@178: adamc@178: | (_ ++ _)%source => fun ct disc => adamc@178: Case disc adamc@178: (fun x => expand out (fst ct) (#x)) adamc@178: (fun y => expand out (snd ct) (#y)) adamc@178: adamc@178: | _ => fun ct disc => adamc@178: x <- disc; out (ct (#x)) adamc@178: end. adamc@178: adamc@178: Definition mergeOpt A (o1 o2 : option A) := adamc@178: match o1 with adamc@178: | None => o2 adamc@178: | _ => o1 adamc@178: end. adamc@178: adamc@178: Import Source. adamc@178: adamc@178: Fixpoint elaborateMatches var t1 t2 adamc@178: (tss : list (list type)) {struct tss} adamc@178: : (forall ts, member ts tss -> pat t1 ts) adamc@178: -> (forall ts, member ts tss -> hlist var ts -> Elab.exp var t2) adamc@178: -> choice_tree var t1 (option (Elab.exp var t2)) := adamc@178: match tss return (forall ts, member ts tss -> pat t1 ts) adamc@178: -> (forall ts, member ts tss -> _) adamc@178: -> _ with adamc@178: | nil => fun _ _ => adamc@178: everywhere (fun _ => None) adamc@178: | ts :: tss' => fun (ps : forall ts', member ts' (ts :: tss') -> pat t1 ts') adamc@178: (es : forall ts', member ts' (ts :: tss') -> hlist var ts' -> Elab.exp var t2) => adamc@178: merge (@mergeOpt _) adamc@178: (elaboratePat (ps _ (hfirst (refl_equal _))) adamc@178: (fun ts => Some (letify adamc@178: (fun ts' => es _ (hfirst (refl_equal _)) ts') adamc@178: ts)) adamc@178: None) adamc@178: (elaborateMatches tss' adamc@178: (fun _ mem => ps _ (hnext mem)) adamc@178: (fun _ mem => es _ (hnext mem))) adamc@178: end. adamc@178: adamc@178: Implicit Arguments elaborateMatches [var t1 t2 tss]. adamc@178: adamc@178: Open Scope cps_scope. adamc@178: adamc@178: Fixpoint elaborate var t (e : Source.exp var t) {struct e} : Elab.exp var t := adamc@178: match e in (Source.exp _ t) return (Elab.exp var t) with adamc@178: | Var _ v => #v adamc@178: adamc@178: | EUnit => () adamc@178: adamc@178: | App _ _ e1 e2 => elaborate e1 @ elaborate e2 adamc@178: | Abs _ _ e' => \x, elaborate (e' x) adamc@178: adamc@178: | Pair _ _ e1 e2 => [elaborate e1, elaborate e2] adamc@178: | EInl _ _ e' => Inl (elaborate e') adamc@178: | EInr _ _ e' => Inr (elaborate e') adamc@178: adamc@178: | Case _ _ _ e' ps es def => adamc@178: expand adamc@178: (fun eo => match eo with adamc@178: | None => elaborate def adamc@178: | Some e => e adamc@178: end) adamc@178: (elaborateMatches ps (fun _ mem env => elaborate (es _ mem env))) adamc@178: (elaborate e') adamc@178: end. adamc@178: End elaborate. adamc@178: adamc@178: Definition Elaborate t (E : Source.Exp t) : Elab.Exp t := adamc@178: fun _ => elaborate (E _). adamc@178: adamc@179: Fixpoint grab t result : choice_tree typeDenote t result -> typeDenote t -> result := adamc@179: match t return (choice_tree typeDenote t result -> typeDenote t -> result) with adamc@179: | t1 ** t2 => fun ct v => adamc@179: grab t2 _ (grab t1 _ ct (fst v)) (snd v) adamc@179: | t1 ++ t2 => fun ct v => adamc@179: match v with adamc@179: | inl v' => grab t1 _ (fst ct) v' adamc@179: | inr v' => grab t2 _ (snd ct) v' adamc@179: end adamc@179: | t => fun ct v => ct (#v)%elab adamc@179: end%source%type. adamc@179: adamc@179: Implicit Arguments grab [t result]. adamc@179: adamc@179: Ltac my_crush := adamc@179: crush; adamc@179: repeat (match goal with adamc@179: | [ |- context[match ?E with inl _ => _ | inr _ => _ end] ] => adamc@179: destruct E adamc@179: end; crush). adamc@179: adamc@179: Lemma expand_grab : forall t2 t1 result adamc@179: (out : result -> Elab.exp typeDenote t2) adamc@179: (ct : choice_tree typeDenote t1 result) adamc@179: (disc : Elab.exp typeDenote t1), adamc@179: Elab.expDenote (expand out ct disc) = Elab.expDenote (out (grab ct (Elab.expDenote disc))). adamc@179: induction t1; my_crush. adamc@179: Qed. adamc@179: adamc@179: Lemma recreate_pair : forall t1 t2 adamc@179: (x : Elab.exp typeDenote t1) adamc@179: (x0 : Elab.exp typeDenote t2) adamc@179: (v : typeDenote (t1 ** t2)), adamc@179: expDenote x = fst v adamc@179: -> expDenote x0 = snd v adamc@179: -> @eq (typeDenote t1 * typeDenote t2) (expDenote [x, x0]) v. adamc@179: destruct v; crush. adamc@179: Qed. adamc@179: adamc@179: Lemma everywhere_correct : forall t1 result adamc@179: (succ : Elab.exp typeDenote t1 -> result) disc, adamc@179: exists disc', grab (everywhere succ) (Elab.expDenote disc) = succ disc' adamc@179: /\ Elab.expDenote disc' = Elab.expDenote disc. adamc@179: Hint Resolve recreate_pair. adamc@179: adamc@179: induction t1; my_crush; eauto; fold choice_tree; adamc@179: repeat (fold typeDenote in *; crush; adamc@179: match goal with adamc@179: | [ IH : forall result succ, _ |- context[grab (everywhere ?S) _] ] => adamc@179: generalize (IH _ S); clear IH adamc@179: | [ e : exp typeDenote (?T ** _), IH : forall _ : exp typeDenote ?T, _ |- _ ] => adamc@179: generalize (IH (#1 e)); clear IH adamc@179: | [ e : exp typeDenote (_ ** ?T), IH : forall _ : exp typeDenote ?T, _ |- _ ] => adamc@179: generalize (IH (#2 e)); clear IH adamc@179: | [ e : typeDenote ?T, IH : forall _ : exp typeDenote ?T, _ |- _ ] => adamc@179: generalize (IH (#e)); clear IH adamc@179: end; crush); eauto. adamc@179: Qed. adamc@179: adamc@179: Lemma merge_correct : forall t result adamc@179: (ct1 ct2 : choice_tree typeDenote t result) adamc@179: (mr : result -> result -> result) v, adamc@179: grab (merge mr ct1 ct2) v = mr (grab ct1 v) (grab ct2 v). adamc@179: induction t; crush. adamc@179: Qed. adamc@179: adamc@179: Lemma everywhere_fail : forall t result adamc@179: (fail : result) v, adamc@179: grab (everywhere (fun _ : Elab.exp typeDenote t => fail)) v = fail. adamc@179: induction t; crush. adamc@179: Qed. adamc@179: adamc@179: Lemma elaboratePat_correct : forall t1 ts (p : pat t1 ts) adamc@179: result (succ : hlist (Elab.exp typeDenote) ts -> result) adamc@179: (fail : result) v env, adamc@179: patDenote p v = Some env adamc@179: -> exists env', grab (elaboratePat typeDenote p succ fail) v = succ env' adamc@179: /\ env = hmap Elab.expDenote env'. adamc@179: Hint Resolve hmap_happ. adamc@179: adamc@179: induction p; crush; fold choice_tree; adamc@179: repeat (match goal with adamc@179: | [ |- context[grab (everywhere ?succ) ?v] ] => adamc@179: generalize (everywhere_correct succ (#v)%elab) adamc@179: adamc@179: | [ H : forall result sudc fail, _ |- context[grab (elaboratePat _ _ ?S ?F) ?V] ] => adamc@179: generalize (H _ S F V); clear H adamc@179: | [ H1 : context[match ?E with Some _ => _ | None => _ end], adamc@179: H2 : forall env, ?E = Some env -> _ |- _ ] => adamc@179: destruct E adamc@179: | [ H : forall env, Some ?E = Some env -> _ |- _ ] => adamc@179: generalize (H _ (refl_equal _)); clear H adamc@179: end; crush); eauto. adamc@179: Qed. adamc@179: adamc@179: Lemma elaboratePat_fails : forall t1 ts (p : pat t1 ts) adamc@179: result (succ : hlist (Elab.exp typeDenote) ts -> result) adamc@179: (fail : result) v, adamc@179: patDenote p v = None adamc@179: -> grab (elaboratePat typeDenote p succ fail) v = fail. adamc@179: Hint Resolve everywhere_fail. adamc@179: adamc@179: induction p; try solve [ crush ]; adamc@179: simpl; fold choice_tree; intuition; simpl in *; adamc@179: repeat match goal with adamc@179: | [ IH : forall result succ fail v, patDenote ?P v = _ -> _ adamc@179: |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] => adamc@179: generalize (IH _ S F V); clear IH; intro IH; adamc@179: generalize (elaboratePat_correct P S F V); intros; adamc@179: destruct (patDenote P V); try discriminate adamc@179: | [ H : forall env, Some _ = Some env -> _ |- _ ] => adamc@179: destruct (H _ (refl_equal _)); clear H; intuition adamc@179: | [ H : _ |- _ ] => rewrite H; intuition adamc@179: end. adamc@179: Qed. adamc@179: adamc@179: Implicit Arguments letify [var t ts]. adamc@179: adamc@179: Lemma letify_correct : forall t ts (f : hlist typeDenote ts -> Elab.exp typeDenote t) adamc@179: (env : hlist (Elab.exp typeDenote) ts), adamc@179: Elab.expDenote (letify f env) adamc@179: = Elab.expDenote (f (hmap Elab.expDenote env)). adamc@179: induction ts; crush. adamc@179: Qed. adamc@179: adamc@179: Theorem elaborate_correct : forall t (e : Source.exp typeDenote t), adamc@179: Elab.expDenote (elaborate e) = Source.expDenote e. adamc@179: Hint Rewrite expand_grab merge_correct letify_correct : cpdt. adamc@179: Hint Rewrite everywhere_fail elaboratePat_fails using assumption : cpdt. adamc@179: adamc@179: induction e; crush; try (ext_eq; crush); adamc@179: match goal with adamc@179: | [ tss : list (list type) |- _ ] => adamc@179: induction tss; crush; adamc@179: match goal with adamc@179: | [ |- context[grab (elaboratePat _ ?P ?S ?F) ?V] ] => adamc@179: case_eq (patDenote P V); [intros env Heq; adamc@179: destruct (elaboratePat_correct P S F _ Heq); crush; adamc@179: match goal with adamc@179: | [ H : _ |- _ ] => rewrite <- H; crush adamc@179: end adamc@179: | crush ] adamc@179: end adamc@179: end. adamc@179: Qed. adamc@179: adamc@179: Theorem Elaborate_correct : forall t (E : Source.Exp t), adamc@179: Elab.ExpDenote (Elaborate E) = Source.ExpDenote E. adamc@179: unfold Elab.ExpDenote, Elaborate, Source.ExpDenote; adamc@179: intros; apply elaborate_correct. adamc@179: Qed. adamc@179: adamc@177: End PatMatch.