Certified Programming with Dependent Types: src/StackMachine.v comparison

comparison src/StackMachine.v @ 447:9e3333bd08a1

Proofreading pass through Chapter 2

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 17 Aug 2012 12:22:26 -0400
parents	89c67796754e
children	2740b8a23cce

comparison

equal deleted inserted replaced

-:a0c604da96d3
+:9e3333bd08a1
 *)
 (** %\chapter{Some Quick Examples}% *)
-(** I will start off by jumping right in to a fully worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  This chapter is not meant to give full explanations of the features that are employed.  Rather, it is meant more as an advertisement of what is possible.  Later chapters will introduce all of the concepts in bottom-up fashion.
+(** I will start off by jumping right in to a fully worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  This chapter is not meant to give full explanations of the features that are employed.  Rather, it is meant more as an advertisement of what is possible.  Later chapters will introduce all of the concepts in bottom-up fashion.  In other words, it is expected that most readers will not understand what exactly is going on here, but I hope this demo will whet your appetite for the remaining chapters!
 As always, you can step through the source file <<StackMachine.v>> for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new <<.v>> file in an Emacs buffer.  If you do the latter, include these two lines at the start of the file. *)
 Require Import Bool Arith List CpdtTactics.
 Set Implicit Arguments.
 (** We begin with the syntax of the source language.%\index{Vernacular commands!Inductive}% *)
 Inductive binop : Set := Plus | Times.
-(** Our first line of Coq code should be unsurprising to ML and Haskell programmers.  We define an %\index{algebraic datatypes}%algebraic datatype [binop] to stand for the binary operators of our source language.  There are just two wrinkles compared to ML and Haskell.  First, we use the keyword [Inductive], in place of <<data>>, <<datatype>>, or <<type>>.  This is not just a trivial surface syntax difference; inductive types in Coq are much more expressive than garden variety algebraic datatypes, essentially enabling us to encode all of mathematics, though we begin humbly in this chapter.  Second, there is the %\index{Gallina terms!Set}%[: Set] fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs.  Later, we will see other options for defining datatypes in the universe of proofs or in an infinite hierarchy of universes, encompassing both programs and proofs, that bis useful in higher-order constructions. *)
+(** Our first line of Coq code should be unsurprising to ML and Haskell programmers.  We define an %\index{algebraic datatypes}%algebraic datatype [binop] to stand for the binary operators of our source language.  There are just two wrinkles compared to ML and Haskell.  First, we use the keyword [Inductive], in place of <<data>>, <<datatype>>, or <<type>>.  This is not just a trivial surface syntax difference; inductive types in Coq are much more expressive than garden variety algebraic datatypes, essentially enabling us to encode all of mathematics, though we begin humbly in this chapter.  Second, there is the %\index{Gallina terms!Set}%[: Set] fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs.  Later, we will see other options for defining datatypes in the universe of proofs or in an infinite hierarchy of universes, encompassing both programs and proofs, that is useful in higher-order constructions. *)
 Inductive exp : Set :=
 | Const : nat -> exp
 | Binop : binop -> exp -> exp -> exp.
 Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2))
 (Const 7))) nil.
 (** [= Some (28 :: nil) : option stack] *)
+(** %\smallskip{}%So far so good, but how can we be sure the compiler operates correctly for _all_ input programs? *)
 (** ** Translation Correctness *)
 (** We are ready to prove that our compiler is implemented correctly.  We can use a new vernacular command [Theorem] to start a correctness proof, in terms of the semantics we defined earlier:%\index{Vernacular commands!Theorem}% *)
 reflexivity.
 Qed.
 (* end thide *)
-(** This proof can be shortened and made automated, but we leave that as an exercise for the reader. *)
+(** This proof can be shortened and made automated, but we leave that task as an exercise for the reader. *)
 (** * Typed Expressions *)
 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *)
 Inductive texp : type -> Set :=
 | TNConst : nat -> texp Nat
 | TBConst : bool -> texp Bool
 | TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.
-(** Thanks to our use of dependent types, every well-typed [texp] represents a well-typed source expression, by construction.  This turns out to be very convenient for many things we might want to do with expressions.  For instance, it is easy to adapt our interpreter approach to defining semantics.  We start by defining a function mapping the types of our languages into Coq types: *)
+(** Thanks to our use of dependent types, every well-typed [texp] represents a well-typed source expression, by construction.  This turns out to be very convenient for many things we might want to do with expressions.  For instance, it is easy to adapt our interpreter approach to defining semantics.  We start by defining a function mapping the types of our object language into Coq types: *)
 Definition typeDenote (t : type) : Set :=
 match t with
 | Nat => nat
 | Bool => bool
 | TiBConst _ b => (b, s)
 | TiBinop _ _ _ _ b =>
 let '(arg1, (arg2, s')) := s in
 ((tbinopDenote b) arg1 arg2, s')
 end.
+]]
-]]
+The Coq type checker complains that:
-The Coq type-checker complains that:
 <<
 The term "(n, s)" has type "(nat * vstack ts)%type"
 while it is expected to have type "vstack ?119".
 >>
 Fixpoint tprogDenote ts ts' (p : tprog ts ts') : vstack ts -> vstack ts' :=
 match p with
 | TNil _ => fun s => s
 | TCons _ _ _ i p' => fun s => tprogDenote p' (tinstrDenote i s)
 end.
+(** The same argument-postponing trick is crucial for this definition. *)
 (** ** Translation *)
 (** To define our compilation, it is useful to have an auxiliary function for concatenating two stack machine programs. *)

Mercurial > cpdt > repo

comparison src/StackMachine.v @ 447:9e3333bd08a1