Mercurial > cpdt > repo

comparison src/StackMachine.v @ 442:89c67796754e

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