Mercurial > cpdt > repo
comparison src/StackMachine.v @ 471:51a8472aca68
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 08 Oct 2012 16:04:49 -0400 |
| parents | b36876d4611e |
| children | 1fd4109f7b31 |
comparison
equal
deleted
inserted
replaced
| 470:0df6dde807ab | 471:51a8472aca68 |
|---|---|
| 146 (** With the two programming languages defined, we can turn to the compiler definition. *) | 146 (** With the two programming languages defined, we can turn to the compiler definition. *) |
| 147 | 147 |
| 148 | 148 |
| 149 (** ** Translation *) | 149 (** ** Translation *) |
| 150 | 150 |
| 151 (** Our compiler itself is now unsurprising. The list concatenation operator %\index{Gallina operators!++}%[++] comes from the Coq standard library. *) | 151 (** Our compiler itself is now unsurprising. The list concatenation operator %\index{Gallina operators!++}\coqdocnotation{%#<tt>#++#</tt>#%}% comes from the Coq standard library. *) |
| 152 | 152 |
| 153 Fixpoint compile (e : exp) : prog := | 153 Fixpoint compile (e : exp) : prog := |
| 154 match e with | 154 match e with |
| 155 | Const n => iConst n :: nil | 155 | Const n => iConst n :: nil |
| 156 | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil | 156 | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil |
| 301 end) ((iConst n :: nil) ++ p) s = | 301 end) ((iConst n :: nil) ++ p) s = |
| 302 progDenote p (n :: s) | 302 progDenote p (n :: s) |
| 303 | 303 |
| 304 ]] | 304 ]] |
| 305 | 305 |
| 306 This last [unfold] has left us with an anonymous fixpoint version of [progDenote], which will generally happen when unfolding recursive definitions. Note that Coq has automatically renamed the [fix] arguments [p] and [s] to [p0] and [s0], to avoid clashes with our local free variables. There is also a subterm [None (A:=stack)], which has an annotation specifying that the type of the term ought to be [option stack]. This is phrased as an explicit instantiation of a named type parameter [A] from the definition of [option]. | 306 This last [unfold] has left us with an anonymous recursive definition of [progDenote] (similarly to how [fun] or "lambda" constructs in general allow anonymous non-recursive functions), which will generally happen when unfolding recursive definitions. Note that Coq has automatically renamed the [fix] arguments [p] and [s] to [p0] and [s0], to avoid clashes with our local free variables. There is also a subterm [None (A:=stack)], which has an annotation specifying that the type of the term ought to be [option stack]. This is phrased as an explicit instantiation of a named type parameter [A] from the definition of [option]. |
| 307 | 307 |
| 308 Fortunately, in this case, we can eliminate the complications of anonymous recursion right away, since the structure of the argument ([iConst n :: nil) ++ p] is known, allowing us to simplify the internal pattern match with the [simpl] tactic, which applies the same reduction strategy that we used earlier with [Eval] (and whose details we still postpone).%\index{tactics!simpl}% | 308 Fortunately, in this case, we can eliminate the complications of anonymous recursion right away, since the structure of the argument ([iConst n :: nil) ++ p] is known, allowing us to simplify the internal pattern match with the [simpl] tactic, which applies the same reduction strategy that we used earlier with [Eval] (and whose details we still postpone).%\index{tactics!simpl}% |
| 309 *) | 309 *) |
| 310 | 310 |
| 311 simpl. | 311 simpl. |
| 388 progDenote ((compile e2 ++ compile e1 ++ iBinop b :: nil) ++ p) s = | 388 progDenote ((compile e2 ++ compile e1 ++ iBinop b :: nil) ++ p) s = |
| 389 progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) | 389 progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s) |
| 390 | 390 |
| 391 ]] | 391 ]] |
| 392 | 392 |
| 393 What we need is the associative law of list concatenation, which is available as a theorem [app_assoc_reverse] in the standard library.%\index{Vernacular commands!Check}% *) | 393 What we need is the associative law of list concatenation, which is available as a theorem [app_assoc_reverse] in the standard library.%\index{Vernacular commands!Check}% (Here and elsewhere, it is possible to tell the difference between inputs and outputs to Coq by periods at the ends of the inputs.) *) |
| 394 | 394 |
| 395 Check app_assoc_reverse. | 395 Check app_assoc_reverse. |
| 396 (** %\vspace{-.15in}%[[ | 396 (** %\vspace{-.15in}%[[ |
| 397 app_assoc_reverse | 397 app_assoc_reverse |
| 398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n | 398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n |
| 585 | TLt => leb | 585 | TLt => leb |
| 586 end. | 586 end. |
| 587 | 587 |
| 588 (** This function has just a few differences from the denotation functions we saw earlier. First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote]. Second, we need to perform a genuine%\index{dependent pattern matching}% _dependent pattern match_, where the necessary _type_ of each case body depends on the _value_ that has been matched. At this early stage, we will not go into detail on the many subtle aspects of Gallina that support dependent pattern-matching, but the subject is central to Part II of the book. | 588 (** This function has just a few differences from the denotation functions we saw earlier. First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote]. Second, we need to perform a genuine%\index{dependent pattern matching}% _dependent pattern match_, where the necessary _type_ of each case body depends on the _value_ that has been matched. At this early stage, we will not go into detail on the many subtle aspects of Gallina that support dependent pattern-matching, but the subject is central to Part II of the book. |
| 589 | 589 |
| 590 The same tricks suffice to define an expression denotation function in an unsurprising way: | 590 The same tricks suffice to define an expression denotation function in an unsurprising way. Note that the [type] arguments to the [TBinop] constructor must be included explicitly in pattern-matching, but here we write underscores because we do not need to refer to those arguments directly. *) |
| 591 *) | |
| 592 | 591 |
| 593 Fixpoint texpDenote t (e : texp t) : typeDenote t := | 592 Fixpoint texpDenote t (e : texp t) : typeDenote t := |
| 594 match e with | 593 match e with |
| 595 | TNConst n => n | 594 | TNConst n => n |
| 596 | TBConst b => b | 595 | TBConst b => b |