# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220468721 14400
# Node ID 4d8ca6845e671b5bb16ecc4891c2ce889d42d1ab
# Parent  d8c81e19e7d3ea1020ae330c45e704a1ee61b455
Source language examples

diff -r d8c81e19e7d3 -r 4d8ca6845e67 src/StackMachine.v
--- a/src/StackMachine.v	Wed Sep 03 15:00:56 2008 -0400
+++ b/src/StackMachine.v	Wed Sep 03 15:05:21 2008 -0400
@@ -93,6 +93,12 @@
 
 (** We declare explicitly that this is a recursive definition, using the keyword [Fixpoint].  The rest should be old hat for functional programmers. *)
 
+(** 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. *)
+
+Eval simpl in expDenote (Const 42).
+Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
+Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
+
 
 (** ** Target language *)
 
@@ -145,6 +151,19 @@
   end.
 
 
+(** Before we set about proving that this compiler is correct, we can try a few test runs, using our sample programs from earlier. *)
+
+Eval simpl in compile (Const 42).
+Eval simpl in compile (Binop Plus (Const 2) (Const 2)).
+Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
+
+(** We can also run our compiled programs and chedk that they give the right results. *)
+
+Eval simpl in progDenote (compile (Const 42)) nil.
+Eval simpl in progDenote (compile (Binop Plus (Const 2) (Const 2))) nil.
+Eval simpl in progDenote (compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7))) nil.
+
+
 (** ** Translation correctness *)
 
 (** 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: *)