From 17b78ef2298355c93e557017e0487423ea42c97a Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Sun, 11 Sep 2016 19:50:14 -0400 Subject: [PATCH] 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? --- turnstile/examples/rosette/lib/lift.rkt | 22 ++ turnstile/examples/rosette/rosette-notes.txt | 3 + turnstile/examples/rosette/rosette2.rkt | 134 ++++++++++- .../rosette/rosette-guide-sec7-tests.rkt | 225 ++++++++++++++++++ .../rosette/run-all-rosette-tests-script.rkt | 3 +- 5 files changed, 381 insertions(+), 6 deletions(-) create mode 100644 turnstile/examples/rosette/lib/lift.rkt create mode 100644 turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt diff --git a/turnstile/examples/rosette/lib/lift.rkt b/turnstile/examples/rosette/lib/lift.rkt new file mode 100644 index 0000000..75cce20 --- /dev/null +++ b/turnstile/examples/rosette/lib/lift.rkt @@ -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-]))]]) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index 1d66678..5f816f5 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -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 -------------------- diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 174c638..a667ae0 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -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 diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt new file mode 100644 index 0000000..af300f4 --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette-guide-sec7-tests.rkt @@ -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)]) +;; '(# integer?) +;; > (match x +;; [(term content type) (list content type)]) +;; '(# 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 +;; # +;; d +;; # +;; c +;; # +;; b +;; # +;; 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))) +;; # +;; d +;; # +;; c +;; # +;; b +;; # +;; 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)) + diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt index 6117282..822ee3a 100644 --- a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt +++ b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt @@ -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")