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@182: Require Import String List.
adamc@182: 
adamc@182: Require Import Axioms Tactics DepList.
adamc@182: 
adamc@182: Set Implicit Arguments.
adamc@182: (* end hide *)
adamc@182: 
adamc@182: 
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@182: Section 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@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@182:   Infix "@@" := App (no associativity, at level 75) : 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@182:   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@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@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: