Mercurial > cpdt > repo

comparison src/StackMachine.v @ 20:c0cbf324ec7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished typed example
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 16:14:47 -0400
parents 5db67b182ef8
children 91e247c68ee8
comparison
equal deleted inserted replaced
19:5db67b182ef8 20:c0cbf324ec7d
21 As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% 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 %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer. If you do the latter, include a line [Require Import List Tactics] at the start of the file, to match some code hidden from the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book. In either case, if you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs. 21 As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% 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 %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer. If you do the latter, include a line [Require Import List Tactics] at the start of the file, to match some code hidden from the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book. In either case, if you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
22 22
23 With Proof General, the portion of a buffer that Coq has processed is highlighted in some way, like being given a blue background. You step through Coq source files by positioning the point at the position you want Coq to run to and pressing C-C C-RET. This can be used both for normal step-by-step coding, by placing the point inside some command past the end of the highlighted region; and for undoing, by placing the point inside the highlighted region. *) 23 With Proof General, the portion of a buffer that Coq has processed is highlighted in some way, like being given a blue background. You step through Coq source files by positioning the point at the position you want Coq to run to and pressing C-C C-RET. This can be used both for normal step-by-step coding, by placing the point inside some command past the end of the highlighted region; and for undoing, by placing the point inside the highlighted region. *)
24 24
25 25
26 (** * Arithmetic expressions over natural numbers *) 26 (** * Arithmetic Expressions Over Natural Numbers *)
27 27
28 (** We will begin with that staple of compiler textbooks, arithemtic expressions over a single type of numbers. *) 28 (** We will begin with that staple of compiler textbooks, arithemtic expressions over a single type of numbers. *)
29 29
30 (** ** Source language *) 30 (** ** Source Language *)
31 31
32 (** We begin with the syntax of the source language. *) 32 (** We begin with the syntax of the source language. *)
33 33
34 Inductive binop : Set := Plus | Times. 34 Inductive binop : Set := Plus | Times.
35 35
106 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). 106 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
107 (** [[ 107 (** [[
108 = 28 : nat 108 = 28 : nat
109 ]] *) 109 ]] *)
110 110
111 (** ** Target language *) 111 (** ** Target Language *)
112 112
113 (** We will compile our source programs onto a simple stack machine, whose syntax is: *) 113 (** We will compile our source programs onto a simple stack machine, whose syntax is: *)
114 114
115 Inductive instr : Set := 115 Inductive instr : Set :=
116 | IConst : nat -> instr 116 | IConst : nat -> instr
188 (** [[ 188 (** [[
189 = Some (28 :: nil) : option stack 189 = Some (28 :: nil) : option stack
190 ]] *) 190 ]] *)
191 191
192 192
193 (** ** Translation correctness *) 193 (** ** Translation Correctness *)
194 194
195 (** 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: *) 195 (** 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: *)
196 196
197 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). 197 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
198 (* begin hide *) 198 (* begin hide *)
511 511
512 reflexivity. 512 reflexivity.
513 Qed. 513 Qed.
514 514
515 515
516 (** * Typed expressions *) 516 (** * Typed Expressions *)
517 517
518 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *) 518 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *)
519 519
520 (** ** Source language *) 520 (** ** Source Language *)
521 521
522 (** We define a trivial language of types to classify our expressions: *) 522 (** We define a trivial language of types to classify our expressions: *)
523 523
524 Inductive type : Set := Nat | Bool. 524 Inductive type : Set := Nat | Bool.
525 525
629 (** [[ 629 (** [[
630 = true : typeDenote Bool 630 = true : typeDenote Bool
631 ]] *) 631 ]] *)
632 632
633 633
634 (** ** Target language *) 634 (** ** Target Language *)
635 635
636 (** Now we want to define a suitable stack machine target for compilation. In the example of the untyped language, stack machine programs could encounter stack underflows and "get stuck." This was unfortunate, since we had to deal with this complication even though we proved that our compiler never produced underflowing programs. We could have used dependent types to force all stack machine programs to be underflow-free. 636 (** Now we want to define a suitable stack machine target for compilation. In the example of the untyped language, stack machine programs could encounter stack underflows and "get stuck." This was unfortunate, since we had to deal with this complication even though we proved that our compiler never produced underflowing programs. We could have used dependent types to force all stack machine programs to be underflow-free.
637 637
638 For our new languages, besides underflow, we also have the problem of stack slots with naturals instead of bools or vice versa. This time, we will use indexed typed families to avoid the need to reason about potential failures. 638 For our new languages, besides underflow, we also have the problem of stack slots with naturals instead of bools or vice versa. This time, we will use indexed typed families to avoid the need to reason about potential failures.
639 639
783 (** [[ 783 (** [[
784 = (true, tt) : vstack (Bool :: nil) 784 = (true, tt) : vstack (Bool :: nil)
785 ]] *) 785 ]] *)
786 786
787 787
788 (** ** Translation correctness *) 788 (** ** Translation Correctness *)
789
790 (** We can state a correctness theorem similar to the last one. *)
791
792 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
793 (* begin hide *)
794 Abort.
795 (* end hide *)
796
797 (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *)
789 798
790 Lemma tcompileCorrect' : forall t (e : texp t) 799 Lemma tcompileCorrect' : forall t (e : texp t)
791 ts (s : vstack ts), 800 ts (s : vstack ts),
792 tprogDenote (tcompile e ts) s 801 tprogDenote (tcompile e ts) s
793 = (texpDenote e, s). 802 = (texpDenote e, s).
803
804 (** While lemma [compileCorrect'] quantified over a program that is the "continuation" for the expression we are considering, here we avoid drawing in any extra syntactic elements. In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it. Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it.
805
806 Let us try to prove this theorem in the same way that we settled on in the last section. *)
807
794 induction e; crush. 808 induction e; crush.
809
810 (** We are left with this unproved conclusion:
811
812 [[
813
814 tprogDenote
815 (tconcat (tcompile e2 ts)
816 (tconcat (tcompile e1 (arg2 :: ts))
817 (TCons (TIBinop ts t) (TNil (res :: ts))))) s =
818 (tbinopDenote t (texpDenote e1) (texpDenote e2), s)
819 ]]
820
821 We need an analogue to the [app_ass] theorem that we used to rewrite the goal in the last section. We can abort this proof and prove such a lemma about [tconcat].
822 *)
795 Abort. 823 Abort.
796 824
797 Lemma tconcatCorrect : forall ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'') 825 Lemma tconcatCorrect : forall ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'')
798 (s : vstack ts), 826 (s : vstack ts),
799 tprogDenote (tconcat p p') s 827 tprogDenote (tconcat p p') s
800 = tprogDenote p' (tprogDenote p s). 828 = tprogDenote p' (tprogDenote p s).
801 induction p; crush. 829 induction p; crush.
802 Qed. 830 Qed.
803 831
832 (** This one goes through completely automatically.
833
834 Some code behind the scenes registers [app_ass] for use by [crush]. We must register [tconcatCorrect] similarly to get the same effect: *)
835
804 Hint Rewrite tconcatCorrect : cpdt. 836 Hint Rewrite tconcatCorrect : cpdt.
837
838 (** We ask that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush]. Now we are ready to return to [tcompileCorrect'], proving it automatically this time. *)
805 839
806 Lemma tcompileCorrect' : forall t (e : texp t) 840 Lemma tcompileCorrect' : forall t (e : texp t)
807 ts (s : vstack ts), 841 ts (s : vstack ts),
808 tprogDenote (tcompile e ts) s 842 tprogDenote (tcompile e ts) s
809 = (texpDenote e, s). 843 = (texpDenote e, s).
810 induction e; crush. 844 induction e; crush.
811 Qed. 845 Qed.
812 846
847 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *)
848
813 Hint Rewrite tcompileCorrect' : cpdt. 849 Hint Rewrite tcompileCorrect' : cpdt.
814 850
815 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 851 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
816 crush. 852 crush.
817 Qed. 853 Qed.