commit a56250b26e9ef4056223279e9984b73e09158f66 parent 3d92dbdde32e62c2060ea590a72d50679b477fc0 Author: AlexKnauth <alexander@knauth.org> Date: Wed, 31 Aug 2016 18:59:54 -0400 start on tests from section 3 of the Guide Diffstat:
| A | turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt | | | 20 | ++++++++++++++++++++ |
1 file changed, 20 insertions(+), 0 deletions(-)
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt @@ -0,0 +1,20 @@ +#lang s-exp "../../rosette/rosette2.rkt" +(require "../rackunit-typechecking.rkt" + "check-type+asserts.rkt") + +;; Examples from the Rosette Guide, Section 3 + +;; Symbolic effects +(define y1 (ann 0 : Nat)) +(check-type (if #t (void) (set! y1 3)) : CUnit -> (void)) +;; y1 unchanged: 0 +(check-type y1 : Nat -> 0) +(check-type (if #f (set! y1 3) (void)) : CUnit -> (void)) +;; y1 unchanged: 0 +(check-type y1 : Nat -> 0) +;; symbolic effect! +(define-symbolic x1 boolean? : Bool) +(check-type (if x1 (void) (set! y1 3)) : Unit -> (void)) +;; y1 symbolic: (ite x1 0 3) +(check-type y1 : Nat -> (if x1 0 3)) +