add remaining sec44 guide tests; use term cache to improve testing

turnstile/examples/rosette/rosette-notes.txt

@@ -9,7 +9,8 @@
 
 res has type (Constant Int) but (constant? res) is false
 
-** Workaround: 
+** Workaround: special case in evaluate
+ - still unsound with polymorphism
 
 2016-09-08 --------------------
 
@@ -97,6 +98,8 @@ minimal example:
 Interesting parts of Typed Rosette
 - only need a single U symbolic constructor
 - assert-type, using cast-type and assertion store
+- solvable?, function?, typefor tags
+- Constant constructor?
 
 2016-08-25 --------------------
 
@@ -109,14 +112,16 @@ TODOs:
    - disadvantage: cannot compute pred in define-symbolic
      - Rosette users won't care?
      - TODO: add extra type rules to propagate 'typefor tag
+ - DONE (alternative) 2016-09-07
 - implement assert-type, which adds to the assertion store
  - DONE 2016-08-25
 - add polymorphism
  - regular polymorphism
+ - BV size polymorphism?
 - extend BV type with a size
  - requires BV-size-polymorpism?
 - add Any type?
- - STARTED 2016-08-26
+ - STARTED 2016-08-26 DONE?
 - support internal definition contexts
 - fix type of Vector and List to differentiate homogeneous/hetero
   - 2016-09-01: add CList for hetero lists
@@ -129,15 +134,19 @@ TODOs:
   - depends on macrotypes and rosette
 - create version of turnstile that does not provide #%module-begin
   - eg rename existing turnstile to turnstile/lang?
+  - DONE, see Alex's commit 2016-08-31
+   - fixed set! bug
 - remove my-this-syntax stx param
 - add symbolic True and False?
 - orig stx prop confuses distinction between symbolic and non-sym values
+  in err msgs
 - use variance information in type constructors?
   - instead of special-casing individual constructors
 - ok to say "Rosette type" in type err msgs?
-- 2016-09-08: fix Constant soundness wrt evaluate
-- 2016-09-08: transfer "typefor" and "solvable?" props to id in define
+- ADD 2016-09-08: fix Constant soundness wrt evaluate
+- 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?
 
 2016-08-25 --------------------
 

turnstile/examples/rosette/rosette2.rkt

@@ -883,6 +883,14 @@
    --------
    [⊢ [_ ≫ (ro:unbox e-) ⇒ : τ]]])
 
+(define-rosette-primop term-cache
+  : (Ccase-> (C→ (CHashTable Any Any))
+             (C→ (CHashTable Any Any) CUnit)))
+(define-rosette-primop clear-terms! 
+  : (Ccase-> (C→ CUnit)
+             (C→ CFalse CUnit)
+             (C→ (CListof Any) CUnit))) ; list of terms
+
 ;; ---------------------------------
 ;; BV Types and Operations
 
@@ -1004,6 +1012,22 @@
 
 (define-rosette-primop fv? : (C→ Any Bool))
 
+;; function? can produce type CFalse if input does not have type (C→ Any Bool)
+;; result is always CBool, since anything symbolic returns false
+;(define-rosette-primop function? : (C→ Any Bool))
+(define-typed-syntax function?
+  [_:id ≫
+   --------
+   [⊢ [_ ≫ ro:function? ⇒ : (C→ Any CBool)]]]
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇐ : (C→ Any Bool)]]
+   --------
+   [⊢ [_ ≫ (ro:function? e-) ⇒ : CBool]]]
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇒ : _]]
+   --------
+   [⊢ [_ ≫ (ro:function? e-) ⇒ : CFalse]]])
+
 ;; ---------------------------------
 ;; Logic operators
 (provide (rosette-typed-out [! : (C→ Bool Bool)]

turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt

@@ -22,29 +22,41 @@
 (define-symbolic x real?)
 ; typed Rosette rejects tis program
 (typecheck-fail (f x) #:with-msg "expected Int, given.*Num")
+;; must use assert-type to cast to Int
 (check-type (f (assert-type x : Int)) 
             : Bool -> (f (assert-type x : Int))) ;(app f (real->integer x)))
 (check-type (asserts) : CAsserts -> (list (integer? x)))
+(clear-asserts!)
+;(clear-terms!) ; must not clear terms
 
+;; typed Rosette rejects this program
+(typecheck-fail (solve (assert (not (equal? (f x) (f 1)))))
+                #:with-msg "expected Int, given.*Num")
+;; must use assert-type to cast x toInt
 (define sol (solve (assert (not (equal? (f (assert-type x : Int)) (f 1))))))
 (check-type sol : CSolution)
 (define g (evaluate f sol)) ; an interpretation of f
 (check-type g : (→ Int Bool)) ; -> (fv (((1) . #f) ((0) . #t)) #f integer?~>boolean?)
-;; should this be Num or Int?
-;(check-type (evaluate x sol) : Int -> 0)
-(check-type (evaluate x sol) : Num -> 0) ; nondeterministic result
-;; check soundness of Constant
-(check-not-type (evaluate x sol) : (Constant Num))
 ; f is a function value
 (check-type (fv? f) : Bool -> #t)
 ; and so is g
 (check-type (fv? g) : Bool -> #t)
+
+;; The tests below depend on a specific term-cache (should be commented out above)
+;; at the time solve was called
+;; should this be Num or Int?
+;(check-type (evaluate x sol) : Int -> 0)
+(check-type (evaluate x sol) : Num -> 0)
+;; check soundness of Constant
+(check-not-type (evaluate x sol) : (Constant Num))
 ; we can apply g to concrete values
 (check-type (g 2) : Bool -> #f)
 ; and to symbolic values
-(check-type (g (assert-type x : Int)) : Bool -> (= 0 (real->integer x))) ; nondet result
-;; this should be the only test that is deterministic
+(check-type (g (assert-type x : Int)) : Bool -> (= 0 (real->integer x)))
+
+;; this test does not depend on the term cache
 (check-type (equal? (g 1) (g (assert-type (evaluate x sol) : Int))) : Bool -> #f)
+(clear-asserts!)
 
 ;; ~>
 (define t (~> integer? real? boolean? (bitvector 4)))
@@ -55,3 +67,49 @@
 (typecheck-fail (~> integer? (if b boolean? real?))
  #:with-msg "Expected a Rosette-solvable type, given")
 (typecheck-fail (~> real?) #:with-msg "expected more terms")
+
+;; function?
+(define t0? (~> integer? real? boolean? (bitvector 4)))
+(define t1? (~> integer? real?))
+(check-type (function? t0?) : Bool -> #t)
+(check-type (function? t1?) : Bool -> #t)
+;> (define-symbolic b boolean?)
+(check-type (function? (if b t0? t1?)) : Bool -> #f) ; not a concrete type
+(check-type (function? integer?) : Bool -> #f)       ; not a function type
+(check-type (function? 3) : Bool -> #f)              ; not a type
+
+;; should always be CBool, and sometimes CFalse
+(check-type (function? t0?) : CBool -> #t)
+(check-type (function? t1?) : CBool -> #t)
+(check-type (function? (if b t0? t1?)) : CBool -> #f) ; not a concrete type
+(check-type (function? integer?) : CBool -> #f)       ; not a function type
+(check-type (function? 3) : CBool -> #f)              ; not a type
+
+(check-type (function? t0?) : CBool -> #t)
+(check-type (function? t1?) : CBool -> #t)
+(check-type (function? (if b t0? t1?)) : CFalse -> #f) ; not a concrete type
+(check-type (function? integer?) : CBool -> #f)       ; not a function type
+(check-type (function? 3) : CFalse -> #f)              ; not a type
+
+;; fv?
+(define-symbolic f2 (~> boolean? boolean?))
+(check-type (fv? f2) : Bool -> #t)
+(check-not-type (fv? f2) : CBool)
+(check-type (fv? (lambda ([x : Int]) x)) : Bool -> #f)
+;> (define-symbolic b boolean?)
+(check-type (fv? (if b f2 1)) : Bool -> b)
+(define sol2
+  (solve
+   (begin
+     (assert (not (f2 #t)))
+     (assert (f2 #f)))))
+(check-type sol2 : CSolution)
+(check-type (sat? sol2) : Bool -> #t)
+(define g2 (evaluate f2 sol2))
+(check-type g2 : (→ Bool Bool)) ; g2 implements logical negation
+;(fv (((#f) . #t) ((#t) . #f)) #t boolean?~>boolean?)
+(check-type (fv? g2) : Bool -> #t)
+; verify that g implements logical negation:
+(check-type (verify (assert (equal? (g2 b) (not b)))) : CSolution -> (unsat))
+(check-type (g2 #t) : Bool -> #f)
+(check-type (g2 #f) : Bool -> #t)