Changes needed for Ocelot

.travis.yml

@@ -4,9 +4,7 @@ env:
   global:
     - RACKET_DIR=~/racket
   matrix:
-    - RACKET_VERSION="6.6"
-    - RACKET_VERSION="6.7"
-    - RACKET_VERSION="6.8"
+    - RACKET_VERSION="6.9"
     - RACKET_VERSION="HEAD"
 matrix:
   allow_failures:
@@ -30,4 +28,10 @@ install:
 
 script:
  - raco test --package typed-rosette
- - raco setup
+ # Install the Typed Rosette version of Ocelot
+ - raco pkg install -j 1 --auto git://github.com/AlexKnauth/ocelot#typed-rosette
+ - raco setup
+
+after_success:
+ # this currently fails 1 out of 728 tests
+ - raco test --package ocelot

info.rkt

@@ -3,11 +3,14 @@
 (define collection 'multi)
 
 (define deps
-  '(("racket" #:version "6.6")
+  '(("racket" #:version "6.8.0.3")
     "base"
     "rosette"
     "turnstile"
     "rackunit-lib"
+    "lens-common"
+    "lens-unstable"
+    "syntax-classes-lib"
     ))
 
 (define build-deps

sdsl/typed-fsm/fsm.rkt

@@ -1,5 +1,5 @@
 #lang turnstile
-(extends typed/main #:prefix rosette: #:except #%datum #%app define)
+(extends typed/main #:prefix rosette: #:except #%datum #%app define ?)
 (require (prefix-in ro: rosette) ; untyped 
          (prefix-in rosette: "../../typed/lib/synthax.rkt")
          (prefix-in rosette: "../../typed/query/debug.rkt")

sdsl/typed-synthcl/synthcl.rkt

@@ -199,7 +199,7 @@
          (define len-str (caddr split-ty))]
    #:do [(define sels (length (stx->list #'selector)))]
    #:with e-out (if (= sels 1) #'(ro:vector-ref vec- (ro:car 'selector))
-                               #'(for/list ([idx 'selector])
+                               #'(ro:for/list ([idx 'selector])
                                    (ro:vector-ref vec- idx)))
    #:with ty-out ((current-type-eval)
                   (if (= sels 1) (format-id #'here "~a" base-str)
@@ -580,6 +580,6 @@
                (ro:and (ro:sat? cex)
                        (displayln "counterexample found:")
                        (ro:for ([i '(id ...)] [i- (ro:list id- ...)])
-                               (printf "~a = ~a\n" i (ro:evaluate i- cex)))
+                               (ro:printf "~a = ~a\n" i (ro:evaluate i- cex)))
                        cex))
               (begin (displayln "no counterexample found") (ro:unsat))))) ⇒ void]])

test/rosette-guide-sec5-tests.rkt

@@ -5,20 +5,23 @@
 
 ; immutable transparent type
 (struct point ([x : Int] [y : Int]) #:transparent)
-(check-type point : (C→ Int Int (CPoint Int Int)))
-(check-type point-x : (C→ (CPoint Int Int) Int))
-(check-type point-y : (C→ (CPoint Int Int) Int))
+(check-type point : (C→ Int Int CPoint))
+(check-type point : (C→ Int Int (Struct point Int Int)))
+(check-type point-x : (C→ CPoint Int))
+(check-type point-y : (C→ CPoint Int))
 (check-type point? : (C→ Any Bool))
 
 ; opaque immutable type
 (struct pt ([x : Int] [y : Int]))
 ; mutable transparent type
 (struct pnt ([x : Int] [y : Int]) #:mutable #:transparent)
 
-(check-type (point 1 2) : (CPoint Int Int) -> (point 1 2))
+(check-type (point 1 2) : CPoint -> (point 1 2))
+(check-type (point 1 2) : (Struct point Int Int) -> (point 1 2))
+
 (typecheck-fail (point #f 2) #:with-msg "expected.*Int.*given.*False")
-(check-type (pt 1 2) : (CPt Int Int)) ; opaque, incomparable
-(check-type (pnt 1 2) : (CPnt Int Int) -> (pnt 1 2))
+(check-type (pt 1 2) : CPt) ; opaque, incomparable
+(check-type (pnt 1 2) : CPnt -> (pnt 1 2))
 
 (check-type (eq? (point 1 2) (point 1 2)) : Bool -> #t) ; point structures are values
 (check-type (eq? (pt 1 2) (pt 1 2)) : Bool -> #f) ; pt structures are references
@@ -27,33 +30,36 @@
 
 (define-symbolic b boolean?)
 (define p (if b (point 1 2) (point 3 4))) ; p holds a symbolic structure
-(check-type p : (Point Int Int))
-(check-not-type p : (CPoint Int Int))
+(check-type p : Point)
+(check-not-type p : CPoint)
 (check-type (point-x p) : Int -> (if b 1 3)) ;(ite b 1 3)
 (check-type (point-y p) : Int -> (if b 2 4)) ;(ite b 2 4)
 (define sol (solve (assert (= (point-x p) 3))))
-(check-type (evaluate p sol) : (Point Int Int) -> (point 3 4)) ;#(struct:point 3 4)
+(check-type (evaluate p sol) : Point -> (point 3 4)) ;#(struct:point 3 4)
 (check-type (= (point-x (evaluate p sol)) 3) : Bool -> #t) 
 
 ;; Generics
-(define-generics viewable (view viewable -> Nat))
+(define-generics viewable
+  [(view [viewable : Viewable]) -> Nat])
+
 (typecheck-fail 
  (struct square (side)
    #:methods gen:viewable
    [(define (view self) (square-side self))])
  #:with-msg "Missing type annotations for fields")
 (struct square ([side : Nat])
   #:methods gen:viewable
-  [(define (view [self : (Square Nat)]) -> Nat (square-side self))])
+  [(define (view self) (square-side self))])
 (struct circle ([radius : Nat])
   #:transparent
   #:methods gen:viewable
-  [(define (view [self : (Circle Nat)]) -> Nat (circle-radius self))])
+  [(define (view self) (circle-radius self))])
+
 ;(define-symbolic b boolean?)
 (define p2 (if b (square 2) (circle 3))) ; p holds a symbolic structure
-(check-type p2 : (U (CSquare Nat) (CCircle Nat)))
-(check-type p2 : (U (Square Nat) (Circle Nat)))
-(check-type (apply-view p2) : Nat -> (if b 2 3)) ;(ite b 2 3)
-(define sol2 (solve (assert (= (apply-view p2) 3))))
-(check-type (evaluate p2 sol2) : (U (Square Nat) (Circle Nat)) -> (circle 3))
-(check-type (= (apply-view (evaluate p2 sol2)) 3) : Bool -> #t)
+(check-type p2 : (U CSquare CCircle))
+(check-type p2 : (U Square Circle))
+(check-type (view p2) : Nat -> (if b 2 3)) ;(ite b 2 3)
+(define sol2 (solve (assert (= (view p2) 3))))
+(check-type (evaluate p2 sol2) : (U Square Circle) -> (circle 3))
+(check-type (= (view (evaluate p2 sol2)) 3) : Bool -> #t)

test/rosette-tests.rkt

@@ -361,17 +361,17 @@
 (check-type (not #f) : CAny)
 (check-type (equal? 1 2) : CAny)
 
-;; data structures have type CAny only if elements are concrete
+;; data structures have type CAnyDeep only if elements are concrete
 ;; (even if outer structure is concrete)
-(check-type (list 1 2 3) : CAny)
-(check-not-type (list i0 b0) : CAny)
-(check-type (list (list 1 2) (list 3 4)) : CAny)
-(check-type (list (list (list 1 2) 3) 4) : CAny)
-(check-not-type (list (list (list i0 2) 3) 4) : CAny)
+(check-type (list 1 2 3) : CAnyDeep)
+(check-not-type (list i0 b0) : CAnyDeep)
+(check-type (list (list 1 2) (list 3 4)) : CAnyDeep)
+(check-type (list (list (list 1 2) 3) 4) : CAnyDeep)
+(check-not-type (list (list (list i0 2) 3) 4) : CAnyDeep)
 
 ;; Boxes are mutable, so they contain possibly-symbolic types
-(check-not-type (box 1) : CAny)
-(check-not-type (box i0) : CAny)
+(check-not-type (box 1) : CAnyDeep)
+(check-not-type (box i0) : CAnyDeep)
 
 ;; Subtyping between Terms and Unions
 (check-type (ann (ann 1 : CNum) : (Term CNum)) : Num)

test/typed-rosette/for-tests.rkt

@@ -0,0 +1,145 @@
+#lang typed/rosette
+
+(require turnstile/rackunit-typechecking)
+
+;; These tests make sure that #:when conditions can refer to
+;; identifiers defined in previous clauses.
+
+(: string=? : (C→ CString CString CBool))
+(define (string=? a b)
+  (equal? a b))
+
+(check-type (for/list () 1) : (CListof CInt) -> (list 1))
+(check-type (for/list () #t) : (CListof CBool) -> (list #t))
+(check-type (for/list () #f) : (CListof CBool) -> (list #f))
+
+(check-type (for/list (#:when #t) 1) : (CListof CInt) -> (list 1))
+(check-type (for/list (#:when #f) 1) : (CListof CInt) -> (list))
+(check-type (for/list ([x (in-range 5)]) x)
+            : (CListof CInt)
+            -> (list 0 1 2 3 4))
+
+(check-type (for/list ([s (in-list (list "a" "b" "c"))]
+                       [i (in-naturals)])
+              (list s i))
+            : (CListof (CList CString CInt))
+            -> (list (list "a" 0) (list "b" 1) (list "c" 2)))
+
+(check-type (for/list ([s (in-list (list "a" "b" "c"))]
+                       [i (in-naturals)]
+                       #:when (even? i))
+              (list s i))
+            : (CListof (CList CString CInt))
+            -> (list (list "a" 0) (list "c" 2)))
+
+(check-type (for/list ([s (in-list (list "a" "b" "c" "d" "e"))]
+                       [i (in-naturals)]
+                       #:when (even? i)
+                       [j (in-range i)])
+              (list s i j))
+            : (CListof (CList CString CInt CInt))
+            -> (list (list "c" 2 0)
+                     (list "c" 2 1)
+                     (list "e" 4 0)
+                     (list "e" 4 1)
+                     (list "e" 4 2)
+                     (list "e" 4 3)))
+
+;; ------------------------------------------------------------------------
+
+;; Test based on section 11 of the racket guide
+
+(check-type (for/list ([book (in-list (list "Guide" "Reference" "Notes"))]
+                       #:when (not (string=? book "Notes"))
+                       [i (in-naturals 1)]
+                       [chapter (in-list (list "Intro" "Details" "Conclusion" "Index"))]
+                       #:when (not (string=? chapter "Index")))
+              (list book i chapter))
+            : (CListof (CList CString CInt CString))
+            -> (list (list "Guide" 1 "Intro")
+                     (list "Guide" 2 "Details")
+                     (list "Guide" 3 "Conclusion")
+                     (list "Reference" 1 "Intro")
+                     (list "Reference" 2 "Details")
+                     (list "Reference" 3 "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:break (string=? book "Story")
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+              (list book chapter))
+            : (CListof (CList CString CString))
+            -> (list (list "Guide" "Intro")
+                     (list "Guide" "Details")
+                     (list "Guide" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:when #true
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+                       #:break (and (string=? book "Story")
+                                    (string=? chapter "Conclusion")))
+              (list book chapter))
+            : (CListof (CList CString CString))
+            -> (list (list "Guide" "Intro")
+                     (list "Guide" "Details")
+                     (list "Guide" "Conclusion")
+                     (list "Story" "Intro")
+                     (list "Story" "Details")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:when #true
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+                       #:final (and (string=? book "Story")
+                                    (string=? chapter "Conclusion")))
+              (list book chapter))
+            : (CListof (CList CString CString))
+            -> (list (list "Guide" "Intro")
+                     (list "Guide" "Details")
+                     (list "Guide" "Conclusion")
+                     (list "Story" "Intro")
+                     (list "Story" "Details")
+                     (list "Story" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+                       #:final (string=? book "Story")
+                       [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+              (list book chapter))
+            : (CListof (CList CString CString))
+            -> (list (list "Guide" "Intro")
+                     (list "Guide" "Details")
+                     (list "Guide" "Conclusion")
+                     (list "Story" "Intro")))
+
+;; ------------------------------------------------------------------------
+
+;; Tests based on section 3.18 of the racket reference
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:when (odd? i)
+                       [k (in-list (list #t #f))])
+              (list i j k))
+            : (CListof (CList CInt CString CBool))
+            -> (list (list 1 "a" #t)
+                     (list 1 "a" #f)
+                     (list 3 "c" #t)
+                     (list 3 "c" #f)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:break (not (odd? i))
+                       [k (in-list (list #t #f))])
+              (list i j k))
+            : (CListof (CList CInt CString CBool))
+            -> (list (list 1 "a" #true)
+                     (list 1 "a" #false)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+                       [j (in-list (list "a" "b" "c"))]
+                       #:final (not (odd? i))
+                       [k (in-list (list #t #f))])
+              (list i j k))
+            : (CListof (CList CInt CString CBool))
+            -> (list (list 1 "a" #true)
+                     (list 1 "a" #false)
+                     (list 2 "b" #true)))
+