commit 98e5cdc77f2a8c9ce1653ad5b2413e9730776f49
parent a9cf9cb2179c959e528558cf63815f37d9b5d5f4
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 29 Aug 2016 11:26:22 -0400
add more assert-type tests
Diffstat:
2 files changed, 57 insertions(+), 10 deletions(-)
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -10,7 +10,8 @@
CU U
C→ → (for-syntax ~C→ C→?)
Ccase-> ; TODO: symbolic case-> not supported yet
- CUnit CList CParam ; TODO: symbolic Param not supported yet
+ CList CParam ; TODO: symbolic Param not supported yet
+ CUnit Unit
CNegInt NegInt
CZero Zero
CPosInt PosInt
@@ -104,15 +105,22 @@
(define-syntax-parser add-predm
[(_ stx pred) (add-pred #'stx #'pred)])
-(define-named-type-alias NegInt (U CNegInt))
-(define-named-type-alias Zero (U CZero))
-(define-named-type-alias PosInt
- (add-predm (U CPosInt)
- (lambda (x)
- (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:positive? x)))))
+(ro:define (ro:zero-integer? x)
+ (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:zero? x)))
+(ro:define (ro:positive-integer? x)
+ (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:positive? x)))
+(ro:define (ro:negative-integer? x)
+ (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:negative? x)))
+(ro:define (no:nonnegative-integer? x)
+ (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:not (ro:#%app ro:negative? x))))
+
+(define-named-type-alias NegInt (add-predm (U CNegInt) ro:negative-integer?))
+(define-named-type-alias Zero (add-predm (U CZero) ro:zero-integer?))
+(define-named-type-alias PosInt (add-predm (U CPosInt) ro:positive-integer?))
(define-named-type-alias Float (U CFloat))
(define-named-type-alias Bool (add-predm (U CBool) ro:boolean?))
(define-named-type-alias String (U CString))
+(define-named-type-alias Unit (add-predm (U CUnit) ro:void?))
(define-named-type-alias (CParam X) (Ccase-> (C→ X)
(C→ X CUnit)))
@@ -132,8 +140,7 @@
(define-named-type-alias CName Cτ)
(define-named-type-alias Name (add-predm (U CName) p?)))]))
-(define-symbolic-named-type-alias Nat (CU CZero CPosInt)
- #:pred (lambda (x) (ro:and (ro:integer? x) (ro:not (ro:negative? x)))))
+(define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred no:nonnegative-integer?)
(define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?)
(define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?)
@@ -346,6 +353,16 @@
(C→ Int Int Int)
(C→ CNum CNum CNum)
(C→ Num Num Num)))
+(define-rosette-primop = : (Ccase-> (C→ CInt CInt CBool)
+ (C→ Int Int Bool)))
+(define-rosette-primop < : (Ccase-> (C→ CInt CInt CBool)
+ (C→ Int Int Bool)))
+(define-rosette-primop > : (Ccase-> (C→ CInt CInt CBool)
+ (C→ Int Int Bool)))
+(define-rosette-primop <= : (Ccase-> (C→ CInt CInt CBool)
+ (C→ Int Int Bool)))
+(define-rosette-primop >= : (Ccase-> (C→ CInt CInt CBool)
+ (C→ Int Int Bool)))
(define-rosette-primop not : (C→ Any Bool))
(define-rosette-primop false? : (C→ Any Bool))
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -262,12 +262,42 @@
(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) ((bitvector 2) bv))) : BVPred)
;; assert-type tests
-(check-type (assert-type (sub1 10) : PosInt) : PosInt -> 9)
+(check-type+asserts (assert-type (sub1 10) : PosInt) : PosInt -> 9 (list))
(check-runtime-exn (assert-type (sub1 1) : PosInt))
(define-symbolic b1 b2 boolean? : Bool)
(check-type (clear-asserts!) : CUnit -> (void))
+;; asserts directly on a symbolic union
(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)))
+;; asserts on the (pc)
+(check-type+asserts (if b1 (assert-type 1 : Int) (assert-type #f : Int)) : Int
+ -> 1 (list b1))
+(check-type+asserts (if b2 (assert-type 1 : Bool) (assert-type #f : Bool)) : Bool
+ -> #f (list (not b2)))
+;; asserts on a define-symbolic value
+(define-symbolic i1 integer? : Int)
+(check-type+asserts (assert-type i1 : PosInt) : PosInt -> i1 (list (< 0 i1)))
+(check-type+asserts (assert-type i1 : Zero) : Zero -> i1 (list (= 0 i1)))
+(check-type+asserts (assert-type i1 : NegInt) : NegInt -> i1 (list (< i1 0)))
+;; TODO: should this assertion be equivalent to (<= 0 i1) ?
+(check-type+asserts (assert-type i1 : Nat) : Nat -> i1 (list (not (< i1 0))))
+;; asserts on other terms involving define-symbolic values
+(check-type+asserts (assert-type (+ i1 1) : PosInt) : PosInt -> (+ 1 i1) (list (< 0 (+ 1 i1))))
+(check-type+asserts (assert-type (+ i1 1) : Zero) : Zero -> (+ 1 i1) (list (= 0 (+ 1 i1))))
+(check-type+asserts (assert-type (+ i1 1) : NegInt) : NegInt -> (+ 1 i1) (list (< (+ 1 i1) 0)))
+
+(check-type+asserts (assert-type (if b1 i1 b2) : Int) : Int -> (if b1 i1 b2) (list b1))
+(check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> (if b1 i1 b2) (list (not b1)))
+;; asserts on the (pc)
+(check-type+asserts (if b1 (assert-type i1 : Int) (assert-type b2 : Int)) : Int
+ -> i1 (list b1))
+(check-type+asserts (if b1 (assert-type i1 : Bool) (assert-type b2 : Bool)) : Bool
+ -> b2 (list (not b1)))
+;; TODO: should assert-type cause some predicates to return true or return false?
+(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Int)) : Bool -> b1 (list b1))
+(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> b1 (list (not b1)))
+(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> (not b1) (list b1))
+(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> (not b1) (list (not b1)))
(check-type (asserts) : (CList Bool) -> (list))
