Mercurial > cpdt > repo

comparison src/StackMachine.v @ 16:4d8ca6845e67

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Source language examples
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 15:05:21 -0400
parents d8c81e19e7d3
children 2c5a2a221b85
comparison
equal deleted inserted replaced
15:d8c81e19e7d3 16:4d8ca6845e67
91 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2) 91 | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
92 end. 92 end.
93 93
94 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *) 94 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint]. The rest should be old hat for functional programmers. *)
95 95
96 (** It is convenient to be able to test definitions before starting to prove things about them. We can verify that our semantics is sensible by evaluating some sample uses. *)
97
98 Eval simpl in expDenote (Const 42).
99 Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
100 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
101
96 102
97 (** ** Target language *) 103 (** ** Target language *)
98 104
99 (** We will compile our source programs onto a simple stack machine, whose syntax is: *) 105 (** We will compile our source programs onto a simple stack machine, whose syntax is: *)
100 106
141 Fixpoint compile (e : exp) : prog := 147 Fixpoint compile (e : exp) : prog :=
142 match e with 148 match e with
143 | Const n => IConst n :: nil 149 | Const n => IConst n :: nil
144 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil 150 | Binop b e1 e2 => compile e2 ++ compile e1 ++ IBinop b :: nil
145 end. 151 end.
152
153
154 (** Before we set about proving that this compiler is correct, we can try a few test runs, using our sample programs from earlier. *)
155
156 Eval simpl in compile (Const 42).
157 Eval simpl in compile (Binop Plus (Const 2) (Const 2)).
158 Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
159
160 (** We can also run our compiled programs and chedk that they give the right results. *)
161
162 Eval simpl in progDenote (compile (Const 42)) nil.
163 Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil.
164 Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) nil.
146 165
147 166
148 (** ** Translation correctness *) 167 (** ** Translation correctness *)
149 168
150 (** 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: *) 169 (** 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: *)