suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

eliminate type annotation in define-symbolic

Browse Source 
- relevant preds have analogous type as stx prop
- add extra more precise solvable? and function? stx props
- define-symbolic et al require explicit preds (no exprs) (for now)
This commit is contained in:
Stephen Chang 2016-09-07 12:23:50 -04:00
parent e3fc26354d
commit 8e55e44363
9 changed files with 202 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
turnstile/examples/rosette/rosette-notes.txt
View File

@ -54,6 +54,11 @@ TODOs:
- add pred properties to types
- use it to validate given pred in define-symbolic
- STARTED 2016-08-25
- alternative: don't require type, but associate type with pred?
- advantage: soundness
- disadvantage: cannot compute pred in define-symbolic
- Rosette users won't care?
- TODO: add extra type rules to propagate 'typefor tag
- implement assert-type, which adds to the assertion store
- DONE 2016-08-25
- add polymorphism

166
turnstile/examples/rosette/rosette2.rkt
View File

@ -85,7 +85,8 @@
(define-type-constructor CMVectorof #:arity = 1)
(define-type-constructor CBoxof #:arity = 1)
;; TODO: Hash subtyping?
(define-type-constructor HashTable #:arity = 2)
;; - invariant for now, like TR, though Rosette only uses immutable hashes?
(define-type-constructor CHashTable #:arity = 2)
(define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X)))
(define-type-constructor CList #:arity >= 0)
@ -134,10 +135,28 @@
(define (add-pred stx pred)
(set-stx-prop/preserved stx 'pred pred))
(define (get-pred stx)
(syntax-property stx 'pred)))
(syntax-property stx 'pred))
(define (add-typefor stx t)
(set-stx-prop/preserved stx 'typefor t))
(define (get-typefor stx)
(syntax-property stx 'typefor))
(define (mark-solvable stx)
(set-stx-prop/preserved stx 'solvable? #t))
(define (solvable? stx)
(syntax-property stx 'solvable?))
(define (mark-function stx)
(set-stx-prop/preserved stx 'function? #t))
(define (function? stx)
(syntax-property stx 'function?)))
(define-syntax-parser add-predm
[(_ stx pred) (add-pred #'stx #'pred)])
(define-syntax-parser add-typeform
[(_ stx t) (add-typefor #'stx #'t)])
(define-syntax-parser mark-solvablem
[(_ stx) (mark-solvable #'stx)])
(define-syntax-parser mark-functionm
[(_ stx) (mark-function #'stx)])
(define-named-type-alias NegInt (add-predm (U CNegInt) negative-integer?))
(define-named-type-alias Zero (add-predm (U CZero) zero-integer?))
@ -177,51 +196,55 @@
;; ---------------------------------
;; define-symbolic
(define-typed-syntax define-symbolic #:datum-literals (:)
[(_ x:id ...+ pred : ty:type) ≫
#:fail-when (concrete? #'ty.norm)
(format "A symbolic value cannot have a concrete type, given ~a."
(type->str #'ty.norm))
;; TODO: still unsound
[⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
(define-typed-syntax define-symbolic
[(_ x:id ...+ pred?) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
#:with (y ...) (generate-temporaries #'(x ...))
--------
[_ ≻ (begin-
(define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
(ro:define-symbolic y ... pred-))]])
(define-syntax- x (make-rename-transformer (⊢ y : ty))) ...
(ro:define-symbolic y ... pred?-))]])
(define-typed-syntax define-symbolic* #:datum-literals (:)
[(_ x:id ...+ pred : ty:type) ≫
#:fail-when (concrete? #'ty.norm)
(format "A symbolic value cannot have a concrete type, given ~a."
(type->str #'ty.norm))
;; TODO: still unsound
[⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
(define-typed-syntax define-symbolic*
[(_ x:id ...+ pred?) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
#:with (y ...) (generate-temporaries #'(x ...))
--------
[_ ≻ (begin-
(define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
(ro:define-symbolic* y ... pred-))]])
(define-syntax- x (make-rename-transformer (⊢ y : ty))) ...
(ro:define-symbolic* y ... pred?-))]])
;; TODO: support internal definition contexts
(define-typed-syntax let-symbolic
[(_ ([(x:id ...+) pred : ty:type]) e ...) ≫
[⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
[([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
[(_ (x:id ...+ pred?) e ...) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
[([x ≫ x- : ty] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
--------
[⊢ [_ ≫ (ro:let-values
([(x- ...) (ro:let ()
(ro:define-symbolic x ... pred-)
(ro:define-symbolic x ... pred?-)
(ro:values x ...))])
e-) ⇒ : τ_out]]])
(define-typed-syntax let-symbolic*
[(_ ([(x:id ...+) pred : ty:type]) e ...) ≫
[⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
[([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
[(_ (x:id ...+ pred?) e ...) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
#:fail-unless (syntax-e #'s?)
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'pred?))
[([x ≫ x- : ty] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
--------
[⊢ [_ ≫ (ro:let-values
([(x- ...) (ro:let ()
(ro:define-symbolic* x ... pred-)
(ro:define-symbolic* x ... pred?-)
(ro:values x ...))])
e-) ⇒ : τ_out]]])
@ -455,7 +478,11 @@
;; ---------------------------------
;; hash tables
(define-rosette-primop hash-keys : (C→ (HashTable Any Any) (CListof Any)))
(define-typed-syntax hash-keys
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : (~CHashTable τ _)]]
--------
[⊢ [_ ≫ (ro:hash-keys e-) ⇒ : (CListof τ)]]])
;; ---------------------------------
;; lists
@ -734,9 +761,6 @@
[true : CTrue]
[false : CFalse]
[boolean? : (C→ Any Bool)]
[integer? : (C→ Any Bool)]
[real? : (C→ Any Bool)]
[number? : (C→ Any Bool)]
[positive? : (Ccase-> (C→ CNum CBool)
(C→ Num Bool))]
@ -763,6 +787,49 @@
[asserts : (C→ (CListof Bool))]
[clear-asserts! : (C→ CUnit)]))
;; ---------------------------------
;; more built-in ops
;(define-rosette-primop boolean? : (C→ Any Bool))
(define-typed-syntax boolean?
[_:id ≫
--------
[⊢ [_ ≫ (mark-solvablem
(add-typeform
ro:boolean?
Bool))
⇒ : (C→ Any Bool)]]]
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : ty]]
--------
[⊢ [_ ≫ (ro:boolean? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]])
;(define-rosette-primop integer? : (C→ Any Bool))
(define-typed-syntax integer?
[_:id ≫
--------
[⊢ [_ ≫ (mark-solvablem
(add-typeform
ro:integer?
Int))
⇒ : (C→ Any Bool)]]]
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : ty]]
--------
[⊢ [_ ≫ (ro:integer? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]])
;(define-rosette-primop real? : (C→ Any Bool))
(define-typed-syntax real?
[_:id ≫
--------
[⊢ [_ ≫ (mark-solvablem
(add-typeform
ro:real?
Num)) ⇒ : (C→ Any Bool)]]]
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : ty]]
--------
[⊢ [_ ≫ (ro:real? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]])
;; ---------------------------------
;; mutable boxes
@ -801,7 +868,6 @@
(provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV)
(C→ CInt CPosInt CBV))]
[bv? : (C→ Any Bool)]
[bitvector : (C→ CPosInt CBVPred)]
[bitvector? : (C→ Any Bool)]
[bveq : (C→ BV BV Bool)]
@ -846,14 +912,38 @@
[bitvector-size : (C→ CBVPred CPosInt)]))
;(define-rosette-primop bitvector : (C→ CPosInt CBVPred))
(define-typed-syntax bitvector
[_:id ≫
--------
[⊢ [_ ≫ ro:bitvector ⇒ : (C→ CPosInt CBVPred)]]]
[(_ n) ≫
[⊢ [n ≫ n- ⇐ : CPosInt]]
--------
[⊢ [_ ≫ (mark-solvablem
(add-typeform
(ro:bitvector n-)
BV)) ⇒ : CBVPred]]])
;; ---------------------------------
;; Uninterpreted functions
(define-typed-syntax ~>
[(_ e ...+) ≫
[⊢ [e ≫ e- ⇐ : (C→ Nothing Bool)] ...]
[(_ pred? ...+) ≫
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
#:fail-unless (stx-andmap syntax-e #'(s? ...))
(format "Must provide a Rosette-solvable type, given ~a."
(syntax->datum #'(pred? ...)))
#:fail-when (stx-ormap syntax-e #'(f? ...))
(format "Must provide a non-function Rosette type, given ~a."
(syntax->datum #'(pred? ...)))
--------
[⊢ [_ ≫ (ro:~> e- ...) ⇒ : (C→ Any Bool)]]])
[⊢ [_ ≫ (mark-solvablem
(mark-functionm
(add-typeform
(ro:~> pred?- ...)
(C→ ty ...))))
⇒ : (C→ Any Bool)]]])
;; ---------------------------------
;; Logic operators
@ -925,9 +1015,9 @@
(provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
; TODO: implement hash
[model : (C→ CSolution (HashTable Any Any))]
[model : (C→ CSolution (CHashTable Any Any))]
[sat : (Ccase-> (C→ CSolution)
(C→ (HashTable Any Any) CSolution))]
(C→ (CHashTable Any Any) CSolution))]
[sat? : (C→ Any Bool)]
[unsat? : (C→ Any Bool)]
[unsat : (Ccase-> (C→ CSolution)

4
turnstile/examples/tests/rosette/bv-tests.rkt
View File

@ -17,8 +17,8 @@
(check-type (if 1 (bv 1) (bv 0)) : BV -> (bv 1))
(check-type (if #f (bv 1) (bv 0)) : BV -> (bv 0))
(define-symbolic i integer? : Int)
(define-symbolic b boolean? : Bool)
(define-symbolic i integer?)
(define-symbolic b boolean?)
(check-type (if i (bv 1) (bv 0)) : BV -> (bv 1))
(check-type (if b (bv 1) (bv 0)) : BV -> (if b (bv 1) (bv 0)))

16
turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
View File

@ -4,7 +4,7 @@
;; all examples from the Rosette Guide, Sec 2
(define-symbolic b boolean? : Bool)
(define-symbolic b boolean?)
(check-type b : Bool)
(check-type (boolean? b) : Bool -> #t)
(check-type (integer? b) : Bool -> #f)
@ -25,17 +25,17 @@
(check-type (not b) : Bool -> (! b))
(check-type (boolean? (not b)) : Bool -> #t)
(define-symbolic* n integer? : Int)
(define-symbolic* n integer?)
;; TODO: support internal definition contexts
(define (static -> Bool)
(let-symbolic ([(x) boolean? : Bool]) x))
(let-symbolic (x boolean?) x))
#;(define (static -> Bool)
(define-symbolic x boolean? : Bool) ; creates the same constant when evaluated
x)
(define (dynamic -> Int)
(let-symbolic* ([(y) integer? : Int]) y))
(let-symbolic* (y integer?) y))
#;(define (dynamic -> Int)
(define-symbolic* y integer? : Int) ; creates a different constant when evaluated
y)
@ -52,7 +52,7 @@
(check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2))
(define (yet-another-x -> Bool)
(let-symbolic ([(x) boolean? : Bool]) x))
(let-symbolic (x boolean?) x))
(check-type (eq? (static) (yet-another-x))
: Bool -> (<=> (static) (yet-another-x)))
@ -82,7 +82,7 @@
;; 2.3.1 Verification
(define-symbolic i integer? : Int)
(define-symbolic i integer?)
(define cex (verify (same poly factored i)))
(check-type cex : CSolution)
(check-type (sat? cex) : Bool -> #t)
@ -124,7 +124,7 @@
;; 2.3.4 Angelic Execution
(define-symbolic x y integer? : Int)
(define-symbolic x y integer?)
(define sol
(solve (begin (assert (not (= x y)))
(assert (< (abs x) 10))
@ -141,7 +141,7 @@
;; 2.4 Symbolic Reasoning
(define-symbolic x1 y1 real? : Num)
(define-symbolic x1 y1 real?)
(check-type (current-bitwidth) : (CU CPosInt CFalse) -> 5)
(check-type (current-bitwidth #f) : CUnit -> (void))
(check-type (current-bitwidth) : (CU CPosInt CFalse) -> #f)

17
turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
View File

@ -13,7 +13,8 @@
;; y1 unchanged: 0
(check-type y1 : Nat -> 0)
;; symbolic effect!
(define-symbolic x1 boolean? : Bool)
(define-symbolic x1 boolean?)
(typecheck-fail (define-symbolic x1 boolean? : Bool))
(check-type (if x1 (void) (set! y1 3)) : Unit -> (void))
;; y1 symbolic: (ite x1 0 3)
(check-type y1 : Nat -> (if x1 0 3))
@ -25,7 +26,7 @@
(printf "y unchanged: ~a\n" y)
(if #f (set! y 3) (void))
(printf "y unchanged: ~a\n" y)
(let-symbolic ([(x) boolean? : Bool])
(let-symbolic (x boolean?)
(if x (void) (set! y 3))
(printf "y symbolic: ~a\n" y)
(list x y))))
@ -41,13 +42,13 @@
;; 3.2.1 Symbolic Constants
(define (always-same -> Int)
(let-symbolic ([(x) integer? : Int])
(let-symbolic (x integer?)
x))
(check-type (always-same) : Int)
(check-type (eq? (always-same) (always-same)) : Bool -> #t)
(define (always-different -> Int)
(let-symbolic* ([(x) integer? : Int])
(let-symbolic* (x integer?)
x))
(check-type (always-different) : Int)
(define diff-sym*1 (always-different))
@ -58,7 +59,7 @@
(check-type+asserts (assert #t) : Unit -> (void) (list))
(check-type+asserts (assert 1) : Unit -> (void) (list))
(define-symbolic x123 boolean? : Bool)
(define-symbolic x123 boolean?)
(check-type+asserts (assert x123) : Unit -> (void) (list x123))
(check-runtime-exn (assert #f "bad value"))
@ -67,7 +68,7 @@
(check-type (asserts) : (CListof Bool) -> (list))
;; 3.2.3 Angelic Execution
(define-symbolic x y boolean? : Bool)
(define-symbolic x y boolean?)
(check-type (assert x) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list x))
(define solve-sol (solve (assert y)))
@ -90,7 +91,7 @@
(clear-asserts!)
;; 3.2.5 Synthesis
(define-symbolic synth-x synth-c integer? : Int)
(define-symbolic synth-x synth-c integer?)
(check-type (assert (even? synth-x)) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
(define synth-sol
@ -103,7 +104,7 @@
;; 3.2.6 Optimization
(current-bitwidth #f) ; use infinite-precision arithmetic
(define-symbolic opt-x opt-y integer? : Int)
(define-symbolic opt-x opt-y integer?)
(check-type (assert (< opt-x 2)) : Unit -> (void))
(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
(define opt-sol

30
turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
View File

@ -2,7 +2,7 @@
(require "../rackunit-typechecking.rkt"
"check-type+asserts.rkt")
;; Examples from the Rosette Guide, Section 4
;; Examples from the Rosette Guide, Section 4.1 - 4.2
;; 4.1 Equality
@ -22,15 +22,16 @@
(check-type (equal? (list (box 1)) (list (box 1))) : Bool -> #t)
(check-type (equal? (list (box 1)) (list (box 1.0))) : Bool -> #t)
(define-symbolic n integer? : Int)
(define-symbolic n integer?)
(check-type (equal? n 1) : Bool -> (= 1 n))
(check-type (equal? (box n) (box 1)) : Bool -> (= 1 n))
(check-not-type (equal? n 1) : CBool)
(check-not-type (equal? (box n) (box 1)) : CBool)
(define-symbolic f g (~> integer? integer?) : (→ Int Int))
(typecheck-fail
(define-symbolic f g (~> integer? integer?) : (C→ Int Int))
#:with-msg "symbolic value cannot have a concrete type")
(typecheck-fail (~> positive?)
#:with-msg "Must provide a Rosette\\-solvable type, given.*positive?")
(typecheck-fail (~> (~> integer?))
#:with-msg "Must provide a non\\-function Rosette type, given.*~> integer?")
(define-symbolic f g (~> integer? integer?))
(check-type f : (→ Int Int))
(check-type g : (→ Int Int))
(check-type (equal? f g) : Bool -> #f)
@ -49,16 +50,16 @@
(check-type (distinct?) : Bool -> #t)
(check-type (distinct? 1) : Bool -> #t)
(check-type (distinct? (list 1 2) (list 3) (list 1 2)) : Bool -> #f)
(define-symbolic x y z integer? : Int)
(define-symbolic x y z integer?)
(check-type (distinct? 3 z x y 2) : Bool -> (distinct? 2 3 x y z))
(define-symbolic b boolean? : Bool)
(define-symbolic b boolean?)
(check-type (distinct? 3 (bv 3 4) (list 1) (list x) y 2)
: Bool -> (&& (! (= 3 y)) (&& (! (= 1 x)) (! (= 2 y)))))
(clear-asserts!)
;; 4.2 Booleans, Integers, and Reals
;(define-symbolic b boolean? : Bool)
;(define-symbolic b boolean?)
(check-type (boolean? b) : Bool -> #t)
(check-type (boolean? #t) : Bool -> #t)
(check-type (boolean? #f) : Bool -> #t)
@ -211,7 +212,7 @@
(check-type (||) : Bool -> #f)
; no shortcircuiting
(check-type (&& #f (begin (displayln "hello") #t)) : Bool -> #f)
(define-symbolic a boolean? : Bool)
(define-symbolic a boolean?)
; 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
@ -227,21 +228,22 @@
(current-bitwidth #f)
(define-symbolic a1 b1 integer? : Int)
(define-symbolic a1 b1 integer?)
(check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1))
(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
; so the model has no bindings
(define sol1 (solve (assert f1)))
(check-type sol1 : CSolution)
(check-type (model sol1) : (HashTable Any Any))
(check-type (model sol1) : (CHashTable Any Any))
(check-type (hash-keys (model sol1)) : (CListof Any) -> (list)) ; empty solution
(check-type (sat? sol1) : Bool -> #t)
(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b is free in g
(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b1 is free in g1
; so the model has a binding for b
(define sol2 (solve (assert g1)))
(check-type sol2 : CSolution)
(check-type (sat? sol2) : Bool -> #t)
(check-type (evaluate b1 sol2) : Int -> 0)
(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1))))) ; body refers to the innermost a
; body refers to the innermost a1
(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1)))))
; so h is unsatisfiable.
(check-type (solve (assert h)) : CSolution -> (unsat))

22
turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt Normal file
View File

@ -0,0 +1,22 @@
#lang s-exp "../../rosette/rosette2.rkt"
(require "../rackunit-typechecking.rkt"
"check-type+asserts.rkt")
;; Examples from the Rosette Guide, Section 4.3
;; 4.3 Bitvectors
; a bitvector literal of size 7
(check-type (bv 4 (bitvector 7)) : BV -> (bv 4 7))
(check-type (bv 4 7) : BV -> (bv 4 7))
(define-symbolic x y (bitvector 7)) ; symbolic bitvector constants
(check-type x : BV)
(check-type y : BV)
(check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #f)
;; > (bvult (bv 4 7) (bv -1 7)) ; unsigned 7-bit < comparison of 4 and -1
;; #t
;; > (define-symbolic b boolean?)
;; > (bvadd x (if b y (bv 3 4))) ; this typechecks only when b is true
;; (bvadd x y)
;; > (asserts) ; so Rosette emits a corresponding assertion
;; '(b)

18
turnstile/examples/tests/rosette/rosette2-tests.rkt
View File

@ -99,8 +99,10 @@
;; non-bool test
(check-type (if 1 2 3) : CInt)
;; else, if expr produces symbolic type
(define-symbolic b0 boolean? : Bool)
(define-symbolic i0 integer? : Int)
(define-symbolic b0 boolean?)
(define-symbolic i0 integer?)
(typecheck-fail (define-symbolic posint1 positive?)
#:with-msg "Must provide a Rosette-solvable type, given positive?")
(check-type (if b0 1 2) : Int)
(check-not-type (if b0 1 2) : CInt)
(check-type (if #t i0 2) : Int)
@ -154,7 +156,7 @@
(check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3))
(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
(define-symbolic b boolean? : Bool)
(define-symbolic b boolean?)
(check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV
-> (if b (bv 3 4) (bv 2 4)))
@ -166,7 +168,7 @@
(check-type (bvneg (bv -1 4)) : BV -> (bv 1 4))
(check-type (bvneg (bv 0 4)) : BV -> (bv 0 4))
(define-symbolic z (bitvector 3) : BV)
(define-symbolic z (bitvector 3))
(check-type (bvneg z) : BV)
(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))
@ -184,13 +186,13 @@
(check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2))
(check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1))
(define-symbolic i j integer? : Int)
(define-symbolic i j integer?)
(check-type (extract i j (bv 1 2)) : BV)
; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...})
(check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6))
(check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6))
(define-symbolic c boolean? : Bool)
(define-symbolic c boolean?)
(check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))
: BV -> (if b (bv 13 5) (bv 13 6)))
(check-type+asserts
@ -264,7 +266,7 @@
;; assert-type tests
(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)
(define-symbolic b1 b2 boolean?)
(check-type (clear-asserts!) : CUnit -> (void))
;; asserts directly on a symbolic union
@ -276,7 +278,7 @@
(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)
(define-symbolic i1 integer?)
(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)))

3
turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
View File

@ -5,7 +5,8 @@
(do-tests "rosette2-tests.rkt" "General"
"rosette-guide-sec2-tests.rkt" "Rosette Guide, Section 2"
"rosette-guide-sec3-tests.rkt" "Rosette Guide, Section 3"
"rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4")
"rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4.1-4.2"
"rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3")
(do-tests "bv-tests.rkt" "BV SDSL - General"
"bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")