Mercurial > cpdt > repo

comparison src/Hoas.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
232 232
233 Eval compute in CountVars zero. 233 Eval compute in CountVars zero.
234 (** %\vspace{-.15in}% [[ 234 (** %\vspace{-.15in}% [[
235 = 0 235 = 0
236 : nat 236 : nat
237 ]] *) 237 ]]
238 *)
238 239
239 Eval compute in CountVars one. 240 Eval compute in CountVars one.
240 (** %\vspace{-.15in}% [[ 241 (** %\vspace{-.15in}% [[
241 = 0 242 = 0
242 : nat 243 : nat
243 ]] *) 244 ]]
245 *)
244 246
245 Eval compute in CountVars one_again. 247 Eval compute in CountVars one_again.
246 (** %\vspace{-.15in}% [[ 248 (** %\vspace{-.15in}% [[
247 = 0 249 = 0
248 : nat 250 : nat
249 ]] *) 251 ]]
252 *)
250 253
251 Eval compute in CountVars ident. 254 Eval compute in CountVars ident.
252 (** %\vspace{-.15in}% [[ 255 (** %\vspace{-.15in}% [[
253 = 1 256 = 1
254 : nat 257 : nat
255 ]] *) 258 ]]
259 *)
256 260
257 Eval compute in CountVars app_ident. 261 Eval compute in CountVars app_ident.
258 (** %\vspace{-.15in}% [[ 262 (** %\vspace{-.15in}% [[
259 = 1 263 = 1
260 : nat 264 : nat
261 ]] *) 265 ]]
266 *)
262 267
263 Eval compute in CountVars app. 268 Eval compute in CountVars app.
264 (** %\vspace{-.15in}% [[ 269 (** %\vspace{-.15in}% [[
265 = 2 270 = 2
266 : nat 271 : nat
267 ]] *) 272 ]]
273 *)
268 274
269 Eval compute in CountVars app_ident'. 275 Eval compute in CountVars app_ident'.
270 (** %\vspace{-.15in}% [[ 276 (** %\vspace{-.15in}% [[
271 = 3 277 = 3
272 : nat 278 : nat
273 ]] *) 279 ]]
280 *)
274 281
275 282
276 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) 283 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
277 284
278 (** We might want to go further and count occurrences of a single distinguished free variable in an expression. In this case, it is useful to instantiate [var] as [fun _ => bool]. We will represent the distinguished variable with [true] and all other variables with [false]. *) 285 (** We might want to go further and count occurrences of a single distinguished free variable in an expression. In this case, it is useful to instantiate [var] as [fun _ => bool]. We will represent the distinguished variable with [true] and all other variables with [false]. *)
304 311
305 Eval compute in CountOne ident1. 312 Eval compute in CountOne ident1.
306 (** %\vspace{-.15in}% [[ 313 (** %\vspace{-.15in}% [[
307 = 1 314 = 1
308 : nat 315 : nat
309 ]] *) 316 ]]
317 *)
310 318
311 Eval compute in CountOne add_self. 319 Eval compute in CountOne add_self.
312 (** %\vspace{-.15in}% [[ 320 (** %\vspace{-.15in}% [[
313 = 2 321 = 2
314 : nat 322 : nat
315 ]] *) 323 ]]
324 *)
316 325
317 Eval compute in CountOne app_zero. 326 Eval compute in CountOne app_zero.
318 (** %\vspace{-.15in}% [[ 327 (** %\vspace{-.15in}% [[
319 = 1 328 = 1
320 : nat 329 : nat
321 ]] *) 330 ]]
331 *)
322 332
323 Eval compute in CountOne app_ident1. 333 Eval compute in CountOne app_ident1.
324 (** %\vspace{-.15in}% [[ 334 (** %\vspace{-.15in}% [[
325 = 1 335 = 1
326 : nat 336 : nat
327 ]] *) 337 ]]
338 *)
328 339
329 340
330 (* EX: Define a function to pretty-print [Exp]s as strings. *) 341 (* EX: Define a function to pretty-print [Exp]s as strings. *)
331 342
332 (** The PHOAS encoding turns out to be just as general as the first-order encodings we saw previously. To provide a taste of that generality, we implement a translation into concrete syntax, rendered in human-readable strings. This is as easy as representing variables as strings. *) 343 (** The PHOAS encoding turns out to be just as general as the first-order encodings we saw previously. To provide a taste of that generality, we implement a translation into concrete syntax, rendered in human-readable strings. This is as easy as representing variables as strings. *)
366 377
367 Eval compute in ToString zero. 378 Eval compute in ToString zero.
368 (** %\vspace{-.15in}% [[ 379 (** %\vspace{-.15in}% [[
369 = "O"%string 380 = "O"%string
370 : string 381 : string
371 ]] *) 382 ]]
383 *)
372 384
373 Eval compute in ToString one. 385 Eval compute in ToString one.
374 (** %\vspace{-.15in}% [[ 386 (** %\vspace{-.15in}% [[
375 = "S(O)"%string 387 = "S(O)"%string
376 : string 388 : string
377 ]] *) 389 ]]
390 *)
378 391
379 Eval compute in ToString one_again. 392 Eval compute in ToString one_again.
380 (** %\vspace{-.15in}% [[ 393 (** %\vspace{-.15in}% [[
381 = "(O) + (S(O))"%string 394 = "(O) + (S(O))"%string
382 : string 395 : string
383 ]] *) 396 ]]
397 *)
384 398
385 Eval compute in ToString ident. 399 Eval compute in ToString ident.
386 (** %\vspace{-.15in}% [[ 400 (** %\vspace{-.15in}% [[
387 = "(\x, x)"%string 401 = "(\x, x)"%string
388 : string 402 : string
389 ]] *) 403 ]]
404 *)
390 405
391 Eval compute in ToString app_ident. 406 Eval compute in ToString app_ident.
392 (** %\vspace{-.15in}% [[ 407 (** %\vspace{-.15in}% [[
393 = "((\x, x)) ((O) + (S(O)))"%string 408 = "((\x, x)) ((O) + (S(O)))"%string
394 : string 409 : string
395 ]] *) 410 ]]
411 *)
396 412
397 Eval compute in ToString app. 413 Eval compute in ToString app.
398 (** %\vspace{-.15in}% [[ 414 (** %\vspace{-.15in}% [[
399 = "(\x, (\x', (x) (x')))"%string 415 = "(\x, (\x', (x) (x')))"%string
400 : string 416 : string
401 ]] *) 417 ]]
418 *)
402 419
403 Eval compute in ToString app_ident'. 420 Eval compute in ToString app_ident'.
404 (** %\vspace{-.15in}% [[ 421 (** %\vspace{-.15in}% [[
405 = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string 422 = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string
406 : string 423 : string
407 ]] *) 424 ]]
425 *)
408 426
409 427
410 (* EX: Define a substitution function. *) 428 (* EX: Define a substitution function. *)
411 429
412 (** Our final example is crucial to using PHOAS to encode standard operational semantics. We define capture-avoiding substitution, in terms of a function [flatten] which takes in an expression that represents variables as expressions. [flatten] replaces every node [Var e] with [e]. *) 430 (** Our final example is crucial to using PHOAS to encode standard operational semantics. We define capture-avoiding substitution, in terms of a function [flatten] which takes in an expression that represents variables as expressions. [flatten] replaces every node [Var e] with [e]. *)
433 451
434 Eval compute in Subst one ident1. 452 Eval compute in Subst one ident1.
435 (** %\vspace{-.15in}% [[ 453 (** %\vspace{-.15in}% [[
436 = fun var : type -> Type => Const' 1 454 = fun var : type -> Type => Const' 1
437 : Exp Nat 455 : Exp Nat
438 ]] *) 456 ]]
457 *)
439 458
440 Eval compute in Subst one add_self. 459 Eval compute in Subst one add_self.
441 (** %\vspace{-.15in}% [[ 460 (** %\vspace{-.15in}% [[
442 = fun var : type -> Type => Plus' (Const' 1) (Const' 1) 461 = fun var : type -> Type => Plus' (Const' 1) (Const' 1)
443 : Exp Nat 462 : Exp Nat
444 ]] *) 463 ]]
464 *)
445 465
446 Eval compute in Subst ident app_zero. 466 Eval compute in Subst ident app_zero.
447 (** %\vspace{-.15in}% [[ 467 (** %\vspace{-.15in}% [[
448 = fun var : type -> Type => 468 = fun var : type -> Type =>
449 App' (Abs' (fun X : var Nat => Var X)) (Const' 0) 469 App' (Abs' (fun X : var Nat => Var X)) (Const' 0)
450 : Exp Nat 470 : Exp Nat
451 ]] *) 471 ]]
472 *)
452 473
453 Eval compute in Subst one app_ident1. 474 Eval compute in Subst one app_ident1.
454 (** %\vspace{-.15in}% [[ 475 (** %\vspace{-.15in}% [[
455 = fun var : type -> Type => 476 = fun var : type -> Type =>
456 App' (Abs' (fun x : var Nat => Var x)) (Const' 1) 477 App' (Abs' (fun x : var Nat => Var x)) (Const' 1)
457 : Exp Nat 478 : Exp Nat
458 ]] *) 479 ]]
480 *)
459 481
460 482
461 (** * A Type Soundness Proof *) 483 (** * A Type Soundness Proof *)
462 484
463 (** With [Subst] defined, there are few surprises encountered in defining a standard small-step, call-by-value semantics for our object language. We begin by classifying a subset of expressions as values. *) 485 (** With [Subst] defined, there are few surprises encountered in defining a standard small-step, call-by-value semantics for our object language. We begin by classifying a subset of expressions as values. *)