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@175: Require Import AxiomsImpred Tactics.
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@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@175:     Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : 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@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@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@175: End STLC.