Skip to content

Commit

Permalink
Merge pull request #28 from AlexKnauth/patch-1
Browse files Browse the repository at this point in the history
use make-variable-like-transformer for bitvector and bv
  • Loading branch information
emina authored Jul 29, 2016
2 parents 1226edf + 07aacdb commit 4c6a5bb
Showing 1 changed file with 4 additions and 7 deletions.
11 changes: 4 additions & 7 deletions rosette/base/core/bitvector.rkt
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#lang racket

(require (for-syntax racket/syntax) racket/stxparam racket/stxparam-exptime)
(require racket/stxparam racket/stxparam-exptime
(for-syntax racket/syntax syntax/transformer))
(require "term.rkt" "union.rkt" "bool.rkt" "polymorphic.rkt"
"merge.rkt" "safe.rkt" "lift.rkt" "forall.rkt")
(require (only-in "real.rkt" @>= @> @= @integer? T*->integer?))
Expand Down Expand Up @@ -70,9 +71,7 @@
(define-match-expander @bitvector
(syntax-rules ()
[(_ sz) (bitvector sz)])
(syntax-id-rules (set!)
[(@bitvector sz) (bitvector-type sz)]
[@bitvector bitvector-type]))
(make-variable-like-transformer #'bitvector-type))

(define (bvsmin t) (- (expt 2 (- (bitvector-size t) 1))))
(define (bvsmin? b) (and (bv? b) (= (bv-value b) (bvsmin (bv-type b)))))
Expand Down Expand Up @@ -127,9 +126,7 @@
(define-match-expander @bv
(syntax-rules ()
[(_ val-pat type-pat) (bv val-pat type-pat)])
(syntax-id-rules (set!)
[(@bv v t) (make-bv v t)]
[@bv make-bv]))
(make-variable-like-transformer #'make-bv))

(define (@bv? v)
(match v
Expand Down

0 comments on commit 4c6a5bb

Please sign in to comment.