# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220468908 14400
# Node ID 2c5a2a221b85175d1104f3113a447e0da3bf86f2
# Parent  4d8ca6845e671b5bb16ecc4891c2ce889d42d1ab
Target language source examples

diff -r 4d8ca6845e67 -r 2c5a2a221b85 src/StackMachine.v
--- a/src/StackMachine.v	Wed Sep 03 15:05:21 2008 -0400
+++ b/src/StackMachine.v	Wed Sep 03 15:08:28 2008 -0400
@@ -581,6 +581,14 @@
     | TBinop _ _ _ b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2)
   end.
 
+(** We can evaluate a few example programs to convince ourselves that this semantics is correct. *)
+
+Eval simpl in texpDenote (TNConst 42).
+Eval simpl in texpDenote (TBConst true).
+Eval simpl in texpDenote (TBinop TTimes (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
+Eval simpl in texpDenote (TBinop (TEq Nat) (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
+Eval simpl in texpDenote (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
+
 
 (** ** Target language *)