add symbolic reflection forms; add sec7 guide tests
- for/all and define-lift not working with assert-type - how to associate pred with newly lifted (type) of values?
This commit is contained in:
Stephen Chang
parent
583469c25f
commit
17b78ef229
22
turnstile/examples/rosette/lib/lift.rkt
Normal file
22
turnstile/examples/rosette/lib/lift.rkt
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(prefix-in t/ro: (only-in "../rosette2.rkt" U ~C→ C→))
|
||||
(prefix-in ro: rosette/lib/lift))
|
||||
|
||||
(define-typed-syntax define-lift
|
||||
[(_ x:id [(pred? ...) racket-fn:id]) ≫
|
||||
[⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]] ...
|
||||
[⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]]
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2)))))
|
||||
(ro:define-lift y [(pred?- ...) racket-fn-]))]]
|
||||
[(_ x:id [pred? racket-fn:id]) ≫
|
||||
[⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]]
|
||||
[⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]]
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2)))))
|
||||
(ro:define-lift y [pred?- racket-fn-]))]])
|
||||
|
|
@ -150,6 +150,9 @@ TODOs:
|
|||
- ADD 2016-09-08: transfer "typefor" and "solvable?" props to id in define
|
||||
- DONE 2016-09-08
|
||||
- is there a way to determine when evaluate produces concrete vals?
|
||||
- ADD 2016-09-10: implement typed define-synthax
|
||||
- ADD 2016-09-11: get assert-type to work with for/all and define-lift
|
||||
- ADD 2016-09-11: implement multiple values (for with-asserts)
|
||||
|
||||
2016-08-25 --------------------
|
||||
|
||||
|
|
|
|||
|
|
@ -11,8 +11,10 @@
|
|||
Constant
|
||||
C→ → (for-syntax ~C→ C→?)
|
||||
Ccase-> (for-syntax ~Ccase-> Ccase->?) ; TODO: symbolic case-> not supported yet
|
||||
CListof Listof Pair CVectorof MVectorof IVectorof CMVectorof CIVectorof
|
||||
CListof Listof CPair Pair
|
||||
CVectorof MVectorof IVectorof Vectorof CMVectorof CIVectorof
|
||||
CParamof ; TODO: symbolic Param not supported yet
|
||||
CListof Listof CPair Pair CVectorof MVectorof IVectorof Vectorof
|
||||
CBoxof MBoxof IBoxof
|
||||
CUnit Unit
|
||||
CNegInt NegInt
|
||||
|
|
@ -95,6 +97,7 @@
|
|||
(define-type-constructor CList #:arity >= 0)
|
||||
(define-type-constructor CPair #:arity = 2)
|
||||
|
||||
;; TODO: update orig to use reduced type
|
||||
(define-syntax (CU stx)
|
||||
(syntax-parse stx
|
||||
[(_ . tys)
|
||||
|
|
@ -197,6 +200,7 @@
|
|||
(define-named-type-alias (CParamof X) (Ccase-> (C→ X)
|
||||
(C→ X CUnit)))
|
||||
(define-named-type-alias (Listof X) (U (CListof X)))
|
||||
(define-named-type-alias (Vectorof X) (U (CVectorof X)))
|
||||
(define-named-type-alias (MVectorof X) (U (CMVectorof X)))
|
||||
(define-named-type-alias (IVectorof X) (U (CIVectorof X)))
|
||||
(define-named-type-alias (MBoxof X) (U (CMBoxof X)))
|
||||
|
|
@ -228,6 +232,8 @@
|
|||
(define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?)
|
||||
(define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?)
|
||||
|
||||
(define-named-type-alias CPred (C→ Any Bool))
|
||||
|
||||
;; ---------------------------------
|
||||
;; define-symbolic
|
||||
|
||||
|
|
@ -297,6 +303,9 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:assert e- m-) ⇒ : CUnit]]])
|
||||
|
||||
;; TODO: assert-type wont work with unlifted types
|
||||
;; but sometimes it should, eg in with for/all lifted functions
|
||||
;; - but this means we need to lift a pred (eg string?) and associate it with the newly lifted type
|
||||
(define-typed-syntax assert-type #:datum-literals (:)
|
||||
[(_ e : ty:type) ≫
|
||||
[⊢ [e ≫ e- ⇒ : _]]
|
||||
|
|
@ -376,13 +385,18 @@
|
|||
;; ---------------------------------
|
||||
;; quote
|
||||
|
||||
;; TODO: don't duplicate #%datum code here
|
||||
(define-typed-syntax quote
|
||||
[(_ x:id) ≫
|
||||
--------
|
||||
[⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]]
|
||||
[(_ (x:integer ...)) ≫
|
||||
#:with ty_out (let ([xs (syntax->datum #'(x ...))])
|
||||
(cond [(andmap zero? xs) #'CZero]
|
||||
[(andmap positive? xs) #'CPosInt]
|
||||
[else #'CNegInt]))
|
||||
--------
|
||||
[⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CInt)]]]
|
||||
[⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof ty_out)]]]
|
||||
[(_ (x:id ...)) ≫
|
||||
--------
|
||||
[⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CSymbol)]]]
|
||||
|
|
@ -571,6 +585,8 @@
|
|||
#'(CMVectorof (CU τ ...))
|
||||
#'(CMVectorof (U τ ...)))]]])
|
||||
|
||||
(define-rosette-primop vector? : CPred)
|
||||
|
||||
;; immutable constructor
|
||||
(define-typed-syntax vector-immutable
|
||||
[(_ e ...) ≫
|
||||
|
|
@ -625,6 +641,12 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:hash-keys e-) ⇒ : (CListof τ)]]])
|
||||
|
||||
(define-typed-syntax hash-values
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : (~CHashTable _ τ)]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:hash-values e-) ⇒ : (CListof τ)]]])
|
||||
|
||||
;; ---------------------------------
|
||||
;; lists
|
||||
|
||||
|
|
@ -632,6 +654,7 @@
|
|||
(C→ (Listof Any) Bool)))
|
||||
(define-rosette-primop empty? : (Ccase-> (C→ (CListof Any) CBool)
|
||||
(C→ (Listof Any) Bool)))
|
||||
(define-rosette-primop list? : CPred)
|
||||
|
||||
(define-typed-syntax list
|
||||
[(_ e ...) ≫
|
||||
|
|
@ -679,7 +702,7 @@
|
|||
(define-typed-syntax car
|
||||
[_:id ≫ ;; TODO: use polymorphism
|
||||
--------
|
||||
[⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pairof Any Any) Any)
|
||||
[⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any)
|
||||
(C→ (Listof Any) Any))]]]
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : (~CListof τ)]]
|
||||
|
|
@ -874,6 +897,50 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:reverse e-) ⇒ : (U (CList . τs/rev) ...)]]])
|
||||
|
||||
(define-typed-syntax build-list
|
||||
[_:id ≫ ;; TODO: use polymorphism
|
||||
--------
|
||||
[⊢ [_ ≫ ro:build-list ⇒ : (C→ CNat (C→ CNat Any) (CListof Any))]]]
|
||||
[(_ n f) ≫
|
||||
[⊢ [n ≫ n- ⇐ : CNat]]
|
||||
[⊢ [f ≫ f- ⇒ : (~C→ ty1 ty2)]]
|
||||
#:fail-unless (typecheck? #'ty1 ((current-type-eval) #'CNat))
|
||||
"expected function that consumes concrete Nat"
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof ty2)]]])
|
||||
(define-typed-syntax map
|
||||
#;[_:id ≫ ;; TODO: use polymorphism
|
||||
--------
|
||||
[⊢ [_ ≫ ro:map ⇒ : (C→ (C→ Any Any) (CListof Any) (CListof Any))]]]
|
||||
[(_ f lst) ≫
|
||||
[⊢ [f ≫ f- ⇒ : (~C→ ~! ty1 ty2)]]
|
||||
[⊢ [lst ≫ lst- ⇐ : (CListof ty1)]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]
|
||||
[(_ f lst) ≫
|
||||
[⊢ [lst ≫ lst- ⇒ : (~CListof ty1)]]
|
||||
[⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match
|
||||
#:with (~C→ _ ty2)
|
||||
(for/first ([ty-fn (stx->list #'(ty-fns ...))]
|
||||
#:when (syntax-parse ty-fn
|
||||
[(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t]
|
||||
[_ #f]))
|
||||
(displayln (syntax->datum ty-fn))
|
||||
ty-fn)
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]
|
||||
[(_ f lst) ≫
|
||||
[⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]]
|
||||
[⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match
|
||||
#:with (~C→ _ ty2)
|
||||
(for/first ([ty-fn (stx->list #'(ty-fns ...))]
|
||||
#:when (syntax-parse ty-fn
|
||||
[(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t]
|
||||
[_ #f]))
|
||||
ty-fn)
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]])
|
||||
|
||||
(define-typed-syntax sort
|
||||
[_:id ≫ ;; TODO: use polymorphism
|
||||
--------
|
||||
|
|
@ -909,10 +976,13 @@
|
|||
(C→ CString Any CUnit)
|
||||
(C→ CString Any Any CUnit))]
|
||||
[displayln : (C→ Any CUnit)]
|
||||
[pretty-print : (C→ Any CUnit)]
|
||||
[error : (Ccase-> (C→ (CU CString CSymbol) Nothing)
|
||||
(C→ CSymbol CString Nothing))]
|
||||
[void : (C→ CUnit)]
|
||||
|
||||
[string-length : (C→ CString CNat)]
|
||||
|
||||
[equal? : (C→ Any Any Bool)]
|
||||
[eq? : (C→ Any Any Bool)]
|
||||
[distinct? : (Ccase-> (C→ Bool)
|
||||
|
|
@ -1098,6 +1168,7 @@
|
|||
(C→ Int Int Int))]
|
||||
|
||||
;; rosette-specific
|
||||
[pc : (C→ Bool)]
|
||||
[asserts : (C→ CAsserts)]
|
||||
[clear-asserts! : (C→ CUnit)]))
|
||||
|
||||
|
|
@ -1117,6 +1188,7 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:boolean? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]])
|
||||
|
||||
(define-rosette-primop string? : (C→ Any Bool))
|
||||
;(define-rosette-primop integer? : (C→ Any Bool))
|
||||
(define-typed-syntax integer?
|
||||
[_:id ≫
|
||||
|
|
@ -1144,6 +1216,12 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:real? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]])
|
||||
|
||||
(define-typed-syntax time
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : ty]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:time e-) ⇒ : ty]]])
|
||||
|
||||
;; ---------------------------------
|
||||
;; mutable boxes
|
||||
|
||||
|
|
@ -1169,6 +1247,14 @@
|
|||
--------
|
||||
[⊢ [_ ≫ (ro:unbox e-) ⇒ : (U τ ...)]]])
|
||||
|
||||
;; TODO: implement multiple values
|
||||
;; result type should be (Valuesof ty CAsserts)
|
||||
(define-typed-syntax with-asserts
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : ty]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:with-asserts e-) ⇒ : ty]]])
|
||||
|
||||
(define-rosette-primop term-cache
|
||||
: (Ccase-> (C→ (CHashTable Any Any))
|
||||
(C→ (CHashTable Any Any) CUnit)))
|
||||
|
|
@ -1195,7 +1281,6 @@
|
|||
[⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]])
|
||||
|
||||
(define-named-type-alias BV (add-predm (U CBV) bv?))
|
||||
(define-named-type-alias CPred (C→ Any Bool))
|
||||
(define-symbolic-named-type-alias BVPred (C→ Any Bool) #:pred lifted-bitvector?)
|
||||
(define-named-type-alias BVMultiArgOp (Ccase-> (C→ BV BV BV)
|
||||
(C→ BV BV BV BV)))
|
||||
|
|
@ -1544,11 +1629,50 @@
|
|||
;(define-rosette-primop z3 : (C→ CSolver))
|
||||
|
||||
;; ---------------------------------
|
||||
;; Symbolic reflection
|
||||
;; Reflecting on symbolic values
|
||||
|
||||
(define-rosette-primop term? : CPred)
|
||||
(define-rosette-primop expression? : CPred)
|
||||
(define-rosette-primop constant? : CPred)
|
||||
(define-rosette-primop type? : CPred)
|
||||
(define-rosette-primop solvable? : CPred)
|
||||
(define-rosette-primop union? : CPred)
|
||||
|
||||
(define-typed-syntax union-contents
|
||||
[(_ u) ≫
|
||||
;; TODO: can U sometimes be converted to CU?
|
||||
[⊢ [u ≫ u- ⇒ : (~and τ (~U* _ ...))]] ; input must be symbolic, and not constant
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:union-contents u-) ⇒ : (CListof (CPair Bool τ))]]])
|
||||
|
||||
;; TODO: add match and match expanders
|
||||
|
||||
;; TODO: should a type-of expression have a solvable stx prop?
|
||||
(define-rosette-primop type-of : (Ccase-> (C→ Any CPred)
|
||||
(C→ Any Any CPred)))
|
||||
(define-rosette-primop any/c : (C→ Any CTrue))
|
||||
|
||||
(define-typed-syntax for/all
|
||||
;; symbolic e
|
||||
[(_ ([x:id e]) e_body) ≫
|
||||
[⊢ [e ≫ e- ⇒ : (~U* τ_x)]]
|
||||
[() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : (U τ_body)]]]
|
||||
[(_ ([x:id e]) e_body) ≫
|
||||
[⊢ [e ≫ e- ⇒ : τ_x]]
|
||||
[() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : (U τ_body)]]])
|
||||
|
||||
(define-typed-syntax for*/all
|
||||
[(_ () e_body) ≫
|
||||
--------
|
||||
[_ ≻ e_body]]
|
||||
[(_ ([x e] [x_rst e_rst] ...) e_body) ≫
|
||||
--------
|
||||
[_ ≻ (for/all ([x e]) (for*/all ([x_rst e_rst] ...) e_body))]])
|
||||
|
||||
|
||||
;; ---------------------------------
|
||||
;; Subtyping
|
||||
|
|
|
|||
225
turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt
Normal file
225
turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt
Normal file
|
|
@ -0,0 +1,225 @@
|
|||
#lang s-exp "../../rosette/rosette2.rkt"
|
||||
(require "../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 7 Reflecting on Symbolic Values
|
||||
|
||||
;; 7.1.1 Symbolic Terms
|
||||
(define-symbolic x integer?) ; constant
|
||||
(define e (+ x 1)) ; expression
|
||||
(check-type (list (term? x) (term? e)) : (CListof Bool) -> (list #t #t))
|
||||
(check-type (list (constant? x) (constant? e)) : (CListof Bool) -> (list #t #f))
|
||||
(check-type (list (expression? x) (expression? e)) : (CListof Bool) -> (list #f #t))
|
||||
(check-type (term? 1) : Bool -> #f)
|
||||
|
||||
;; TODO: match and match expanders
|
||||
;; > (define-symbolic x integer?) ; constant
|
||||
;; > (define e (+ x 1)) ; expression
|
||||
;; > (match x
|
||||
;; [(constant identifier type) (list identifier type)])
|
||||
;; '(#<syntax:8:0 x> integer?)
|
||||
;; > (match x
|
||||
;; [(term content type) (list content type)])
|
||||
;; '(#<syntax:8:0 x> integer?)
|
||||
;; > (match e
|
||||
;; [(expression op child ...) (cons op child)])
|
||||
;; '(+ 1 x)
|
||||
;; > (match e
|
||||
;; [(term content type) (list content type)])
|
||||
;; '((+ 1 x) integer?)
|
||||
|
||||
;(define-symbolic x integer?)
|
||||
(check-type (type-of x) : (C→ Any Bool) -> integer?)
|
||||
(check-type (type-of (+ x 1)) : (C→ Any Bool) -> integer?)
|
||||
(check-type (type-of x 3.14) : (C→ Any Bool) -> real?)
|
||||
(check-type (type-of #t) : (C→ Any Bool) -> boolean?)
|
||||
(check-type (type-of #t 1) : (C→ Any Bool) -> any/c)
|
||||
|
||||
(check-type (type? integer?) : Bool -> #t)
|
||||
(check-type (type? boolean?) : Bool -> #t)
|
||||
(check-type (type? list?) : Bool -> #t)
|
||||
(struct circle ([radius : Nat]))
|
||||
(check-type (type? circle?) : Bool -> #t)
|
||||
(check-type (type? any/c) : Bool -> #t)
|
||||
(check-type (type? 1) : Bool -> #f)
|
||||
|
||||
(check-type (solvable? boolean?) : Bool -> #t)
|
||||
(check-type (solvable? integer?) : Bool -> #t)
|
||||
(check-type (solvable? real?) : Bool -> #t)
|
||||
(check-type (solvable? (~> (bitvector 3) (bitvector 4))) : Bool -> #t)
|
||||
(check-type (solvable? list?) : Bool -> #f)
|
||||
;(struct circle (radius))
|
||||
(check-type (solvable? circle?) : Bool -> #f)
|
||||
(check-type (solvable? any/c) : Bool -> #f)
|
||||
|
||||
;; 7.1.2 Symbolic Unions
|
||||
(define-symbolic b boolean?)
|
||||
(define v (vector 1))
|
||||
(check-type v : (CVectorof CPosInt))
|
||||
(define w (vector 2 3))
|
||||
(check-type v : (CVectorof CPosInt))
|
||||
(define s (if b v w))
|
||||
(check-type s : (Vectorof CPosInt)) ;{[b #(1)] [(! b) #(2 3)]}
|
||||
(check-not-type s : (CVectorof CPosInt)) ; check union doesnt have concrete type
|
||||
(check-type (type-of s) : (C→ Any Bool) -> vector?)
|
||||
(check-type (eq? s v) : Bool -> b)
|
||||
(check-type (eq? s w) : Bool -> (! b))
|
||||
|
||||
; (define-symbolic b boolean?)
|
||||
(define-symbolic c boolean?)
|
||||
(define v2 (if c "c" 0))
|
||||
(check-type v2 : (U String Int))
|
||||
(check-type v2 : (U CString CInt))
|
||||
(check-not-type v2 : (CU CString CInt)) ; check not concrete
|
||||
(check-type v2 : (U CString CInt))
|
||||
(check-type v2 : (U CString CZero))
|
||||
(define u (if b (vector v2) 4))
|
||||
(check-type u : (U (CVectorof (U CString CZero)) Int)) ;{[b #({[c "c"] [(! c) 0]})] [(! b) 4]}
|
||||
(check-type (type-of u) : (C→ Any Bool) -> any/c)
|
||||
|
||||
(check-type '(1 2) : (CListof CPosInt))
|
||||
;> (define-symbolic b boolean?)
|
||||
(define u2 (if b '(1 2) 3))
|
||||
(check-type u2 : (U (CListof CPosInt) CPosInt))
|
||||
(check-type (union? u2) : Bool -> #t)
|
||||
(check-type (union? b) : Bool -> #f)
|
||||
(define v3 (if b '(1 2) 3))
|
||||
(check-type (union-contents v3)
|
||||
: (CListof (CPair Bool (U (CListof CPosInt) CPosInt)))
|
||||
-> (list (cons b '(1 2)) (cons (! b) 3)))
|
||||
|
||||
;; 7.1.3 Symbolic Lifting
|
||||
(require (only-in "../../rosette/rosette2.rkt" [string-length racket/string-length]))
|
||||
|
||||
(define (string-length [value : String] -> Nat)
|
||||
(for/all ([str value])
|
||||
(racket/string-length str)))
|
||||
|
||||
|
||||
(check-type (string-length "abababa") : Nat -> 7)
|
||||
(check-type (racket/string-length "abababa") : CNat -> 7)
|
||||
(check-not-type (string-length "abababa") : CNat)
|
||||
|
||||
(typecheck-fail (string-length 3) #:with-msg "expected String")
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (string-length (if b "a" "abababa")) : Nat -> (if b 1 7)) ;(ite b 1 7)
|
||||
(check-not-type (string-length (if b "a" "abababa")) : CNat)
|
||||
|
||||
;; Typed Rosette rejects this program
|
||||
(typecheck-fail (string-length (if b "a" 3)) #:with-msg "expected String")
|
||||
;; need assert-type
|
||||
;; TODO: this doesnt work yet because String has no pred
|
||||
;; - and we cant use string? bc it's unlifted --- will always be assert fail
|
||||
;(check-type (string-length (assert-type (if b "a" 3) : String)) : Nat -> 1)
|
||||
;;(check-type (asserts) : CAsserts -> (list b))
|
||||
(typecheck-fail (string-length (if b 3 #f)) #:with-msg "expected String")
|
||||
;; not runtime exn: for/all: all paths infeasible
|
||||
|
||||
;; Making symbolic evaluation more efficient.
|
||||
;; (require (only-in racket build-list))
|
||||
|
||||
(define limit 1000)
|
||||
|
||||
(define (slow [xs : (Listof CInt)] -> (U CFalse Int))
|
||||
(and (= (length xs) limit) (car (map add1 xs))))
|
||||
|
||||
(define (fast [xs : (Listof CInt)] -> (U CFalse Int))
|
||||
(for/all ([xs xs]) (slow xs)))
|
||||
|
||||
(define ys (build-list limit (lambda ([x : CNat]) x)))
|
||||
(check-type ys : (CListof CInt))
|
||||
|
||||
(define-symbolic a boolean?)
|
||||
|
||||
(define xs (if a ys (cdr ys)))
|
||||
(check-type xs : (Listof CInt))
|
||||
(check-not-type xs : (CListof CInt))
|
||||
|
||||
(check-type (time (slow xs)) : (U CFalse Int) -> (if a 1 #f))
|
||||
;; cpu time: 1 real time: 2 gc time: 0
|
||||
;; {[a 1] [(! a) #f]}
|
||||
(check-type (time (fast xs)) : (U CFalse Int) -> (if a 1 #f))
|
||||
;; cpu time: 0 real time: 0 gc time: 0
|
||||
;; {[a 1] [(! a) #f]}
|
||||
(printf "First printed time should be slightly slower than second time\n")
|
||||
|
||||
;; define-lift
|
||||
(require "../../rosette/lib/lift.rkt")
|
||||
(define-lift lifted-string-length [(string?) racket/string-length])
|
||||
|
||||
(check-type (lifted-string-length "abababa") : Nat -> 7)
|
||||
(check-not-type (lifted-string-length "abababa") : CNat)
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (lifted-string-length (if b "a" "abababa"))
|
||||
: Nat -> (if b 1 7)) ;(ite b 1 7)
|
||||
;; typed rosette rejects this progrm
|
||||
(typecheck-fail (lifted-string-length (if b "a" 3)) #:with-msg "expected.*String")
|
||||
;; TODO: need type-assert
|
||||
;; (check-type (lifted-string-length (assert-type (if b "a" 3) : String)) : Nat -> 1)
|
||||
;; (check-type (asserts) : CAsserts -> (list b))
|
||||
|
||||
;; 7.2 Reflecting on Symbolic State
|
||||
;> (define-symbolic a b boolean?)
|
||||
(check-type (if a
|
||||
(if b
|
||||
#f
|
||||
(pc))
|
||||
#f) : Bool -> (&& a (! b)))
|
||||
|
||||
(check-type (assert a) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list a))
|
||||
(check-type (assert b) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list b a))
|
||||
(check-type (clear-asserts!) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list))
|
||||
|
||||
(printf "expected output: 4 and (list b a)\n")
|
||||
(with-asserts
|
||||
(begin (assert a)
|
||||
(assert b)
|
||||
4))
|
||||
(check-type (asserts) : CAsserts -> (list))
|
||||
|
||||
;; term-cache
|
||||
(clear-terms!)
|
||||
(check-type (term-cache) : (CHashTable Any Any) -> (term-cache))
|
||||
(check-type (hash-keys (term-cache)) : (CListof Any) -> (list))
|
||||
|
||||
(define-symbolic a1 b1 c1 d1 integer?)
|
||||
|
||||
(check-type (hash-values (term-cache)) : (CListof Any) -> (list a1 b1 c1 d1))
|
||||
;; (hash
|
||||
;; #<syntax:23:0 d>
|
||||
;; d
|
||||
;; #<syntax:23:0 c>
|
||||
;; c
|
||||
;; #<syntax:23:0 b>
|
||||
;; b
|
||||
;; #<syntax:23:0 a>
|
||||
;; a)
|
||||
(check-type (* d1 (- (+ a1 b1) c1)) : Int -> (* d1 (- (+ a1 b1) c1)))
|
||||
;(check-type (hash-keys (term-cache)) : CUnit -> (list (list * d (+ (+ a b) (- c))) d c b a))
|
||||
(printf "expected output: hash with a-d and large arith op with all subexprs\n")
|
||||
(pretty-print (term-cache))
|
||||
;; (hash
|
||||
;; (list * d (+ (+ a b) (- c)))
|
||||
;; (* d (+ (+ a b) (- c)))
|
||||
;; #<syntax:23:0 d>
|
||||
;; d
|
||||
;; #<syntax:23:0 c>
|
||||
;; c
|
||||
;; #<syntax:23:0 b>
|
||||
;; b
|
||||
;; #<syntax:23:0 a>
|
||||
;; a
|
||||
;; (list - c)
|
||||
;; (- c)
|
||||
;; (list + a b)
|
||||
;; (+ a b)
|
||||
;; (list + (+ a b) (- c))
|
||||
;; (+ (+ a b) (- c)))
|
||||
(check-type (clear-terms! (list c1 d1)) : CUnit -> (void))
|
||||
(printf "expected output: hash with c and d missing\n")
|
||||
(pretty-print (term-cache))
|
||||
(check-type (clear-terms!) : CUnit -> (void))
|
||||
(check-type (hash-keys (term-cache)) : (CListof Any) -> (list))
|
||||
|
||||
|
|
@ -13,7 +13,8 @@
|
|||
"rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9")
|
||||
|
||||
(do-tests "rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures"
|
||||
"rosette-guide-sec6-tests.rkt" "Rosette Guide, Section 6 Libraries")
|
||||
"rosette-guide-sec6-tests.rkt" "Rosette Guide, Section 6 Libraries"
|
||||
"rosette-guide-sec7-tests.rkt" "Rosette Guide, Section 7 Reflecting on Symbolic Values")
|
||||
|
||||
(do-tests "bv-tests.rkt" "BV SDSL - General"
|
||||
"bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user