Mercurial > cpdt > repo
comparison src/StackMachine.v @ 279:fabbc71abd80
Incorporate PC's comments on InductiveTypes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 01 Oct 2010 14:19:20 -0400 |
parents | e7ed2fddd29a |
children | 2c88fc1dbe33 |
comparison
equal
deleted
inserted
replaced
278:e7ed2fddd29a | 279:fabbc71abd80 |
---|---|
17 | 17 |
18 | 18 |
19 (** %\chapter{Some Quick Examples}% *) | 19 (** %\chapter{Some Quick Examples}% *) |
20 | 20 |
21 | 21 |
22 (** 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. I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions. | 22 (** 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. |
23 | |
24 I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions. | |
23 | 25 |
24 To set up your Proof General environment to process the source to this chapter, a few simple steps are required. | 26 To set up your Proof General environment to process the source to this chapter, a few simple steps are required. |
25 | 27 |
26 %\begin{enumerate}%#<ol># | 28 %\begin{enumerate}%#<ol># |
27 | 29 |
604 (** It can take a few moments to come to terms with the fact that [Set], the type of types of programs, is itself a first-class type, and that we can write functions that return [Set]s. Past that wrinkle, the definition of [typeDenote] is trivial, relying on the [nat] and [bool] types from the Coq standard library. | 606 (** It can take a few moments to come to terms with the fact that [Set], the type of types of programs, is itself a first-class type, and that we can write functions that return [Set]s. Past that wrinkle, the definition of [typeDenote] is trivial, relying on the [nat] and [bool] types from the Coq standard library. |
605 | 607 |
606 We need to define one auxiliary function, implementing a boolean binary "less-than" operator, which only appears in the standard library with a type fancier than what we are prepared to deal with here. The code is entirely standard and ML-like, with the one caveat being that the Coq [nat] type uses a unary representation, where [O] is zero and [S n] is the successor of [n]. | 608 We need to define one auxiliary function, implementing a boolean binary "less-than" operator, which only appears in the standard library with a type fancier than what we are prepared to deal with here. The code is entirely standard and ML-like, with the one caveat being that the Coq [nat] type uses a unary representation, where [O] is zero and [S n] is the successor of [n]. |
607 *) | 609 *) |
608 | 610 |
609 Fixpoint lt (n1 n2 : nat) : bool := | 611 Fixpoint lessThan (n1 n2 : nat) : bool := |
610 match n1, n2 with | 612 match n1, n2 with |
611 | O, S _ => true | 613 | O, S _ => true |
612 | S n1', S n2' => lt n1' n2' | 614 | S n1', S n2' => lessThan n1' n2' |
613 | _, _ => false | 615 | _, _ => false |
614 end. | 616 end. |
615 | 617 |
616 (** Now we can interpret binary operators, relying on standard-library equality test functions [eqb] and [beq_nat] for booleans and naturals, respectively: *) | 618 (** Now we can interpret binary operators, relying on standard-library equality test functions [eqb] and [beq_nat] for booleans and naturals, respectively: *) |
617 | 619 |
621 return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with | 623 return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with |
622 | TPlus => plus | 624 | TPlus => plus |
623 | TTimes => mult | 625 | TTimes => mult |
624 | TEq Nat => beq_nat | 626 | TEq Nat => beq_nat |
625 | TEq Bool => eqb | 627 | TEq Bool => eqb |
626 | TLt => lt | 628 | TLt => lessThan |
627 end. | 629 end. |
628 | 630 |
629 (** 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 %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks. In each branch of the [match], we need to use branch-specific information about the indices to [tbinop]. General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match]. | 631 (** 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 %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks. In each branch of the [match], we need to use branch-specific information about the indices to [tbinop]. General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match]. |
630 | 632 |
631 The [in] annotation restates the type of the term being case-analyzed. Though we use the same names for the indices as we use in the type of the original argument binder, these are actually fresh variables, and they are %\textit{%#<i>#binding occurrences#</i>#%}%. Their scope is the [return] clause. That is, [arg1], [arg2], and [res] are new bound variables bound only within the return clause [typeDenote arg1 -> typeDenote arg2 -> typeDenote res]. By being explicit about the functional relationship between the type indices and the match result, we regain decidable type inference. | 633 The [in] annotation restates the type of the term being case-analyzed. Though we use the same names for the indices as we use in the type of the original argument binder, these are actually fresh variables, and they are %\textit{%#<i>#binding occurrences#</i>#%}%. Their scope is the [return] clause. That is, [arg1], [arg2], and [res] are new bound variables bound only within the return clause [typeDenote arg1 -> typeDenote arg2 -> typeDenote res]. By being explicit about the functional relationship between the type indices and the match result, we regain decidable type inference. |
640 match b with | 642 match b with |
641 | TPlus => plus | 643 | TPlus => plus |
642 | TTimes => mult | 644 | TTimes => mult |
643 | TEq Nat => beq_nat | 645 | TEq Nat => beq_nat |
644 | TEq Bool => eqb | 646 | TEq Bool => eqb |
645 | TLt => lt | 647 | TLt => lessThan |
646 end. | 648 end. |
647 | 649 |
648 (** | 650 (** |
649 The same tricks suffice to define an expression denotation function in an unsurprising way: | 651 The same tricks suffice to define an expression denotation function in an unsurprising way: |
650 *) | 652 *) |