--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Intensional.v	Sun Nov 16 11:54:51 2008 -0500
@@ -0,0 +1,271 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import String List.
+
+Require Import Axioms Tactics DepList.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{Intensional Transformations}% *)
+
+(** TODO: Prose for this chapter *)
+
+
+(** * Closure Conversion *)
+
+Module Source.
+  Inductive type : Type :=
+  | TNat : type
+  | Arrow : type -> type -> type.
+
+  Notation "'Nat'" := TNat : source_scope.
+  Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
+
+  Open Scope source_scope.
+  Bind Scope source_scope with type.
+  Delimit Scope source_scope with source.
+
+  Section vars.
+    Variable var : type -> Type.
+
+    Inductive exp : type -> Type :=
+    | Var : forall t,
+      var t
+      -> exp t
+
+    | Const : nat -> exp Nat
+    | Plus : exp Nat -> exp Nat -> exp Nat
+
+    | App : forall t1 t2,
+      exp (t1 --> t2)
+      -> exp t1
+      -> exp t2
+    | Abs : forall t1 t2,
+      (var t1 -> exp t2)
+      -> exp (t1 --> t2).
+  End vars.
+
+  Definition Exp t := forall var, exp var t.
+
+  Implicit Arguments Var [var t].
+  Implicit Arguments Const [var].
+  Implicit Arguments Plus [var].
+  Implicit Arguments App [var t1 t2].
+  Implicit Arguments Abs [var t1 t2].
+
+  Notation "# v" := (Var v) (at level 70) : source_scope.
+
+  Notation "^ n" := (Const n) (at level 70) : source_scope.
+  Infix "+^" := Plus (left associativity, at level 79) : source_scope.
+
+  Infix "@" := App (left associativity, at level 77) : source_scope.
+  Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
+  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
+
+  Bind Scope source_scope with exp.
+
+  Definition zero : Exp Nat := fun _ => ^0.
+  Definition one : Exp Nat := fun _ => ^1.
+  Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
+  Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
+  Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
+  Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
+    \f, \x, #f @ #x.
+  Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
+
+  Fixpoint typeDenote (t : type) : Set :=
+    match t with
+      | Nat => nat
+      | t1 --> t2 => typeDenote t1 -> typeDenote t2
+    end.
+
+  Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
+    match e in (exp _ t) return (typeDenote t) with
+      | Var _ v => v
+        
+      | Const n => n
+      | Plus e1 e2 => expDenote e1 + expDenote e2
+        
+      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
+      | Abs _ _ e' => fun x => expDenote (e' x)
+    end.
+
+  Definition ExpDenote t (e : Exp t) := expDenote (e _).
+
+  Section exp_equiv.
+    Variables var1 var2 : type -> Type.
+
+    Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
+    | EqVar : forall G t (v1 : var1 t) v2,
+      In (existT _ t (v1, v2)) G
+      -> exp_equiv G (#v1) (#v2)
+
+    | EqConst : forall G n,
+      exp_equiv G (^n) (^n)
+    | EqPlus : forall G x1 y1 x2 y2,
+      exp_equiv G x1 x2
+      -> exp_equiv G y1 y2
+      -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
+
+    | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
+      exp_equiv G f1 f2
+      -> exp_equiv G x1 x2
+      -> exp_equiv G (f1 @ x1) (f2 @ x2)
+    | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
+      (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
+      -> exp_equiv G (Abs f1) (Abs f2).
+  End exp_equiv.
+
+  Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
+    exp_equiv nil (E var1) (E var2).
+End Source.
+
+Section Closed.
+  Inductive type : Type :=
+  | TNat : type
+  | Arrow : type -> type -> type
+  | Code : type -> type -> type -> type
+  | Prod : type -> type -> type
+  | TUnit : type.
+
+  Notation "'Nat'" := TNat : cc_scope.
+  Notation "'Unit'" := TUnit : cc_scope.
+  Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
+  Infix "**" := Prod (right associativity, at level 59) : cc_scope.
+  Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
+
+  Bind Scope cc_scope with type.
+  Delimit Scope cc_scope with cc.
+
+  Open Local Scope cc_scope.
+
+  Section vars.
+    Variable var : type -> Set.
+
+    Inductive exp : type -> Type :=
+    | Var : forall t,
+      var t
+      -> exp t
+
+    | Const : nat -> exp Nat
+    | Plus : exp Nat -> exp Nat -> exp Nat
+
+    | App : forall dom ran,
+      exp (dom --> ran)
+      -> exp dom
+      -> exp ran
+
+    | Pack : forall env dom ran,
+      exp (env @@ dom ---> ran)
+      -> exp env
+      -> exp (dom --> ran)
+
+    | EUnit : exp Unit
+
+    | Pair : forall t1 t2,
+      exp t1
+      -> exp t2
+      -> exp (t1 ** t2)
+    | Fst : forall t1 t2,
+      exp (t1 ** t2)
+      -> exp t1
+    | Snd : forall t1 t2,
+      exp (t1 ** t2)
+      -> exp t2.
+
+    Section funcs.
+      Variable T : Type.
+
+      Inductive funcs : Type :=
+      | Main : T -> funcs
+      | Abs : forall env dom ran,
+        (var env -> var dom -> exp ran)
+        -> (var (env @@ dom ---> ran) -> funcs)
+        -> funcs.
+    End funcs.
+
+    Definition prog t := funcs (exp t).
+  End vars.
+
+  Implicit Arguments Var [var t].
+  Implicit Arguments Const [var].
+  Implicit Arguments EUnit [var].
+  Implicit Arguments Fst [var t1 t2].
+  Implicit Arguments Snd [var t1 t2].
+
+  Implicit Arguments Main [var T].
+  Implicit Arguments Abs [var T env dom ran].
+
+  Notation "# v" := (Var v) (at level 70) : cc_scope.
+
+  Notation "^ n" := (Const n) (at level 70) : cc_scope.
+  Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
+
+  Infix "@@" := App (no associativity, at level 75) : cc_scope.
+  Infix "##" := Pack (no associativity, at level 71) : cc_scope.
+
+  Notation "()" := EUnit : cc_scope.
+
+  Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
+  Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
+  Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
+
+  Notation "f <= \\ x , y , e ; fs" :=
+    (Abs (fun x y => e) (fun f => fs))
+    (right associativity, at level 80, e at next level) : cc_scope.
+
+  Bind Scope cc_scope with exp funcs prog.
+
+  Fixpoint typeDenote (t : type) : Set :=
+    match t with
+      | Nat => nat
+      | Unit => unit
+      | dom --> ran => typeDenote dom -> typeDenote ran
+      | t1 ** t2 => typeDenote t1 * typeDenote t2
+      | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
+    end%type.
+
+  Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
+    match e in (exp _ t) return (typeDenote t) with
+      | Var _ v => v
+
+      | Const n => n
+      | Plus e1 e2 => expDenote e1 + expDenote e2
+
+      | App _ _ f x => (expDenote f) (expDenote x)
+      | Pack _ _ _ f env => (expDenote f) (expDenote env)
+
+      | EUnit => tt
+
+      | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
+      | Fst _ _ e' => fst (expDenote e')
+      | Snd _ _ e' => snd (expDenote e')
+    end.
+
+  Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
+    match fs with
+      | Main v => v
+      | Abs _ _ _ e fs =>
+        funcsDenote (fs (fun env arg => expDenote (e env arg)))
+    end.
+
+  Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
+    expDenote (funcsDenote p).
+
+  Definition Exp t := forall var, exp var t.
+  Definition Prog t := forall var, prog var t.
+
+  Definition ExpDenote t (E : Exp t) := expDenote (E _).
+  Definition ProgDenote t (P : Prog t) := progDenote (P _).
+End Closed.
+