Mercurial > cpdt > repo
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 *)