add structs (generics dont completely work); add sec5 guide tests

macrotypes/stx-utils.rkt

@@ -83,6 +83,22 @@
 (define (stx-drop stx n)
   (drop (stx->list stx) n))
 
+(define (id-lower-case? stx)
+  (unless (identifier? stx)
+    (error 'stx-upcase "Expected identifier, given ~a" stx))
+  (char-lower-case? 
+   (car (string->list (symbol->string (syntax->datum stx))))))
+
+(define (id-upcase stx)
+  (unless (identifier? stx)
+    (error 'stx-upcase "Expected identifier, given ~a" stx))
+  (define chars (string->list (symbol->string (syntax->datum stx))))
+  (define fst (car chars))
+  (define rst (cdr chars))
+  (datum->syntax 
+   stx 
+   (string->symbol (apply string (cons (char-upcase fst) rst)))))
+
 (define (generate-temporariess stx)
   (stx-map generate-temporaries stx))
 (define (generate-temporariesss stx)

turnstile/examples/rosette/rosette2.rkt

@@ -326,6 +326,53 @@
           (ro:define f-
             (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]])
 
+;; TODO: get subtyping to work for struct-generated types?
+;; TODO: handle mutable structs properly
+(define-typed-syntax struct #:datum-literals (:)
+  [(_ name:id (x:id ...) ~! . rst) ≫
+   #:fail-when #t "Missing type annotations for fields"
+   --------
+   [_ ≻ (ro:struct name (x ...) . rst)]]
+  [(_ name:id ([x:id : ty:type] ...) . kws) ≫
+   #:fail-unless (id-lower-case? #'name)
+                 (format "Expected lowercase struct name, given ~a" #'name)
+   #:with name* (generate-temporary #'name)
+   #:with Name (id-upcase #'name)
+   #:with CName (format-id #'name "C~a" #'Name)
+   #:with TyOut #'(Name ty ...)
+   #:with CTyOut #'(CName ty ...)
+   #:with (name-x ...) (stx-map (lambda (f) (format-id #'name "~a-~a" #'name f)) #'(x ...))
+   #:with (name-x* ...) (stx-map (lambda (f) (format-id #'name* "~a-~a" #'name* f)) #'(x ...))
+   #:with name? (format-id #'name "~a?" #'name)
+   #:with name?* (format-id #'name* "~a?" #'name*)
+   --------
+   [_ ≻ (ro:begin
+          (ro:struct name* (x ...) . kws)
+          (define-type-constructor CName #:arity = #,(stx-length #'(x ...)))
+          (define-named-type-alias (Name x ...) (U (CName x ...)))
+          (define-syntax name   ; constructor
+            (make-variable-like-transformer 
+             (assign-type #'name* #'(C→ ty ... CTyOut))))
+          (define-syntax name?  ; predicate
+            (make-variable-like-transformer 
+             (assign-type #'name?* #'(C→ Any Bool))))
+          (define-syntax name-x ; accessors
+            (make-variable-like-transformer 
+             (assign-type #'name-x* #'(C→ TyOut ty)))) ...)]])
+
+;; TODO: add type rules for generics
+(define-typed-syntax define-generics #:datum-literals (: ->)
+  [(_ name:id (f:id x:id ... -> ty-out)) ≫
+   #:with app-f (format-id #'f "apply-~a" #'f)
+   --------
+   [_ ≻ (ro:begin
+         (ro:define-generics name (f x ...))
+         (define-syntax app-f ; tmp workaround: each gen fn has its own apply
+           (syntax-parser
+             [(_ . es)
+              #:with es+ (stx-map expand/df #'es)
+              (assign-type #'(ro:#%app f . es+) #'ty-out)])))]])
+
 ;; ---------------------------------
 ;; quote
 

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

@@ -0,0 +1,59 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; Examples from the Rosette Guide, Section 5 Structures
+
+; 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→ 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))
+(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 (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
+
+(check-type (eq? (pnt 1 2) (pnt 1 2)) : Bool -> #f) ; pnt structures are references
+
+(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 (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 (= (point-x (evaluate p sol)) 3) : Bool -> #t) 
+
+;; Generics
+(define-generics viewable (view 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))])
+(struct circle ([radius : Nat])
+  #:transparent
+  #:methods gen:viewable
+  [(define (view [self : (Circle Nat)] -> Nat) (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)

turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt

@@ -12,6 +12,8 @@
           "rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8"
           "rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9")
 
+(do-tests "rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures")
+
 (do-tests "bv-tests.rkt" "BV SDSL - General"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")