From 32c13d9ae24fba69122950513eb3e3b0326a5d41 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 25 Aug 2016 15:27:24 -0400 Subject: [PATCH] fix BVPred to not use old rosette version --- turnstile/examples/rosette/rosette-notes.txt | 7 +++++++ turnstile/examples/rosette/rosette2.rkt | 17 +++++++++++++--- .../examples/tests/rosette/rosette2-tests.rkt | 20 ++++++++++++++++++- 3 files changed, 40 insertions(+), 4 deletions(-) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index 19c9864..976e337 100644 --- 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 index 8cf72a2..5866b10 100644 --- 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+)])) @@ -171,6 +171,15 @@ (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) -------- [⊢ [_ ≫ (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] ...] @@ -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 index 88d8733..1ba10b0 100644 --- 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)