add tests for assert-type; use new lifted bitvector? as BVPred "pred" stx prop

turnstile/examples/rosette/bv.rkt

@@ -2,7 +2,8 @@
 #lang racket/base
 (require (except-in "../../../turnstile/turnstile.rkt" 
           #%module-begin 
-          zero? void sub1 or and not add1 = - * + boolean? integer? real? positive? string? quote pregexp make-parameter equal? eq? list ~Any)
+          zero? void error sub1 or and not add1 = - * + boolean? integer? real? positive? string? quote pregexp 
+          make-parameter equal? eq? list ~Any)
          (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
 (extends "rosette2.rkt" ; extends typed rosette
          #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
@@ -25,7 +26,7 @@
   [(_ e) ≫
    [⊢ [e ≫ e- ⇒ : CBVPred]]
    --------
-   [⊢ [_ ≫ (bv:BV e-) ⇒ : Unit]]])
+   [⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]])
 
 (define-primop bv : (Ccase-> (C→ CInt CBV)
                              (C→ CInt CBVPred CBV)

turnstile/examples/rosette/rosette2.rkt

@@ -4,13 +4,13 @@
 (reuse #%datum #:from "../stlc+union.rkt")
 (reuse define-type-alias #:from "../stlc+reco+var.rkt")
 (reuse define-named-type-alias #:from "../stlc+union.rkt")
-(reuse void Unit List list #:from "../stlc+cons.rkt")
+(reuse void list #:from "../stlc+cons.rkt")
 
 (provide Any
          CU U
          C→ → (for-syntax ~C→ C→?)
          Ccase-> ; TODO: symbolic case-> not supported yet
-         CParam ; TODO: symbolic Param not supported yet
+         CUnit CList CParam ; TODO: symbolic Param not supported yet
          CNegInt NegInt
          CZero Zero
          CPosInt PosInt
@@ -30,10 +30,13 @@
  (prefix-in ro: rosette)
  (only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?)
  (prefix-in C
-   (only-in "../stlc+union+case.rkt"
-            PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?))
+   (combine-in
+    (only-in "../stlc+union+case.rkt"
+             PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)
+    (only-in "../stlc+cons.rkt" Unit List)))
  (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
- (only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop))
+ (only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop)
+ (only-in "lifted-bitvector-pred.rkt" [bitvector? lifted-bitvector?]))
 
 ;; copied from rosette.rkt
 (define-simple-macro (define-rosette-primop op:id : ty)
@@ -44,7 +47,11 @@
 ;; ---------------------------------
 ;; Concrete and Symbolic union types
 
-(define-base-types Any CBV CStx)
+(begin-for-syntax
+  (define (concrete? t)
+    (not (or (Any? t) (U*? t)))))
+
+(define-base-types Any CBV CStx CSymbol)
 
 (define-syntax (CU stx)
   (syntax-parse stx
@@ -54,6 +61,8 @@
                    "CU requires concrete types"
      #'(CU* . tys+)]))
 
+(define-named-type-alias Nothing (CU))
+
 ;; internal symbolic union constructor
 (define-type-constructor U* #:arity >= 0)
 
@@ -66,10 +75,6 @@
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...))
      #'(U* . tys-)]))
 
-(begin-for-syntax
-  (define (concrete? t)
-    (not (or (Any? t) (U*? t)))))
-
 ;; ---------------------------------
 ;; case-> and Ccase->
 
@@ -109,7 +114,7 @@
 (define-named-type-alias Bool (add-predm (U CBool) ro:boolean?))
 (define-named-type-alias String (U CString))
 (define-named-type-alias (CParam X) (Ccase-> (C→ X)
-                                             (C→ X stlc+cons:Unit)))
+                                             (C→ X CUnit)))
 
 (define-syntax →
   (syntax-parser
@@ -146,7 +151,18 @@
           (ro:define-symbolic y ... pred-))]])
 
 ;; ---------------------------------
-;; assert-type
+;; assert, assert-type
+
+(define-typed-syntax assert
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇒ : _]]
+   --------
+   [⊢ [_ ≫ (ro:assert e-) ⇒ : CUnit]]]
+  [(_ e m) ≫
+   [⊢ [e ≫ e- ⇒ : _]]
+   [⊢ [m ≫ m- ⇐ : (CU CString (C→ Nothing))]]
+   --------
+   [⊢ [_ ≫ (ro:assert e- m-) ⇒ : CUnit]]])
 
 (define-typed-syntax assert-type #:datum-literals (:)
   [(_ e : ty:type) ≫
@@ -175,6 +191,17 @@
           (define-syntax- f (make-rename-transformer (⊢ f- : (C→ ty ... ty_out))))
           (ro:define f- (stlc:λ ([x : ty] ...) (ann e : ty_out))))]])
 
+;; ---------------------------------
+;; quote
+
+(define-typed-syntax quote
+  [(_ x:id) ≫
+   --------
+   [⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]]
+  [(_ (x:id ...)) ≫
+   --------
+   [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CList CSymbol)]]])
+
 ;; ---------------------------------
 ;; Function Application
 
@@ -284,12 +311,14 @@
    --------
    [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
 
-
 ;; ---------------------------------
 ;; Types for built-in operations
 
 (define-rosette-primop equal? : (C→ Any Any Bool))
 (define-rosette-primop eq? : (C→ Any Any Bool))
+(define-rosette-primop error : (C→ (CU CString CSymbol) Nothing))
+
+(define-rosette-primop pi : CNum)
 
 (define-rosette-primop add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
                                        (C→ NegInt (U NegInt Zero))
@@ -329,14 +358,14 @@
                                             (C→ Num Bool)))
 
 ;; rosette-specific
-(define-rosette-primop asserts : (C→ (stlc+cons:List Bool)))
-(define-rosette-primop clear-asserts! : (C→ stlc+cons:Unit))
+(define-rosette-primop asserts : (C→ (CList Bool)))
+(define-rosette-primop clear-asserts! : (C→ CUnit))
 
 ;; ---------------------------------
 ;; BV Types and Operations
 
 (define-named-type-alias BV (add-predm (U CBV) bv?))
-(define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred ro:bitvector?)
+(define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred lifted-bitvector?)
 
 (define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV)
                                      (C→ CInt CPosInt CBV)))

turnstile/examples/stlc+union.rkt

@@ -34,7 +34,7 @@
 
 
 (define-base-types Zero NegInt PosInt Float)
-(define-type-constructor U* #:arity > 0)
+(define-type-constructor U* #:arity >= 0)
 
 (define-for-syntax (prune+sort tys)
   (stx-sort 

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

@@ -3,9 +3,9 @@
 
 (check-type current-bvpred : (CParam CBVPred))
 (check-type (current-bvpred) : BVPred -> (bitvector 4))
-(check-type (current-bvpred (bitvector 5)) : Unit -> (void))
+(check-type (current-bvpred (bitvector 5)) : CUnit -> (void))
 (check-type (current-bvpred) : BVPred -> (bitvector 5))
-(check-type (current-bvpred (bitvector 4)) : Unit -> (void))
+(check-type (current-bvpred (bitvector 4)) : CUnit -> (void))
 
 (check-type (bv 1) : BV)
 (check-type ((bitvector 4) (bv 1)) : Bool -> #t)

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

@@ -4,7 +4,7 @@
 
 (require turnstile/turnstile
          "check-asserts.rkt"
-         (only-in "../../rosette/rosette2.rkt" List Bool Unit))
+         (only-in "../../rosette/rosette2.rkt" CList Bool CUnit))
 
 (define-typed-syntax check-type+asserts #:datum-literals (: ->)
   [(_ e : τ-expected -> v asserts) ≫
@@ -12,6 +12,6 @@
    --------
    [⊢ [_ ≫ (check-equal?/asserts e-
                                  (add-expected v τ-expected)
-                                 (add-expected asserts (List Bool)))
-         ⇒ : Unit]]])
+                                 (add-expected asserts (CList Bool)))
+         ⇒ : CUnit]]])
 

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

@@ -132,27 +132,15 @@
 (typecheck-fail ((bitvector 4) 1))
 (check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool)
 
-;; ;; same as above, but with bvpred
-;; (check-type bvpred : (→ PosInt BVPred))
-;; (check-type (bvpred 3) : BVPred)
-;; (typecheck-fail ((bvpred 4) 1))
-;; (check-type ((bvpred 4) (bv 10 (bvpred 4))) :  Bool)
-;; ;; typed rosette catches this during typechecking, 
-;; ;; whereas untyped rosette uses a runtime exn
-;; (typecheck-fail (bvpred -1) #:with-msg "expected PosInt, given NegInt")
-;; ;(check-runtime-exn (bvpred -1))
-
-;; (typecheck-fail (bitvector? "2"))
-;; (check-type (bitvector? (bitvector 10)) : Bool -> #t)
-;; (typecheck-fail (bvpred? "2"))
-;; (check-type (bvpred? (bvpred 10)) : Bool -> #t)
+(check-type (bitvector? "2") : Bool -> #f)
+(check-type (bitvector? (bitvector 10)) : Bool -> #t)
 
 ;; bvops
 (check-type (bveq (bv 1 3) (bv 1 3)) : Bool -> #t)
 (typecheck-fail (bveq (bv 1 3) 1))
 (check-type (bveq (bv 1 2) (bv 1 3)) : Bool) ; -> runtime exn
 (check-runtime-exn (bveq (bv 1 2) (bv 1 3)))
-
+(clear-asserts!)
 
 (check-type (bvand (bv -1 4) (bv 2 4)) : BV 
             -> (bv 2 4))
@@ -173,7 +161,7 @@
 (check-type (bvshl  (bv 1 4) (bv 2 4)) : BV -> (bv 4 4))
 (check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3))
 (check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5))
-;; TODO: see rosette issue #23
+;; TODO: see rosette issue #23 --- issue closed, won't fix
 (check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV)
 
 (check-type (bvneg (bv -1 4)) : BV -> (bv 1 4))
@@ -183,14 +171,13 @@
 (check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4))
 (check-type (bvsub (bv 0 3)  (bv 1 3)) : BV -> (bv -1 3))
 (check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5))
-;; TODO: see rosette issue #23
+;; TODO: see rosette issue #23 --- issue closed, won't fix
 (check-type (bvadd (bvadd (bv -1 4) (bv 2 4)) (if b (bv 1 4) (bv 3 4))) : BV)
 (check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4))
 (check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3))
 (check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5))
 (check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV 
             -> (if b (bv -1 4) (bv 0 4)))
-
 (check-type (concat (concat (bv -1 4) (bv 0 1)) (bv -1 3)) : BV -> (bv -9 8))
 (check-type (concat (concat (bv -1 4) (if b (bv 0 1) (bv 0 2))) (bv -1 3)) : BV
             -> (if b (bv -9 8) (bv -25 9)))
@@ -206,24 +193,30 @@
 (define-symbolic c boolean? : Bool)
 (check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) 
   : BV -> (if b (bv 13 5) (bv 13 6)))
-;; TODO: change this test to use assert-type
-#;(check-type (zero-extend (bv -3 4) (if b (bitvector 5) "bad"))
-  : BV -> (bv 13 5))
-(check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) 
-  : BV -> (bv 13 5))
+(check-type+asserts
+ (zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred))
+  : BV -> (bv 13 5) (list b))
+(check-type+asserts (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) 
+  : BV -> (bv 13 5) (list c))
 
 (check-type (bitvector->integer (bv -1 4)) : Int -> -1)
 (check-type (bitvector->natural (bv -1 4)) : Int -> 15)
 (check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) 
   : Int -> (if b -1 -3))
-;; TODO: change this test to use assert-type
-;(check-type (bitvector->integer (if b (bv -1 3) "bad")) : BV -> -1)
+(check-type+asserts
+ (bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV))
+ : Int -> -1 (list b))
 (check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2))
 (check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4))
-;; TODO: change this test to use assert-type
-#;(check-type (integer->bitvector (if b pi 3) 
-              (if c (bitvector 5) (bitvector 6))) 
-  : BV -> {[c (bv 3 5)] [(! c) (bv 3 6)]})
+(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : Int)
+                                        (if c (bitvector 5) (bitvector 6)))
+ : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6)))
+         (list (not b)))
+;; TODO: check that CInt also has the right pred (do we want this?)
+#;(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : CInt)
+                                        (if c (bitvector 5) (bitvector 6)))
+ : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6)))
+         (list (not b)))
 (check-type (integer->bitvector 3
               (if c (bitvector 5) (bitvector 6))) 
   : BV -> (if c (bv 3 5) (bv 3 6)))
@@ -273,6 +266,8 @@
 (check-runtime-exn (assert-type (sub1 1) : PosInt))
 (define-symbolic b1 b2 boolean? : Bool)
 
-(check-type (clear-asserts!) : Unit -> (void))
+(check-type (clear-asserts!) : CUnit -> (void))
 (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)))
+
+(check-type (asserts) : (CList Bool) -> (list))