commit 6fdffbcb34361287b432749f69d52d6344ec2a81
parent e17ae9e5feb5992e6e4e5955afa7414919275f7a
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 19 Jul 2016 15:46:03 -0400
fix bv tests
Diffstat:
4 files changed, 24 insertions(+), 33 deletions(-)
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -1,13 +1,12 @@
#lang turnstile
-(extends "rosette.rkt" #:except bv) ; extends typed rosette
+(extends "rosette.rkt" #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) ; extends typed rosette
(require (prefix-in ro: rosette)) ; untyped
-(require (except-in "rosette.rkt" #%app define)) ; typed
+;(require (except-in "rosette.rkt" #%app define)) ; typed
(require (only-in sdsl/bv/lang/bvops bvredand bvredor)
(prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
(require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
(provide bool->bv thunk)
-;(define current-bvpred-internal (ro:make-parameter (ro:bitvector 4)))
;; this must be a macro in order to support Racket's overloaded set/get
;; parameter patterns
(define-typed-syntax current-bvpred
@@ -39,15 +38,10 @@
--------
[⊢ [[_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b))] ⇒ : BV]]])
-(define-syntax-rule (bool->bv b) (if b (bv 1) (bv 0)))
-#;(define-typed-syntax bool->bv
- [(_ e) ≫
- [⊢ [[e ≫ e-] ⇐ : Bool]]
- --------
- [⊢ [[_ ≫ (if- e- (bv 1) (bv 0))] ⇒ : BV]]])
-
-;; (define- (bvredor x) (ro:bveq (ro:bveq x (bv 0)) (bv 0)))
-;; (define- (bvredand x) (ro:bveq x (bv -1)))
+(define-syntax-rule (bool->bv b)
+ (rosette:if b
+ (bv (rosette:#%datum . 1))
+ (bv (rosette:#%datum . 0))))
(define-primop bvredor : (→ BV BV))
(define-primop bvredand : (→ BV BV))
@@ -64,7 +58,7 @@
(define-typed-syntax define-fragment
[(_ (id param ...) #:implements spec #:library lib-expr) ≫
--------
- [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
+ [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette:#%datum . 4))]]
[(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
[⊢ [[spec ≫ spec-] ⇒ : ty_spec]]
[#:fail-unless (→? #'ty_spec) "spec must be a function"]
@@ -96,18 +90,4 @@
--------
[⊢ [[_ ≫ (bv:bvlib [{id- ...} n-] ...)] ⇒ : Lib]]])
-
-#;(define-typed-syntax synthesize-fragment
- [(_ (id param ...) #:implements spec #:library lib-expr)
- --------
- [_ ≻ (synthesize-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
- [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv)
- [⊢ [[spec ≫ spec-] ⇐ : Spec]]
- [⊢ [[lib-expr ≫ lib-expr-] ⇐ : Lib]]
- [⊢ [[minbv ≫ minbv-] ⇐ : Int]]]
- --------
- [⊢ [[_ ≫ (bv:synthesize-fragment (id param) #:implements spec-
- #:library lib-expr-
- #:minbv minbv-)] ⇒ : BV]])
-
-(define-syntax-rule (thunk e) (λ () e))
+(define-syntax-rule (thunk e) (rosette:λ () e))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -2,8 +2,9 @@
;(require (only-in rosette bv bitvector))
;(require (only-in rosette [exact-integer? integer?]))
(extends "../ext-stlc.rkt" #:except if)
+(reuse List #:from "../stlc+cons.rkt")
(require (prefix-in stlc: (only-in "../stlc+reco+var.rkt" define λ)))
-(require (only-in "../stlc+reco+var.rkt" define-type-alias))
+(require (only-in "../stlc+reco+var.rkt" define-type-alias Int Bool →))
(require (prefix-in ro: rosette))
(provide BVPred)
@@ -31,6 +32,16 @@
;; ----------------------------------------------------------------------------
;; Racket stuff
+(define-base-type Symbol)
+
+(define-typed-syntax quote
+ [(_ x:id) ≫
+ --------
+ [⊢ [[_ ≫ (quote- x)] ⇒ : Symbol]]]
+ [(_ (x:id ...)) ≫
+ --------
+ [⊢ [[_ ≫ (quote- (x ...))] ⇒ : (stlc+cons:List Symbol)]]])
+
(define-type-constructor Param #:arity = 1)
(define-rosette-primop boolean? : (→ Bool Bool))
diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt
@@ -19,8 +19,8 @@
(syntax-parser #:datum-literals (:)
[(define-primop op:id : τ:type)
#:with op/tc (generate-temporary #'op)
- #'(begin-
- (provide- (rename-out- [op/tc op]))
+ #`(begin-
+ (provide- #,(syntax/loc this-syntax (rename-out- [op/tc op])))
(define-primop op/tc op : τ))]
[(define-primop op/tc op : τ)
#'(begin-
diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt
@@ -22,8 +22,8 @@
(check-type (bool->bv i) : BV -> (bv 1))
(check-type (bool->bv b) : BV -> (if b (bv 1) (bv 0)))
-(check-type (bvredor (bv 1)) : Bool)
-(check-type (bvredand (bv 1)) : Bool)
+(check-type (bvredor (bv 1)) : BV)
+(check-type (bvredand (bv 1)) : BV)
(check-type bveq : (→ BV BV BV))
(check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1))
