Mercurial > cpdt > repo

comparison src/Extensional.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
341 341
342 Eval compute in CpsExp zero. 342 Eval compute in CpsExp zero.
343 (** %\vspace{-.15in}% [[ 343 (** %\vspace{-.15in}% [[
344 = fun var : type -> Type => x <- ^0; Halt x 344 = fun var : type -> Type => x <- ^0; Halt x
345 : Prog 345 : Prog
346 ]] *) 346 ]]
347 *)
347 348
348 Eval compute in CpsExp one. 349 Eval compute in CpsExp one.
349 (** %\vspace{-.15in}% [[ 350 (** %\vspace{-.15in}% [[
350 = fun var : type -> Type => x <- ^1; Halt x 351 = fun var : type -> Type => x <- ^1; Halt x
351 : Prog 352 : Prog
352 ]] *) 353 ]]
354 *)
353 355
354 Eval compute in CpsExp zpo. 356 Eval compute in CpsExp zpo.
355 (** %\vspace{-.15in}% [[ 357 (** %\vspace{-.15in}% [[
356 = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1 358 = fun var : type -> Type => x <- ^0; x0 <- ^1; x1 <- (x +^ x0); Halt x1
357 : Prog 359 : Prog
358 ]] *) 360 ]]
361 *)
359 362
360 Eval compute in CpsExp app_ident. 363 Eval compute in CpsExp app_ident.
361 (** %\vspace{-.15in}% [[ 364 (** %\vspace{-.15in}% [[
362 = fun var : type -> Type => 365 = fun var : type -> Type =>
363 f <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x); 366 f <- (\ p, x <- #1 p; kf <- #2 p; kf @@ x);
364 x <- ^0; 367 x <- ^0;
365 x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p 368 x0 <- ^1; x1 <- (x +^ x0); kf <- (\ r, Halt r); p <- [x1, kf]; f @@ p
366 : Prog 369 : Prog
367 ]] *) 370 ]]
371 *)
368 372
369 Eval compute in CpsExp app_ident'. 373 Eval compute in CpsExp app_ident'.
370 (** %\vspace{-.15in}% [[ 374 (** %\vspace{-.15in}% [[
371 = fun var : type -> Type => 375 = fun var : type -> Type =>
372 f <- 376 f <-
384 x <- ^0; 388 x <- ^0;
385 x0 <- ^1; 389 x0 <- ^1;
386 x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p); 390 x1 <- (x +^ x0); kf <- (\ r0, Halt r0); p <- [x1, kf]; r @@ p);
387 p <- [f0, kf]; f @@ p 391 p <- [f0, kf]; f @@ p
388 : Prog 392 : Prog
389 ]] *) 393 ]]
394 *)
390 395
391 Eval compute in ProgDenote (CpsExp zero). 396 Eval compute in ProgDenote (CpsExp zero).
392 (** %\vspace{-.15in}% [[ 397 (** %\vspace{-.15in}% [[
393 = 0 398 = 0
394 : nat 399 : nat
395 ]] *) 400 ]]
401 *)
396 402
397 Eval compute in ProgDenote (CpsExp one). 403 Eval compute in ProgDenote (CpsExp one).
398 (** %\vspace{-.15in}% [[ 404 (** %\vspace{-.15in}% [[
399 = 1 405 = 1
400 : nat 406 : nat
401 ]] *) 407 ]]
408 *)
402 409
403 Eval compute in ProgDenote (CpsExp zpo). 410 Eval compute in ProgDenote (CpsExp zpo).
404 (** %\vspace{-.15in}% [[ 411 (** %\vspace{-.15in}% [[
405 = 1 412 = 1
406 : nat 413 : nat
407 ]] *) 414 ]]
415 *)
408 416
409 Eval compute in ProgDenote (CpsExp app_ident). 417 Eval compute in ProgDenote (CpsExp app_ident).
410 (** %\vspace{-.15in}% [[ 418 (** %\vspace{-.15in}% [[
411 = 1 419 = 1
412 : nat 420 : nat
413 ]] *) 421 ]]
422 *)
414 423
415 Eval compute in ProgDenote (CpsExp app_ident'). 424 Eval compute in ProgDenote (CpsExp app_ident').
416 (** %\vspace{-.15in}% [[ 425 (** %\vspace{-.15in}% [[
417 = 1 426 = 1
418 : nat 427 : nat
419 ]] *) 428 ]]
429 *)
420 430
421 431
422 (** Our main inductive lemma about [cpsExp] needs a notion of compatibility between source-level and CPS-level values. We express compatibility with a %\textit{%#<i>#logical relation#</i>#%}%; that is, we define a binary relation by recursion on type structure, and the function case of the relation considers functions related if they map related arguments to related results. In detail, the function case is slightly more complicated, since it must deal with our continuation-based calling convention. *) 432 (** Our main inductive lemma about [cpsExp] needs a notion of compatibility between source-level and CPS-level values. We express compatibility with a %\textit{%#<i>#logical relation#</i>#%}%; that is, we define a binary relation by recursion on type structure, and the function case of the relation considers functions related if they map related arguments to related results. In detail, the function case is slightly more complicated, since it must deal with our continuation-based calling convention. *)
423 433
424 (* begin thide *) 434 (* begin thide *)