Mercurial > cpdt > repo

comparison src/StackMachine.v @ 279:fabbc71abd80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 *)