Mercurial > cpdt > repo

comparison src/Extensional.v @ 292:2c88fc1dbe33

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of double-quotes and LaTeX operator beautification
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 16:31:04 -0500
parents 108ec446fbaf
children b441010125d4
comparison
equal deleted inserted replaced
291:da9ccc6bf572 292:2c88fc1dbe33
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
35 | TNat : type 35 | TNat : type
36 | Arrow : type -> type -> type. 36 | Arrow : type -> type -> type.
37 (* end hide *) 37 (* end hide *)
38 38
39 Notation "'Nat'" := TNat : source_scope. 39 Notation "'Nat'" := TNat : source_scope.
40 (** printing --> $\longrightarrow$ *)
40 Infix "-->" := Arrow (right associativity, at level 60) : source_scope. 41 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
41 42
42 Open Scope source_scope. 43 Open Scope source_scope.
43 Bind Scope source_scope with type. 44 Bind Scope source_scope with type.
44 Delimit Scope source_scope with source. 45 Delimit Scope source_scope with source.
125 | EqVar : forall G t (v1 : var1 t) v2, 126 | EqVar : forall G t (v1 : var1 t) v2,
126 In (existT _ t (v1, v2)) G 127 In (existT _ t (v1, v2)) G
127 -> exp_equiv G (#v1) (#v2) 128 -> exp_equiv G (#v1) (#v2)
128 129
129 | EqConst : forall G n, 130 | EqConst : forall G n,
130 exp_equiv G (^n) (^n) 131 exp_equiv G (^ n) (^ n)
131 | EqPlus : forall G x1 y1 x2 y2, 132 | EqPlus : forall G x1 y1 x2 y2,
132 exp_equiv G x1 x2 133 exp_equiv G x1 x2
133 -> exp_equiv G y1 y2 134 -> exp_equiv G y1 y2
134 -> exp_equiv G (x1 +^ y1) (x2 +^ y2) 135 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
135 136
156 | TNat : type 157 | TNat : type
157 | Cont : type -> type 158 | Cont : type -> type
158 | Prod : type -> type -> type. 159 | Prod : type -> type -> type.
159 160
160 Notation "'Nat'" := TNat : cps_scope. 161 Notation "'Nat'" := TNat : cps_scope.
162 (** printing ---> $\Longrightarrow$ *)
161 Notation "t --->" := (Cont t) (at level 61) : cps_scope. 163 Notation "t --->" := (Cont t) (at level 61) : cps_scope.
162 Infix "**" := Prod (right associativity, at level 60) : cps_scope. 164 Infix "**" := Prod (right associativity, at level 60) : cps_scope.
163 165
164 Bind Scope cps_scope with type. 166 Bind Scope cps_scope with type.
165 Delimit Scope cps_scope with cps. 167 Delimit Scope cps_scope with cps.
275 277
276 (* begin thide *) 278 (* begin thide *)
277 Fixpoint cpsType (t : Source.type) : CPS.type := 279 Fixpoint cpsType (t : Source.type) : CPS.type :=
278 match t with 280 match t with
279 | Nat => Nat%cps 281 | Nat => Nat%cps
280 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps 282 | t1 --> t2 => (cpsType t1 ** (cpsType t2 ---> ) ---> )%cps
281 end%source. 283 end%source.
282 284
283 (** Now we can define the expression translation. The notation [x <-- e1; e2] stands for translating source-level expression [e1], binding [x] to the CPS-level result of running the translated program, and then evaluating CPS-level expression [e2] in that context. *) 285 (** Now we can define the expression translation. The notation [x <-- e1; e2] stands for translating source-level expression [e1], binding [x] to the CPS-level result of running the translated program, and then evaluating CPS-level expression [e2] in that context. *)
284 286
287 (** printing <-- $\longleftarrow$ *)
285 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). 288 Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level).
286 289
287 Section cpsExp. 290 Section cpsExp.
288 Variable var : CPS.type -> Type. 291 Variable var : CPS.type -> Type.
289 292
296 : (var (cpsType t) -> prog var) -> prog var := 299 : (var (cpsType t) -> prog var) -> prog var :=
297 match e with 300 match e with
298 | Var _ v => fun k => k v 301 | Var _ v => fun k => k v
299 302
300 | Const n => fun k => 303 | Const n => fun k =>
301 x <- ^n; 304 x <- ^ n;
302 k x 305 k x
303 | Plus e1 e2 => fun k => 306 | Plus e1 e2 => fun k =>
304 x1 <-- e1; 307 x1 <-- e1;
305 x2 <-- e2; 308 x2 <-- e2;
306 x <- x1 +^ x2; 309 x <- x1 +^ x2;
307 k x 310 k x
308 311
309 | App _ _ e1 e2 => fun k => 312 | App _ _ e1 e2 => fun k =>
310 f <-- e1; 313 f <-- e1;
311 x <-- e2; 314 x <-- e2;
312 kf <- \r, k r; 315 kf <- \ r, k r;
313 p <- [x, kf]; 316 p <- [x, kf];
314 f @@ p 317 f @@ p
315 | Abs _ _ e' => fun k => 318 | Abs _ _ e' => fun k =>
316 f <- CPS.Abs (var := var) (fun p => 319 f <- CPS.Abs (var := var) (fun p =>
317 x <- #1 p; 320 x <- #1 p;