bv.rkt (3522B)
1 #lang turnstile 2 (extends "rosette2.rkt" ; extends typed rosette 3 #:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) 4 (require (prefix-in ro: rosette)) ; untyped 5 (require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*) 6 (prefix-in bv: (only-in sdsl/bv/lang/bvops BV))) 7 (require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form)) 8 9 (provide Prog Lib 10 (typed-out [bv : (Ccase-> (C→ CInt CBV) 11 (C→ CInt CBVPred CBV) 12 (C→ CInt CPosInt CBV))] 13 [bv* : (Ccase-> (C→ BV) 14 (C→ CBVPred BV))] 15 [bvredor : (C→ BV BV)] 16 [bvredand : (C→ BV BV)]) 17 current-bvpred define-fragment bvlib thunk) 18 19 ;; this must be a macro in order to support Racket's overloaded set/get 20 ;; parameter patterns 21 (define-typed-syntax current-bvpred 22 [c-bvpred:id ≫ 23 -------- 24 [⊢ [_ ≫ bv:BV ⇒ : (CParamof CBVPred)]]] 25 [(_) ≫ 26 -------- 27 [⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]] 28 [(_ e) ≫ 29 [⊢ [e ≫ e- ⇐ : CBVPred]] 30 -------- 31 [⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]]) 32 33 (define-syntax-rule (bv:bool->bv b) 34 (ro:if b 35 (bv (rosette2:#%datum . 1)) 36 (bv (rosette2:#%datum . 0)))) 37 38 (define-simple-macro (define-comparators id ...) 39 #:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...)) 40 #:with (id/tc ...) (generate-temporaries #'(id ...)) 41 (begin- 42 (define- (id x y) (bv:bool->bv (ro:#%app op x y))) ... 43 (provide (rename-out [id/tc id] ...)) 44 (define-primop id/tc id (C→ BV BV BV)) ...)) 45 46 (define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge) 47 48 (define-base-types Prog Lib) 49 50 (define-typed-syntax define-fragment 51 [(_ (id param ...) #:implements spec #:library lib-expr) ≫ 52 -------- 53 [_ ≻ (define-fragment (id param ...) 54 #:implements spec #:library lib-expr #:minbv (rosette2:#%datum . 4))]] 55 [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫ 56 [⊢ [spec ≫ spec- ⇒ : ty_spec]] 57 #:fail-unless (C→? #'ty_spec) "spec must be a function" 58 [⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]] 59 [⊢ [minbv ≫ minbv- ⇐ : Int]] 60 #:with id-stx (format-id #'id "~a-stx" #'id #:source #'id) 61 -------- 62 [_ ≻ (begin- 63 (define-values- (id-internal id-stx-internal) 64 (bv:synthesize-fragment (id param ...) 65 #:implements spec- 66 #:library lib-expr- 67 #:minbv minbv-)) 68 (define-syntax id 69 (make-rename-transformer (⊢ id-internal : ty_spec))) 70 (define-syntax id-stx 71 (make-rename-transformer (⊢ id-stx-internal : CStx))) 72 )]]) 73 74 (define-typed-syntax bvlib 75 [(_ [(~and ids (id ...)) n] ...) ≫ 76 #:fail-unless (stx-andmap brace? #'(ids ...)) 77 "given ops must be enclosed with braces" 78 [⊢ [n ≫ n- ⇐ : Int] ...] 79 [⊢ [id ≫ id- ⇒ : ty_id] ... ...] 80 #:fail-unless (stx-andmap C→? #'(ty_id ... ...)) 81 "given op must be a function" 82 #:with ((~C→ ty ...) ...) #'(ty_id ... ...) 83 #:fail-unless (stx-andmap τ⊑BV? #'(ty ... ...)) 84 "given op must have BV inputs and output" 85 -------- 86 [⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]]) 87 88 (begin-for-syntax 89 (define BV* ((current-type-eval) #'BV)) 90 (define (τ⊑BV? τ) 91 (typecheck? τ BV*))) 92 93 (define-syntax-rule (thunk e) (rosette2:λ () e))