diff src/StackMachine.v @ 17:2c5a2a221b85

Target language source examples
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 15:08:28 -0400
parents 4d8ca6845e67
children 82618ad75252
line wrap: on
line diff
--- 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 *)