Mercurial > cpdt > repo

annotate src/Extensional.v @ 175:022feabdff50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
STLC cpsExp
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 11:05:49 -0500
parents
children 9b1f58dbc464
rev   line source
adamc@175 1 (* Copyright (c) 2008, Adam Chlipala
adamc@175 2 *
adamc@175 3 * This work is licensed under a
adamc@175 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@175 5 * Unported License.
adamc@175 6 * The license text is available at:
adamc@175 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@175 8 *)
adamc@175 9
adamc@175 10 (* begin hide *)
adamc@175 11 Require Import String List.
adamc@175 12
adamc@175 13 Require Import AxiomsImpred Tactics.
adamc@175 14
adamc@175 15 Set Implicit Arguments.
adamc@175 16 (* end hide *)
adamc@175 17
adamc@175 18
adamc@175 19 (** %\chapter{Certifying Extensional Transformations}% *)
adamc@175 20
adamc@175 21 (** TODO: Prose for this chapter *)
adamc@175 22
adamc@175 23
adamc@175 24 (** * Simply-Typed Lambda Calculus *)
adamc@175 25
adamc@175 26 Module STLC.
adamc@175 27 Module Source.
adamc@175 28 Inductive type : Type :=
adamc@175 29 | TNat : type
adamc@175 30 | Arrow : type -> type -> type.
adamc@175 31
adamc@175 32 Notation "'Nat'" := TNat : source_scope.
adamc@175 33 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@175 34
adamc@175 35 Open Scope source_scope.
adamc@175 36 Bind Scope source_scope with type.
adamc@175 37 Delimit Scope source_scope with source.
adamc@175 38
adamc@175 39 Section vars.
adamc@175 40 Variable var : type -> Type.
adamc@175 41
adamc@175 42 Inductive exp : type -> Type :=
adamc@175 43 | Var : forall t,
adamc@175 44 var t
adamc@175 45 -> exp t
adamc@175 46
adamc@175 47 | Const : nat -> exp Nat
adamc@175 48 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@175 49
adamc@175 50 | App : forall t1 t2,
adamc@175 51 exp (t1 --> t2)
adamc@175 52 -> exp t1
adamc@175 53 -> exp t2
adamc@175 54 | Abs : forall t1 t2,
adamc@175 55 (var t1 -> exp t2)
adamc@175 56 -> exp (t1 --> t2).
adamc@175 57 End vars.
adamc@175 58
adamc@175 59 Definition Exp t := forall var, exp var t.
adamc@175 60
adamc@175 61 Implicit Arguments Var [var t].
adamc@175 62 Implicit Arguments Const [var].
adamc@175 63 Implicit Arguments Plus [var].
adamc@175 64 Implicit Arguments App [var t1 t2].
adamc@175 65 Implicit Arguments Abs [var t1 t2].
adamc@175 66
adamc@175 67 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@175 68
adamc@175 69 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@175 70 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@175 71
adamc@175 72 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@175 73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@175 74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@175 75
adamc@175 76 Bind Scope source_scope with exp.
adamc@175 77
adamc@175 78 Definition zero : Exp Nat := fun _ => ^0.
adamc@175 79 Definition one : Exp Nat := fun _ => ^1.
adamc@175 80 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@175 81 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@175 82 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@175 83 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@175 84 \f, \x, #f @ #x.
adamc@175 85 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@175 86
adamc@175 87 Fixpoint typeDenote (t : type) : Set :=
adamc@175 88 match t with
adamc@175 89 | Nat => nat
adamc@175 90 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@175 91 end.
adamc@175 92
adamc@175 93 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@175 94 match e in (exp _ t) return (typeDenote t) with
adamc@175 95 | Var _ v => v
adamc@175 96
adamc@175 97 | Const n => n
adamc@175 98 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@175 99
adamc@175 100 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@175 101 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@175 102 end.
adamc@175 103
adamc@175 104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@175 105 End Source.
adamc@175 106
adamc@175 107 Module CPS.
adamc@175 108 Inductive type : Type :=
adamc@175 109 | TNat : type
adamc@175 110 | Cont : type -> type
adamc@175 111 | TUnit : type
adamc@175 112 | Prod : type -> type -> type.
adamc@175 113
adamc@175 114 Notation "'Nat'" := TNat : cps_scope.
adamc@175 115 Notation "'Unit'" := TUnit : cps_scope.
adamc@175 116 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
adamc@175 117 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
adamc@175 118
adamc@175 119 Bind Scope cps_scope with type.
adamc@175 120 Delimit Scope cps_scope with cps.
adamc@175 121
adamc@175 122 Section vars.
adamc@175 123 Variable var : type -> Type.
adamc@175 124
adamc@175 125 Inductive prog : Type :=
adamc@175 126 | PHalt :
adamc@175 127 var Nat
adamc@175 128 -> prog
adamc@175 129 | App : forall t,
adamc@175 130 var (t --->)
adamc@175 131 -> var t
adamc@175 132 -> prog
adamc@175 133 | Bind : forall t,
adamc@175 134 primop t
adamc@175 135 -> (var t -> prog)
adamc@175 136 -> prog
adamc@175 137
adamc@175 138 with primop : type -> Type :=
adamc@175 139 | Var : forall t,
adamc@175 140 var t
adamc@175 141 -> primop t
adamc@175 142
adamc@175 143 | Const : nat -> primop Nat
adamc@175 144 | Plus : var Nat -> var Nat -> primop Nat
adamc@175 145
adamc@175 146 | Abs : forall t,
adamc@175 147 (var t -> prog)
adamc@175 148 -> primop (t --->)
adamc@175 149
adamc@175 150 | Pair : forall t1 t2,
adamc@175 151 var t1
adamc@175 152 -> var t2
adamc@175 153 -> primop (t1 ** t2)
adamc@175 154 | Fst : forall t1 t2,
adamc@175 155 var (t1 ** t2)
adamc@175 156 -> primop t1
adamc@175 157 | Snd : forall t1 t2,
adamc@175 158 var (t1 ** t2)
adamc@175 159 -> primop t2.
adamc@175 160 End vars.
adamc@175 161
adamc@175 162 Implicit Arguments PHalt [var].
adamc@175 163 Implicit Arguments App [var t].
adamc@175 164
adamc@175 165 Implicit Arguments Var [var t].
adamc@175 166 Implicit Arguments Const [var].
adamc@175 167 Implicit Arguments Plus [var].
adamc@175 168 Implicit Arguments Abs [var t].
adamc@175 169 Implicit Arguments Pair [var t1 t2].
adamc@175 170 Implicit Arguments Fst [var t1 t2].
adamc@175 171 Implicit Arguments Snd [var t1 t2].
adamc@175 172
adamc@175 173 Notation "'Halt' x" := (PHalt x) (no associativity, at level 75) : cps_scope.
adamc@175 174 Infix "@@" := App (no associativity, at level 75) : cps_scope.
adamc@175 175 Notation "x <- p ; e" := (Bind p (fun x => e))
adamc@175 176 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 177 Notation "! <- p ; e" := (Bind p (fun _ => e))
adamc@175 178 (right associativity, at level 76, p at next level) : cps_scope.
adamc@175 179
adamc@175 180 Notation "# v" := (Var v) (at level 70) : cps_scope.
adamc@175 181
adamc@175 182 Notation "^ n" := (Const n) (at level 70) : cps_scope.
adamc@175 183 Infix "+^" := Plus (left associativity, at level 79) : cps_scope.
adamc@175 184
adamc@175 185 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : cps_scope.
adamc@175 186 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : cps_scope.
adamc@175 187
adamc@175 188 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cps_scope.
adamc@175 189 Notation "#1 x" := (Fst x) (at level 72) : cps_scope.
adamc@175 190 Notation "#2 x" := (Snd x) (at level 72) : cps_scope.
adamc@175 191
adamc@175 192 Bind Scope cps_scope with prog primop.
adamc@175 193
adamc@175 194 Open Scope cps_scope.
adamc@175 195
adamc@175 196 Fixpoint typeDenote (t : type) : Set :=
adamc@175 197 match t with
adamc@175 198 | Nat => nat
adamc@175 199 | t' ---> => typeDenote t' -> nat
adamc@175 200 | Unit => unit
adamc@175 201 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type
adamc@175 202 end.
adamc@175 203
adamc@175 204 Fixpoint progDenote (e : prog typeDenote) : nat :=
adamc@175 205 match e with
adamc@175 206 | PHalt n => n
adamc@175 207 | App _ f x => f x
adamc@175 208 | Bind _ p x => progDenote (x (primopDenote p))
adamc@175 209 end
adamc@175 210
adamc@175 211 with primopDenote t (p : primop typeDenote t) {struct p} : typeDenote t :=
adamc@175 212 match p in (primop _ t) return (typeDenote t) with
adamc@175 213 | Var _ v => v
adamc@175 214
adamc@175 215 | Const n => n
adamc@175 216 | Plus n1 n2 => n1 + n2
adamc@175 217
adamc@175 218 | Abs _ e => fun x => progDenote (e x)
adamc@175 219
adamc@175 220 | Pair _ _ v1 v2 => (v1, v2)
adamc@175 221 | Fst _ _ v => fst v
adamc@175 222 | Snd _ _ v => snd v
adamc@175 223 end.
adamc@175 224
adamc@175 225 Definition Prog := forall var, prog var.
adamc@175 226 Definition Primop t := forall var, primop var t.
adamc@175 227 Definition ProgDenote (E : Prog) := progDenote (E _).
adamc@175 228 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
adamc@175 229 End CPS.
adamc@175 230
adamc@175 231 Import Source CPS.
adamc@175 232
adamc@175 233 Fixpoint cpsType (t : Source.type) : CPS.type :=
adamc@175 234 match t with
adamc@175 235 | Nat => Nat%cps
adamc@175 236 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
adamc@175 237 end%source.
adamc@175 238
adamc@175 239 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
adamc@175 240
adamc@175 241 Section cpsExp.
adamc@175 242 Variable var : CPS.type -> Type.
adamc@175 243
adamc@175 244 Import Source.
adamc@175 245 Open Scope cps_scope.
adamc@175 246
adamc@175 247 Fixpoint cpsExp t (e : exp (fun t => var (cpsType t)) t) {struct e}
adamc@175 248 : (var (cpsType t) -> prog var) -> prog var :=
adamc@175 249 match e in (exp _ t) return ((var (cpsType t) -> prog var) -> prog var) with
adamc@175 250 | Var _ v => fun k => k v
adamc@175 251
adamc@175 252 | Const n => fun k =>
adamc@175 253 x <- ^n;
adamc@175 254 k x
adamc@175 255 | Plus e1 e2 => fun k =>
adamc@175 256 x1 <-- e1;
adamc@175 257 x2 <-- e2;
adamc@175 258 x <- x1 +^ x2;
adamc@175 259 k x
adamc@175 260
adamc@175 261 | App _ _ e1 e2 => fun k =>
adamc@175 262 f <-- e1;
adamc@175 263 x <-- e2;
adamc@175 264 kf <- \r, k r;
adamc@175 265 p <- [x, kf];
adamc@175 266 f @@ p
adamc@175 267 | Abs _ _ e' => fun k =>
adamc@175 268 f <- CPS.Abs (var := var) (fun p =>
adamc@175 269 x <- #1 p;
adamc@175 270 kf <- #2 p;
adamc@175 271 r <-- e' x;
adamc@175 272 kf @@ r);
adamc@175 273 k f
adamc@175 274 end
adamc@175 275
adamc@175 276 where "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)).
adamc@175 277 End cpsExp.
adamc@175 278
adamc@175 279 Notation "x <-- e1 ; e2" := (cpsExp e1 (fun x => e2)) : cps_scope.
adamc@175 280 Notation "! <-- e1 ; e2" := (cpsExp e1 (fun _ => e2))
adamc@175 281 (right associativity, at level 76, e1 at next level) : cps_scope.
adamc@175 282
adamc@175 283 Implicit Arguments cpsExp [var t].
adamc@175 284 Definition CpsExp (E : Exp Nat) : Prog :=
adamc@175 285 fun var => cpsExp (E _) (PHalt (var := _)).
adamc@175 286
adamc@175 287 Eval compute in CpsExp zero.
adamc@175 288 Eval compute in CpsExp one.
adamc@175 289 Eval compute in CpsExp zpo.
adamc@175 290 Eval compute in CpsExp app_ident.
adamc@175 291 Eval compute in CpsExp app_ident'.
adamc@175 292
adamc@175 293 Eval compute in ProgDenote (CpsExp zero).
adamc@175 294 Eval compute in ProgDenote (CpsExp one).
adamc@175 295 Eval compute in ProgDenote (CpsExp zpo).
adamc@175 296 Eval compute in ProgDenote (CpsExp app_ident).
adamc@175 297 Eval compute in ProgDenote (CpsExp app_ident').
adamc@175 298
adamc@175 299 End STLC.