Mercurial > cpdt > repo
diff src/OpSem.v @ 292:2c88fc1dbe33
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 | dce88a5c170c |
children | d5787b70cf48 |
line wrap: on
line diff
--- a/src/OpSem.v Wed Nov 10 15:42:05 2010 -0500 +++ b/src/OpSem.v Wed Nov 10 16:31:04 2010 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2009, Adam Chlipala +(* Copyright (c) 2009-2010, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -20,7 +20,7 @@ (** The last few chapters have shown how PHOAS can make it relatively painless to reason about program transformations. Each of our example languages so far has had a semantics that is easy to implement with an interpreter in Gallina. Since Gallina is designed to rule out non-termination, we cannot hope to give interpreter-based semantics to Turing-complete programming languages. Falling back on standard operational semantics leaves us with the old bureaucratic concerns about capture-avoiding substitution. Can we encode Turing-complete, higher-order languages in Coq without sacrificing the advantages of higher-order encoding? - Any approach that applies to basic untyped lambda calculus is likely to extend to most object languages of interest. We can attempt the "obvious" way of equipping a PHOAS definition for use in an operational semantics, without mentioning substitution explicitly. Specifically, we try to work with expressions with [var] instantiated with a type of values. *) + Any approach that applies to basic untyped lambda calculus is likely to extend to most object languages of interest. We can attempt the %``%#"#obvious#"#%''% way of equipping a PHOAS definition for use in an operational semantics, without mentioning substitution explicitly. Specifically, we try to work with expressions with [var] instantiated with a type of values. *) Section exp. Variable var : Type. @@ -58,7 +58,7 @@ ]] - Of course, this kind of definition is not structurally recursive, so Coq will not allow it. Getting "substitution for free" seems to require some similar kind of self-reference. + Of course, this kind of definition is not structurally recursive, so Coq will not allow it. Getting %``%#"#substitution for free#"#%''% seems to require some similar kind of self-reference. In this chapter, we will consider an alternate take on the problem. We add a level of indirection, introducing more explicit syntax to break the cycle in type definitions. Specifically, we represent function values as numbers that index into a %\emph{%#<i>#closure heap#</i>#%}% that our operational semantics maintains alongside the expression being evaluated. *) @@ -83,6 +83,7 @@ (** The second of our two definitions expresses when one list extends another. We will write [ls1 ~> ls2] to indicate that [ls1] could evolve into [ls2]; that is, [ls1] is a suffix of [ls2]. *) Definition extends (ls1 ls2 : list A) := exists ls, ls2 = ls ++ ls1. + (** printing ~> $\leadsto$ *) Infix "~>" := extends (no associativity, at level 80). (** We prove and add as hints a few basic theorems about [lookup] and [extends]. *) @@ -292,6 +293,7 @@ (** Finally, we define a CPS translation in the same way as in our previous example for simply-typed lambda calculus. *) +(** printing <-- $\longleftarrow$ *) Reserved Notation "x <-- e1 ; e2" (right associativity, at level 76, e1 at next level). Section cpsExp. @@ -364,6 +366,8 @@ -> cr (Source.VFun l1) (CPS.VFun l2). End cr. +(** printing |-- $\vdash$ *) +(** printing ~~ $\sim$ *) Notation "s1 & s2 |-- v1 ~~ v2" := (cr s1 s2 v1 v2) (no associativity, at level 70). Hint Constructors cr.