Mercurial > cpdt > repo

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