Mercurial > cpdt > repo

comparison src/StackMachine.v @ 417:539ed97750bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala <adam@chlipala.net>
date Tue, 17 Jul 2012 16:37:58 -0400
parents 5986e9fd40b5
children 686cf945dd02
comparison
equal deleted inserted replaced
416:ded318830bb0 417:539ed97750bb
49 | Const : nat -> exp 49 | Const : nat -> exp
50 | Binop : binop -> exp -> exp -> exp. 50 | Binop : binop -> exp -> exp -> exp.
51 51
52 (** Now we define the type of arithmetic expressions. We write that a constant may be built from one argument, a natural number; and a binary operation may be built from a choice of operator and two operand expressions. 52 (** Now we define the type of arithmetic expressions. We write that a constant may be built from one argument, a natural number; and a binary operation may be built from a choice of operator and two operand expressions.
53 53
54 A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in LaTeX or HTML. Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%. Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}%, the inverted %`%#'#A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%, and the Cartesian product %`%#'#X' for %\texttt{%#<tt>#*#</tt>#%}%. When in doubt about the ASCII version of a symbol, you can consult the chapter source code. 54 A note for readers following along in the PDF version: %\index{coqdoc}%coqdoc supports pretty-printing of tokens in %\LaTeX{}%#LaTeX# or HTML. Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%. Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}%, the inverted %`%#'#A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%, and the Cartesian product %`%#'#X' for %\texttt{%#<tt>#*#</tt>#%}%. When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
55 55
56 %\medskip% 56 %\medskip%
57 57
58 Now we are ready to say what these programs mean. We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics. (If you are not familiar with these semantic techniques, no need to worry; we will stick to %``%#"#common sense#"#%''% constructions.)%\index{Vernacular commands!Definition}% *) 58 Now we are ready to say what these programs mean. We will do this by writing an %\index{interpreters}%interpreter that can be thought of as a trivial operational or denotational semantics. (If you are not familiar with these semantic techniques, no need to worry; we will stick to %``%#"#common sense#"#%''% constructions.)%\index{Vernacular commands!Definition}% *)
59 59
506 ]] 506 ]]
507 %\index{tactics!rewrite}% *) 507 %\index{tactics!rewrite}% *)
508 508
509 rewrite (app_nil_end (compile e)). 509 rewrite (app_nil_end (compile e)).
510 510
511 (** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion. [rewrite] might choose the wrong place to rewrite if we did not specify which we want. 511 (** This time, we explicitly specify the value of the variable [l] from the theorem statement, since multiple expressions of list type appear in the conclusion. The [rewrite] tactic might choose the wrong place to rewrite if we did not specify which we want.
512 512
513 [[ 513 [[
514 e : exp 514 e : exp
515 ============================ 515 ============================
516 progDenote (compile e ++ nil) nil = Some (expDenote e :: nil) 516 progDenote (compile e ++ nil) nil = Some (expDenote e :: nil)
560 560
561 The inuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t]. For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is boolean. The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type. 561 The inuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t]. For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is boolean. The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type.
562 562
563 ML and Haskell have indexed algebraic datatypes. For instance, their list types are indexed by the type of data that the list carries. However, compared to Coq, ML and Haskell 98 place two important restrictions on datatype definitions. 563 ML and Haskell have indexed algebraic datatypes. For instance, their list types are indexed by the type of data that the list carries. However, compared to Coq, ML and Haskell 98 place two important restrictions on datatype definitions.
564 564
565 First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition. There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat]. %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADT's)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell and other languages that removes this first restriction. 565 First, the indices of the range of each data constructor must be type variables bound at the top level of the datatype definition. There is no way to do what we did here, where we, for instance, say that [TPlus] is a constructor building a [tbinop] whose indices are all fixed at [Nat]. %\index{generalized algebraic datatypes}\index{GADTs|see{generalized algebraic datatypes}}% _Generalized algebraic datatypes_ (GADTs)%~\cite{GADT}% are a popular feature in %\index{GHC Haskell}%GHC Haskell and other languages that removes this first restriction.
566 566
567 The second restriction is not lifted by GADT's. In ML and Haskell, indices of types must be types and may not be _expressions_. In Coq, types may be indexed by arbitrary Gallina terms. Type indices can live in the same universe as programs, and we can compute with them just like regular programs. Haskell supports a hobbled form of computation in type indices based on %\index{Haskell}%multi-parameter type classes, and recent extensions like type functions bring Haskell programming even closer to %``%#"#real#"#%''% functional programming with types, but, without dependent typing, there must always be a gap between how one programs with types and how one programs normally. 567 The second restriction is not lifted by GADTs. In ML and Haskell, indices of types must be types and may not be _expressions_. In Coq, types may be indexed by arbitrary Gallina terms. Type indices can live in the same universe as programs, and we can compute with them just like regular programs. Haskell supports a hobbled form of computation in type indices based on %\index{Haskell}%multi-parameter type classes, and recent extensions like type functions bring Haskell programming even closer to %``%#"#real#"#%''% functional programming with types, but, without dependent typing, there must always be a gap between how one programs with types and how one programs normally.
568 *) 568 *)
569 569
570 (** We can define a similar type family for typed expressions, where a term of type [texp t] can be assigned object language type [t]. (It is conventional in the world of interactive theorem proving to call the language of the proof assistant the%\index{meta language}% _meta language_ and a language being formalized the%\index{object language}% _object language_.) *) 570 (** We can define a similar type family for typed expressions, where a term of type [texp t] can be assigned object language type [t]. (It is conventional in the world of interactive theorem proving to call the language of the proof assistant the%\index{meta language}% _meta language_ and a language being formalized the%\index{object language}% _object language_.) *)
571 571
572 Inductive texp : type -> Set := 572 Inductive texp : type -> Set :=