commit eb3ff404041693b2dda708589adc097662d53008
parent d7ab2d0f2957dfb12194df77f13ade19b413e0e1
Author: AlexKnauth <alexander@knauth.org>
Date: Fri, 26 Aug 2016 11:56:21 -0400
convert bv.rkt to extend rosette2
Diffstat:
5 files changed, 75 insertions(+), 58 deletions(-)
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -2,37 +2,37 @@
#lang racket/base
(require (except-in "../../../turnstile/turnstile.rkt"
#%module-begin
- zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal? list)
+ zero? void sub1 or and not add1 = - * + boolean? integer? real? positive? string? quote pregexp make-parameter equal? list)
(for-syntax (except-in "../../../turnstile/turnstile.rkt")))
-(extends "rosette.rkt" ; extends typed rosette
+(extends "rosette2.rkt" ; extends typed rosette
#: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)
+(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv)
(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)
+(provide thunk)
;; this must be a macro in order to support Racket's overloaded set/get
;; parameter patterns
(define-typed-syntax current-bvpred
[c-bvpred:id ≫
--------
- [⊢ [_ ≫ bv:BV ⇒ : (Param BVPred)]]]
+ [⊢ [_ ≫ bv:BV ⇒ : (CParam CBVPred)]]]
[(_) ≫
--------
- [⊢ [_ ≫ (bv:BV) ⇒ : BVPred]]]
+ [⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]]
[(_ e) ≫
- [⊢ [e ≫ e- ⇒ : BVPred]]
+ [⊢ [e ≫ e- ⇒ : CBVPred]]
--------
[⊢ [_ ≫ (bv:BV e-) ⇒ : Unit]]])
-(define-typed-syntax bv
- [(_ e_val) ≫
- --------
- [_ ≻ (rosette:bv e_val (current-bvpred))]]
- [(_ e_val e_size) ≫
- --------
- [_ ≻ (rosette:bv e_val e_size)]])
+(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)))
(define-typed-syntax bv*
[(_) ≫
@@ -43,18 +43,18 @@
--------
[⊢ [_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b)) ⇒ : BV]]])
-(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))
+(define-syntax-rule (bv:bool->bv b)
+ (ro:if b
+ (bv (rosette2:#%datum . 1))
+ (bv (rosette2:#%datum . 0))))
+(define-primop bvredor : (C→ BV BV))
+(define-primop bvredand : (C→ BV BV))
(define-simple-macro (define-comparators id ...)
#:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...))
(begin-
- (define- (id x y) (bool->bv (op x y))) ...
- (define-primop id : (→ BV BV BV)) ...))
+ (define- (id x y) (bv:bool->bv (ro:#%app op x y))) ...
+ (define-primop id : (C→ BV BV BV)) ...))
(define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
@@ -63,10 +63,10 @@
(define-typed-syntax define-fragment
[(_ (id param ...) #:implements spec #:library lib-expr) ≫
--------
- [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette:#%datum . 4))]]
+ [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv (rosette2:#%datum . 4))]]
[(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
[⊢ [spec ≫ spec- ⇒ : ty_spec]]
- #:fail-unless (→? #'ty_spec) "spec must be a function"
+ #:fail-unless (C→? #'ty_spec) "spec must be a function"
[⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]]
[⊢ [minbv ≫ minbv- ⇐ : Int]]
#:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)
@@ -78,7 +78,7 @@
#:library lib-expr-
#:minbv minbv-))
(define-syntax id (make-rename-transformer (⊢ id-internal : ty_spec)))
- (define-syntax id-stx (make-rename-transformer (⊢ id-stx-internal : Stx)))
+ (define-syntax id-stx (make-rename-transformer (⊢ id-stx-internal : CStx)))
)]])
(define-typed-syntax bvlib
@@ -87,12 +87,17 @@
"given ops must be enclosed with braces"
[⊢ [n ≫ n- ⇐ : Int] ...]
[⊢ [id ≫ id- ⇒ : ty_id] ... ...]
- #:fail-unless (stx-andmap →? #'(ty_id ... ...))
+ #:fail-unless (stx-andmap C→? #'(ty_id ... ...))
"given op must be a function"
- #:with ((~→ ty ...) ...) #'(ty_id ... ...)
- #:fail-unless (stx-andmap BV? #'(ty ... ...))
+ #:with ((~C→ ty ...) ...) #'(ty_id ... ...)
+ #:fail-unless (stx-andmap τ⊑BV? #'(ty ... ...))
"given op must have BV inputs and output"
--------
[⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]])
-(define-syntax-rule (thunk e) (rosette:λ () e))
+(begin-for-syntax
+ (define BV* ((current-type-eval) #'BV))
+ (define (τ⊑BV? τ)
+ (typecheck? τ BV*)))
+
+(define-syntax-rule (thunk e) (rosette2:λ () e))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -165,7 +165,7 @@
--------
[_ ≻ (begin-
(define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
- (stlc:define f- (stlc+union:λ ([x : ty] ...) e)))]])
+ (stlc:define f- (stlc+union+case:λ ([x : ty] ...) e)))]])
(define-base-type Stx)
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -4,11 +4,13 @@
(reuse #%datum #:from "../stlc+union.rkt")
(reuse define-type-alias #:from "../stlc+reco+var.rkt")
(reuse define-named-type-alias #:from "../stlc+union.rkt")
-(reuse void Unit List define list #:from "../stlc+cons.rkt")
+(reuse void Unit List list #:from "../stlc+cons.rkt")
+(reuse define #:from "rosette.rkt")
(provide CU U
- C→ →
+ C→ → (for-syntax ~C→ C→?)
Ccase-> ; TODO: symbolic case-> not supported yet
+ CParam ; TODO: symbolic Param not supported yet
CNegInt NegInt
CZero Zero
CPosInt PosInt
@@ -18,6 +20,7 @@
CNum Num
CBool Bool
CString String
+ CStx ; symblic Stx not supported
;; BV types
CBV BV
CBVPred BVPred
@@ -31,7 +34,7 @@
(only-in "../stlc+union+case.rkt"
PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)
(only-in "rosette.rkt"
- BV)))
+ BV Stx)))
(only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
(only-in "../ext-stlc.rkt" define-primop))
@@ -106,8 +109,8 @@
(define-named-type-alias Float (U CFloat))
(define-named-type-alias Bool (add-predm (U CBool) ro:boolean?))
(define-named-type-alias String (U CString))
-(define-named-type-alias (Param X) (Ccase-> (C→ X)
- (C→ X Unit)))
+(define-named-type-alias (CParam X) (Ccase-> (C→ X)
+ (C→ X stlc+cons:Unit)))
(define-syntax →
(syntax-parser
@@ -274,6 +277,13 @@
;; ---------------------------------
;; Types for built-in operations
+(define-typed-syntax equal?
+ [(equal? e1 e2) ≫
+ [⊢ [e1 ≫ e1- ⇒ : ty1]]
+ [⊢ [e2 ≫ e2- ⇐ : (U ty1)]]
+ --------
+ [⊢ [_ ≫ (ro:equal? e1- e2-) ⇒ : Bool]]])
+
(define-rosette-primop add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
(C→ NegInt (U NegInt Zero))
(C→ CZero CPosInt)
@@ -366,6 +376,8 @@
(define-rosette-primop bitvector->natural : (C→ BV Nat))
(define-rosette-primop integer->bitvector : (C→ Int BVPred BV))
+(define-rosette-primop bitvector-size : (C→ CBVPred CPosInt))
+
;; ---------------------------------
;; Subtyping
diff --git a/turnstile/examples/tests/rosette/bv-ref-tests.rkt b/turnstile/examples/tests/rosette/bv-ref-tests.rkt
@@ -10,24 +10,24 @@
;
; The first 20 benchmarks are also used in the SyGuS competition: http://www.sygus.org
-(current-bvpred (bvpred 32))
+(current-bvpred (bitvector 32))
-(check-type (thunk (bv 1)) : (→ BV))
+(check-type (thunk (bv 1)) : (C→ BV))
; Constants.
(define bv1 (thunk (bv 1)))
(define bv2 (thunk (bv 2)))
-(define bvsz (thunk (bv (sub1 (bvpred-size (current-bvpred))))))
+(define bvsz (thunk (bv (sub1 (bitvector-size (current-bvpred))))))
-(check-type bv1 : (→ BV))
+(check-type bv1 : (C→ BV))
(check-type (bv1) : BV -> (bv 1))
-(check-type ((bvpred 4) (bv1)) : Bool -> #f)
-(check-type ((bvpred 32) (bv1)) : Bool -> #t)
-(check-type bv2 : (→ BV))
-(check-type bvsz : (→ BV))
+(check-type ((bitvector 4) (bv1)) : Bool -> #f)
+(check-type ((bitvector 32) (bv1)) : Bool -> #t)
+(check-type bv2 : (C→ BV))
+(check-type bvsz : (C→ BV))
(check-type (bvsub (bv 1) (bv1)) : BV -> (bv 0))
-(check-type ((bvpred 32) (bvsub (bv 1) (bv1))) : Bool -> #t)
+(check-type ((bitvector 32) (bvsub (bv 1) (bv1))) : Bool -> #t)
; Mask off the rightmost 1-bit.
(define (p1 [x : BV] -> BV)
@@ -36,7 +36,7 @@
o2))
(check-type (p1 (bv 1)) : BV -> (bv 0))
-(check-type ((bvpred 32) (p1 (bv 1))) : Bool -> #t)
+(check-type ((bitvector 32) (p1 (bv 1))) : Bool -> #t)
; Test whether an unsigned integer is of the form 2^n-1.
(define (p2 [x : BV] -> BV)
diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt
@@ -1,26 +1,26 @@
#lang s-exp "../../rosette/bv.rkt"
(require "../rackunit-typechecking.rkt")
-(check-type current-bvpred : (Param BVPred))
-(check-type (current-bvpred) : BVPred -> (bvpred 4))
-(check-type (current-bvpred (bvpred 5)) : Unit -> (void))
-(check-type (current-bvpred) : BVPred -> (bvpred 5))
-(check-type (current-bvpred (bvpred 4)) : Unit -> (void))
+(check-type current-bvpred : (CParam CBVPred))
+(check-type (current-bvpred) : BVPred -> (bitvector 4))
+(check-type (current-bvpred (bitvector 5)) : Unit -> (void))
+(check-type (current-bvpred) : BVPred -> (bitvector 5))
+(check-type (current-bvpred (bitvector 4)) : Unit -> (void))
(check-type (bv 1) : BV)
-(check-type ((bvpred 4) (bv 1)) : Bool -> #t)
-(check-type ((bvpred 1) (bv 1)) : Bool -> #f)
-(check-type (bv 2 (bvpred 3)) : BV)
-(check-type ((bvpred 3) (bv 2 (bvpred 3))) : Bool -> #t)
+(check-type ((bitvector 4) (bv 1)) : Bool -> #t)
+(check-type ((bitvector 1) (bv 1)) : Bool -> #f)
+(check-type (bv 2 (bitvector 3)) : BV)
+(check-type ((bitvector 3) (bv 2 (bitvector 3))) : Bool -> #t)
(check-type (bv*) : BV)
-(check-type (bool->bv 1) : BV -> (bv 1))
-(check-type (bool->bv #f) : BV -> (bv 0))
+(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)
-(check-type (bool->bv i) : BV -> (bv 1))
-(check-type (bool->bv b) : BV -> (if b (bv 1) (bv 0)))
+(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)))
(check-type (bvredor (bv 1)) : BV)
(check-type (bvredand (bv 1)) : BV)
