suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

start typed bv

Browse Source
This commit is contained in:
Stephen Chang 2016-07-11 19:29:35 -04:00
parent fc243732c3
commit 38ba3d273d
2 changed files with 74 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
turnstile/examples/rosette/bv.rkt Normal file
View File

@ -0,0 +1,46 @@
#lang turnstile
;(require (only-in rosette bv bitvector))
(require syntax/parse/define)
(extends "../ext-stlc.rkt")
(require (only-in "../stlc+reco+var.rkt" define-type-alias))
(define-simple-macro (define-rosette-primop op:id : ty)
(begin
(require (only-in rosette [op op]))
(define-primop op : ty)))
(define-simple-macro (define-rosette-primop* op1:id op2:id : ty)
(begin
(require (only-in rosette [op1 op2]))
(define-primop op2 : ty)))
(provide BVPred)
(define-base-type BV) ; represents actual bitvectors
; a predicate recognizing bv's of a certain size
(define-type-alias BVPred (→ BV Bool))
(define-rosette-primop bv : (→ Int BVPred BV))
(define-rosette-primop bv? : (→ BV Bool))
(define-rosette-primop bitvector : (→ Int BVPred))
(define-rosette-primop bitvector? : (→ BVPred Bool))
(define-rosette-primop* bitvector bvpred : (→ Int BVPred))
(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
(define-rosette-primop bveq : (→ BV BV Bool))
(define-rosette-primop bvslt : (→ BV BV Bool))
(define-rosette-primop bvult : (→ BV BV Bool))
(define-rosette-primop bvsle : (→ BV BV Bool))
(define-rosette-primop bvule : (→ BV BV Bool))
(define-rosette-primop bvsgt : (→ BV BV Bool))
(define-rosette-primop bvugt : (→ BV BV Bool))
(define-rosette-primop bvsge : (→ BV BV Bool))
(define-rosette-primop bvuge : (→ BV BV Bool))
(define-rosette-primop bvnot : (→ BV BV))
;; (require (postfix-in - (rosette))
;; (define-typed-syntax bvand
;; [(_ e ...+)
;; [⊢ [[e ≫ e-] ⇐ : BV] ...]
;; --------
;; [⊢ [[_ ≫ (bvand- e- ...)] ⇒ : Bool]]])

28
turnstile/examples/tests/rosette/bv-tests.rkt Normal file
View File

@ -0,0 +1,28 @@
#lang s-exp "../../rosette/bv.rkt"
(require "../rackunit-typechecking.rkt")
(check-type bv : (→ Int BVPred BV))
(typecheck-fail (bv "1" 2) #:with-msg "expected Int, given String")
(check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
(check-type bitvector : (→ Int BVPred))
(check-type (bitvector 3) : BVPred)
(typecheck-fail ((bitvector 4) 1))
(check-type ((bitvector 4) (bv 10 (bvpred 4))) : Bool)
;; same as above, but with bvpred
(check-type bvpred : (→ Int BVPred))
(check-type (bvpred 3) : BVPred)
(typecheck-fail ((bvpred 4) 1))
(check-type ((bvpred 4) (bv 10 (bvpred 4))) : Bool)
(typecheck-fail (bitvector? "2"))
(check-type (bitvector? (bitvector 10)) : Bool -> #t)
(typecheck-fail (bvpred? "2"))
(check-type (bvpred? (bvpred 10)) : Bool -> #t)
(check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t)
(typecheck-fail (bveq (bv 1 (bvpred 3)) 1))
(check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> exn