rosette3: add tests checking displayed output

turnstile/examples/rosette/rosette3.rkt

@@ -1,6 +1,6 @@
 #lang turnstile
 ;; reuse unlifted forms as-is
-(reuse define λ let let* letrec begin void #%datum ann
+(reuse define λ let let* letrec begin void #%datum ann #%top-interaction
        require only-in define-type-alias define-named-type-alias
        #:from "../stlc+union.rkt")
 (require
@@ -21,7 +21,7 @@
 
 (provide (rename-out [ro:#%module-begin #%module-begin] 
                      [stlc+union:λ lambda])
-         Any Nothing
+         Any CNothing Nothing
          CU U
          Constant
          C→ → (for-syntax ~C→ C→?)
@@ -96,8 +96,6 @@
                    "CU requires concrete types"
      #'(CU* . tys+)]))
 
-(define-named-type-alias Nothing (CU))
-
 ;; internal symbolic union constructor
 (define-type-constructor U* #:arity >= 0)
 
@@ -110,6 +108,9 @@
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...))
      #'(U* . tys-)]))
 
+(define-named-type-alias CNothing (CU))
+(define-named-type-alias Nothing (U))
+
 ;; internal symbolic constant constructor
 (define-type-constructor Constant* #:arity = 1)
 
@@ -289,7 +290,7 @@
    [⊢ [_ ≫ (ro:assert e-) ⇒ : CUnit]]]
   [(_ e m) ≫
    [⊢ [e ≫ e- ⇒ : _]]
-   [⊢ [m ≫ m- ⇐ : (CU CString (C→ Nothing))]]
+   [⊢ [m ≫ m- ⇐ : (CU CString (C→ CNothing))]]
    --------
    [⊢ [_ ≫ (ro:assert e- m-) ⇒ : CUnit]]])
 
@@ -930,10 +931,12 @@
 (provide (typed-out [printf : (Ccase-> (C→ CString CUnit)
                                                (C→ CString Any CUnit)
                                                (C→ CString Any Any CUnit))]
+                    [display : (C→ Any CUnit)]
                     [displayln : (C→ Any CUnit)]
+                    [with-output-to-string : (C→ (C→ Any) CString)]
                     [pretty-print : (C→ Any CUnit)]
-                    [error : (Ccase-> (C→ (CU CString CSymbol) Nothing)
-                                      (C→ CSymbol CString Nothing))]
+                    [error : (Ccase-> (C→ (CU CString CSymbol) CNothing)
+                                      (C→ CSymbol CString CNothing))]
 
                     [string-length : (C→ CString CNat)]
 

turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt

@@ -132,8 +132,12 @@
 (check-type binding : CSolution)
 (check-type (sat? binding) : Bool -> #t)
 (check-type (unsat? binding) : Bool -> #f)
-;; TESTING TODO: requires visual inspection of stdout
-(check-type (print-forms binding) : Unit -> (void))
+(check-type (print-forms binding) : Unit)
+(check-type
+ (with-output-to-string (lambda () (print-forms binding)))
+ : CString
+ -> "/home/stchang/NEU_Research/macrotypes/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec2-tests.rkt:125:0\n'(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))\n")
+
 ;; typed/rosette should print: 
 ;;  '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
 ;; (untyped) rosette should print: 

turnstile/examples/tests/rosette/rosette3/rosette-guide-sec4-tests.rkt

@@ -210,7 +210,10 @@
 (check-type (&&) : Bool -> #t)
 (check-type (||) : Bool -> #f)
 ; no shortcircuiting
-(check-type (&& #f (begin (displayln "hello") #t))  : Bool -> #f)
+(check-type (&& #f (begin (display "") #t))  : Bool -> #f)
+(check-type
+ (with-output-to-string (λ () (&& #f (begin (displayln "hello") #t))))
+ : CString -> "hello\n")
 (define-symbolic a boolean?)
  ; this typechecks only when b is true
 (check-type (&& a (assert-type (if b #t 1) : Bool)) : Bool -> a)
@@ -218,7 +221,10 @@
 (check-type (asserts) : (CListof Bool) -> (list b))
 (clear-asserts!)
 ; no shortcircuiting
-(check-type (=> #f (begin (displayln "hello") #f))  : Bool -> #t)
+(check-type (=> #f (begin (display "") #f))  : Bool -> #t)
+(check-type
+ (with-output-to-string (λ () (=> #f (begin (displayln "hello") #f))))
+ : CString -> "hello\n")
 ; this typechecks only when b is true
 (check-type (<=> a (assert-type (if b #t 1) : Bool)) : Bool -> a)
 ; so Rosette emits a corresponding assertion

turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt

@@ -10,10 +10,20 @@
 (define (div2 [x : BV] -> BV)
   ([choose bvshl bvashr bvlshr bvadd bvsub bvmul] x (?? (bitvector 8))))
 (define-symbolic i (bitvector 8))
-(print-forms
- (synthesize #:forall (list i)
-             #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))
-(printf "expected output:\n~a\n" 
+(check-type
+ (print-forms
+  (synthesize #:forall (list i)
+              #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))
+ : Unit)
+(check-type
+ (with-output-to-string
+   (λ ()
+     (print-forms
+      (synthesize #:forall (list i)
+                  #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))))
+ : CString
+ -> "/home/stchang/NEU_Research/macrotypes/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt:10:0\n'(define (div2 (x : BV) -> BV) (bvlshr x (bv 1 8)))\n")
+#;(printf "expected output:\n~a\n" 
         "'(define (div2 [x : BV] -> BV) (bvlshr x (bv 1 8)))")
 
 ;; TODO: define-synthax