From 34ded7574444cb56b892fc4c44298bef98be8fc1 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 26 Aug 2016 12:42:06 -0400 Subject: [PATCH] fix bv sdsl tests --- turnstile/examples/rosette/bv.rkt | 17 ++++------------- .../examples/tests/rosette/bv-ref-tests.rkt | 2 +- 2 files changed, 5 insertions(+), 14 deletions(-) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 8f1a21b..7482a12 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -8,7 +8,7 @@ #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) (require (only-in "../stlc+lit.rkt" define-primop)) (require (prefix-in ro: rosette)) ; untyped -(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv) +(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*) (prefix-in bv: (only-in sdsl/bv/lang/bvops BV))) (require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form)) (provide thunk) @@ -28,20 +28,11 @@ [⊢ [_ ≫ (bv:BV e-) ⇒ : Unit]]]) (define-primop bv : (Ccase-> (C→ CInt CBV) - (C→ Int BV) (C→ CInt CBVPred CBV) - (C→ Int CBVPred BV) - (C→ CInt CPosInt CBV) - (C→ Int CPosInt BV))) + (C→ CInt CPosInt CBV))) +(define-primop bv* : (Ccase-> (C→ BV) + (C→ CBVPred BV))) -(define-typed-syntax bv* - [(_) ≫ - -------- - [_ ≻ (bv* (current-bvpred))]] - [(_ e_size) ≫ - [⊢ [e_size ≫ e_size- ⇐ : BVPred]] - -------- - [⊢ [_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b)) ⇒ : BV]]]) (define-syntax-rule (bv:bool->bv b) (ro:if b diff --git a/turnstile/examples/tests/rosette/bv-ref-tests.rkt b/turnstile/examples/tests/rosette/bv-ref-tests.rkt index 437f37a..ee22249 100644 --- a/turnstile/examples/tests/rosette/bv-ref-tests.rkt +++ b/turnstile/examples/tests/rosette/bv-ref-tests.rkt @@ -257,7 +257,7 @@ (define-simple-macro (check-equal/rand/bv f) #:with out (syntax/loc this-syntax - (check-equal/rand f #:process (λ ([x : Int]) (bv x)))) + (check-equal/rand f #:process (λ ([x : CInt]) (bv x)))) out) ;; Mask off the rightmost 1-bit. < 1 sec.