commit 513f6dcfd442011e335c405934b0d207a26ef2cf
parent 1a14c5e377ad173e458194bf2e70f6d3b87edc96
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 29 Aug 2016 16:13:46 -0400
use type-cast and assert-pred for assert-type
Diffstat:
4 files changed, 80 insertions(+), 46 deletions(-)
diff --git a/turnstile/examples/rosette/lifted-bitvector-pred.rkt b/turnstile/examples/rosette/lifted-bitvector-pred.rkt
@@ -1,23 +0,0 @@
-#lang rosette
-
-(provide bitvector?)
-
-(require (only-in rosette [bitvector? concrete-bitvector?]))
-
-(define (bitvector? v)
- (for/all ([v v])
- (concrete-bitvector? v)))
-
-(module+ test
- (require rackunit)
- (define-symbolic b1 b2 b3 boolean?)
- (check-true (bitvector? (if b1 (bitvector 4) (bitvector 3))))
- (check-false (bitvector? (if b1 "bad" 'also-bad)))
- (check-equal? (bitvector? (if b1 (bitvector 4) "bad")) b1)
- (check-equal? (bitvector? (if b1 "bad" (bitvector 4))) (not b1))
-
- (check-true (bitvector? (if b1 (bitvector 4) (if b2 (bitvector 3) (bitvector 2)))))
- (check-false (bitvector? (if b1 "bad" (if b2 'also-bad 5))))
- (check-equal? (bitvector? (if b1 (bitvector 4) (if b2 "bad" (bitvector 2)))) (or b1 (not b2)))
- (check-equal? (bitvector? (if b1 "bad" (if b2 (bitvector 4) 'also-bad))) (and (not b1) b2))
- )
diff --git a/turnstile/examples/rosette/rosette-util.rkt b/turnstile/examples/rosette/rosette-util.rkt
@@ -0,0 +1,66 @@
+#lang rosette
+
+(provide assert-pred
+ bitvector?
+ zero-integer?
+ positive-integer?
+ negative-integer?
+ nonnegative-integer?)
+
+(require (only-in rosette [bitvector? concrete-bitvector?]))
+
+;; bitvector? : Any -> Bool
+(define (bitvector? v)
+ (for/all ([v v])
+ (concrete-bitvector? v)))
+
+;; assert-pred : A [A -> Bool] -> A
+(define (assert-pred a pred)
+ (if (type? pred)
+ (type-cast pred a)
+ (begin
+ (assert (pred a))
+ a)))
+
+;; zero-integer? : Any -> Bool
+(define (zero-integer? x)
+ (and (integer? x) (zero? x)))
+
+;; positive-integer? : Any -> Bool
+(define (positive-integer? x)
+ (and (integer? x) (positive? x)))
+
+;; negative-integer? : Any -> Bool
+(define (negative-integer? x)
+ (and (integer? x) (negative? x)))
+
+;; nonnegative-integer? : Any -> Bool
+(define (nonnegative-integer? x)
+ (and (integer? x) (not (negative? x))))
+
+(module+ test
+ (require rackunit "../tests/rosette/check-asserts.rkt")
+ (define-symbolic b1 b2 b3 boolean?)
+
+ ;; bitvector?
+ (check-true (bitvector? (if b1 (bitvector 4) (bitvector 3))))
+ (check-false (bitvector? (if b1 "bad" 'also-bad)))
+ (check-equal? (bitvector? (if b1 (bitvector 4) "bad")) b1)
+ (check-equal? (bitvector? (if b1 "bad" (bitvector 4))) (not b1))
+
+ (check-true (bitvector? (if b1 (bitvector 4) (if b2 (bitvector 3) (bitvector 2)))))
+ (check-false (bitvector? (if b1 "bad" (if b2 'also-bad 5))))
+ (check-equal? (bitvector? (if b1 (bitvector 4) (if b2 "bad" (bitvector 2)))) (or b1 (not b2)))
+ (check-equal? (bitvector? (if b1 "bad" (if b2 (bitvector 4) 'also-bad))) (and (not b1) b2))
+
+ (clear-asserts!)
+
+ ;; assert-pred with type? predicates
+ (check-equal?/asserts (assert-pred (if b1 1 #f) integer?) 1 (list b1))
+ (check-equal?/asserts (assert-pred (if b1 1 #f) boolean?) #f (list (not b1)))
+ (check-equal?/asserts (assert-pred (if b1 (bv 3 4) "bad") (bitvector 4)) (bv 3 4) (list b1))
+
+ ;; assert-pred with non-type? predicates
+ (check-equal?/asserts (assert-pred (if b1 1 -1) positive?) (if b1 1 -1) (list b1))
+ (check-equal?/asserts (assert-pred (if b1 1 -1) negative?) (if b1 1 -1) (list (not b1)))
+ )
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -38,7 +38,7 @@
(only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
(only-in "../stlc+cons.rkt" [~List ~CList])
(only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop)
- (only-in "lifted-bitvector-pred.rkt" [bitvector? lifted-bitvector?]))
+ (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?]))
;; copied from rosette.rkt
(define-simple-macro (define-rosette-primop op:id : ty)
@@ -107,18 +107,9 @@
(define-syntax-parser add-predm
[(_ stx pred) (add-pred #'stx #'pred)])
-(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 NegInt (add-predm (U CNegInt) negative-integer?))
+(define-named-type-alias Zero (add-predm (U CZero) zero-integer?))
+(define-named-type-alias PosInt (add-predm (U CPosInt) 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))
@@ -142,7 +133,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 no:nonnegative-integer?)
+(define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred 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?)
@@ -210,7 +201,7 @@
[⊢ [e ≫ e- ⇒ : _]]
#:with pred (get-pred #'ty.norm)
--------
- [⊢ [_ ≫ (ro:let ([x e-]) (ro:assert (ro:#%app pred x)) x) ⇒ : ty.norm]]])
+ [⊢ [_ ≫ (ro:#%app assert-pred e- pred) ⇒ : ty.norm]]])
;; ---------------------------------
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -268,8 +268,8 @@
(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)))
+(check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> 1 (list b1))
+(check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> #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))
@@ -287,17 +287,17 @@
(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)))
+(check-type+asserts (assert-type (if b1 i1 b2) : Int) : Int -> i1 (list b1))
+(check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> 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 (integer? (assert-type (if b1 i1 b2) : Int)) : Bool -> #t (list b1))
+(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #f (list (not b1)))
+(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> #f (list b1))
+(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1)))
(check-type (asserts) : (CList Bool) -> (list))
