www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

rosette-guide-sec3-tests.rkt (599B)

      1 #lang s-exp "../../rosette/rosette2.rkt"
      2 (require "../rackunit-typechecking.rkt"
      3          "check-type+asserts.rkt")
      4 
      5 ;; Examples from the Rosette Guide, Section 3
      6 
      7 ;; Symbolic effects
      8 (define y1 (ann 0 : Nat))
      9 (check-type (if #t (void) (set! y1 3)) : CUnit -> (void))
     10 ;; y1 unchanged: 0
     11 (check-type y1 : Nat -> 0)
     12 (check-type (if #f (set! y1 3) (void)) : CUnit -> (void))
     13 ;; y1 unchanged: 0
     14 (check-type y1 : Nat -> 0)
     15 ;; symbolic effect!
     16 (define-symbolic x1 boolean? : Bool)
     17 (check-type (if x1 (void) (set! y1 3)) : Unit -> (void))
     18 ;; y1 symbolic: (ite x1 0 3)
     19 (check-type y1 : Nat -> (if x1 0 3))
     20