Mercurial > cpdt > repo
comparison src/StackMachine.v @ 442:89c67796754e
Undo some overzealous vspace tweaks
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 01 Aug 2012 16:09:37 -0400 |
parents | 393b8ed99c2f |
children | 9e3333bd08a1 |
comparison
equal
deleted
inserted
replaced
441:cbfd23b4364d | 442:89c67796754e |
---|---|
101 (** [= 4 : nat] *) | 101 (** [= 4 : nat] *) |
102 | 102 |
103 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). | 103 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). |
104 (** [= 28 : nat] *) | 104 (** [= 28 : nat] *) |
105 | 105 |
106 (** %\smallskip{}%Nothing too surprising goes on here, so we are ready to move on to the target language of our compiler. *) | |
107 | |
108 | |
106 (** ** Target Language *) | 109 (** ** Target Language *) |
107 | 110 |
108 (** We will compile our source programs onto a simple stack machine, whose syntax is: *) | 111 (** We will compile our source programs onto a simple stack machine, whose syntax is: *) |
109 | 112 |
110 Inductive instr : Set := | 113 Inductive instr : Set := |
138 | None => None | 141 | None => None |
139 | Some s' => progDenote p' s' | 142 | Some s' => progDenote p' s' |
140 end | 143 end |
141 end. | 144 end. |
142 | 145 |
146 (** With the two programming languages defined, we can turn to the compiler definition. *) | |
147 | |
143 | 148 |
144 (** ** Translation *) | 149 (** ** Translation *) |
145 | 150 |
146 (** 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!++}%[++] comes from the Coq standard library. *) |
147 | 152 |
161 (** [= iConst 2 :: iConst 2 :: iBinop Plus :: nil : prog] *) | 166 (** [= iConst 2 :: iConst 2 :: iBinop Plus :: nil : prog] *) |
162 | 167 |
163 Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). | 168 Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)). |
164 (** [= iConst 7 :: iConst 2 :: iConst 2 :: iBinop Plus :: iBinop Times :: nil : prog] *) | 169 (** [= iConst 7 :: iConst 2 :: iConst 2 :: iBinop Plus :: iBinop Times :: nil : prog] *) |
165 | 170 |
166 (** We can also run our compiled programs and check that they give the right results. *) | 171 (** %\smallskip{}%We can also run our compiled programs and check that they give the right results. *) |
167 | 172 |
168 Eval simpl in progDenote (compile (Const 42)) nil. | 173 Eval simpl in progDenote (compile (Const 42)) nil. |
169 (** [= Some (42 :: nil) : option stack] *) | 174 (** [= Some (42 :: nil) : option stack] *) |
170 | 175 |
171 Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil. | 176 Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil. |
613 | 618 |
614 Eval simpl in texpDenote (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) | 619 Eval simpl in texpDenote (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) |
615 (TNConst 7)). | 620 (TNConst 7)). |
616 (** [= true : typeDenote Bool] *) | 621 (** [= true : typeDenote Bool] *) |
617 | 622 |
623 (** %\smallskip{}%Now we are ready to define a suitable stack machine target for compilation. *) | |
624 | |
618 | 625 |
619 (** ** Target Language *) | 626 (** ** Target Language *) |
620 | 627 |
621 (** 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. | 628 (** 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. |
622 | 629 |
623 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. | 630 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. |
624 | 631 |
625 We start by defining stack types, which classify sets of possible stacks. *) | 632 We start by defining stack types, which classify sets of possible stacks. *) |
626 | 633 |
758 (** [= (false, tt) : vstack (Bool :: nil)] *) | 765 (** [= (false, tt) : vstack (Bool :: nil)] *) |
759 | 766 |
760 Eval simpl in tprogDenote (tcompile (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) | 767 Eval simpl in tprogDenote (tcompile (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) |
761 (TNConst 7)) nil) tt. | 768 (TNConst 7)) nil) tt. |
762 (** [= (true, tt) : vstack (Bool :: nil)] *) | 769 (** [= (true, tt) : vstack (Bool :: nil)] *) |
770 | |
771 (** %\smallskip{}%The compiler seems to be working, so let us turn to proving that it _always_ works. *) | |
763 | 772 |
764 | 773 |
765 (** ** Translation Correctness *) | 774 (** ** Translation Correctness *) |
766 | 775 |
767 (** We can state a correctness theorem similar to the last one. *) | 776 (** We can state a correctness theorem similar to the last one. *) |