add check-type+asserts

turnstile/examples/tests/rosette/check-asserts.rkt

@@ -0,0 +1,31 @@
+#lang racket/base
+
+(provide check-equal?/asserts)
+
+(require rackunit
+         racket/set
+         syntax/srcloc
+         syntax/location
+         (only-in rosette with-asserts)
+         (for-syntax racket/base
+                     syntax/parse
+                     ))
+
+(define-binary-check (check-set=? actual expected)
+  (set=? actual expected))
+
+(define-syntax check-equal?/asserts
+  (lambda (stx)
+    (syntax-parse stx
+      [(check-equal?/asserts actual-expr expected-expr expected-asserts-expr)
+       #`(with-check-info*
+          (list (make-check-name 'check-equal?/asserts)
+                (make-check-location (build-source-location-list
+                                      (quote-srcloc #,stx)))
+                (make-check-expression '#,stx))
+          (λ ()
+            (test-begin
+             (let-values ([(actual asserts) (with-asserts actual-expr)])
+               (check-equal? actual expected-expr)
+               (check-set=? asserts expected-asserts-expr)))))])))
+

turnstile/examples/tests/rosette/check-type+asserts.rkt

@@ -0,0 +1,17 @@
+#lang racket/base
+
+(provide check-type+asserts)
+
+(require turnstile/turnstile
+         "check-asserts.rkt"
+         (only-in "../../rosette/rosette2.rkt" List Bool Unit))
+
+(define-typed-syntax check-type+asserts #:datum-literals (: ->)
+  [(_ e : τ-expected -> v asserts) ≫
+   [⊢ [e ≫ e- ⇐ : τ-expected]]
+   --------
+   [⊢ [_ ≫ (check-equal?/asserts e-
+                                 (add-expected v τ-expected)
+                                 (add-expected asserts (List Bool)))
+         ⇒ : Unit]]])
+

turnstile/examples/tests/rosette/rosette2-tests.rkt

@@ -1,5 +1,6 @@
 #lang s-exp "../../rosette/rosette2.rkt"
-(require "../rackunit-typechecking.rkt")
+(require "../rackunit-typechecking.rkt"
+         "check-type+asserts.rkt")
 
 ;; subtyping among concrete
 (check-type     ((λ ([x : CPosInt]) x) ((λ ([x : CPosInt]) x) 1)) : CPosInt -> 1)
@@ -273,6 +274,5 @@
 (define-symbolic b1 b2 boolean? : Bool)
 
 (check-type (clear-asserts!) : Unit -> (void))
-(check-type (assert-type (if b1 1 #f) : Int) : Int -> (if b1 1 #f))
-(check-type (assert-type (if b2 1 #f) : Bool) : Bool -> (if b2 1 #f))
-(check-type (asserts) : (List Bool) -> (list (not b2) b1))
+(check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> (if b1 1 #f) (list b1))
+(check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> (if b2 1 #f) (list (not b2)))