commit 32c13d9ae24fba69122950513eb3e3b0326a5d41
parent 9e2b2ddd3c3fd302533c8e6627590b2f12aba63d
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 25 Aug 2016 15:27:24 -0400
fix BVPred to not use old rosette version
Diffstat:
3 files changed, 40 insertions(+), 4 deletions(-)
diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
@@ -1,5 +1,12 @@
2016-08-25 --------------------
+TODOs:
+- add pred properties to types
+ and use it to validate given pred in define-symbolic
+- implement assert-type, which adds to the assertion store
+
+2016-08-25 --------------------
+
** Problem:
The following subtyping relation holds but is potentially unintuitive for a
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -30,7 +30,7 @@
(only-in "../stlc+union+case.rkt"
PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)
(only-in "rosette.rkt"
- BV BVPred)))
+ BV)))
(only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
(only-in "../ext-stlc.rkt" define-primop))
@@ -75,7 +75,7 @@
(syntax-parse stx
[(_ . tys)
#:with tys+ (stx-map (current-type-eval) #'tys)
- #:fail-unless (stx-andmap →? #'tys+)
+ #:fail-unless (stx-andmap C→? #'tys+)
"CU require concrete arguments"
#'(Ccase->* . tys+)]))
@@ -172,6 +172,15 @@
--------
[⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
[(_ e_fn e_arg ...) ≫
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]]
+ [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+ #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
+ [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
+ ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
+ ...
+ --------
+ [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : (CU τ_out ...)]]]
+ [(_ e_fn e_arg ...) ≫
[⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]]
[⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
#:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
@@ -237,12 +246,14 @@
(define-rosette-primop boolean? : (C→ Bool Bool))
(define-rosette-primop integer? : (C→ Num Bool))
(define-rosette-primop real? : (C→ Num Bool))
+(define-rosette-primop positive? : (Ccase-> (C→ CNum CBool)
+ (C→ Num Bool)))
;; ---------------------------------
;; BV Types and Operations
(define-named-type-alias BV (U CBV))
-(define-named-type-alias BVPred (U CBVPred))
+(define-symbolic-named-type-alias BVPred (C→ BV Bool))
(define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV)
(C→ Int CBVPred BV)
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -131,7 +131,7 @@
(check-type bitvector : (C→ CPosInt CBVPred))
(check-type (bitvector 3) : CBVPred)
(typecheck-fail ((bitvector 4) 1))
-(check-type ((bitvector 4) (bv 10 (bitvector 4))) : CBool)
+(check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool)
;; ;; same as above, but with bvpred
;; (check-type bvpred : (→ PosInt BVPred))
@@ -246,4 +246,22 @@
;; it's either (→ CInt CInt) or (→ CInt CBool), but not both, so
;; add1 can have this type even though it never returns a boolean
(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (U Int Bool) -> 11)
+(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10))
+ (if #t add1 positive?))
+ : (U CInt Bool) -> 11)
+(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10))
+ (if #t add1 positive?))
+ : (U Int Bool) -> 11)
+;; concrete union of functions
+(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (CU CInt CBool) -> 11)
+(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10))
+ (if #t add1 positive?))
+ : (CU CInt CBool) -> 11)
+;; check BVPred as type annotation
+;; CBV input annotation on arg is too restrictive to work as BVPred
+(typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : CBV]) #t))
+ #:with-msg "expected BVPred.*given.*CBV")
+(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t)) : BVPred)
+;; this should pass, but will not if BVPred is a case->
+(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) ((bitvector 2) bv))) : BVPred)
