From 07aacdbd74005353ee3b1801b3125720f567ff17 Mon Sep 17 00:00:00 2001
From: Alex Knauth <alexander@knauth.org>
Date: Thu, 28 Jul 2016 20:06:44 -0400
Subject: [PATCH] use make-variable-like-transformer for bitvector and bv

---
 rosette/base/core/bitvector.rkt | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/rosette/base/core/bitvector.rkt b/rosette/base/core/bitvector.rkt
index 76e3b2a8..9c60275f 100644
--- a/rosette/base/core/bitvector.rkt
+++ b/rosette/base/core/bitvector.rkt
@@ -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?))
@@ -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)))))
@@ -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