Mercurial > cpdt > repo

comparison src/StackMachine.v @ 17:2c5a2a221b85

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Target language source examples
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 15:08:28 -0400
parents 4d8ca6845e67
children 82618ad75252
comparison
equal deleted inserted replaced
16:4d8ca6845e67 17:2c5a2a221b85
579 | TNConst n => n 579 | TNConst n => n
580 | TBConst b => b 580 | TBConst b => b
581 | TBinop _ _ _ b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2) 581 | TBinop _ _ _ b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2)
582 end. 582 end.
583 583
584 (** We can evaluate a few example programs to convince ourselves that this semantics is correct. *)
585
586 Eval simpl in texpDenote (TNConst 42).
587 Eval simpl in texpDenote (TBConst true).
588 Eval simpl in texpDenote (TBinop TTimes (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
589 Eval simpl in texpDenote (TBinop (TEq Nat) (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
590 Eval simpl in texpDenote (TBinop TLt (TBinop TPlus (TNConst 2) (TNConst 2)) (TNConst 7)).
591
584 592
585 (** ** Target language *) 593 (** ** Target language *)
586 594
587 Definition tstack := list type. 595 Definition tstack := list type.
588 596