diff --git a/.travis.yml b/.travis.yml index 96a1672..0f0be8a 100644 --- a/.travis.yml +++ b/.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 \ No newline at end of file + # 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 diff --git a/info.rkt b/info.rkt index a3a6a69..cff0e67 100644 --- a/info.rkt +++ b/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 diff --git a/sdsl/typed-fsm/fsm.rkt b/sdsl/typed-fsm/fsm.rkt index faec12e..809d21c 100644 --- a/sdsl/typed-fsm/fsm.rkt +++ b/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") diff --git a/sdsl/typed-synthcl/synthcl.rkt b/sdsl/typed-synthcl/synthcl.rkt index c1df3c6..cbbf641 100644 --- a/sdsl/typed-synthcl/synthcl.rkt +++ b/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]]) diff --git a/test/rosette-guide-sec5-tests.rkt b/test/rosette-guide-sec5-tests.rkt index ca0cf38..7a06f24 100644 --- a/test/rosette-guide-sec5-tests.rkt +++ b/test/rosette-guide-sec5-tests.rkt @@ -5,9 +5,10 @@ ; 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 @@ -15,10 +16,12 @@ ; 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,16 +30,18 @@ (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 @@ -44,16 +49,17 @@ #: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) diff --git a/test/rosette-tests.rkt b/test/rosette-tests.rkt index d3c003d..d47c6c6 100644 --- a/test/rosette-tests.rkt +++ b/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) diff --git a/test/typed-rosette/for-tests.rkt b/test/typed-rosette/for-tests.rkt new file mode 100644 index 0000000..8b2f52e --- /dev/null +++ b/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))) + diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt new file mode 100644 index 0000000..ecdeec1 --- /dev/null +++ b/test/typed-rosette/occurrence.rkt @@ -0,0 +1,116 @@ +#lang typed/rosette + +(require turnstile/rackunit-typechecking + typed/rosette/types + (only-in typed/rosette/base-forms unsafe-assign-type) + (prefix-in $ rosette)) + +(define natural? + (unsafe-assign-type $exact-nonnegative-integer? + : (Ccase-> + (C→* [CAny] [] CBool + : #:+ (@ 0 : CNat) #:- (!@ 0 : CNat)) + (C→* [Any] [] Bool + : #:+ (@ 0 : Nat) #:- (!@ 0 : Nat))))) + +(define unneg + (unsafe-assign-type $- + : (Ccase-> (C→ CNegInt CPosInt) + (C→ NegInt PosInt)))) + +(: f : (C→ CInt CPosInt)) +(define (f x) + (if (natural? x) + (add1 x) + (unneg x))) + +(: f/restricted : (C→ CPosInt CPosInt)) +(define (f/restricted x) + (if (natural? x) + (add1 x) + (unneg x))) + +(: f* : (C→ Int PosInt)) +(define (f* x) + (if (natural? x) + (add1 x) + (unneg x))) + +;; --------------------------------------------------------- + +;; Testing type restricting behavior + +(: g : (C→ (CU CNegInt CZero) CNat)) +(define (g x) + (if (natural? x) + (ann x : CZero) + (unneg x))) + +(: g* : (C→ (Term (CU CNegInt CZero)) Nat)) +(define (g* x) + (if (natural? x) + (ann x : Zero) + (unneg x))) + +;; --------------------------------------------------------- + +;; Unions with Nothings and non-Nothings in them should not +;; be Nothing! + +(typecheck-fail + (λ ([x : (CU CNothing CString)]) + (ann x : CNothing)) + #:with-msg + "expected CNothing, given \\(CU CNothing CString\\)") + +;; --------------------------------------------------------- + +;; Testing occurrence typing with case-> + +(: h : (Ccase-> (C→ CInt CInt) + (C→ CString CString))) +(define (h x) + (if (integer? x) + (f x) + (string-append "|" (string-append x "|")))) + +(check-type (h 4) : CInt -> 5) +(check-type (h -4) : CInt -> 4) +(check-type (h "four") : CString -> "|four|") + +;; --------------------------------------------------------- + +;; Testing occurrence typing with or + +(: f/intstr : (C→ (CU CInt CString) CInt)) +(define (f/intstr x) + (if (integer? x) + x + (string-length x))) + +(: f/or : (C→ CAny CInt)) +(define (f/or x) + (if (or (integer? x) (string? x)) + (f/intstr x) + 0)) + +(check-type (f/or 5) : CInt -> 5) +(check-type (f/or "five") : CInt -> 4) +(check-type (f/or (list 1 2 3 4 5)) : CInt -> 0) + +(: bool->int : (C→ Bool Int)) +(define (bool->int b) + (if b 1 0)) + +(: f/intbool* : (C→ (U Int Bool) Int)) +(define (f/intbool* x) + (if (integer? x) + x + (bool->int x))) + +(: f/or* : (C→ Any Int)) +(define (f/or* x) + (if (or (integer? x) (boolean? x)) + (f/intbool* x) + 0)) + diff --git a/test/typed-rosette/occurrence2.rkt b/test/typed-rosette/occurrence2.rkt new file mode 100644 index 0000000..79d94c6 --- /dev/null +++ b/test/typed-rosette/occurrence2.rkt @@ -0,0 +1,7 @@ +#lang typed/rosette + +(: f : (C→ (CU CInt CFalse) CInt)) +(define (f x) + (if (not (false? x)) + (ann x : CInt) + 0)) diff --git a/typed/rosette-util.rkt b/typed/rosette-util.rkt index 91e5189..ac46918 100644 --- a/typed/rosette-util.rkt +++ b/typed/rosette-util.rkt @@ -18,8 +18,11 @@ (define (assert-pred a pred) (if (type? pred) (type-cast pred a) - (begin - (assert (pred a)) + (let ([pass? (pred a)]) + (when (and (not (union? pass?)) (not (term? pass?)) (false? pass?)) + (printf "assert-pred failed outright\n a: ~v\n pred: ~v\n" + a pred)) + (assert pass?) a))) ;; zero-integer? : Any -> Bool diff --git a/typed/rosette.rkt b/typed/rosette.rkt index e1fb531..e12ef4c 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -11,23 +11,48 @@ ;; import typed rosette types "rosette/types.rkt" ;; import base forms - (rename-in "rosette/base-forms.rkt" [#%app app]) + (rename-in (except-in "rosette/base-forms.rkt" list) [#%app app]) + (except-in "rosette/bool.rkt" and or not) + (except-in "rosette/list.rkt" pair) + "rosette/match-core.rkt" + "rosette/match-pat-forms.rkt" + "rosette/struct.rkt" "rosette/struct-type-properties.rkt" + "rosette/generic-interfaces.rkt" + "rosette/for-forms.rkt" + "rosette/format.rkt" + "rosette/vector.rkt" + "rosette/hash.rkt" + "rosette/function.rkt" ;; base lang - (prefix-in ro: (combine-in rosette rosette/lib/synthax)) + (prefix-in ro: (combine-in rosette rosette/lib/synthax + "rosette/concrete-predicate.rkt")) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) -(provide : define set! λ apply ann begin list +(provide : define set! λ apply ann begin let (rename-out [app #%app] [ro:#%module-begin #%module-begin] - [λ lambda]) - prop:procedure struct-field-index + [λ lambda] + [ro:begin splicing-begin]) + match match-let _ var ? + (all-from-out "rosette/bool.rkt" + "rosette/match-pat-forms.rkt" + "rosette/struct.rkt" + "rosette/struct-type-properties.rkt" + "rosette/generic-interfaces.rkt" + "rosette/for-forms.rkt" + "rosette/format.rkt" + "rosette/list.rkt" + "rosette/vector.rkt" + "rosette/hash.rkt" + "rosette/function.rkt") (for-syntax get-pred expand/ro) - CAny Any CNothing Nothing + CAnyDeep CAny Any CNothing Nothing Term CU U (for-syntax ~CU* ~U*) Constant + Struct C→ C→* → (for-syntax ~C→ ~C→* C→? concrete-function-type?) Ccase-> (for-syntax ~Ccase-> Ccase->?) ; TODO: sym case-> not supported CListof Listof CList CPair Pair @@ -55,6 +80,7 @@ CSolution CSolver CPict CRegexp LiftedPred LiftedPred2 LiftedNumPred LiftedIntPred UnliftedPred) + ;; a legacy auto-providing version of define-typed-syntax ;; TODO: convert everything to new define-typed-syntax (define-syntax (define-typed-syntax stx) @@ -155,7 +181,7 @@ ;; TODO: get subtyping to work for struct-generated types? ;; TODO: handle mutable structs properly -(define-typed-syntax struct #:datum-literals (:) +#;(define-typed-syntax struct #:datum-literals (:) [(_ name:id (x:id ...) ~! . rst) ≫ #:fail-when #t "Missing type annotations for fields" -------- @@ -188,7 +214,7 @@ (assign-type #'name-x* #'(C→ TyOut ty)))) ...)]]) ;; TODO: add type rules for generics -(define-typed-syntax define-generics #:datum-literals (: ->) +#;(define-typed-syntax define-generics #:datum-literals (: ->) [(_ name:id (f:id x:id ... -> ty-out)) ≫ #:with app-f (format-id #'f "apply-~a" #'f) -------- @@ -200,125 +226,6 @@ #:with es+ (stx-map expand/df #'es) (assign-type #'(ro:#%app f . es+) #'ty-out)])))]]) -;; --------------------------------- -;; quote - -(define-typed-syntax quote - ;; base case: symbol - [(_ x:id) ≫ - -------- - [⊢ (ro:quote x) ⇒ CSymbol]] - ;; recur: list (this clause should come before pair) - [(_ (x ...)) ≫ - [⊢ (quote x) ≫ (_ x-) ⇒ τ] ... - -------- - [⊢ (ro:quote (x- ...)) ⇒ (CList τ ...)]] - ;; recur: pair - [(_ (x . y)) ≫ - [⊢ (quote x) ≫ (_ x-) ⇒ τx] - [⊢ (quote y) ≫ (_ y-) ⇒ τy] - -------- - [⊢ (ro:quote (x- . y-)) ⇒ (CPair τx τy)]] - ;; base case: other datums - [(_ x) ≫ - [⊢ (stlc+union:#%datum . x) ≫ (_ x-) ⇒ τ] - -------- - [⊢ (ro:quote x-) ⇒ τ]]) - -;; --------------------------------- -;; if - -;; TODO: this is not precise enough -;; specifically, a symbolic non-bool should produce a concrete val -(define-typed-syntax if - [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]] - #:when (or (concrete? #'ty_tst) ; either concrete - ; or non-bool symbolic - ; (not a super-type of CFalse) - (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) - (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) - [⊢ [e1 ≫ e1- ⇒ : ty1]] - [⊢ [e2 ≫ e2- ⇒ : ty2]] - #:when (and (concrete? #'ty1) (concrete? #'ty2)) - -------- - [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (CU ty1 ty2)]]] - [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : _]] - [⊢ [e1 ≫ e1- ⇒ : ty1]] - [⊢ [e2 ≫ e2- ⇒ : ty2]] - #:with τ_out (type-merge #'ty1 #'ty2) - -------- - [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) - -;; --------------------------------- -;; vector - -;; mutable constructor -(define-typed-syntax vector - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] - #:with τ* (type-merge* - (stx-map type-merge #'[τ ...] #'[τ ...])) - -------- - [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CMVectorof (U τ*))]]]) - -(provide (typed-out [vector? : LiftedPred])) - -;; immutable constructor -(define-typed-syntax vector-immutable - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] - -------- - [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) - #'(CIVectorof (CU τ ...)) - #'(CIVectorof (U τ ...)))]]]) - -;; TODO: add CList case? -;; returne mutable vector -(define-typed-syntax list->vector - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:list->vector ⇒ : (Ccase-> (C→ (CListof Any) (CMVectorof Any)) - (C→ (Listof Any) (MVectorof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof #,(if (concrete? #'τ) #'(U τ) #'τ))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - #:with [τ* ...] (stx-map (λ (τ) (if (concrete? τ) #`(U #,τ) τ)) #'[τ ...]) - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVectorof τ*) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof (U τ ...))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVector (U τ ...)) ...)]]]) - -(define-typed-syntax vector-ref - [(_ e n) ≫ - [⊢ [e ≫ e- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] - [⊢ [n ≫ n- ⇐ : Int]] - -------- - [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : τ]]] - [(_ e n) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~and (~or (~CMVectorof τ) (~CIVectorof τ))) ...)]] - [⊢ [n ≫ n- ⇐ : Int]] - -------- - [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : (U τ ...)]]]) - -(define-typed-syntax vector-set! - [(_ v:expr i:expr x:expr) ≫ - [⊢ v ≫ v- ⇒ (~CMVectorof τ)] - [⊢ i ≫ i- ⇐ Nat] - [⊢ x ≫ x- ⇐ τ] - -------- - [⊢ (ro:vector-set! v- i- x-) ⇒ CUnit]]) - ;; --------------------------------- ;; hash tables @@ -337,173 +244,7 @@ ;; --------------------------------- ;; lists -(provide (typed-out [null? : (Ccase-> (C→ (CListof Any) CBool) - (C→ (Listof Any) Bool))] - [empty? : (Ccase-> (C→ (CListof Any) CBool) - (C→ (Listof Any) Bool))] - [list? : LiftedPred])) - -(define-typed-syntax cons - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> - (C→ Any Any (CPair Any Any)) - (C→ Any (CListof Any) (CListof Any)) - (C→ Any (Listof Any) (Listof Any)))]]] - [(_ e1 e2) ≫ - [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]] - [⊢ [e1 ≫ e1- ⇒ : τ2]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) - ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2)) - #'(CListof (CU τ1 τ2)) - #'(CListof (U τ1 τ2)))]]] - [(_ e1 e2) ≫ - [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] - [⊢ [e1 ≫ e1- ⇒ : τ1]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : τ2]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) - -;; car and cdr additionally support pairs -(define-typed-syntax car - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any) - (C→ (Listof Any) Any))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ1 ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CPair τ _)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CPair τ _) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]]) - -(define-typed-syntax cdr - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:cdr ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) - (C→ (Listof Any) (Listof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CListof τ) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CList τ ...) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CPair _ τ)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CPair _ τ) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U τ ...)]]]) - - -(define-typed-syntax first - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : τ1]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ1 ...)]]]) - -(define-typed-syntax rest - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) - (C→ (Listof Any) (Listof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (CListof τ)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CListof τ) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (CList τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CList τ ...) ...)]]]) -(define-typed-syntax second - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ2 τ ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : τ2]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ2 ...)]]]) ;; n must be Int bc Rosette does not have symbolic Nats (define-typed-syntax take @@ -532,28 +273,6 @@ -------- [⊢ [_ ≫ (ro:take e- n-) ⇒ : (U (CList (U τ ...)) ...)]]]) -(define-typed-syntax length - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:length ⇒ : (Ccase-> (C→ (CListof Any) CNat) - (C→ (Listof Any) Nat))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇐ : (CListof Any)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof _) ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList _ ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList _ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]]) - (define-typed-syntax reverse [_:id ≫ ;; TODO: use polymorphism -------- @@ -578,130 +297,21 @@ -------- [⊢ [_ ≫ (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)]]]) - -;; TODO: finish andmap -(define-typed-syntax andmap - #;[_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] - [(_ f lst) ≫ - [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool)]] - [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] - -------- - [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : Bool]]] - #;[(_ f lst) ≫ - [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] - [⊢ [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 - -------- - [⊢ [_ ≫ ro:sort ⇒ : (Ccase-> (C→ (CListof Any) LiftedPred2 (CListof Any)) - (C→ (Listof Any) LiftedPred2 (Listof Any)))]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ τ τ Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof τ)]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ...) (U τ ...) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CListof τ) ...)]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~CList . τs)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U . τs) (U . τs) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof (U . τs))]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ... ...) (U τ ... ...) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CList (U τ ...)) ...)]]]) - ;; --------------------------------- ;; IO and other built-in ops -(provide (typed-out [void : (C→ CUnit)] - [printf : (Ccase-> (C→ CString CUnit) - (C→ CString Any CUnit) - (C→ CString Any Any CUnit))] +(provide (typed-out [void : (C→* [] [] #:rest (Listof Any) CUnit)] [display : (C→ Any CUnit)] [displayln : (C→ Any CUnit)] [with-output-to-string : (C→ (C→ Any) CString)] [string-contains? : (C→ CString CString CBool)] [pretty-print : (C→ Any CUnit)] - [error : (Ccase-> (C→ (CU CString CSymbol) CNothing) - (C→ CSymbol CString CNothing))] - + [string-length : (C→ CString CNat)] [string-append : (C→ CString CString CString)] - [equal? : LiftedPred2] - [eq? : LiftedPred2] + [equal? : LiftedPredDeep2] + [eq? : LiftedPredDeep2] [distinct? : (Ccase-> (C→* [] [] #:rest (CListof CAny) CBool) (C→* [] [] #:rest (CListof Any) Bool) (C→* [] [] #:rest (Listof Any) Bool))] @@ -830,6 +440,19 @@ (C→ Num Num))] [truncate : (Ccase-> (C→ CNum CNum) (C→ Num Num))] + [exact-round : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [exact-floor : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [exact-ceiling : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [sgn : (Ccase-> (C→ CZero CZero) (C→ Zero Zero) (C→ CInt CInt) @@ -845,22 +468,20 @@ (C→ Int Int Int) (C→ CNum CNum CNum) (C→ Num Num Num))] + + [exp : (C→ CNum CNum)] + [log : (C→ CNum CNum)] - [not : LiftedPred] - [xor : (Ccase-> (C→ CAny CAny CAny) - (C→ Any Any Any))] - [false? : LiftedPred] - - [true : CTrue] - [false : CFalse] [real->integer : (C→ Num Int)] - [string? : UnliftedPred] - [number? : LiftedPred] + [string? : (UnliftedPredFor CString)] + [number? : (LiftedPredFor Num)] [positive? : LiftedNumPred] [negative? : LiftedNumPred] [zero? : LiftedNumPred] [even? : LiftedIntPred] [odd? : LiftedIntPred] + [exact-nonnegative-integer? : (LiftedPredFor Nat)] + [inexact->exact : (Ccase-> (C→ CNum CNum) (C→ Num Num))] [exact->inexact : (Ccase-> (C→ CNum CNum) @@ -883,44 +504,28 @@ ;; --------------------------------- ;; more built-in ops +(define-simple-macro + (define-solvable-type-predicate pred? ro-pred? CType Type) + (begin- + (provide- pred?) + (define-syntax- pred? + (make-variable-like-transformer + (attach (⊢ (mark-solvablem ro-pred?) : (LiftedPredFor Type)) + 'typefor + ((current-type-eval) #'(Term CType))))))) + ;(define-rosette-primop boolean? : (C→ Any Bool)) -(define-typed-syntax boolean? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:boolean?) - (⇒ : LiftedPred) - (⇒ typefor (Term CBool))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:boolean? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate boolean? ro:boolean? CBool Bool) ;(define-rosette-primop integer? : (C→ Any Bool)) -(define-typed-syntax integer? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:integer?) - (⇒ : LiftedPred) - (⇒ typefor (Term CInt))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:integer? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate integer? ro:integer? CInt Int) ;(define-rosette-primop real? : (C→ Any Bool)) -(define-typed-syntax real? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:real?) - (⇒ : LiftedPred) - (⇒ typefor (Term CNum))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:real? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate real? ro:real? CNum Num) + +(provide (typed-out [concrete-boolean? + : (C→* [Any] [] CBool : + #:+ (@ 0 : CBool) #:- (!@ 0 : CBool))])) (define-typed-syntax time [(_ e) ≫ @@ -993,7 +598,7 @@ (provide (typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) (C→ CInt CPosInt CBV))] - [bv? : LiftedPred] + [bv? : (LiftedPredFor BV)] [bveq : (C→ BV BV Bool)] [bvslt : (C→ BV BV Bool)] @@ -1114,9 +719,7 @@ [_:id ≫ -------- [⊢ [_ ≫ ro:&& ⇒ : - (Ccase-> (C→ Bool) - (C→ Bool Bool) - (C→ Bool Bool Bool))]]] + (C→* [] [] #:rest (Listof Bool) Bool)]]] [(_ e ...) ≫ [⊢ [e ≫ e- ⇐ : Bool] ...] -------- @@ -1125,39 +728,14 @@ [_:id ≫ -------- [⊢ [_ ≫ ro:|| ⇒ : - (Ccase-> (C→ Bool) - (C→ Bool Bool) - (C→ Bool Bool Bool))]]] + (C→* [] [] #:rest (Listof Bool) Bool)]]] [(_ e ...) ≫ [⊢ [e ≫ e- ⇐ : Bool] ...] -------- [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]]) -(define-typed-syntax and - [(_) ≫ - -------- - [⊢ [_ ≫ (ro:and) ⇒ : CTrue]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇐ : Bool] ...] - -------- - [⊢ [_ ≫ (ro:and e- ...) ⇒ : Bool]]] - [(_ e ... elast) ≫ - [⊢ [e ≫ e- ⇒ : ty] ...] - [⊢ [elast ≫ elast- ⇒ : ty-last]] - -------- - [⊢ [_ ≫ (ro:and e- ... elast-) ⇒ : #,(type-merge typeCFalse #'ty-last)]]]) -(define-typed-syntax or - [(_) ≫ - -------- - [⊢ [_ ≫ (ro:or) ⇒ : CFalse]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇐ : Bool] ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) ⇒ : Bool]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : ty] ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) +;; and, or, and not are defined in rosette/forms-pre-match.rkt + (define-typed-syntax nand [(_) ≫ -------- @@ -1184,7 +762,7 @@ (provide (typed-out [sat? : UnliftedPred] [unsat? : UnliftedPred] - [solution? : UnliftedPred] + [solution? : (UnliftedPredFor CSolution)] [unknown? : UnliftedPred] [sat : (Ccase-> (C→ CSolution) (C→ (CHashTable Any Any) CSolution))] @@ -1320,7 +898,7 @@ ;(define-rosette-primop gen:solver : CSolver) (provide (typed-out - [solver? : UnliftedPred] + [solver? : (UnliftedPredFor CSolver)] [solver-assert : (C→ CSolver (CListof Bool) CUnit)] [solver-clear : (C→ CSolver CUnit)] [solver-minimize : (C→ CSolver (CListof (U Int Num BV)) CUnit)] @@ -1359,6 +937,21 @@ (define-typed-syntax for/all ;; symbolic e + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : (~U* τ_case ...)]] + #:with τ_x (cond [(= 1 (stx-length #'[τ_case ...])) + (stx-car #'[τ_case ...])] + [(stx-andmap concrete? #'[τ_case ...]) + #'(CU τ_case ...)] + [else + #'(U τ_case ...)]) + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + ;; Merge the τ_body with itself + #:with τ_out (type-merge #'τ_body #'τ_body) + ;; Check that it's a subtype of τ_body, context is expecting that + [τ_out τ⊑ τ_body] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : (~U* τ_case ...)]] #:with τ_x (cond [(= 1 (stx-length #'[τ_case ...])) @@ -1373,6 +966,12 @@ -------- [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : τ_out]]] ;; known concrete e + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : τ_x]] + #:when (concrete? #'τ_x) + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : τ_x]] #:when (concrete? #'τ_x) @@ -1381,6 +980,15 @@ [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : τ_body]]] ;; other, for example a symbolic constant, an Any type, or a symbolic union ;; type that didn't pass the first case + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : τ_x]] + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + ;; Merge the τ_body with itself + #:with τ_out (type-merge #'τ_body #'τ_body) + ;; Check that it's a subtype of τ_body, context is expecting that + [τ_out τ⊑ τ_body] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : τ_x]] [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]] @@ -1397,4 +1005,38 @@ -------- [_ ≻ (for/all ([x e]) (for*/all ([x_rst e_rst] ...) e_body))]]) +;; ------------------------------------------------------------------------ + +;; Errors + +(provide (typed-out + [exn:fail? (C→ Any Bool)] + [raise-argument-error (C→ CSymbol CString Any CNothing)])) + +(define-typed-syntax raise-arguments-error + [(_ name message (~seq field v) ...) ≫ + [⊢ name ≫ name- ⇐ CSymbol] + [⊢ message ≫ message- ⇐ CString] + [⊢ [field ≫ field- ⇐ CString] ...] + [⊢ [v ≫ v- ⇐ Any] ...] + #:with [[field/v- ...] ...] #'[[field- v-] ...] + -------- + [⊢ (ro:raise-arguments-error name- message- field/v- ... ...) + ⇒ CNothing]]) + +;; ------------------------------------------------------------------------ + +;; Other + +(provide define-syntax-rule + define-syntax) + +(define-typed-syntax begin0 + [(_ e0:expr e:expr ...) ≫ + [⊢ e0 ≫ e0- ⇒ τ] + [⊢ [e ≫ e- ⇐ Void] ...] + -------- + [⊢ (ro:begin0 e0- e- ...) ⇒ τ]]) + +;; ------------------------------------------------------------------------ diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 2b89e74..0ae9c39 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -95,6 +95,21 @@ ;; ---------------------------------------------------------------------------- +;; Environments and Variables + +(begin-for-syntax + ;; var-assign/orig-binding : + ;; Id (Listof Sym) (StxListof TypeStx) -> Stx + (define (var-assign/orig-binding x seps τs) + (attachs (attach x 'orig-binding x) + seps + τs + #:ev (current-type-eval))) + + (current-var-assign var-assign/orig-binding)) + +;; ---------------------------------------------------------------------------- + ;; Declaring Types before Definitions (begin-for-syntax @@ -331,7 +346,10 @@ [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ f ≫ f-- ⇒ (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] τ_out) ~!)] #:with f-- (expand/ro #'f) - #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] τ_out) ~!) + #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] + τ_out + : #:+ posprop #:- negprop) + ~!) (typeof #'f--) #:with f- (replace-stx-loc #'f-- #'f) #:fail-unless (stx-length=? #'[a ...] #'[τ_a ...]) @@ -355,12 +373,17 @@ (typecheck-fail-msg/multi #'[τ_a ... τ_b ...] #'[τ_a* ... τ_b* ...] #'[a ... b ...]) #:with [[kw/b- ...] ...] #'[[kw b-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- - [⊢ (ro:#%app f- a- ... kw/b- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app f- a- ... kw/b- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] [(_ f:expr ab:expr ... (~seq kw:keyword c:expr) ...) ≫ ;[⊢ f ≫ f-- ⇒ (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out) ~!)] #:with f-- (expand/ro #'f) - #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out) ~!) + #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out + : #:+ posprop #:- negprop) ~!) (typeof #'f--) #:with f- (replace-stx-loc #'f-- #'f) #:fail-unless (stx-length>=? #'[ab ...] #'[τ_a ...]) @@ -392,8 +415,12 @@ #'[τ_a* ... τ_c* ... τ_rst*] #'[a ... c ... (list b ...)]) #:with [[kw/c- ...] ...] #'[[kw c-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- - [⊢ (ro:#%app ro:apply f- a- ... rst- kw/c- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app ro:apply f- a- ... rst- kw/c- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] ;; concrete case-> [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ f ≫ f- ⇒ (~and (~Ccase-> ~! τ_f ...) ~!)] @@ -406,10 +433,11 @@ #:with [b- ...] (stx-map expand/ro #'[b ...]) #:with [τ_a ...] (stx-map typeof #'(a- ...)) #:with [τ_b ...] (stx-map typeof #'(b- ...)) - #:with τ_out + #:with result-info (for/or ([τ_f (in-list (stx->list #'[τ_f ...]))]) (syntax-parse τ_f - [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] τ_out) + [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] τ_out + : #:+ posprop #:- negprop) (define kws/τs* (for/list ([kw (in-list (syntax->datum #'[kw* ...]))] [τ (in-list (syntax->list #'[τ_kw* ...]))]) @@ -420,8 +448,9 @@ (define p (assoc kw kws/τs*)) (and p (typecheck? τ_b (second p)))) - #'τ_out)] - [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] #:rest τ_rst* τ_out) + (list #'τ_out #'posprop #'negprop))] + [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] #:rest τ_rst* τ_out + : #:+ posprop #:- negprop) #:when (stx-length>=? #'[τ_a ...] #'[τ_a* ...]) #:with [[τ_fst ...] [τ_rst ...]] (split-at* (stx->list #'[τ_a ...]) (list (stx-length #'[τ_a* ...]))) @@ -436,9 +465,9 @@ (define p (assoc kw kws/τs*)) (and p (typecheck? τ_b (second p)))) - #'τ_out)] + (list #'τ_out #'posprop #'negprop))] [_ #false])) - #:fail-unless (syntax-e #'τ_out) + #:fail-unless (syntax-e #'result-info) ; use (failing) typechecks? to get err msg (let* ([τs_given #'(τ_a ...)] [expressions #'(a ...)]) @@ -452,9 +481,14 @@ "\n ") (string-join (stx-map type->str τs_given) ", ") (string-join (map ~s (stx-map syntax->datum expressions)) ", "))) + #:with [τ_out posprop negprop] #'result-info #:with [[kw/b- ...] ...] #'[[kw b-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- - [⊢ (ro:#%app f- a- ... kw/b- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app f- a- ... kw/b- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] ;; concrete union functions [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ [f ≫ f-- ⇒ : (~and (~CU* τ_f ...) ~!)]] @@ -494,7 +528,7 @@ #:with (b* ...) (generate-temporaries #'(b ...)) #:with [[kw/b* ...] ...] #'[[kw b*] ...] [([f* ≫ _ : τ_f] [a* ≫ _ : τ_a] ... [b* ≫ _ : τ_b] ...) - ⊢ [(app f* a* ... kw/b* ... ...) ≫ _ ⇒ : τ_out]] + ⊢ [#,(syntax/loc this-syntax (app f* a* ... kw/b* ... ...)) ≫ _ ⇒ : τ_out]] ... #:with [[kw/b- ...] ...] #'[[kw b-] ...] -------- @@ -537,7 +571,7 @@ -------- [⊢ (ro:apply f- lst-) ⇒ τ_out]] [(_ f:expr lst:expr) ≫ - [⊢ f ≫ f- ⇒ (~Ccase-> τ_f ...)] + [⊢ f ≫ f- ⇒ (~Ccase-> ~! τ_f ...)] [⊢ lst ≫ lst- ⇒ τ_lst] #:with τ_out (for/or ([τ_f (in-list (stx->list #'[τ_f ...]))]) @@ -572,7 +606,7 @@ (define-typed-syntax let #:datum-literals [:] - [(_ name:id ~! ([x:id : τ_x:type e:expr] ...) :-> τ_out:type b ...+) ≫ + [(_ name:id ([x:id : τ_x:type e:expr] ...) :-> ~! τ_out:type b ...+) ≫ [⊢ [e ≫ e- ⇐ τ_x] ...] #:with body (syntax/loc this-syntax (begin b ...)) [[name ≫ name- : (C→ τ_x ... τ_out)] @@ -580,6 +614,14 @@ ⊢ body ≫ body- ⇐ τ_out] -------- [⊢ (let- name- ([x- e-] ...) body-) ⇒ τ_out]] + [(_ name:id ([x:id : τ_x:type e:expr] ...) b ...+) ⇐ τ_out ≫ + [⊢ [e ≫ e- ⇐ τ_x] ...] + #:with body (syntax/loc this-syntax (begin b ...)) + [[name ≫ name- : (C→ τ_x ... τ_out)] + [x ≫ x- : τ_x] ... + ⊢ body ≫ body- ⇐ τ_out] + -------- + [⊢ (let- name- ([x- e-] ...) body-)]] [(_ ([x m:mut-kw e] ...) e_body ...) ⇐ τ_expected ≫ [⊢ [e ≫ e- ⇒ : τ_x] ...] #:with [τ_x* ...] @@ -610,7 +652,7 @@ #:datum-literals [:] [(_ e:expr : τ:expr) ≫ -------- - [⊢ e ⇒ : τ]]) + [⊢ (ro:#%expression e) ⇒ : τ]]) (define-syntax-parser unsafe-define/assign-type #:datum-literals [:] diff --git a/typed/rosette/bool.rkt b/typed/rosette/bool.rkt new file mode 100644 index 0000000..bed030c --- /dev/null +++ b/typed/rosette/bool.rkt @@ -0,0 +1,171 @@ +#lang turnstile + +(require typed/rosette/types + (only-in typed/rosette/base-forms begin unsafe-assign-type) + (prefix-in ro: rosette) + (postfix-in - rosette)) + +;; --------------------------------- + +;; if + +(provide if) + +;; TODO: this is not precise enough +;; specifically, a symbolic non-bool should produce a concrete val +(define-typed-syntax if + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- + (⇒ : ty_tst) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] + #:when (or (concrete? #'ty_tst) ; either concrete + ; or non-bool symbolic + ; (not a super-type of CFalse) + (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) + (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] + #:with τ_out + (cond [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] + [(typecheck? #'ty1 typeCNothing) #'ty2] + [(typecheck? #'ty2 typeCNothing) #'ty1] + ;; else don't need to merge, but do need U + [else #'(U ty1 ty2)]) + -------- + [⊢ [_ ≫ (ro:if e_tst- + e1- + e2-) + ⇒ : τ_out]]] + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- + (⇒ : _) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] + #:with τ_out (type-merge #'ty1 #'ty2) + -------- + [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) + +;; ---------------------------------------------------------------------------- + +;; Other Conditionals + +(provide when unless cond else) + +(define-typed-syntax when + [(_ condition:expr body:expr ...+) ≫ + [⊢ condition ≫ condition- (⇐ : Bool) (⇒ prop+ posprop)] + [⊢ (with-occurrence-prop posprop (begin body ...)) ≫ body- ⇒ τ] + -------- + [⊢ (ro:when condition- body-) ⇒ (U τ Void)]]) + +(define-typed-syntax unless + [(_ condition:expr body:expr ...+) ≫ + [⊢ condition ≫ condition- (⇐ : Bool) (⇒ prop- negprop)] + [⊢ (with-occurrence-prop negprop (begin body ...)) ≫ body- ⇒ τ] + -------- + [⊢ (ro:unless condition- body-) ⇒ (U τ Void)]]) + +(define-syntax-parser cond + #:literals [else] + [(_ [else ~! body:expr]) + #'body] + [(_ [(~and b:expr (~not else)) ~! v:expr] rst ... [else body:expr]) + (quasisyntax/loc this-syntax + (if b + v + #,(syntax/loc this-syntax (cond rst ... [else body]))))]) + +;; ------------------------------------------------------------------------ + +;; and, or, not + +(provide and or not) + +(define-typed-syntax and + [(_) ≫ + -------- + [⊢ (ro:and) + (⇒ : CTrue) + (⇒ prop+ Prop/Top) + (⇒ prop- Prop/Bot)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ e- (⇒ : τ) (⇒ prop+ (Prop p+)) (⇒ prop- (Prop p-))]] + [(_ e:expr ... e_l:expr) ≫ + [⊢ (and e ...) ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + [⊢ (with-occurrence-prop p+ e_l) ≫ e_l- + (⇒ : τ_l) + (⇒ prop+ pl+) + (⇒ prop- pl-)] + #:with τ_out (cond [(and (concrete? #'τ) (concrete? #'τ_l)) + #'(CU CFalse τ_l)] + [(concrete? #'τ) + #'(U CFalse τ_l)] + [else + (type-merge typeCFalse #'τ_l)]) + -------- + [⊢ (ro:and e- e_l-) + (⇒ : τ_out) + (⇒ prop+ (Prop/And (Prop p+) (Prop pl+))) + (⇒ prop- (Prop/Or (Prop p-) (Prop pl-)))]]) + +(define-typed-syntax or + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:or) + (⇒ : CFalse) + (⇒ prop+ Prop/Bot) + (⇒ prop- Prop/Top)]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : CBool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : Bool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : ty] ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) + +(define-typed-syntax not + [:id ≫ + -------- + [⊢ ro:not ⇒ (LiftedPredFor False)]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + #:when (concrete? #'τ) + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) + +;; ---------------------------------------------------------------------------- + +;; Bool Functions + +(provide (typed-out [xor : (Ccase-> (C→ CAny CAny CAny) + (C→ Any Any Any))] + [false? : (LiftedPredFor False)] + + [true : CTrue] + [false : CFalse] + )) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/concrete-predicate.rkt b/typed/rosette/concrete-predicate.rkt new file mode 100644 index 0000000..b9a4dbd --- /dev/null +++ b/typed/rosette/concrete-predicate.rkt @@ -0,0 +1,47 @@ +#lang racket/base + +(provide concrete-boolean? + concrete-integer? + concrete-zero-integer? + concrete-positive-integer? + concrete-negative-integer? + concrete-nonnegative-integer? + concrete-real? + concrete-positive-real? + concrete-negative-real? + concrete-nonnegative-real? + ) + +(require (only-in racket/base + [boolean? concrete-boolean?] + [integer? concrete-integer?] + [real? concrete-real?])) + +;; concrete-zero-integer? : Any -> Bool +(define (concrete-zero-integer? x) + (and (concrete-integer? x) (zero? x))) + +;; concrete-positive-integer? : Any -> Bool +(define (concrete-positive-integer? x) + (and (concrete-integer? x) (positive? x))) + +;; concrete-negative-integer? : Any -> Bool +(define (concrete-negative-integer? x) + (and (concrete-integer? x) (negative? x))) + +;; concrete-nonnegative-integer? : Any -> Bool +(define (concrete-nonnegative-integer? x) + (and (concrete-integer? x) (not (negative? x)))) + +;; concrete-positive-real? : Any -> Bool +(define (concrete-positive-real? x) + (and (concrete-real? x) (positive? x))) + +;; concrete-negative-real? : Any -> Bool +(define (concrete-negative-real? x) + (and (concrete-real? x) (negative? x))) + +;; concrete-nonnegative-real? : Any -> Bool +(define (concrete-nonnegative-real? x) + (and (concrete-real? x) (not (negative? x)))) + diff --git a/typed/rosette/for-forms.rkt b/typed/rosette/for-forms.rkt new file mode 100644 index 0000000..c7a2889 --- /dev/null +++ b/typed/rosette/for-forms.rkt @@ -0,0 +1,197 @@ +#lang turnstile + +(provide for/fold for for/list for/and for/or + for*/list + in-list in-naturals in-range) + +(require typed/rosette/types + (except-in typed/rosette/base-forms #%app) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Syntax Classes for For Clauses + +;; NOTE: +;; Rosette's for forms are unlifted, so these for syntax clases require +;; concrete sequence types and guaurd types. + +(begin-for-syntax + (define-splicing-syntax-class (for-clause-group env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern (~seq (~var clause (for-clause env)) + ...) + #:with [clause- ...] #'[clause.clause- ... ...] + #:with [[env.x env.τ] ...] #'[[clause.env.x clause.env.τ] ... ...]]) + + (define-splicing-syntax-class (guard-clause env) + #:attributes [[clause- 1]] + [pattern (~and (~seq #:when bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:when (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:unless bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:unless (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:break bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:break (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:final bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:final (let- ([x- x] ...) bool-)]]) + + (define-splicing-syntax-class (for-clause env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern (~and [x:id seq:expr] + (~typecheck + #:with [[y τ_y] ...] env + [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~CSequenceof τ_x)])) + #:with [clause- ...] #'[[x (let- ([y- y] ...) seq-)]] + #:with [[env.x env.τ] ...] #'[[x τ_x]]]) + + (define-syntax-class (for-clauses env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern ((~var group (for-clause-group env))) + #:with [clause- ...] #'[group.clause- ...] + #:with [[env.x env.τ] ...] #'[[group.env.x group.env.τ] ...]] + [pattern ((~var fst (for-clause-group env)) + (~var guard (guard-clause (stx-append env #'[[fst.env.x fst.env.τ] ...]))) + . + (~var rst (for-clauses (stx-append env #'[[fst.env.x fst.env.τ] ...])))) + #:with [clause- ...] #'[fst.clause- ... guard.clause- ... rst.clause- ...] + #:with [[env.x env.τ] ...] #'[[fst.env.x fst.env.τ] ... [rst.env.x rst.env.τ] ...]])) + +;; ---------------------------------------------------------------------------- + +;; For Loops + +(define-typed-syntax for/fold + [(_ ([acc:id e_init:expr]) + (~var clauses (for-clauses #'[])) + body:expr ...+) ⇐ τ_acc ≫ + [⊢ e_init ≫ e_init- ⇐ τ_acc] + [[acc ≫ acc- : τ_acc] [clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ (begin body ...) ≫ body- ⇐ τ_acc] + -------- + [⊢ (ro:for/fold ([acc- e_init-]) + (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-))]] + [(_ ([acc:id : τ_acc e_init:expr]) + (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ + [⊢ e_init ≫ e_init- ⇐ τ_acc] + [[acc ≫ acc- : τ_acc] [clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ (begin body ...) ≫ body- ⇐ τ_acc] + -------- + [⊢ (ro:for/fold ([acc- e_init-]) + (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-)) + ⇒ τ_acc]]) + +(define-typed-syntax for + [(_ (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ + [[clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ [body ≫ body- ⇒ _] ...] + -------- + [⊢ (ro:for (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body- ...)) + ⇒ CVoid]]) + +(define-typed-syntax for/list + [(_ (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ + [[clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ (begin body ...) ≫ body- ⇒ τ_body] + -------- + [⊢ (ro:for/list (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-)) + ⇒ (CListof τ_body)]]) + +(define-typed-syntax for*/list + #:datum-literals [:] + [(_ ([x:id : τ_x:type seq:expr] ...) body:expr) ≫ + #:do [(define (triangle lst) + (for/list ([i (in-range (stx-length lst))]) + (take (stx->list lst) i)))] + #:with [[x_prev ...] ...] (triangle #'[x ...]) + #:with [[τ_x_prev ...] ...] (triangle #'[τ_x ...]) + [[x_prev ≫ x_prev- : τ_x_prev] ... + ⊢ seq ≫ seq- ⇐ (CSequenceof τ_x)] + ... + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with [[x-_prev ...] ...] (triangle #'[x- ...]) + -------- + [⊢ (ro:for*/list ([x- (let- ([x_prev- x-_prev] ...) seq-)] ...) + body-) + ⇒ (CListof τ_body)]]) + +(define-typed-syntax for/and + [(_ ([x:id seq:expr] ...) body:expr) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with τ_out (cond [(concrete? #'τ_body) #'(CU CTrue τ_body)] + [else (type-merge* #'[CTrue τ_body τ_body])]) + -------- + [⊢ (ro:for/and ([x- seq-] ...) body-) + ⇒ τ_out]]) + +(define-typed-syntax for/or + [(_ ([x:id seq:expr] ...) body:expr) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with τ_out (cond [(concrete? #'τ_body) #'(CU CFalse τ_body)] + [else (type-merge* #'[CFalse τ_body τ_body])]) + -------- + [⊢ (ro:for/or ([x- seq-] ...) body-) + ⇒ τ_out]]) + +;; ---------------------------------------------------------------------------- + +;; Sequences + +(define-typed-syntax in-list + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇒ : (~CListof ~! τ)] + -------- + [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇒ : (~CList ~! τ ...)] + #:with τ* (cond [(stx-andmap concrete? #'[τ ...]) + #'(CU τ ...)] + [(= 1 (stx-length #'[τ ...])) + (stx-car #'[τ ...])] + [else + #'(U τ ...)]) + -------- + [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ*)]]) + +(define-typed-syntax in-naturals + [(_) ≫ + -------- + [⊢ (ro:in-naturals) ⇒ : (CSequenceof CNat)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇐ CNat] + -------- + [⊢ (ro:in-naturals e-) ⇒ : (CSequenceof CNat)]]) + +(define-typed-syntax in-range + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇐ CNat] + -------- + [⊢ (ro:in-range e-) ⇒ (CSequenceof CNat)]] + [(_ a:expr b:expr) ≫ + [⊢ a ≫ a- ⇐ CNat] + [⊢ b ≫ b- ⇐ CNat] + -------- + [⊢ (ro:in-range a- b-) ⇒ (CSequenceof CNat)]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/format.rkt b/typed/rosette/format.rkt new file mode 100644 index 0000000..799a728 --- /dev/null +++ b/typed/rosette/format.rkt @@ -0,0 +1,62 @@ +#lang turnstile + +(provide ~v format fprintf printf error) + +(require typed/rosette/types + (only-in typed/rosette/base-forms define unsafe-assign-type) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Formatting values as strings + +(begin-for-syntax + ;; format-string-matches? : String [Listof Any] -> Bool + (define (format-string-matches? fmt vals) + (with-handlers ([exn:fail? (λ (e) #false)]) + (apply format fmt vals) + #true)) + ) + +(define ~v (unsafe-assign-type ro:~v : (C→ Any CString))) + +(define-typed-syntax format + [(_ fmt:str v:expr ...) ≫ + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:format fmt v- ...) ⇒ CString]]) + +(define-typed-syntax fprintf + [(_ out:expr fmt:str v:expr ...) ≫ + [⊢ out ≫ out- ⇐ COutputPort] + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:fprintf out- fmt v- ...) ⇒ CUnit]]) + +(define-typed-syntax printf + [(_ fmt:str v:expr ...) ≫ + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:printf fmt v- ...) ⇒ CUnit]]) + +(define-typed-syntax error + [(_ sym:expr fmt:str v:expr ...) ≫ + [⊢ sym ≫ sym- ⇐ CSymbol] + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:error sym- fmt v- ...) ⇒ CNothing]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/forms-pre-match.rkt b/typed/rosette/forms-pre-match.rkt new file mode 100644 index 0000000..64b80a5 --- /dev/null +++ b/typed/rosette/forms-pre-match.rkt @@ -0,0 +1,39 @@ +#lang turnstile + +(provide quote) + +(require "types.rkt" + (rename-in "base-forms.rkt" [#%app app]) + "bool.rkt" + (prefix-in ro: rosette) + (prefix-in stlc+union: turnstile/examples/stlc+union) + ) + +;; ------------------------------------------------------------------------ + +;; quote + +(define-typed-syntax quote + ;; base case: symbol + [(_ x:id) ≫ + -------- + [⊢ (ro:quote x) ⇒ CSymbol]] + ;; recur: list (this clause should come before pair) + [(_ (x ...)) ≫ + [⊢ (quote x) ≫ (_ x-) ⇒ τ] ... + -------- + [⊢ (ro:quote (x- ...)) ⇒ (CList τ ...)]] + ;; recur: pair + [(_ (x . y)) ≫ + [⊢ (quote x) ≫ (_ x-) ⇒ τx] + [⊢ (quote y) ≫ (_ y-) ⇒ τy] + -------- + [⊢ (ro:quote (x- . y-)) ⇒ (CPair τx τy)]] + ;; base case: other datums + [(_ x) ≫ + [⊢ (stlc+union:#%datum . x) ≫ (_ x-) ⇒ τ] + -------- + [⊢ (ro:quote x-) ⇒ τ]]) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/function.rkt b/typed/rosette/function.rkt new file mode 100644 index 0000000..dd87256 --- /dev/null +++ b/typed/rosette/function.rkt @@ -0,0 +1,82 @@ +#lang turnstile + +(provide partial partialr) + +(require typed/rosette/types + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Functions + +;; partial* : [A ... B ... -> C] A ... -> [B ... -> C] +(ro:define ((partial* f . as) . bs) + (ro:apply f (ro:append as bs))) + +;; partialr* : [A ... B ... -> C] B ... -> [A ... -> C] +(ro:define ((partialr* f . bs) . as) + (ro:apply f (ro:append as bs))) + +(define-typed-syntax partial + [(_ f:expr a:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~C→ τ_ab ... τ_c)] + #:do [(define na (stx-length #'[a ...])) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na))] + #:with [τ_a ...] τs_a + #:with [τ_b ...] τs_b + [⊢ [a ≫ a- ⇐ : τ_a] ...] + -------- + [⊢ (partial* f- a- ...) ⇒ : (C→ τ_b ... τ_c)]] + [(_ f:expr a:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~Ccase-> τ_f ...)] + [⊢ [a ≫ a- ⇒ : τ_a*] ...] + #:do [(define na (stx-length #'[a ...])) + (define results + (filter + list? + (for/list ([τ_f (in-list (stx->list #'[τ_f ...]))]) + (define/syntax-parse (~C→ τ_ab ... τ_c) τ_f) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na)) + (and (typechecks? #'[τ_a* ...] τs_a) + (list τs_b #'τ_c)))))] + #:fail-when (empty? results) "no cases match" + #:with [([τ_b ...] τ_c) ...] results + -------- + [⊢ (partial* f- a- ...) ⇒ : (Ccase-> (C→ τ_b ... τ_c) + ...)]]) + +(define-typed-syntax partialr + [(_ f:expr b:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~C→ τ_ab ... τ_c)] + #:do [(define na (- (stx-length #'[τ_ab ...]) (stx-length #'[b ...]))) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na))] + #:with [τ_a ...] τs_a + #:with [τ_b ...] τs_b + [⊢ [b ≫ b- ⇐ : τ_b] ...] + -------- + [⊢ (partialr* f- b- ...) ⇒ : (C→ τ_a ... τ_c)]] + [(_ f:expr b:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~Ccase-> τ_f ...)] + [⊢ [b ≫ b- ⇒ : τ_b*] ...] + #:do [(define nb (stx-length #'[b ...])) + (define results + (filter + list? + (for/list ([τ_f (in-list (stx->list #'[τ_f ...]))]) + (define/syntax-parse (~C→ τ_ab ... τ_c) τ_f) + (define na (- (stx-length #'[τ_ab ...]) nb)) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na)) + (and (typechecks? #'[τ_b* ...] τs_b) + (list τs_a #'τ_c)))))] + #:fail-when (empty? results) "no cases match" + #:with [([τ_a ...] τ_c) ...] results + -------- + [⊢ (partialr* f- b- ...) ⇒ : (Ccase-> (C→ τ_a ... τ_c) + ...)]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/generic-interfaces.rkt b/typed/rosette/generic-interfaces.rkt new file mode 100644 index 0000000..620d00a --- /dev/null +++ b/typed/rosette/generic-interfaces.rkt @@ -0,0 +1,117 @@ +#lang turnstile + +(provide gen:custom-write gen:equal+hash define-generics) + +(require "types.rkt" + "struct.rkt" + (prefix-in ro: (only-in rosette define-generics))) +(module+ test + (require turnstile/rackunit-typechecking + "base-forms.rkt" + (only-in "forms-pre-match.rkt" quote) + (only-in "format.rkt" fprintf))) + +(define-syntax gen:custom-write + (generic-interface-type-info + #'gen:custom-write- + (λ (τ) + (list + (list 'write-proc + #`(C→ #,τ COutputPort (CU CBool CNat) CVoid)))))) + +(define-syntax gen:equal+hash + (generic-interface-type-info + #'gen:equal+hash- + (λ (τ) + (list + (list 'equal-proc + #`(C→ #,τ #,τ (C→ Any Any CBool) CBool)) + (list 'hash-proc + #`(C→ #,τ (C→ Any CInt) CInt)) + (list 'hash2-proc + #`(C→ #,τ (C→ Any CInt) CInt)))))) + +;; ---------------------------------------------------------------------------- + +(begin-for-syntax + (define-syntax-class -> + [pattern (~or (~datum →) (~datum ->))]) + + (define (method-args-erase args) + (syntax-parse args + #:datum-literals [:] + [([x:id : τ_in] ...) #'(x ...)] + [([x:id : τ_in] ... . [rst:id : τ_rst]) #'(x ... . rst)])) + + (define (method-args->τ args τ_out) + (syntax-parse args + #:datum-literals [:] + [([x:id : τ_in] ...) #`(C→ τ_in ... #,τ_out)] + [([x:id : τ_in] ... . [rst:id : τ_rst]) + #`(C→* [τ_in ...] [] #:rest τ_rst #,τ_out)]))) + +(define-syntax-parser define-generics + [(_ generic-id:id + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'generic-id) + (format "Expected lowercase struct name, given ~a" #'generic-id)) + (~parse Name:id (id-upcase #'generic-id)))) + [(method-id:id . method-args) :-> method-τ_out] + ...) + #:with gen-generic-id (format-id #'generic-id "gen:~a" #'generic-id) + #:with [method-args- ...] + (stx-map method-args-erase #'[method-args ...]) + #:with [method-τ ...] + (stx-map method-args->τ #'[method-args ...] #'[method-τ_out ...]) + #:do [(define intro (make-syntax-introducer))] + #:with [generic-id* gen-generic-id* [method-id* ...] [method-args* ...]] + (intro #'[generic-id gen-generic-id [method-id ...] [method-args- ...]]) + #'(begin- + (ro:define-generics generic-id* + (method-id* . method-args*) + ...) + (define-syntax gen-generic-id + (generic-interface-type-info + #'gen-generic-id* + (λ (τ) + (with-syntax ([Name τ]) + (list + (list 'method-id #'method-τ) + ...))))) + (define-syntax method-id + (make-variable-like-transformer + ; TODO: Define Name as a non-Any type that is a + ; supertype of all structs that implement + ; this, but not of anything else. + (with-syntax ([Name #'Any]) + (⊢ method-id* : method-τ)))) + ...)]) + +;; ---------------------------------------------------------------------------- + +(module+ test + (struct foo ([a : Int]) + #:type-name Foo + #:transparent + #:methods gen:custom-write + [(define (write-proc this out mode) + (fprintf out "~v" (foo-a this)))]) + + (define-generics colorable #:type-name Colorable + [(get-color [colorable : Colorable]) -> String] + [(set-color [colorable : Colorable] [color : String]) -> Colorable]) + + (struct point ([x : Float] [y : Float] [color : String]) + #:type-name Point + #:transparent + #:methods gen:colorable + [(define (get-color self) + (point-color self)) + (define (set-color self color) + (point (point-x self) (point-y self) color))]) + + (check-type (get-color (point '1.2 '2.4 '"blue")) : String -> '"blue") + ;; TODO: return Colorable instead of Any + (check-type (set-color (point '1.2 '2.4 '"blue") '"green") : Any + -> (point '1.2 '2.4 '"green")) + ) diff --git a/typed/rosette/hash.rkt b/typed/rosette/hash.rkt new file mode 100644 index 0000000..acb98db --- /dev/null +++ b/typed/rosette/hash.rkt @@ -0,0 +1,64 @@ +#lang turnstile + +(provide make-hash hash-ref hash-set! hash-ref! hash-remove! hash-copy) + +(require (except-in typed/rosette/base-forms #%app) + typed/rosette/types + (prefix-in ro: rosette)) + +;; ------------------------------------------------------------------------ + +;; Hash Tables + +(define-typed-syntax make-hash + [(_) ⇐ (~CHashof K V) ≫ --- [⊢ (ro:make-hash)]] + [(_) ≫ --- [⊢ (ro:make-hash) ⇒ (CHashof Any Any)]] + [(_ e:expr ~!) ≫ + [⊢ e ≫ e- ⇒ (~CListof (~CPair τ_key τ_val))] + -------- + [⊢ (ro:make-hash e-) ⇒ (CHashof τ_key τ_val)]]) + +(define-typed-syntax hash-ref + [(_ hsh:expr key:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + -------- + [⊢ (ro:hash-ref hsh- key-) ⇒ : τ_val]] + [(_ hsh:expr key:expr fail:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ fail ≫ fail- ⇐ : (C→ τ_val)] + -------- + [⊢ (ro:hash-ref hsh- key- fail-) ⇒ : τ_val]]) + +(define-typed-syntax hash-set! + [(_ hsh:expr key:expr val:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ val ≫ val- ⇐ : τ_val] + -------- + [⊢ (ro:hash-set! hsh- key- val-) ⇒ : CVoid]]) + +(define-typed-syntax hash-ref! + [(_ hsh:expr key:expr to-set:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ to-set ≫ to-set- ⇐ : (C→ τ_val)] + -------- + [⊢ (ro:hash-ref! hsh- key- to-set-) ⇒ : τ_val]]) + +(define-typed-syntax hash-remove! + [(_ hsh:expr key:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + -------- + [⊢ (ro:hash-remove! hsh- key-) ⇒ : CVoid]]) + +(define-typed-syntax hash-copy + [(_ hsh:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + -------- + [⊢ (ro:hash-copy hsh-) ⇒ : (CHashof τ_key τ_val)]]) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/list.rkt b/typed/rosette/list.rkt new file mode 100644 index 0000000..abe68b4 --- /dev/null +++ b/typed/rosette/list.rkt @@ -0,0 +1,427 @@ +#lang turnstile + +(provide cons pair car cdr + length list-ref first rest second make-list build-list + map foldl member? + cartesian-product* append* sort + andmap) + +(require (rename-in typed/rosette/base-forms [#%app tro:#%app]) + typed/rosette/types + typed/rosette/bool + typed/rosette/forms-pre-match + (only-in turnstile/examples/stlc+tup + tup proj) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Basic list and pair stuff + +(provide (typed-out [null? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [empty? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [list? : LiftedPred])) + +(define-typed-syntax cons + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> + (C→ Any Any (CPair Any Any)) + (C→ Any (CListof Any) (CListof Any)) + (C→ Any (Listof Any) (Listof Any)))]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]] + [⊢ [e1 ≫ e1- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) + ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2)) + #'(CListof (CU τ1 τ2)) + #'(CListof (U τ1 τ2)))]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [e1 ≫ e1- ⇒ : τ1]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) + +(define-typed-syntax pair + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) + +;; car and cdr additionally support pairs +(define-typed-syntax car + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any) + (C→ (Listof Any) Any))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ1 ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair τ _)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair τ _) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]]) + +(define-typed-syntax cdr + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cdr ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CListof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CList τ ...) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair _ τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair _ τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U τ ...)]]]) + +;; ------------------------------------------------------------------------ + +;; Lists + +(define-typed-syntax length + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:length ⇒ : (Ccase-> (C→ (CListof Any) CNat) + (C→ (Listof Any) Nat))]]] + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof _)] + -------- + [⊢ (ro:length lst-) ⇒ CNat]] + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~U* (~CListof _) ...)] + -------- + [⊢ (ro:length lst-) ⇒ Nat]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList _ ...)]] + -------- + [⊢ [_ ≫ (ro:length lst-) ⇒ : CNat]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList _ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:length lst-) ⇒ : Nat]]]) + +(define-typed-syntax list-ref + [(_ lst:expr i:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof τ)] + [⊢ i ≫ i- ⇐ CNat] + -------- + [⊢ (ro:list-ref lst- i-) ⇒ τ]] + [(_ lst:expr i:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~or (~CListof τ) + (~U* (~CListof τ)))] + [⊢ i ≫ i- ⇐ Nat] + -------- + [⊢ (ro:list-ref lst- i-) ⇒ (U τ)]]) + +(define-typed-syntax first + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : τ]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : (U τ ...)]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : τ1]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : (U τ1 ...)]]]) + +(define-typed-syntax rest + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (CListof τ)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (U (CListof τ) ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (CList τ ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (U (CList τ ...) ...)]]]) + +(define-typed-syntax second + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : τ]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : (U τ ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ2 τ ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : τ2]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : (U τ2 ...)]]]) + +(define-typed-syntax build-list + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ ro:build-list ⇒ : (C→ CNat (C→ CNat Any) (CListof Any))]] + [(_ n:expr f:expr) ≫ + [⊢ n ≫ n- ⇐ : CNat] + [⊢ f ≫ f- ⇒ : (~C→ X Y)] + #:fail-unless (typecheck? #'X ((current-type-eval) #'CNat)) + "expected function that consumes concrete Nat" + -------- + [⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof Y)]]]) + +(define-typed-syntax make-list + [(_ n:expr v:expr) ≫ + [⊢ n ≫ n- ⇐ : CNat] + [⊢ v ≫ v- ⇒ : τ] + -------- + [⊢ (ro:make-list n- v-) ⇒ : (CListof τ)]]) + +;; ------------------------------------------------------------------------ + +(define-typed-syntax map + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:map ⇒ : (C→ (C→ Any Any) (CListof Any) (CListof Any))]]] + [(_ f:expr lst:expr) ⇐ (~CListof Y) ≫ + [⊢ f ≫ f- ⇒ (~C→ X Y*)] + ; Y* must be usable as Y, because the Y* value will be used + ; as an element the return value + [Y* τ⊑ Y #:for f] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:map f- lst-)]] + [(_ f:expr lst:expr) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! X Y)]] + [⊢ [lst ≫ lst- ⇐ : (CListof X)]] + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]] + [(_ f:expr lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof X)]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ Y) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ X* _) #:when (typecheck? #'X #'X*) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]] + [(_ f:expr lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof X))]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ Y) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ X* _) #:when (typecheck? #'X #'X*) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]]) + + + +(define-typed-syntax foldl + [(_ f:expr base:expr lst:expr) ⇐ Y ≫ + [⊢ f ≫ f- ⇒ (~C→ X Y* Z)] + ; Z must be usable as Y*, because the Z value will be + ; used as the Y* argument on the next iteration + [Z τ⊑ Y* #:for f] + ; Z must be usable as Y, because the Z value will be used + ; as the return value + [Z τ⊑ Y #:for f] + ; Y must be usable as Y*, because the base Y value will + ; be used as the Y* argument on the first iteration + [Y τ⊑ Y* #:for f] + ; base must be usable as Y, because the base value will + ; be used as the return value + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-)]] + [(_ f:expr base:expr lst:expr) ⇐ Y ≫ + ; TODO: fix this to take X into account when choosing + ; which case to commit to + [⊢ f ≫ f- ⇒ + (~Ccase-> _ ... + (~and (~C→ X Y* Z) + (~fail #:unless (typecheck? #'Z #'Y*)) + (~fail #:unless (typecheck? #'Z #'Y)) + (~fail #:unless (typecheck? #'Y #'Y*))) + _ ...)] + ; base must be usable as Y, because the base value will + ; be used as the return value + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-)]] + [(_ f:expr base:expr lst:expr) ≫ + ; TODO: fix this to try all options in the Ccase-> + [⊢ f ≫ f- ⇒ (~Ccase-> _ ... (~C→ X Y Z))] + ; Z must be usable as Y, because the Z value will be used + ; as the Y argument on the next iteration + [Z τ⊑ Y #:for f] + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-) ⇒ Y]]) + +(define member + (unsafe-assign-type ro:member : + (C→ Any (Listof Any) Any))) + +(: member? : (C→ Any (Listof Any) Bool)) +(define (member? v lov) + (if (tro:#%app member v lov) '#true '#false)) + +(define-typed-syntax cartesian-product* + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof (~CListof τ))] + -------- + [⊢ (ro:apply ro:cartesian-product lst-)]]) + +(define-typed-syntax append* + [(_ lol:expr) ≫ + [⊢ lol ≫ lol- ⇒ (~CListof (~CListof τ))] + -------- + [⊢ (ro:append* lol-) ⇒ (CListof τ)]]) + +(define-typed-syntax sort + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:sort ⇒ : (Ccase-> (C→ (CListof Any) LiftedPred2 (CListof Any)) + (C→ (Listof Any) LiftedPred2 (Listof Any)))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ τ τ Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof τ)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ...) (U τ ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CListof τ) ...)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CList . τs)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U . τs) (U . τs) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof (U . τs))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ... ...) (U τ ... ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CList (U τ ...)) ...)]]]) + +;; ------------------------------------------------------------------------ + +;; TODO: finish andmap +(define-typed-syntax andmap + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] + [(_ f lst) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool : #:+ p+ #:- _)]] + [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] + #:with prop_out+ + (syntax-parse #'p+ + [(~Prop/IndexType (_ 0) τ_elem) + #`(Prop/ObjType #,(get-arg-obj #'lst-) : (CListof τ_elem))] + [_ #`Prop/Top]) + -------- + [⊢ [_ ≫ (ro:andmap f- lst-) (⇒ : Bool) (⇒ prop+ prop_out+)]]] + #;[(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] + [⊢ [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:andmap 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:andmap f- lst-) ⇒ : (CListof ty2)]]]) diff --git a/typed/rosette/match-core.rkt b/typed/rosette/match-core.rkt new file mode 100644 index 0000000..7d800de --- /dev/null +++ b/typed/rosette/match-core.rkt @@ -0,0 +1,344 @@ +#lang turnstile + +(provide match match-let + _ var ? + (for-syntax prop:match-pattern-id + match-pattern-id + macro/match-pattern-id + struct-predicate-accessor-pattern-id + ;; syntax classes + pat + pat-info + ;; other helpers + λ/pat-info + map-app3)) + +(require (postfix-in - rosette) + "types.rkt" + (only-in "base-forms.rkt" [#%app app*]) + (for-syntax lens/common + unstable/lens/syntax/stx + syntax/parse/class/local-value)) + +;; ------------------------------------------------------------------------ + +;; Match Patterns + +;; pat ::= derived-pat +;; | literal-pat +;; | id-pat + +;; derived-pat ::= match-pattern-id +;; | (match-pattern-id . rest) + +;; literal-pat ::= bool +;; | string +;; | number + +;; id-pat ::= id ; not match-pattern-id or `...` + +;; derived pats will include patterns like +;; | _ +;; | (var id) +;; | (? pred-expr) +;; | (? pred-expr pat) +;; | (_struct-name pat ...) +;; | (quote datum) +;; | (and pat ...) +;; | (or pat ...) ; TODO: branches conflict? +;; | (not pat) +;; | (list lv-pat ...) + +(begin-for-syntax + (define-values [prop:match-pattern-id + match-pattern-id? + match-pattern-id-ref] + (make-struct-type-property 'match-pattern-id)) + (define-syntax-class match-pat-id + #:attributes [get-get-pat-info] + [pattern (~var id (local-value match-pattern-id?)) + #:attr get-get-pat-info + (get-match-pattern-id-function (attribute id.local-value))]) + (define (get-match-pattern-id-function value) + (cond [(match-pattern-id? value) + (get-match-pattern-id-function + ((match-pattern-id-ref value) value))] + [else value])) + + ;; A PatInfo is a + ;; (StxList (StxListof (StxList Id TypeStx)) + ;; PropStx + ;; ExprStx) + (define-syntax-class pat-info + #:attributes [[x 1] [τ 1] pos-prop maybe-vec test-concrete?] + [pattern [([x:id τ:expr] ...) pos-prop maybe-vec test-concrete?]]) + (define-syntax-rule (λ/pat-info v-pat τ-pat obj-pat body ...) + (λ (v τ obj) + (syntax-parse (list v τ obj) + [[v-pat τ-pat obj-pat] body ...]))) + + ;; map-app3 : A B C (Listof [A B C -> D]) -> (Listof D) + (define (map-app3 a b c fs) + (for/list ([f (in-list fs)]) + (f a b c))) + + (define-syntax-class pat + #:attributes [get-pat-info] + ;; get-pat-info : [Stx TypeStx ObjStx -> PatInfo] + [pattern :derived-pat] + [pattern :literal-pat] + [pattern :id-pat]) + + (define-syntax-class id-pat + #:attributes [get-pat-info] + #:datum-literals [_ ...] + [pattern (~and x:id (~not (~or :match-pat-id ...))) + #:attr get-pat-info + (λ/pat-info v τ o #'[([x τ]) Prop/Top (vector-immutable- v) #t])]) + + (define-syntax-class literal-pat + #:attributes [get-pat-info] + [pattern b:boolean + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- b)) #() #f) #f])] + [pattern s:str + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- s)) #() #f) #f])] + [pattern n:number + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- n)) #() #f) #f])] + ) + + (define-syntax-class derived-pat + #:attributes [get-pat-info] + [pattern (~and stx id:match-pat-id) + #:attr get-pat-info + (derived-pat->get-info (attribute id.get-get-pat-info) #'stx)] + [pattern (~and stx (id:match-pat-id . _)) + #:attr get-pat-info + (derived-pat->get-info (attribute id.get-get-pat-info) #'stx)]) + + (define (derived-pat->get-info get-get-pat-info stx) + (define intro (make-syntax-introducer)) + (define stx* (intro stx)) + (define get-pat-info* (get-get-pat-info stx*)) + (define (get-pat-info v τ o) + (intro (get-pat-info* v τ o))) + get-pat-info) + ) + +;; ------------------------------------------------------------------------ + +;; Match + +(define-typed-syntax match + [(_ val:expr [pat:pat body:expr] ...) ≫ + [⊢ val ≫ val- ⇒ τ_val] + #:with obj (get-arg-obj #'val-) + #:with tmp (if (identifier? #'val) #'val- (generate-temporary #'val)) + #:with [p:pat-info ...] + (map-app3 #'tmp #'τ_val #'obj (attribute pat.get-pat-info)) + [[p.x ≫ x- : p.τ] ... + ⊢ (with-occurrence-prop p.pos-prop body) ≫ body- ⇒ τ_body] + ... + #:with τ_out + (cond [(stx-andmap syntax-e #'[p.test-concrete? ...]) + (cond [(stx-andmap concrete? #'[τ_body ...]) + #'(CU τ_body ...)] + [(= 1 (stx-length #'[τ_body ...])) + (stx-car #'[τ_body ...])] + [else + #'(U τ_body ...)])] + [else + (type-merge* #'[τ_body ...])]) + #:with failure- + #'(assert- #false (format- "no matching clause for ~v" tmp)) + #:with matching-expr- + (for/fold ([acc #'failure-]) + ([xs- (in-list (reverse (stx->list #'[[x- ...] ...])))] + [maybe-vec (in-list (reverse (stx->list #'[p.maybe-vec ...])))] + [body- (in-list (reverse (stx->list #'[body- ...])))]) + (with-syntax ([acc acc] + [v-tmp (generate-temporary)] + [maybe-vec maybe-vec] + [(x- ...) xs-] + [(i- ...) (range (stx-length xs-))] + [body- body-]) + (quasisyntax/loc this-syntax + (let- ([v-tmp maybe-vec]) + #,(syntax/loc this-syntax + (if- v-tmp + (let- ([x- (vector-ref- v-tmp i-)] ...) + body-) + acc)))))) + -------- + [⊢ (for/all- ([tmp val-]) matching-expr-) + ⇒ τ_out]]) + +;; ------------------------------------------------------------------------ + +;; Match-Pattern Ids + +(begin-for-syntax + (define match-pattern-id + (local [(struct match-pattern-id [f] + #:property prop:match-pattern-id + (λ (this) (match-pattern-id-f this)))] + match-pattern-id)) + (define macro/match-pattern-id + (local [(struct macro/match-pattern-id [macro-f match-f] + #:property prop:procedure + (struct-field-index macro-f) + #:property prop:match-pattern-id + (λ (this) (macro/match-pattern-id-match-f this)))] + macro/match-pattern-id))) + +(define-syntax _ + (match-pattern-id + (syntax-parser + [_ (λ/pat-info v τ o #'[() Prop/Top #() #t])]))) + +(define-syntax var + (match-pattern-id + (syntax-parser + [(_ x:id) + (λ/pat-info v τ o #'[([x τ]) Prop/Top (vector-immutable- v) #t])]))) + +;; ------------------------------------------------------------------------ + +;; Predicate Patterns + +(define-syntax ? + (match-pattern-id + (syntax-parser + [(~and + (_ pred:expr) + (~⊢ pred ≫ pred- ⇒ : τ_pred)) + (λ/pat-info v τ o + #:with (~and _ + (~typecheck + [[p? ≫ _ : τ_pred] [x ≫ _ : τ] + ⊢ (app* p? x) ≫ _ (⇒ : τ_tst) (⇒ prop+ p+)])) + #'pred + #:with c? (concrete? #'τ_tst) + #'[() + p+ + (and- (pred- v) #()) + c?])] + [(~and + (_ pred:expr p:pat) + (~⊢ pred ≫ pred- ⇒ : τ_pred)) + (λ/pat-info v τ o + #:with sub:pat-info + ((attribute p.get-pat-info) #'v #'τ #'o) ; τ shauld be replaced by p+ + #:with (~and _ + (~typecheck + [[p? ≫ _ : τ_pred] [x ≫ _ : τ] + ⊢ (p? x) ≫ _ (⇒ : τ_tst) (⇒ prop+ p+)])) + #'pred + #:with c? (and (concrete? #'τ_tst) + (syntax-e #'sub.test-concrete?)) + #'[([sub.x sub.τ] ...) + p+ + (and- (pred- v) + sub.maybe-vec) + c?])]))) + +;; ------------------------------------------------------------------------ + +;; Struct Predicate-Accessor Patterns + +;; It's on the user to supply a predicate that implies that the accessors +;; won't fail, and will produce values of the given field types. +;; The predicate must also return a concrete boolean when given a concrete +;; argument. + +(begin-for-syntax + (struct struct-predicate-accessor-pattern-id + [predicate ; Stx + accessors ; [Listof Stx] + field-types] ; [Listof TypeStx] + #:property prop:match-pattern-id + (λ (this) + (match-define + (struct-predicate-accessor-pattern-id predicate + accessors + field-types) + this) + (define n (length accessors)) + (unless (= n (length field-types)) + (error 'struct-precidate-accessor-pattern-id + "must have the same number of accessors and field types")) + (syntax-parser + [(s:id sub-pat:pat ...) + #:fail-unless (= n (stx-length #'[sub-pat ...])) + (format "expected ~v sub-patterns" n) + (λ/pat-info v τ o + #:do [(define τ-concrete? (concrete? #'τ))] + #:with [sub:pat-info ...] + (for/list ([get-pat-info (in-list (attribute sub-pat.get-pat-info))] + [accessor (in-list accessors)] + [field-type (in-list field-types)]) + (get-pat-info #`(#,accessor v) + (if τ-concrete? + field-type + (type-merge field-type field-type)) + #f)) + #:with c? (and τ-concrete? + (stx-andmap syntax-e #'[sub.test-concrete? ...])) + #`[([sub.x sub.τ] ... ...) + (Prop/And (Prop/ObjType o : (Struct s #,@field-types)) + sub.pos-prop + ...) + (and- (#,predicate v) + (maybe-vector-append- sub.maybe-vec ...)) + c?])]))) + ) + +;; ------------------------------------------------------------------------ + +;; Other Match Forms + +(define-typed-syntax match-let + [(_ ([pat:pat e:expr] ...) body:expr) ≫ + [⊢ [e ≫ e- ⇒ τ_e] ...] + #:with [tmp ...] (generate-temporaries #'[e ...]) + #:with [v-tmp ...] (generate-temporaries #'[pat ...]) + #:with [p:pat-info ...] + (for/list ([get-pat-info (in-list (attribute pat.get-pat-info))] + [v (in-list (stx->list #'[tmp ...]))] + [τ_e (in-list (stx->list #'[τ_e ...]))] + [o_e (in-list (stx-map get-arg-obj #'[e- ...]))]) + (get-pat-info v τ_e o_e)) + #:do [(define flat2-lens (stx-flatten/depth-lens 2))] + #:with [x ...] (lens-view flat2-lens #'[[p.x ...] ...]) + #:with [τ_x ...] (lens-view flat2-lens #'[[p.τ ...] ...]) + [[x ≫ x-- : τ_x] ... + ⊢ (with-occurrence-prop (Prop/And (Prop p.pos-prop) ...) body) ≫ body- + ⇒ τ_body] + #:with [[x- ...] ...] (lens-set flat2-lens #'[[p.x ...] ...] #'[x-- ...]) + #:with [[val_x- ...] ...] + (for/list ([n (in-list (stx-map stx-length #'[[p.x ...] ...]))] + [v-tmp (in-list (stx->list #'[v-tmp ...]))]) + (for/list ([i (in-range n)]) + #`(vector-ref- #,v-tmp '#,i))) + -------- + [⊢ (let- ([tmp e-] ...) + (let- ([v-tmp p.maybe-vec] ...) + (assert- v-tmp "match-let pattern failed") + ... + (let- ([x- val_x-] ... ...) + body-))) + ⇒ τ_body]]) + +;; ------------------------------------------------------------------------ + +;; Helpers + +(define (maybe-vector-append- . vs) + (if- (andmap- vector?- vs) + (apply- vector-append- vs) + #false)) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/match-pat-forms.rkt b/typed/rosette/match-pat-forms.rkt new file mode 100644 index 0000000..c442377 --- /dev/null +++ b/typed/rosette/match-pat-forms.rkt @@ -0,0 +1,186 @@ +#lang turnstile + +(provide quote + and or not + list pair) + +(require (postfix-in - rosette) + "types.rkt" + (only-in "base-forms.rkt" + [#%app app*] [list list*]) + (only-in "bool.rkt" + [and and*] [or or*] [not not*]) + (only-in "list.rkt" + [pair pair*]) + (only-in "forms-pre-match.rkt" + [quote quote*]) + "match-core.rkt") + +;; ------------------------------------------------------------------------ + +;; Match Patterns + +;; pat ::= derived-pat +;; | literal-pat +;; | id-pat + +;; derived-pat ::= match-pattern-id +;; | (match-pattern-id . rest) + +;; literal-pat ::= bool +;; | string +;; | number + +;; id-pat ::= id ; not match-pattern-id or `...` + +;; derived pats will include patterns like +;; | _ +;; | (var id) +;; | (quote datum) +;; | (and pat ...) +;; | (or pat ...) ; TODO: branches conflict? +;; | (not pat) +;; | (list lv-pat ...) + +;; ------------------------------------------------------------------------ + +;; Match-Pattern Ids + +(define-syntax quote + (macro/match-pattern-id + (syntax-parser + [(_ datum) #'(quote* datum)]) + (syntax-parser + [(_ datum) + (λ/pat-info v τ o + #:with c? (concrete? #'τ) + #'[() Prop/Top (if- (eq?- v (quote- datum)) #() #f) c?])]))) + +(define-syntax and + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(and* e ...)]) + (syntax-parser + [(_ p:pat ...) + (λ/pat-info v τ o + #:with [sub:pat-info ...] + (map-app3 #'v #'τ #'o (attribute p.get-pat-info)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[([sub.x sub.τ] ... ...) + Prop/Top + (maybe-vector-append- sub.maybe-vec ...) + c?])]))) + +(define-syntax or + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(or* e ...)]) + (syntax-parser + [(_ p:pat ...) + (λ/pat-info v τ o + #:with [sub:pat-info ...] + (map-app3 #'v #'τ #'o (attribute p.get-pat-info)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[() + Prop/Top + (if- (or- sub.maybe-vec ...) #() #f) + c?])]))) + +(define-syntax not + (macro/match-pattern-id + (syntax-parser + [:id #'not*] + [(_ e:expr) #'(not* e)]) + (syntax-parser + [(_ p:pat) + (λ/pat-info v τ o + #:with sub:pat-info ((attribute p.get-pat-info) #'v #'τ #'o) + #:with c? #'sub.test-concrete? + #'[() Prop/Top (if- (not- sub.maybe-vec) #() #f) c?])]))) + +;; ------------------------------------------------------------------------ + +;; Helpers + +(define (maybe-vector-append- . vs) + (if- (andmap- vector?- vs) + (apply- vector-append- vs) + #false)) + +;; ------------------------------------------------------------------------ + +;; List Patterns + +;; list-pat ::= (list lv-pat ...) +;; | (list* lv-pat ... pat) + +;; lv-pat ::= eh-pat ooo +;; | pat + +;; eh-pat ::= pat ; TODO: EH-or patterns? + +;; ooo ::= ... + +;; TODO: implement lv-pats and ellipses + +(define-syntax list + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(list* e ...)]) + (syntax-parser + [(_ p:pat ...) + (define n (stx-length #'[p ...])) + (λ/pat-info v τ o + (syntax-parse #'τ + [(~CList τ_elem ...) + #:when (stx-length=? #'[τ_elem ...] #'[p ...]) + #:with [sub:pat-info ...] + (for/list ([get-pat-info (attribute p.get-pat-info)] + [τ_elem (in-list (stx->list #'[τ_elem ...]))] + [i (in-range n)]) + (get-pat-info #`(list-ref- v #,i) τ_elem #f)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[([sub.x sub.τ] ... ...) + Prop/Top + (maybe-vector-append- sub.maybe-vec ...) + c?]] + [_ + #:with [sub:pat-info ...] + (for/list ([get-pat-info (in-list (attribute p.get-pat-info))] + [i (in-range n)]) + (get-pat-info #`(list-ref- v #,i) #'Any #f)) + #`[([sub.x sub.τ] ... ...) + Prop/Top + (and- (list?- v) + (=- #,n (length- v)) + (maybe-vector-append- sub.maybe-vec ...)) + #f]]))]))) + +(define-syntax pair + (macro/match-pattern-id + (syntax-parser + [(_ e1:expr e2:expr) #'(pair* e1 e2)]) + (syntax-parser + [(_ p1:pat p2:pat) + (λ/pat-info v τ o + (syntax-parse #'τ + [(~CPair τ1 τ2) + #:with s1:pat-info ((attribute p1.get-pat-info) #'(car- v) #'τ1 #f) + #:with s2:pat-info ((attribute p2.get-pat-info) #'(cdr- v) #'τ2 #f) + #:with c? (and (attribute s1.test-concrete?) + (attribute s2.test-concrete?)) + #'[([s1.x s1.τ] ... [s2.x s2.τ] ...) + Prop/Top + (maybe-vector-append- s1.maybe-vec s2.maybe-vec) + c?]] + [_ + #:with s1:pat-info ((attribute p1.get-pat-info) #'(car- v) #'Any #f) + #:with s2:pat-info ((attribute p2.get-pat-info) #'(cdr- v) #'Any #f) + #`[([s1.x s1.τ] ... [s2.x s2.τ] ...) + Prop/Top + (and- (pair?- v) + (maybe-vector-append- s1.maybe-vec s2.maybe-vec)) + #f]]))]))) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/struct.rkt b/typed/rosette/struct.rkt new file mode 100644 index 0000000..766b9c8 --- /dev/null +++ b/typed/rosette/struct.rkt @@ -0,0 +1,340 @@ +#lang turnstile + +(provide struct + (for-syntax generic-interface-type-info)) + +(require racket/splicing + (prefix-in ro: (only-in rosette/safe struct)) + (only-in racket/private/generic-methods + generic-property + generic-method-table) + (only-in turnstile/examples/stlc+union + define-named-type-alias) + typed/rosette/types + typed/rosette/base-forms + typed/rosette/forms-pre-match + typed/rosette/match-core + (for-syntax racket/struct-info + racket/syntax + syntax/parse/class/local-value)) +(module+ test + (require turnstile/rackunit-typechecking)) + +(begin-for-syntax + (define (add-pred stx pred) + (set-stx-prop/preserved stx 'pred pred)) + (define (get-pred stx) + (syntax-property stx 'pred))) + +(define-syntax-parser add-predm + [(_ stx pred) (add-pred #'stx #'pred)]) + +;; ---------------------------------------------------------------------------- + +;; Generic Interfaces + +(begin-for-syntax + (struct generic-interface-type-info [untyped-binding get-methods]) + ;; get-methods : [TypeStx -> (Listof (List Symbol TypeStx))] + (define-syntax-class generic-interface-id + #:attributes [id- get-methods] + [pattern generic-interface + #:declare generic-interface (local-value generic-interface-type-info?) + #:do [(match-define (generic-interface-type-info binding methods) + (attribute generic-interface.local-value))] + #:with id- binding + #:attr get-methods methods])) + +;; ---------------------------------------------------------------------------- + +(begin-for-syntax + (define struct-transformer-binding 'struct-transformer-binding) + (define struct-instance-type 'struct-instance-type) + (define struct-accessors 'struct-accessors) + (define struct-field-types 'struct-field-types) + (define-syntax-class super + [pattern super:typed-struct-id + #:with [accessor ...] #'[super.accessor ...] + #:with [τ_fld ...] #'[super.τ_fld ...] + #:with [τ_fld_merged ...] #'[super.τ_fld_merged ...] + #:attr some-mutable? (attribute super.some-mutable?) + #:with [id-:id τ_inst] + (let ([super (local-expand #'super 'expression '())]) + (list (syntax-property super struct-transformer-binding) + (syntax-property super struct-instance-type)))]) + + ;; ----------------------------------- + ;; Struct Options + + (define-splicing-syntax-class struct-options + #:attributes [get-opts- some-mutable?] + [pattern (~seq mut:struct-opt-mutability + trns:struct-opt-opacity + refl:struct-opt-reflection-name + stpr:struct-opt-property ... + gnrc:struct-opt-generic-methods ...) + #:attr some-mutable? (attribute mut.mutable?) + #:attr get-opts- + (lambda (τ) + (apply stx-append + #'[mut.opt- ... trns.opt- ... refl.opt- ... stpr.opt- ... ...] + (for/list ([get-opts- (in-list (attribute gnrc.get-opts-))]) + (get-opts- τ))))]) + + (define-splicing-syntax-class struct-opt-mutability + [pattern (~seq) + #:attr mutable? #false + #:with [opt- ...] #'[]] + [pattern (~seq #:mutable) + #:attr mutable? #true + #:with [opt- ...] #'[#:mutable]]) + + (define-splicing-syntax-class struct-opt-opacity + [pattern (~seq) + #:with [opt- ...] #'[]] + [pattern (~seq #:transparent) + #:with [opt- ...] #'[#:transparent]]) + + (define-splicing-syntax-class struct-opt-reflection-name + [pattern (~seq) + #:with [opt- ...] #'[]] + [pattern (~seq #:reflection-name + (~and sym-expr:expr + (~⊢ sym-expr ≫ sym-expr- ⇐ CSymbol))) + #:with [opt- ...] #'[#:reflection-name sym-expr-]]) + + (define-splicing-syntax-class struct-opt-property + #:attributes [[opt- 1]] + [pattern (~seq #:property + (~and prop:expr + (~⊢ prop ≫ prop- ⇒ (~CStructTypeProp τ_v))) + val) + #:with [opt- ...] #`[#:property prop- (ann val : τ_v)]]) + + (define-splicing-syntax-class struct-opt-generic-methods + #:attributes [get-opts-] + [pattern (~seq #:methods gnrc:generic-interface-id [method-def:expr ...]) + #:attr get-opts- + (λ (τ) + (define id- + ((make-syntax-delta-introducer #'gnrc #'gnrc.id-) #'gnrc.id- 'flip)) + (define type-decls + (for/list ([method/τ (in-list ((attribute gnrc.get-methods) τ))]) + (define method-id + ;((make-syntax-delta-introducer #'gnrc #'gnrc.id-) + (datum->syntax #'gnrc (first method/τ) #'gnrc));) + (define τ_method (second method/τ)) + #`(: #,method-id : #,τ_method))) + (syntax-parse type-decls + [(type-decl ...) + #`[#:property (generic-property #,id-) + (generic-method-table #,id- #:scope gnrc + type-decl ... + method-def ...)]]))]) + + ;; ----------------------------------- + ) + +(define-syntax-parser struct + #:datum-literals [:] + [(_ name:id (field:id ...+) . _) + (raise-syntax-error #f "Missing type annotations for fields" this-syntax)] + [(_ name:id ([field:id : τ:type] ...) + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'name) + (format "Expected lowercase struct name, given ~a" #'name)) + (~parse Name:id (id-upcase #'name)))) + opts:struct-options) + #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) + #:with constructor/type (generate-temporary #'name) + #:with name? (format-id #'name "~a?" #'name #:source #'name) + #:with [name-field ...] + (for/list ([field (in-list (syntax->list #'[field ...]))]) + (format-id #'name "~a-~a" #'name field #:source #'name #:props #'name)) + #:with [name* internal-name name?* name-field* ...] + ((make-syntax-introducer) #'[name name name? name-field ...]) + #:with [opt- ...] ((attribute opts.get-opts-) #'CName) + #:with [τ_merged ...] (stx-map type-merge #'[τ.norm ...] #'[τ.norm ...]) + #:with n (datum->syntax #'here (stx-length #'[field ...])) + #:with some-mutable? (attribute opts.some-mutable?) + #'(begin- + (ro:struct name* [field ...] opt- ...) + (define-struct-name name constructor/type internal-name CName name? + [name-field ...] + [τ.norm ...] + #false + #true + some-mutable?) + (define-named-type-alias CName + (Struct name τ.norm ...)) + (define-named-type-alias Name + (add-predm (U (Struct name τ_merged ...)) name?)) + (define-syntax- constructor/type + (make-variable-like-transformer + (⊢ name* : (C→ τ.norm ... CName)))) + (: name? : (LiftedPredFor Name)) + (define name? + (unsafe-assign-type name?* : (LiftedPredFor Name))) + (: name-field : (Ccase-> (C→ CName τ) + (C→ Name τ_merged))) + ... + (define name-field + (unsafe-assign-type name-field* : (Ccase-> (C→ CName τ) + (C→ Name τ_merged)))) + ...)] + ;; Sub-structs + ;; TODO: Allow defining a new type for the sub-struct that + ;; is a distinct subtype of the parent's type. + [(_ name:id super:super ([field:id : τ:type] ...) + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'name) + (format "Expected lowercase struct name, given ~a" #'name)) + (~parse Name:id (id-upcase #'name)))) + opts:struct-options) + #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) + #:with name? (format-id #'name "~a?" #'name #:source #'name) + #:with [name-field ...] + (for/list ([field (in-list (syntax->list #'[field ...]))]) + (format-id #'name "~a-~a" #'name field #:source #'name #:props #'name)) + #:with constructor/type (generate-temporary #'name) + #:with [name* internal-name name?* name-field* ...] + ((make-syntax-introducer) #'[name name name? name-field ...]) + #:with [opt- ...] ((attribute opts.get-opts-) #'CName) + #:with [τ_merged ...] (stx-map type-merge #'[τ.norm ...] #'[τ.norm ...]) + #:with some-mutable? (or (attribute super.some-mutable?) + (attribute opts.some-mutable?)) + #'(begin- + (ro:struct name* super [field ...] opt- ...) + (define-struct-name name constructor/type internal-name CName name? + [super.accessor ... name-field ...] + [super.τ_fld ... τ.norm ...] + super + #false + some-mutable?) + (define-named-type-alias CName + (Struct name super.τ_fld ... τ.norm ...)) + (define-named-type-alias Name + (add-predm (U (Struct name super.τ_fld_merged ... τ_merged ...)) name?)) + (define-syntax- constructor/type + (make-variable-like-transformer + (⊢ name* : (C→ super.τ_fld ... τ.norm ... CName)))) + (: name? : LiftedPred) + (define name? + (unsafe-assign-type name?* : (LiftedPredFor Name))) + (: name-field : (Ccase-> (C→ CName τ) + (C→ Name τ_merged))) + ... + (define name-field + (unsafe-assign-type name-field* : + (Ccase-> (C→ CName τ) + (C→ Name τ_merged)))) + ...)] + ) + +(begin-for-syntax + (struct typed-struct-info/match typed-struct-info [] + #:property prop:match-pattern-id + (λ (self) + (struct-predicate-accessor-pattern-id + (typed-struct-info-predicate self) + (typed-struct-info-accessors self) + (typed-struct-info-field-types self)))) + (define (make-typed-struct-info constructor + untyped-id + type + predicate + accessors + field-types + super-id + no-super? + some-mutable?) + (typed-struct-info/match + (make-variable-like-transformer + (set-stx-prop/preserved + (set-stx-prop/preserved + (set-stx-prop/preserved + (set-stx-prop/preserved + constructor + struct-transformer-binding + untyped-id) + struct-instance-type + type) + struct-accessors + accessors) + struct-field-types + field-types)) + untyped-id + predicate + accessors + field-types + super-id + no-super? + some-mutable?))) + +(define-syntax-parser define-struct-name + [(_ name constructor untyped-transformer CName predicate + [accessor ...] + [field-type ...] + (~and super-id (~or :id #false)) + no-super?:boolean + some-mutable?:boolean) + #'(begin- + (define-syntax- name + (make-typed-struct-info (quote-syntax constructor) + (quote-syntax untyped-transformer) + (quote-syntax CName) + (quote-syntax predicate) + (list (quote-syntax accessor) ...) + (list (quote-syntax field-type) ...) + (and (quote super-id) (quote-syntax super-id)) + (quote no-super?) + (quote some-mutable?))) + )]) + +;; ---------------------------------------------------------------------------- + +(module+ test + (struct a () #:transparent) + (struct b () #:transparent) + (struct c () #:transparent) + (struct d () #:transparent) + (struct e () #:transparent) + (struct abc ([a : A] [b : B] [c : C]) #:transparent) + + (check-type (a) : A -> (a)) + (check-type (b) : B -> (b)) + (check-type (c) : C -> (c)) + (check-type (d) : D -> (d)) + (check-type (e) : E -> (e)) + (check-type (abc (a) (b) (c)) : CAbc -> (abc (a) (b) (c))) + (typecheck-fail (abc (a) '3 (c)) + #:with-msg + #;"expected B, given PosInt\n *expression: '3" + "expected: *A, B, C\n *given: *CA, PosInt, CC\n *expressions: \\(a\\), \\(quote 3\\), \\(c\\)") + + ;; predicates + (check-type (a? (a)) : Bool -> '#true) + (check-type (a? (b)) : Bool -> '#false) + (check-type (a? (abc (a) (b) (c))) : Bool -> '#false) + (check-type (abc? (abc (a) (b) (c))) : Bool -> '#true) + + ;; inheritance + ;; This defines a new type, CAbcde, which is a subtype of CAbc. + (struct abcde abc ([d : D] [e : E]) #:transparent) + + (check-type (abcde (a) (b) (c) (d) (e)) : CAbcde + -> (abcde (a) (b) (c) (d) (e))) + (check-type (abcde (a) (b) (c) (d) (e)) : CAbc + -> (abcde (a) (b) (c) (d) (e))) + (typecheck-fail (abcde (a) (b) (c) '3 (e)) + #:with-msg + #;"expected D, given PosInt\n *expression: 3" + "expected: *A, B, C, D, E\n *given: *CA, CB, CC, PosInt, CE\n *expressions: \\(a\\), \\(b\\), \\(c\\), \\(quote 3\\), \\(e\\)") + + ;; inheritance and predicates + (check-type (abc? (abc (a) (b) (c))) : Bool -> '#true) + (check-type (abcde? (abcde (a) (b) (c) (d) (e))) : Bool -> '#true) + (check-type (abc? (abcde (a) (b) (c) (d) (e))) : Bool -> '#true) + (check-type (a? (abcde (a) (b) (c) (d) (e))) : Bool -> '#false) + (check-type (abcde? (abc (a) (b) (c))) : Bool -> '#false) + ) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 5bd0431..338dfeb 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -1,6 +1,6 @@ #lang turnstile -(provide CAny Any +(provide CAnyDeep CAny Any CNothing Nothing Term CU U @@ -9,13 +9,33 @@ ~Term* ~CU* ~U* CU*? U*? ~Constant* Constant*? remove-Constant - concrete?) + concrete? + concrete/shallow-recur?) + ;; Struct types + Struct + (for-syntax typed-struct-id + typed-struct-info + typed-struct-info-predicate + typed-struct-info-accessors + typed-struct-info-field-types) ;; Function types C→ C→* Ccase-> → (for-syntax concrete-function-type? ~C→ ~C→* ~Ccase-> C→? Ccase->?) + ;; Propositions for Occurrence typing + @ !@ + Prop + Prop/Top + Prop/Bot + Prop/ObjType + Prop/ObjNotType + Prop/Or + Prop/And + with-occurrence-prop + (for-syntax prop-instantiate get-arg-obj + ~Prop/IndexType) ;; Parameters CParamof ; TODO: symbolic Param not supported yet ;; List types @@ -24,11 +44,13 @@ (for-syntax ~CListof ~CList ~CPair) ;; Other container types CHashTable + (rename-out [CHashTable CHashof]) CSequenceof CBoxof CMBoxof CIBoxof MBoxof IBoxof CVectorof CMVectorof CIVectorof CVector Vectorof MVectorof IVectorof (for-syntax ~CHashTable + (rename-out [~CHashTable ~CHashof]) ~CSequenceof ~CMBoxof ~CIBoxof ~CMVectorof ~CIVectorof) @@ -40,6 +62,7 @@ (for-syntax ~CStructTypeProp) ;; Other base types CUnit Unit + (rename-out [CUnit CVoid] [Unit Void]) CZero Zero CPosInt PosInt CNegInt NegInt @@ -54,8 +77,12 @@ CAsserts COutputPort CSolution CSolver CPict CRegexp CSymbol - LiftedPred LiftedPred2 LiftedNumPred LiftedIntPred UnliftedPred + LiftedPred LiftedPred2 + LiftedPredDeep LiftedPredDeep2 + LiftedNumPred LiftedIntPred UnliftedPred + LiftedPredFor UnliftedPredFor (for-syntax ~CUnit CUnit? + (rename-out [~CUnit ~CVoid] [CUnit? CVoid?]) ~CString CString? ~CTrue ~CFalse) ;; The relationship between types and @@ -67,8 +94,10 @@ (for-syntax get-pred type-merge type-merge* + typeCNothing typeCFalse - typeCTrue)) + typeCTrue + occurrence-env)) (require (only-in turnstile/examples/stlc+union define-named-type-alias prune+sort current-sub?) @@ -81,6 +110,7 @@ [U CU*] [~U* ~CU*] [U*? CU*?] [case-> Ccase->*] [~case-> ~Ccase->] [case->? Ccase->?] [→ C→/normal] [~→ ~C→/normal] [→? C→/normal?] + [~PosInt ~CPosInt] [~Zero ~CZero] [~NegInt ~CNegInt] [~True ~CTrue] [~False ~CFalse] [~String ~CString] [~Unit ~CUnit]) @@ -88,7 +118,13 @@ [List CListof] [~List ~CListof]) (prefix-in ro: rosette) (prefix-in ro: rosette/lib/synthax) - (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?])) + (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?]) + "concrete-predicate.rkt") + +(require (for-syntax racket/struct-info + syntax/id-table + syntax/parse/class/local-value + syntax/parse/class/struct-id)) ;; --------------------------------- ;; Concrete and Symbolic union types @@ -133,7 +169,7 @@ #:with tys+ (stx-map (current-type-eval) #'tys) #:fail-unless (stx-andmap concrete? #'tys+) "CU requires concrete types" - #'(CU* . tys+)])) + (syntax/loc this-syntax (CU* . tys+))])) ;; user-facing symbolic U constructor: flattens and prunes (define-syntax (U stx) @@ -142,7 +178,7 @@ ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys #:with ((~or (~U* ty1- ...) (~CU* ty2- ...) ty3-) ...) (stx-map (current-type-eval) #'tys) #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...)) - #'(U* . tys-)])) + (syntax/loc this-syntax (U* . tys-))])) ;; user-facing symbolic Term constructor: check solvable (define-syntax-parser Term @@ -171,12 +207,12 @@ [(_ τ:type) #:fail-when (and (not (Term*? #'τ.norm)) #'τ) "Constant requires a symbolic term type" - #'(Constant* τ.norm)])) + (syntax/loc this-syntax (Constant* τ.norm))])) ;; --------------------------------- (define-base-types - CAny Any CBV CStx CSymbol CRegexp + CAnyDeep CAny Any CBV CStx CSymbol CRegexp CSolution CSolver CPict COutputPort) @@ -216,6 +252,45 @@ -------- [⊢ (CVector- τ.norm ...) ⇒ :: #%type]) +;; Struct +(define-internal-type-constructor Struct) + +;; Struct types can't be single-shape types because struct inheritance exists. + +(begin-for-syntax + (struct typed-struct-info + [transformer untyped-id predicate accessors field-types super-id no-super? some-mutable?] + #:property prop:procedure (struct-field-index transformer) + #:property prop:struct-info + (λ (self) + (extract-struct-info + (syntax-local-value (typed-struct-info-untyped-id self))))) + + (define-syntax-class typed-struct-id + #:attributes [[accessor 1] [τ_fld 1] [τ_fld_merged 1] super-id no-super? some-mutable?] + [pattern (~var struct-id (local-value typed-struct-info?)) + #:with [accessor ...] + (typed-struct-info-accessors (attribute struct-id.local-value)) + #:with [τ_fld ...] + (typed-struct-info-field-types (attribute struct-id.local-value)) + #:with [τ_fld_merged ...] + (stx-map type-merge #'[τ_fld ...] #'[τ_fld ...]) + #:attr no-super? + (typed-struct-info-no-super? (attribute struct-id.local-value)) + #:attr super-id + (typed-struct-info-super-id (attribute struct-id.local-value)) + #:attr some-mutable? + (typed-struct-info-some-mutable? (attribute struct-id.local-value))])) + +(define-typed-syntax Struct + [(_ s:typed-struct-id τ:type ...) ≫ + #:fail-unless (stx-length=? #'[s.τ_fld_merged ...] #'[τ.norm ...]) + "wrong number of fields" + [τ.norm τ⊑ s.τ_fld_merged] ... + -------- + [⊢ (Struct- (quote-syntax- s) τ.norm ...) + ⇒ :: #%type]]) + ;; --------------------------------- ;; Pattern Expanders for Types @@ -228,6 +303,58 @@ (define-internal-type-constructor KwArg) ; #:arity = 2 +(define-internal-type-constructor Result) ; #:arity = 3 +(define-internal-type-constructor Prop/And) ; #:arity <= 0 +(define-internal-type-constructor Prop/Or) ; #:arity <= 0 +(define-internal-type-constructor Prop/IndexType) ; #:arity = 2 +(define-internal-type-constructor Prop/IndexNotType) ; #:arity = 2 +(define-internal-type-constructor Prop/ObjType) ; #:arity = 2 +(define-internal-type-constructor Prop/ObjNotType) ; #:arity = 2 + +(define-syntax-parser Prop/Top [:id #'(Prop/And-)]) +(define-syntax-parser Prop/Bot [:id #'(Prop/Or-)]) +(define-syntax-parser @ + #:datum-literals [:] + [(_ i:nat : τ:type) + #'(Prop/IndexType- (quote- i) τ.norm)]) +(define-syntax-parser !@ + #:datum-literals [:] + [(_ i:nat : τ:type) + #'(Prop/IndexNotType- (quote- i) τ.norm)]) + +(define-syntax-parser Prop/ObjType + #:datum-literals [:] + [(_ o : τ:type) + #'(Prop/ObjType- o τ.norm)]) +(define-syntax-parser Prop/ObjNotType + #:datum-literals [:] + [(_ o : τ:type) + #'(Prop/ObjNotType- o τ.norm)]) + +(define-syntax-parser Prop + [(_ p) + (if (syntax-e #'p) + #'p + #'Prop/Top)]) + +(define-syntax-parser Prop/Or + [(_ p ...) + (if (stx-andmap syntax-e #'[p ...]) + #'(Prop/Or- p ...) + #'Prop/Top)]) +(define-syntax-parser Prop/And + [(_ p ...) + #:with [p* ...] + (stx-filter syntax-e #'[p ...]) + #'(Prop/And- p* ...)]) + +(define-internal-type-constructor NoObj) ; #:arity = 0 +(define-internal-type-constructor IdObj) ; #:arity = 1 + +(define-syntax-parser IdObj + [(_ x:id) #`(IdObj- (quote-syntax- + #,(attach #'x 'orig-id (syntax-local-introduce #'x))))]) + (begin-for-syntax (begin-for-syntax (define-syntax-class expr* @@ -235,11 +362,25 @@ (define-syntax-class expr* [pattern (~and :expr (~not [:keyword . _]))]) + (begin-for-syntax + (define-splicing-syntax-class result-prop-pat + #:datum-literals [:] + [pattern (~seq) #:with pat_posprop #'_ #:with pat_negprop #'_] + [pattern (~seq : #:+ pat_posprop #:- pat_negprop)])) + (define-splicing-syntax-class result-prop + #:datum-literals [:] + [pattern (~seq) #:with posprop #'Prop/Top #:with negprop #'Prop/Top] + [pattern (~seq : #:+ posprop #:- negprop)]) + (define-syntax ~C→ (pattern-expander (syntax-parser - [(_ pat_in:expr* ... (~and pat_out:expr* (~not (~literal ...)))) - #'(~C→* [pat_in ...] [] pat_out)]))) + [(_ pat_in:expr* ... + (~and pat_out:expr* (~not (~literal ...))) + props:result-prop-pat) + #'(~C→* [pat_in ...] [] + pat_out + : #:+ props.pat_posprop #:- props.pat_negprop)]))) (define (convert-opt-kws opt-kws) (syntax-parse opt-kws @@ -249,22 +390,25 @@ (define-syntax ~C→* (pattern-expander (syntax-parser - [(_ [pat_in:expr* ...] [pat_kw:expr ...] pat_out:expr*) + [(_ [pat_in:expr* ...] [pat_kw:expr ...] pat_out:expr* + props:result-prop-pat) #:with opt-kws (generate-temporary 'opt-kws) #'(~C→*/internal (~MandArgs pat_in ...) (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~NoRestArg) - pat_out)] - [(_ [pat_in:expr* ...] [pat_kw:expr ...] #:rest pat_rst:expr pat_out:expr*) + (~Result pat_out props.pat_posprop props.pat_negprop))] + [(_ [pat_in:expr* ...] [pat_kw:expr ...] #:rest pat_rst:expr + pat_out:expr* + props:result-prop-pat) #:with opt-kws (generate-temporary 'opt-kws) #'(~C→*/internal (~MandArgs pat_in ...) (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~RestArg pat_rst) - pat_out)]))) + (~Result pat_out props.pat_posprop props.pat_negprop))]))) ) ;; --------------------------------- @@ -279,7 +423,7 @@ #:with tys+ (stx-map (current-type-eval) #'tys) #:fail-unless (stx-andmap concrete-function-type? #'tys+) "Ccase-> require concrete function types" - #'(Ccase->* . tys+)])) + (syntax/loc this-syntax (Ccase->* . tys+))])) ;; TODO: What should case-> do when given symbolic function @@ -322,11 +466,11 @@ ;; --------------------------------- ;; Concrete types -(define-named-type-alias CBool (CU CFalse CTrue)) +(define-named-type-alias CBool (add-predm (CU CFalse CTrue) concrete-boolean?)) -(define-named-type-alias CNat (CU CZero CPosInt)) -(define-named-type-alias CInt (CU CNegInt CNat)) -(define-named-type-alias CNum (CU CFloat CInt)) +(define-named-type-alias CNat (add-predm (CU CZero CPosInt) concrete-nonnegative-integer?)) +(define-named-type-alias CInt (add-predm (CU CNegInt CNat) concrete-integer?)) +(define-named-type-alias CNum (add-predm (CU CFloat CInt) concrete-real?)) (begin-for-syntax (define (concrete-type-solvable? τ) @@ -338,6 +482,7 @@ (stx-andmap type-solvable? #'[τ_in ... τ_out])] [_ #false]))) + (define typeCNothing ((current-type-eval) #'CNothing)) (define typeCFalse ((current-type-eval) #'CFalse)) (define typeCTrue ((current-type-eval) #'CTrue)) (define typeCBool ((current-type-eval) #'CBool)) @@ -372,6 +517,16 @@ (typecheck? b typeCTrue)] [else #false])) + + ;; concrete/shallow-recur? : Type -> Bool + (define (concrete/shallow-recur? t) + (and (concrete? t) + (syntax-parse t + [(~Struct _ _ ...) #t] + [(~CHashTable _ _) #t] + [(~Any _ . tys) + (stx-andmap concrete/shallow-recur? #'tys)] + [_ #t]))) ) ;; --------------------------------- @@ -437,7 +592,8 @@ ;; rest ::= τ ;; output ::= τ (define-typed-syntax C→* - [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] τ_out:expr*) ≫ + [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] τ_out:expr* + props:result-prop) ≫ [⊢ [τ_in ≫ τ_in- ⇐ :: #%type] ...] [⊢ [τ_kw ≫ τ_kw- ⇐ :: #%type] ...] [⊢ τ_out ≫ τ_out- ⇐ :: #%type] @@ -445,9 +601,11 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (NoRestArg-) - τ_out-) + (Result- τ_out- props.posprop props.negprop)) ⇒ :: #%type]] - [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] #:rest τ_rst τ_out:expr*) ≫ + [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] #:rest τ_rst + τ_out:expr* + props:result-prop) ≫ [⊢ [τ_in ≫ τ_in- ⇐ :: #%type] ...] [⊢ [τ_kw ≫ τ_kw- ⇐ :: #%type] ...] [⊢ τ_rst ≫ τ_rst- ⇐ :: #%type] @@ -456,7 +614,7 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (RestArg- τ_rst-) - τ_out-) + (Result- τ_out- props.posprop props.negprop)) ⇒ :: #%type]]) (define-typed-syntax C→ @@ -471,8 +629,12 @@ (define-named-type-alias LiftedPred (Ccase-> (C→ CAny CBool) (C→ Any Bool))) +(define-named-type-alias LiftedPredDeep (Ccase-> (C→ CAnyDeep CBool) + (C→ Any Bool))) (define-named-type-alias LiftedPred2 (Ccase-> (C→ CAny CAny CBool) (C→ Any Any Bool))) +(define-named-type-alias LiftedPredDeep2 (Ccase-> (C→ CAnyDeep CAnyDeep CBool) + (C→ Any Any Bool))) (define-named-type-alias LiftedNumPred (Ccase-> (C→ CNum CBool) (C→ Num Bool))) (define-named-type-alias LiftedIntPred (Ccase-> (C→ CInt CBool) @@ -482,6 +644,13 @@ (define-named-type-alias CBVPred LiftedPred) (define-named-type-alias BVPred (add-predm (U LiftedPred) lifted-bitvector?)) +(define-simple-macro (LiftedPredFor τ:type) + (Ccase-> (C→* [CAny] [] CBool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm)) + (C→* [Any] [] Bool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm)))) + +(define-simple-macro (UnliftedPredFor τ:type) + (C→* [Any] [] CBool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm))) + ;; --------------------------------------------------------- ;; Merging @@ -563,6 +732,8 @@ ;; type-merge : Type Type -> Type (define (type-merge a b) (cond [(types-same-singleton? a b) a] + [(typecheck? a typeCNothing) b] + [(typecheck? b typeCNothing) a] [else ;; Here it will result in some kind of term or union, ;; so remove immediate Constant wrappers @@ -609,6 +780,18 @@ ;; otherwise, some more complicated merging is ;; needed, using both a U on the outside and ;; possibly more merges in sub-parts + [(and (Struct? a) (Struct? b)) + (syntax-parse (list a b) + #:literals [quote-syntax-] + [[(~Struct (quote-syntax- sa:id) τa ...) + (~Struct (quote-syntax- sb:id) τb ...)] + #:when (free-identifier=? #'sa #'sb) + #:with [τab ...] (stx-map type-merge #'[τa ...] #'[τb ...]) + ((current-type-eval) #'(U (Struct sa τab ...)))] + [_ + ;; TODO: do some merging within if they are related by + ;; sub-structing + ((current-type-eval) #`(U #,a #,b))])] [else ;; TODO: do some merging within ((current-type-eval) #`(U #,a #,b))])) @@ -662,6 +845,312 @@ ;; --------------------------------------------------------- +;; Instantiating Propositions for Occurrence Typing + +(begin-for-syntax + (define propProp/Top ((current-type-eval) #'Prop/Top)) + + ;; prop-instantitate : (Listof ObjStx) -> [PropStx -> PropStx] + (define (prop-instantiate arg-objs) + (define (inst p) + (syntax-parse (if (syntax-e p) p propProp/Top) + #:literals [quote-] + [(~Prop/And q ...) + #`(Prop/And- #,@(stx-map inst #'[q ...]))] + [(~Prop/Or q ...) + #`(Prop/Or- #,@(stx-map inst #'[q ...]))] + [(~Prop/IndexType (quote- i:nat) τ) + (syntax-parse (list-ref arg-objs (syntax-e #'i)) + [(~NoObj) #`Prop/Top] + [obj #`(Prop/ObjType- obj τ)])] + [(~Prop/IndexNotType (quote- i:nat) τ) + (syntax-parse (list-ref arg-objs (syntax-e #'i)) + [(~NoObj) #`Prop/Top] + [obj #`(Prop/ObjNotType- obj τ)])] + [(~Prop/ObjType _ _) p] + [(~Prop/ObjNotType _ _) p])) + inst) + + ;; get-arg-obj : Stx -> ObjStx + (define (get-arg-obj stx) + ((current-type-eval) + (syntax-parse stx + [x:id #:do [(define x* (detach #'x 'orig-binding))] + #:when x* + ;; syntax-local-introduce ruins it + #`(IdObj- (quote-syntax- + #,(attach + (attach x* 'orig-id x*) + 'orig-type (typeof #'x))))] + [_ #'(NoObj-)]))) + + ;; prop->env : PropStx -> (Maybe (Listof (List Id Type))) + (define (prop->env p) + (define env + (prop->env/acc p (make-immutable-free-id-table))) + (and env (free-id-table-map env list))) + + ;; prop->env/acc : PropStx (FreeIdTableof Type) -> (Maybe (FreeIdTableof Type)) + (define (prop->env/acc p acc) + (syntax-parse (if (syntax-e p) p propProp/Top) + #:literals [quote-syntax-] + [(~Prop/And q ...) + (for/fold ([acc acc]) ([q (in-list (stx->list #'[q ...]))]) + #:break (false? acc) + (prop->env/acc q acc))] + [(~Prop/Or q) + #false] + [(~Prop/Or q ...) + (for/fold ([sub #false]) + ([q (in-list (stx->list #'[q ...]))]) + (occurrence-env-id-table-or + sub + (prop->env/acc q acc)))] + [(~Prop/ObjType o τ) + (syntax-parse #'o + #:literals [quote-syntax-] + [(~NoObj) acc] + [(~IdObj (quote-syntax- x:id)) + (define x* (syntax-local-introduce (detach #'x 'orig-id))) + (define τ_orig (free-id-table-ref acc x* (λ () (detach #'x 'orig-type)))) + (define τ_new (type-restrict τ_orig #'τ)) + (if (typecheck? τ_new typeCNothing) + #false + (free-id-table-set acc x* τ_new))])] + [(~Prop/ObjNotType o τ) + (syntax-parse #'o + #:literals [quote-syntax-] + [(~NoObj) acc] + [(~IdObj (quote-syntax- x:id)) + (define x* (syntax-local-introduce (detach #'x 'orig-id))) + (define τ_orig (free-id-table-ref acc x* (λ () (detach #'x 'orig-type)))) + (define τ_new (type-remove τ_orig #'τ)) + (if (typecheck? τ_new typeCNothing) + #false + (free-id-table-set acc x* τ_new))])])) + + ;; type-restrict : Type Type -> Type + (define (type-restrict orig new) + (cond [(types-no-overlap? orig new) typeCNothing] + [(typecheck? new orig) new] + [(Un? new) + ((current-type-eval) + (syntax-parse new + [(~CU* n ...) + #`(CU #,@(for/list ([n (in-list (stx->list #'[n ...]))]) + (type-restrict orig n)))] + [(~U* n ...) + (define ns* + (for/list ([n (in-list (stx->list #'[n ...]))]) + (type-restrict orig n))) + (cond + [(and (concrete? orig) (andmap concrete? ns*)) + #`(CU #,@ns*)] + [else + #`(U #,@ns*)])]))] + [(Term*? new) + (syntax-parse new + [(~Term* n) + (define n* (type-restrict orig #'n)) + (cond + [(concrete? orig) n*] + [else ((current-type-eval) #`(Term #,n*))])])] + [(Un? orig) + ((current-type-eval) + (syntax-parse orig + [(~CU* o ...) + #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) + (type-restrict o new)))] + [(~U* o ...) + ;; TODO: What does a U type mean, and can we safely reduce + ;; cases within U types? + (define os* + (for/list ([o (in-list (stx->list #'[o ...]))]) + (type-restrict o new))) + (cond + [(and (concrete? new) (andmap concrete? os*)) + #`(CU #,@os*)] + [else + #`(U #,@os*)])]))] + [(Term*? orig) + (syntax-parse orig + [(~Term* o) + (define o* (type-restrict #'o new)) + (cond + [(concrete? new) o*] + [else ((current-type-eval) #`(Term #,o*))])])] + [else + (syntax-parse (list orig new) + #:literals [quote-syntax-] + [[(~Struct (quote-syntax- sa:typed-struct-id) τa ...) + (~Struct (quote-syntax- sb:typed-struct-id) τb ...)] + #:when (and (free-identifier=? #'sa #'sb) + (not (attribute sa.some-mutable?))) + #:with [τab ...] (stx-map type-restrict #'[τa ...] #'[τb ...]) + ((current-type-eval) #'(Struct sa τab ...))] + [_ + (printf "refine-type:\n orig: ~a\n new: ~a\n" + (type->str orig) + (type->str new)) + new])])) + + ;; type-remove : Type Type -> Type + (define (type-remove orig new-not) + (cond [(typecheck? orig new-not) typeCNothing] + [(Un? orig) + ((current-type-eval) + (syntax-parse orig + [(~CU* o ...) + #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) + (type-remove o new-not)))] + [(~U* o ...) + ;; TODO: What does a U type mean, and can we safely remove + ;; from cases of U types? + (define os* + (for/list ([o (in-list (stx->list #'[o ...]))]) + (type-remove o new-not))) + #`(U #,@os*)]))] + [(Term*? orig) + (syntax-parse orig + [(~Term* o) + (define o* (type-remove #'o new-not)) + ((current-type-eval) #`(Term #,o*))])] + [(types-no-overlap? orig new-not) + orig] + [else + ;; Probably nothing more we can do in the current system + orig])) + + ;; types-no-overlap? : Type Type -> Bool + (define (types-no-overlap? a b) + (syntax-parse (list a b) + #:literals [quote-syntax-] + [[~CPosInt + (~or ~CZero ~CNegInt ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CZero + (~or ~CPosInt ~CNegInt ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CNegInt + (~or ~CPosInt ~CZero ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CString + (~or ~CPosInt ~CZero ~CNegInt ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CTrue + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CFalse (~Struct _ _ ...))] + #true] + [[~CFalse + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CTrue (~Struct _ _ ...))] + #true] + [[(~Struct _ _ ...) + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CTrue ~CFalse)] + #true] + [[(~Struct (quote-syntax- sa:id) _ ...) + (~Struct (quote-syntax- sb:id) _ ...)] + (structs-no-overlap? #'sa #'sb)] + [else #false])) + + ;; structs-no-overlap? : StructId StructId -> Bool + (define (structs-no-overlap? a b) + (syntax-parse (list a b) + [[sa:typed-struct-id sb:typed-struct-id] + (cond + [(free-identifier=? #'sa #'sb) #false] + [(and (attribute sa.no-super?) + (attribute sb.no-super?)) + #true] + [(attribute sa.no-super?) + (structs-no-overlap? #'sa #'sb.super-id)] + [(attribute sb.no-super?) + (structs-no-overlap? #'sa.super-id #'sb)] + [else + (structs-no-overlap? #'sa.super-id #'sb.super-id)])])) + + ;; sub-struct? : StructId StructId -> Bool + (define (sub-struct? a b) + (syntax-parse (list a b) + [[sa:typed-struct-id sb:typed-struct-id] + (cond + [(free-identifier=? #'sa #'sb) #true] + [(attribute sa.no-super?) #false] + [else + (sub-struct? #'sa.super-id #'sb)])])) + + ;; occurrence-env-id-table-or : + ;; (Maybe (FreeIdTableof Type)) (Maybe (FreeIdTableof Type)) -> (Maybe (FreeIdTableof Type)) + ;; Combines two possible occurrence-typing type environments with or. + ;; This means we don't know which environment will be true, so the result + ;; will only include identifiers that are included in both environments, + ;; with the types that are a union of the associated types in both. + (define (occurrence-env-id-table-or a b) + (cond [(false? a) b] + [(false? b) a] + [else + (for/fold ([a a]) + ([(id τ_b) (in-free-id-table b)]) + (cond + [(dict-has-key? a id) + (free-id-table-update + a + id + (λ (τ_a) (type-or τ_a τ_b)))] + [else + (free-id-table-remove a id)]))])) + + ;; type-or : Type Type -> Type + (define (type-or a b) + (cond [(and (concrete? a) (concrete? b)) + ((current-type-eval) #`(CU #,a #,b))] + [else + ((current-type-eval) #`(U #,a #,b))])) + + (define-syntax-class occurrence-env + #:attributes [[x 1] [τ 1] bottom?] + [pattern #false + #:attr bottom? #true + #:with [[x τ] ...] #'[]] + [pattern [[x τ] ...] + #:attr bottom? #false]) + ) + +;; (with-occurrence-env occurrence-env expr) +(define-typed-syntax with-occurrence-env + [(_ #false body:expr) ≫ + #:with DEAD (syntax/loc #'body + (ro:assert #false "this should be dead code")) + -------- + [⊢ DEAD (⇒ : CNothing) (⇒ prop+ Prop/Bot) (⇒ prop- Prop/Bot)]] + [(_ ([x:id τ:expr] ...) body:expr) ⇐ τ_body ≫ + #:do [(define scope + (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] + #:with [x* ...] (scope #'[x ...]) + [[x* ≫ x- : τ] ... ⊢ body ≫ body- ⇐ τ_body] + -------- + [⊢ (let- ([x- x] ...) body-)]] + [(_ ([x:id τ:type] ...) body:expr) ≫ + #:do [(define scope + (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] + #:with [x* ...] (scope #'[x ...]) + [[x* ≫ x- : τ] ... ⊢ body ≫ body- + (⇒ : τ_body) + (⇒ prop+ p+) + (⇒ prop- p-)] + -------- + [⊢ (let- ([x- x] ...) body-) + (⇒ : τ_body) + (⇒ prop+ (Prop p+)) + (⇒ prop- (Prop p-))]]) + +;; (with-occurrence-prop prop expr) +(define-syntax-parser with-occurrence-prop + [(_ prop:expr body:expr) + #:with env:occurrence-env + (prop->env (expand/df (if (syntax-e #'prop) #'prop #'Prop/Top))) + #'(with-occurrence-env env body)]) + +;; --------------------------------------------------------- + ;; Subtyping (begin-for-syntax @@ -673,9 +1162,11 @@ ;; (printf "t2 = ~a\n" (syntax->datum t2)) (or (Any? t2) - (and (concrete/recur? t1) (CAny? t2)) + (and (concrete/shallow-recur? t1) (CAny? t2)) + (and (concrete/recur? t1) (CAnyDeep? t2)) ((current-type=?) t1 t2) (syntax-parse (list t1 t2) + #:literals [quote-syntax-] ;; Constant clause must appear before U, ow (Const Int) <: Int wont hold [((~Constant* ty1) (~Constant* ty2)) (typecheck? #'ty1 #'ty2)] @@ -694,7 +1185,7 @@ [((~CList . tys) (~CListof ty)) (for/and ([t (stx->list #'tys)]) (typecheck? t #'ty))] - ;; vectors, only immutable vectors are invariant + ;; vectors, only immutable vectors are covariant [((~CIVectorof ty1) (~CIVectorof ty2)) (typecheck? #'ty1 #'ty2)] [((~CIBoxof ty1) (~CIBoxof ty2)) @@ -702,6 +1193,14 @@ [((~CPair ty1a ty1b) (~CPair ty2a ty2b)) (and (typecheck? #'ty1a #'ty2a) (typecheck? #'ty1b #'ty2b))] + ;; structs, if they are immutable, they are covariant + [((~Struct (quote-syntax- sa:typed-struct-id) τa ...) + (~Struct (quote-syntax- sb:typed-struct-id) τb ...)) + #:when (sub-struct? #'sa #'sb) + #:when (and (not (attribute sa.some-mutable?)) + (not (attribute sb.some-mutable?))) + (define n (stx-length #'[τb ...])) + (typechecks? (take (stx->list #'[τa ...]) n) #'[τb ...])] ; 2 U types, subtype = subset [((~CU* . ts1) _) (for/and ([t (stx->list #'ts1)]) @@ -728,13 +1227,45 @@ [((~Ccase-> . ts1) _) (for/or ([t (stx->list #'ts1)]) (typecheck? t t2))] - [((~C→ s1 ... s2) (~C→ t1 ... t2)) + [((~C→ s1 ... s2 : #:+ sp+ #:- sp-) + (~C→ t1 ... t2 : #:+ tp+ #:- tp-)) (and (typechecks? #'(t1 ...) #'(s1 ...)) - (typecheck? #'s2 #'t2))] + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] + [((~C→* [s1 ...] [] #:rest srst s2 : #:+ sp+ #:- sp-) + (~C→* [t1 ...] [] t2 : #:+ tp+ #:- tp-)) + (define sn (stx-length #'[s1 ...])) + (define-values [t1ns t1rs] + (split-at (stx->list #'[t1 ...]) sn)) + (define t1r ((current-type-eval) #`(CList #,@t1rs))) + (and (typechecks? t1ns #'(s1 ...)) + (typecheck? t1r #'srst) + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] + [((~C→* [s1 ...] [] #:rest srst s2 : #:+ sp+ #:- sp-) + (~C→* [t1 ...] [] #:rest trst t2 : #:+ tp+ #:- tp-)) + (and (typechecks? #'(t1 ...) #'(s1 ...)) + (typecheck? #'trst #'srst) + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] [_ #f]))) (current-sub? sub?) (current-typecheck-relation sub?) (define (subs? τs1 τs2) (and (stx-length=? τs1 τs2) - (stx-andmap (current-sub?) τs1 τs2)))) + (stx-andmap (current-sub?) τs1 τs2))) + + (define (prop-implies? p1 p2) + (syntax-parse (list p1 p2) + ;; anything implies true + [[_ (~Prop/And)] #true] + ;; false implies anything + [[(~Prop/Or) _] #false] + [[_ _] + (cond [(type=? p1 p2) #true] + [else #false])])) + ) diff --git a/typed/rosette/vector.rkt b/typed/rosette/vector.rkt new file mode 100644 index 0000000..66e1635 --- /dev/null +++ b/typed/rosette/vector.rkt @@ -0,0 +1,99 @@ +#lang turnstile + +(require typed/rosette/types + (prefix-in ro: rosette) + (postfix-in - rosette)) + +;; ------------------------------------------------------------------------ + +(provide (typed-out [vector? : LiftedPred])) + +(provide vector vector-immutable make-vector vector-ref vector-set!) + +;; mutable constructor +(define-typed-syntax vector + [(_ e:expr ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + #:with τ* (type-merge* + (stx-map type-merge #'[τ ...] #'[τ ...])) + -------- + [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CMVectorof (U τ*))]]]) + +;; immutable constructor +(define-typed-syntax vector-immutable + [(_ e:expr ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) + #'(CIVectorof (CU τ ...)) + #'(CIVectorof (U τ ...)))]]]) + +(define-typed-syntax make-vector + [(_ size:expr v:expr) ≫ + [⊢ size ≫ size- ⇐ CNat] + [⊢ v ≫ v- ⇒ τ] + -------- + [⊢ (ro:make-vector size- v-) ⇒ (CMVectorof τ)]]) + +(define-typed-syntax vector-ref + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] + [⊢ [i ≫ i- ⇐ : CInt]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : τ]]] + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] + [⊢ [i ≫ i- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : #,(type-merge #'τ #'τ)]]] + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~U* (~and (~or (~CMVectorof τ) (~CIVectorof τ))) ...)]] + [⊢ [i ≫ i- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : #,(type-merge* #'[τ ...])]]]) + +(define-typed-syntax vector-set! + [(_ v:expr i:expr x:expr) ≫ + [⊢ v ≫ v- ⇒ (~CMVectorof τ)] + [⊢ i ≫ i- ⇐ Nat] + [⊢ x ≫ x- ⇐ τ] + -------- + [⊢ (ro:vector-set! v- i- x-) ⇒ CUnit]]) + +;; ------------------------------------------------------------------------ + +(provide vector->list list->vector) + +(define-typed-syntax vector->list + [(_ v:expr) ≫ + [⊢ v ≫ v- ⇒ (~CMVectorof τ)] + -------- + [⊢ (ro:vector->list v-) ⇒ (CListof τ)]]) + +;; TODO: add CList case? +;; returne mutable vector +(define-typed-syntax list->vector + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:list->vector ⇒ : (Ccase-> (C→ (CListof Any) (CMVectorof Any)) + (C→ (Listof Any) (MVectorof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof #,(if (concrete? #'τ) #'(U τ) #'τ))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + #:with [τ* ...] (stx-map (λ (τ) (if (concrete? τ) #`(U #,τ) τ)) #'[τ ...]) + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVectorof τ*) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof (U τ ...))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVector (U τ ...)) ...)]]]) + +;; ------------------------------------------------------------------------ +