From 530c17ff3236566b025533b7c7a75b215a289177 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Mon, 13 May 2019 15:35:38 -0400 Subject: [PATCH] split out core-expressions with #%app, which is now more explicit --- racket/typed/core-expressions.rkt | 206 ++++++++++++++++ racket/typed/core-types.rkt | 361 ++++++++++++++------------- racket/typed/for-loops.rkt | 64 +++-- racket/typed/hash.rkt | 2 +- racket/typed/list.rkt | 4 +- racket/typed/prim.rkt | 12 +- racket/typed/roles.rkt | 393 +----------------------------- racket/typed/set.rkt | 46 +--- racket/typed/tests/for-loops.rkt | 17 ++ racket/typed/tests/sets.rkt | 22 ++ 10 files changed, 519 insertions(+), 608 deletions(-) create mode 100644 racket/typed/core-expressions.rkt create mode 100644 racket/typed/tests/sets.rkt diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt new file mode 100644 index 0000000..348d049 --- /dev/null +++ b/racket/typed/core-expressions.rkt @@ -0,0 +1,206 @@ +#lang turnstile + +(provide ann + if + when + unless + let + let* + cond + match + tuple + select + (for-syntax (all-defined-out))) + +(require "core-types.rkt") +(require (only-in "prim.rkt" Bool #%datum)) +(require (postfix-in - racket/match)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Core-ish forms +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; copied from stlc +(define-typed-syntax (ann e (~optional (~datum :)) τ:type) ≫ + [⊢ e ≫ e- (⇐ : τ.norm)] + #:fail-unless (pure? #'e-) "expression must be pure" + ------------------------------------------------ + [⊢ e- (⇒ : τ.norm) ]) + +;; copied from ext-stlc +(define-typed-syntax if + [(_ e_tst e1 e2) ⇐ τ-expected ≫ + [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. + #:fail-unless (pure? #'e_tst-) "expression must be pure" + [⊢ e1 ≫ e1- (⇐ : τ-expected) + (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))] + [⊢ e2 ≫ e2- (⇐ : τ-expected) + (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))] + -------- + [⊢ (if- e_tst- e1- e2-) + (⇒ : τ-expected) + (⇒ ν-ep (eps1 ... eps2 ...)) + (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) + (⇒ ν-s (ss1 ... ss2 ...))]] + [(_ e_tst e1 e2) ≫ + [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. + #:fail-unless (pure? #'e_tst-) "expression must be pure" + [⊢ e1 ≫ e1- (⇒ : τ1) + (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))] + [⊢ e2 ≫ e2- (⇒ : τ2) + (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))] + #:with τ (type-eval #'(U τ1 τ2)) + -------- + [⊢ (if- e_tst- e1- e2-) (⇒ : τ) + (⇒ ν-ep (eps1 ... eps2 ...)) + (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) + (⇒ ν-s (ss1 ... ss2 ...))]]) + +(define-typed-syntax (when e s ...+) ≫ + ------------------------------------ + [≻ (if e (begin s ...) #f)]) + +(define-typed-syntax (unless e s ...+) ≫ + ------------------------------------ + [≻ (if e #f (begin s ...))]) + +;; copied from ext-stlc +(define-typed-syntax let + [(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫ + [⊢ e ≫ e- ⇒ : τ_x] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" + [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected) + (⇒ ν-ep (~effs eps ...)) + (⇒ ν-f (~effs fs ...)) + (⇒ ν-s (~effs ss ...))] + ---------------------------------------------------------- + [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_expected) + (⇒ ν-ep (eps ...)) + (⇒ ν-f (fs ...)) + (⇒ ν-s (ss ...))]] + [(_ ([x e] ...) e_body ...) ≫ + [⊢ e ≫ e- ⇒ : τ_x] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" + [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body) + (⇒ ν-ep (~effs eps ...)) + (⇒ ν-f (~effs fs ...)) + (⇒ ν-s (~effs ss ...))] + ---------------------------------------------------------- + [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body) + (⇒ ν-ep (eps ...)) + (⇒ ν-f (fs ...)) + (⇒ ν-s (ss ...))]]) + +;; copied from ext-stlc +(define-typed-syntax let* + [(_ () e_body ...) ≫ + -------- + [≻ (begin e_body ...)]] + [(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫ + -------- + [≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) + +(define-typed-syntax (cond [pred:expr s ...+] ...+) ≫ + [⊢ pred ≫ pred- (⇐ : Bool)] ... + #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure" + [⊢ (begin s ...) ≫ s- (⇒ : τ-s) + (⇒ ν-ep (~effs eps ...)) + (⇒ ν-f (~effs fs ...)) + (⇒ ν-s (~effs ss ...))] ... + ------------------------------------------------ + [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...)) + (⇒ ν-ep (eps ... ...)) + (⇒ ν-f #,(make-Branch #'((fs ...) ...))) + (⇒ ν-s (ss ... ...))]) + +(define-typed-syntax (match e [p s ...+] ...+) ≫ + [⊢ e ≫ e- (⇒ : τ-e)] + #:fail-unless (pure? #'e-) "expression must be pure" + #:with (([x τ] ...) ...) (stx-map pat-bindings #'(p ...)) + [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s) + (⇒ ν-ep (~effs eps ...)) + (⇒ ν-f (~effs fs ...)) + (⇒ ν-s (~effs ss ...))] ... + ;; REALLY not sure how to handle p/p-/p.match-pattern, + ;; particularly w.r.t. typed terms that appear in p.match-pattern + [⊢ p ≫ p-- ⇒ τ-p] ... + #:fail-unless (project-safe? #'τ-e (type-eval #'(U τ-p ...))) "possibly unsafe pattern match" + #:fail-unless (stx-andmap pure? #'(p-- ...)) "patterns must be pure" + #:with (p- ...) (stx-map (lambda (p x-s xs) (substs x-s xs (compile-match-pattern p))) + #'(p ...) + #'((x- ...) ...) + #'((x ...) ...)) + -------------------------------------------------------------- + [⊢ (match- e- [p- s-] ... + [_ (#%app- error "incomplete pattern match")]) + (⇒ : (U τ-s ...)) + (⇒ ν-ep (eps ... ...)) + (⇒ ν-f #,(make-Branch #'((fs ...) ...))) + (⇒ ν-s (ss ... ...))]) + +(define-typed-syntax (tuple e:expr ...) ≫ + [⊢ e ≫ e- (⇒ : τ)] ... + #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects" + ----------------------- + [⊢ (#%app- list- 'tuple e- ...) (⇒ : (Tuple τ ...))]) + +(define-typed-syntax (select n:nat e:expr) ≫ + [⊢ e ≫ e- (⇒ : (~Tuple τ ...))] + #:fail-unless (pure? #'e-) "expression not allowed to have effects" + #:do [(define i (syntax->datum #'n))] + #:fail-unless (< i (stx-length #'(τ ...))) "index out of range" + #:with τr (list-ref (stx->list #'(τ ...)) i) + -------------------------------------------------------------- + [⊢ (#%app- tuple-select n e-) (⇒ : τr)]) + +(define- (tuple-select n t) + (#%app- list-ref- t (#%app- add1- n))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Helpers +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; pat -> ([Id Type] ...) +(define-for-syntax (pat-bindings stx) + (syntax-parse stx + #:datum-literals (bind tuple) + [(bind x:id τ:type) + #'([x τ])] + [(tuple p ...) + #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) + #'([x τ] ... ...)] + [(k:kons1 p) + (pat-bindings #'p)] + [(~constructor-exp cons p ...) + #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) + #'([x τ] ... ...)] + [_ + #'()])) + +;; TODO - figure out why this needs different list identifiers +(define-for-syntax (compile-pattern pat list-binding bind-id-transformer exp-transformer) + (define (l-e stx) (local-expand stx 'expression '())) + (let loop ([pat pat]) + (syntax-parse pat + #:datum-literals (tuple discard bind) + [(tuple p ...) + #`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))] + [(k:kons1 p) + #`(#,(kons1->constructor #'k) #,(loop #'p))] + [(bind x:id τ:type) + (bind-id-transformer #'x)] + [discard + #'_] + [(~constructor-exp ctor p ...) + (define/with-syntax uctor (untyped-ctor #'ctor)) + #`(uctor #,@(stx-map loop #'(p ...)))] + [_ + ;; local expanding "expression-y" syntax allows variable references to transform + ;; according to the mappings set up by turnstile. + (exp-transformer (l-e pat))]))) + +(define-for-syntax (compile-match-pattern pat) + (compile-pattern pat + #'list + identity + (lambda (exp) #`(==- #,exp)))) diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt index 1ceb0b2..a1bd4df 100644 --- a/racket/typed/core-types.rkt +++ b/racket/typed/core-types.rkt @@ -10,6 +10,7 @@ (require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base)) (require (for-syntax turnstile/examples/util/filter-maximal)) +(require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) (require (for-syntax racket/struct-info)) (require macrotypes/postfix-in) (require (rename-in racket/math [exact-truncate exact-truncate-])) @@ -928,172 +929,6 @@ ;; spawned actor OK in specified dataspace (<: r spec)])) -(module+ test - (displayln "skipping commented for-syntax tests because it's slow") - #;(begin-for-syntax - ;; TESTS - (let () - ;; utils - (local-require syntax/parse/define - rackunit) - (define te type-eval) - (define-syntax-parser check-role-implements? - [(_ r1 r2) - (quasisyntax/loc this-syntax - (check-true (role-implements? (te #'r1) (te #'r2))))]) - (define-syntax-parser check-role-not-implements? - [(_ r1 r2) - (quasisyntax/loc this-syntax - (check-false (role-implements? (te #'r1) (te #'r2))))]) - ;; Name Related - (check-role-implements? (Role (x)) (Role (x))) - (check-role-implements? (Role (x)) (Role (y))) - ;; Assertion Related - (check-role-not-implements? (Role (x)) (Role (y) (Shares Int))) - (check-role-implements? (Role (x) (Shares Int)) (Role (y))) - (check-role-implements? (Role (x) (Shares Int)) (Role (y) (Shares Int))) - (check-role-implements? (Role (x) - (Shares Int) - (Shares String)) - (Role (y) - (Shares Int) - (Shares String))) - (check-role-implements? (Role (x) - (Shares String) - (Shares Int)) - (Role (y) - (Shares Int) - (Shares String))) - (check-role-not-implements? (Role (x) - (Shares Int)) - (Role (y) - (Shares Int) - (Shares String))) - ;; Reactions - (check-role-implements? (Role (x) - (Reacts (Know Int))) - (Role (y) - (Reacts (Know Int)))) - (check-role-implements? (Role (x) - (Reacts (Know Int)) - (Shares String)) - (Role (y) - (Reacts (Know Int)))) - (check-role-implements? (Role (x) - (Reacts (Know Int) - (Role (y) (Shares String)))) - (Role (y) - (Reacts (Know Int)))) - (check-role-not-implements? (Role (x)) - (Role (y) - (Reacts (Know Int)))) - (check-role-not-implements? (Role (x) - (Reacts (Know String))) - (Role (y) - (Reacts (Know Int)))) - ;; these two might need to be reconsidered - (check-role-not-implements? (Role (x) - (Shares (Observe ★/t))) - (Role (y) - (Reacts (Know Int)))) - (check-role-not-implements? (Role (x) - (Shares (Observe Int))) - (Role (y) - (Reacts (Know Int)))) - (check-role-implements? (Role (x) - (Reacts (Know Int) - (Role (x2) (Shares String)))) - (Role (y) - (Reacts (Know Int) - (Role (y2) (Shares String))))) - (check-role-implements? (Role (x) - (Reacts (¬Know Int) - (Role (x2) (Shares String)))) - (Role (y) - (Reacts (¬Know Int) - (Role (y2) (Shares String))))) - (check-role-implements? (Role (x) - (Reacts OnStart - (Role (x2) (Shares String)))) - (Role (y) - (Reacts OnStart - (Role (y2) (Shares String))))) - (check-role-implements? (Role (x) - (Reacts OnStop - (Role (x2) (Shares String)))) - (Role (y) - (Reacts OnStop - (Role (y2) (Shares String))))) - (check-role-implements? (Role (x) - (Reacts OnDataflow - (Role (x2) (Shares String)))) - (Role (y) - (Reacts OnDataflow - (Role (y2) (Shares String))))) - (check-role-not-implements? (Role (x) - (Reacts (Know Int) - (Role (x2) (Shares String)))) - (Role (y) - (Reacts (Know Int) - (Role (y2) (Shares String)) - (Role (y3) (Shares Int))))) - (check-role-implements? (Role (x) - (Reacts (Know Int) - (Role (x3) (Shares Int)) - (Role (x2) (Shares String)))) - (Role (y) - (Reacts (Know Int) - (Role (y2) (Shares String)) - (Role (y3) (Shares Int))))) - ;; also not sure about this one - (check-role-implements? (Role (x) - (Reacts (Know Int) - (Role (x2) - (Shares String) - (Shares Int)))) - (Role (y) - (Reacts (Know Int) - (Role (y2) (Shares String)) - (Role (y3) (Shares Int))))) - ;; Stop - ;; these all error when trying to create the Stop type :< -#| - (check-role-implements? (Role (x) - (Reacts OnStart (Stop x))) - (Role (x) - (Reacts OnStart (Stop x)))) - (check-role-implements? (Role (x) - (Reacts OnStart (Stop x))) - (Role (y) - (Reacts OnStart (Stop y)))) - (check-role-implements? (Role (x) - (Reacts OnStart (Stop x (Role (x2) (Shares Int))))) - (Role (y) - (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) - (check-role-not-implements? (Role (x) - (Reacts OnStart (Stop x (Role (x2) (Shares String))))) - (Role (y) - (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) - (check-role-not-implements? (Role (x) - (Reacts OnStart)) - (Role (y) - (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) -|# - ;; Spawning Actors - (check-role-implements? (Role (x) - (Reacts OnStart (Actor Int))) - (Role (x) - (Reacts OnStart (Actor Int)))) - (check-role-implements? (Role (x) - (Reacts OnStart (Actor Int))) - (Role (x) - (Reacts OnStart (Actor (U Int String))))) - (check-role-not-implements? (Role (x) - (Reacts OnStart (Actor Bool))) - (Role (x) - (Reacts OnStart (Actor (U Int String))))) - ))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Effect Checking ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -1327,3 +1162,197 @@ (⇒ ν-ep (#,@ep-effs)) (⇒ ν-f (#,@f-effs)) (⇒ ν-s (#,@s-effs))]]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Sequencing & Definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-typed-syntax #%app + ;; Polymorphic, Pure Function - Perform Local Inference + [(_ e_fn e_arg ...) ≫ + ;; compute fn type (ie ∀ and →) + [⊢ e_fn ≫ e_fn- ⇒ (~∀ Xs (~→fn tyX_in ... tyX_out))] + ;; successfully matched a polymorphic fn type, don't backtrack + #:cut + #:with tyX_args #'(tyX_in ... tyX_out) + ;; solve for type variables Xs + #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax) + ;; instantiate polymorphic function type + #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) + #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) + ;; arity check + #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) + ;; purity check + #:fail-unless (all-pure? #'(e_fn- e_arg- ...)) "expressions must be pure" + ;; compute argument types + #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...)) + ;; typecheck args + [τ_arg τ⊑ τ_in #:for e_arg] ... + #:with τ_out* (if (stx-null? #'(unsolved-X ...)) + #'τ_out + (syntax-parse #'τ_out + [(~?∀ (Y ...) τ_out) + #:fail-unless (→? #'τ_out) + (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) + (for ([X (in-list (syntax->list #'(unsolved-X ...)))]) + (unless (covariant-X? X #'τ_out) + (raise-syntax-error + #f + (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) + this-syntax))) + (mk-∀- #'(unsolved-X ... Y ...) #'(τ_out))])) + -------- + [⊢ (#%plain-app- e_fn- e_arg- ...) ⇒ τ_out*]] + ;; All Other Functions + [(_ e_fn e_arg ...) ≫ + [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in ... (~Computation (~Value τ-out) + (~Endpoints τ-ep ...) + (~Roles τ-f ...) + (~Spawns τ-s ...))))] + #:fail-unless (pure? #'e_fn-) "expression not allowed to have effects" + #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) + [⊢ e_arg ≫ e_arg- (⇐ : τ_in)] ... + #:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects" + ------------------------------------------------------------------------ + [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-out) + (⇒ ν-ep (τ-ep ...)) + (⇒ ν-s (τ-s ...)) + (⇒ ν-f (τ-f ...))]]) + +(begin-for-syntax + ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id) + ;; finds the free Xs in the type + (define (find-free-Xs Xs ty) + (for/list ([X (in-stx-list Xs)] + #:when (stx-contains-id? ty X)) + X)) + + ;; Type -> Bool + ;; checks if the type contains any unions + (define (contains-union? ty) + (syntax-parse ty + [(~U* _ ...) + #t] + [(~Base _) #f] + [X:id #f] + [(~Any/bvs _ _ τ ...) + (stx-ormap contains-union? #'(τ ...))] + [_ + (type-error #:src (get-orig ty) + #:msg "contains-union?: unrecognized-type: ~a" + ty)])) + + ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args + ;; stx = the application stx = (#%app e_fn e_arg ...) + ;; tyXs = input and output types from fn type + ;; ie (typeof e_fn) = (-> . tyXs) + ;; It infers the types of arguments from left-to-right, + ;; and it expands and returns all of the arguments. + ;; It returns list of 3 values if successful, else throws a type error + ;; - a list of all the arguments, expanded + ;; - a list of all the type variables + ;; - the constraints for substituting the types + (define (solve Xs tyXs stx) + (syntax-parse tyXs + [(τ_inX ... τ_outX) + ;; generate initial constraints with expected type and τ_outX + #:with (~?∀ Vs expected-ty) + (and (get-expected-type stx) + ((current-type-eval) (get-expected-type stx))) + (define initial-cs + (if (and (syntax-e #'expected-ty) (stx-null? #'Vs)) + (add-constraints Xs '() (list (list #'expected-ty #'τ_outX))) + '())) + (syntax-parse stx + [(_ e_fn . args) + (define-values (as- cs) + (for/fold ([as- null] [cs initial-cs]) + ([a (in-stx-list #'args)] + [tyXin (in-stx-list #'(τ_inX ...))]) + (define ty_in (inst-type/cs/orig Xs cs tyXin datum=?)) + (when (contains-union? ty_in) + (type-error #:src a + #:msg (format "can't infer types with unions: ~a\nraw: ~a" + (type->str ty_in) ty_in))) + (define/with-syntax [a- ty_a] + (infer+erase (if (null? (find-free-Xs Xs ty_in)) + (add-expected-type a ty_in) + a))) + (when (contains-union? #'ty_a) + (type-error #:src a + #:msg (format "can't infer types with unions: ~a\nraw: ~a" + (type->str #'ty_a) #'ty_a))) + (values + (cons #'a- as-) + (add-constraints Xs cs (list (list ty_in #'ty_a)) + (list (list (inst-type/cs/orig + Xs cs ty_in + datum=?) + #'ty_a)))))) + + (list (reverse as-) Xs cs)])])) + + (define (mk-app-poly-infer-error stx expected-tys given-tys e_fn) + (format (string-append + "Could not infer instantiation of polymorphic function ~s.\n" + " expected: ~a\n" + " given: ~a") + (syntax->datum (get-orig e_fn)) + (string-join (stx-map type->str expected-tys) ", ") + (string-join (stx-map type->str given-tys) ", "))) + + ;; covariant-Xs? : Type -> Bool + ;; Takes a possibly polymorphic type, and returns true if all of the + ;; type variables are in covariant positions within the type, false + ;; otherwise. + (define (covariant-Xs? ty) + (syntax-parse ((current-type-eval) ty) + [(~?∀ Xs ty) + (for/and ([X (in-stx-list #'Xs)]) + (covariant-X? X #'ty))])) + + ;; find-X-variance : Id Type [Variance] -> Variance + ;; Returns the variance of X within the type ty + (define (find-X-variance X ty [ctxt-variance covariant]) + (car (find-variances (list X) ty ctxt-variance))) + + ;; covariant-X? : Id Type -> Bool + ;; Returns true if every place X appears in ty is a covariant position, false otherwise. + (define (covariant-X? X ty) + (variance-covariant? (find-X-variance X ty covariant))) + + ;; contravariant-X? : Id Type -> Bool + ;; Returns true if every place X appears in ty is a contravariant position, false otherwise. + (define (contravariant-X? X ty) + (variance-contravariant? (find-X-variance X ty covariant))) + + ;; find-variances : (Listof Id) Type [Variance] -> (Listof Variance) + ;; Returns the variances of each of the Xs within the type ty, + ;; where it's already within a context represented by ctxt-variance. + (define (find-variances Xs ty [ctxt-variance covariant]) + (syntax-parse ty + [A:id + (for/list ([X (in-list Xs)]) + (cond [(free-identifier=? X #'A) ctxt-variance] + [else irrelevant]))] + [(~Any tycons) + (stx-map (λ _ irrelevant) Xs)] + [(~?∀ () (~Any tycons τ ...)) + #:when (get-arg-variances #'tycons) + #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons)) + (define τ-ctxt-variances + (for/list ([arg-variance (in-list (get-arg-variances #'tycons))]) + (variance-compose ctxt-variance arg-variance))) + (for/fold ([acc (stx-map (λ _ irrelevant) Xs)]) + ([τ (in-stx-list #'[τ ...])] + [τ-ctxt-variance (in-list τ-ctxt-variances)]) + (map variance-join + acc + (find-variances Xs τ τ-ctxt-variance)))] + [ty + #:when (not (for/or ([X (in-list Xs)]) + (stx-contains-id? #'ty X))) + (stx-map (λ _ irrelevant) Xs)] + [_ (stx-map (λ _ invariant) Xs)]))) diff --git a/racket/typed/for-loops.rkt b/racket/typed/for-loops.rkt index e9eb022..4d39143 100644 --- a/racket/typed/for-loops.rkt +++ b/racket/typed/for-loops.rkt @@ -1,13 +1,21 @@ #lang turnstile -(provide for/fold) +(provide for/fold + for/list + for/set + for/sum) (require "core-types.rkt") (require "sequence.rkt") (require (only-in "list.rkt" List ~List)) (require (only-in "set.rkt" Set ~Set)) (require (only-in "hash.rkt" Hash ~Hash)) -(require (only-in "prim.rkt" Bool)) +(require (only-in "prim.rkt" Bool + #%datum)) +(require (only-in "core-expressions.rkt" let)) + +(require (postfix-in - (only-in racket/set + for/set + in-set))) (begin-for-syntax (define-splicing-syntax-class iter-clause @@ -120,20 +128,9 @@ (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs τ-f ...))] #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?) - ;; #:with y (stx-car #'(x ...)) - ;; #:with y- (stx-car #'(x- ...)) - ;; #:with y-- (stx-car #'(x-- ...)) - ;; #:with (_ (_ dbg1)) #'e-body- - ;; #:with (_ (_ dbg2)) #'e-body-- - ;; #:do [(printf "y/dbg1 ~a, ~a\n" (free-identifier=? #'y #'dbg1) (bound-identifier=? #'y #'dbg1)) - ;; (printf "y/dbg2 ~a, ~a\n" (free-identifier=? #'y #'dbg2) (bound-identifier=? #'y #'dbg2)) - ;; (printf "y-/dbg1 ~a, ~a\n" (free-identifier=? #'y- #'dbg1) (bound-identifier=? #'y- #'dbg1)) - ;; (printf "y-/dbg2 ~a, ~a\n" (free-identifier=? #'y- #'dbg2) (bound-identifier=? #'y- #'dbg2)) - ;; (printf "y--/dbg1 ~a, ~a\n" (free-identifier=? #'y-- #'dbg1) (bound-identifier=? #'y-- #'dbg1)) - ;; (printf "y--/dbg2 ~a, ~a\n" (free-identifier=? #'y-- #'dbg2) (bound-identifier=? #'y- #'dbg2))] ------------------------------------------------------- [⊢ (for/fold- ([acc- init-]) - (#,@#'clauses-) + clauses- e-body--) (⇒ : τ-acc) (⇒ ν-ep (τ-ep ...)) @@ -147,3 +144,42 @@ [≻ (for/fold ([acc τ-acc init]) clauses e-body ...)]]) + +(define-typed-syntax (for/list (clause:iter-clause ...) + e-body ...+) ≫ + #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...)) + [[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body- + (⇒ : τ-body) + (⇒ ν-ep (~effs τ-ep ...)) + (⇒ ν-s (~effs τ-s ...)) + (⇒ ν-f (~effs τ-f ...))] + #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?) + ---------------------------------------------------------------------- + [⊢ (for/list- clauses- + e-body--) (⇒ : (List τ-body)) + (⇒ ν-ep (τ-ep ...)) + (⇒ ν-s (τ-s ...)) + (⇒ ν-f (τ-f ...))]) + +(define-typed-syntax (for/set (clause:iter-clause ...) + e-body ...+) ≫ + #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...)) + [[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body- + (⇒ : τ-body) + (⇒ ν-ep (~effs τ-ep ...)) + (⇒ ν-s (~effs τ-s ...)) + (⇒ ν-f (~effs τ-f ...))] + #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?) + ---------------------------------------------------------------------- + [⊢ (for/set- clauses- + e-body--) (⇒ : (Set τ-body)) + (⇒ ν-ep (τ-ep ...)) + (⇒ ν-s (τ-s ...)) + (⇒ ν-f (τ-f ...))]) + +(define-typed-syntax (for/sum (clause ...) + e-body ...+) ≫ + ---------------------------------------------------------------------- + [≻ (for/fold ([acc 0]) + (clause ...) + (+ acc (let () e-body ...)))]) diff --git a/racket/typed/hash.rkt b/racket/typed/hash.rkt index 8433eb7..153fb12 100644 --- a/racket/typed/hash.rkt +++ b/racket/typed/hash.rkt @@ -42,7 +42,7 @@ #:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure" #:with together-again (stx-flatten #'((key- val-) ...)) -------------------------------------------------- - [⊢ (hash- #,@#'together-again) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))]) + [⊢ (#%app- hash- #,@#'together-again) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))]) (require/typed racket/base ;; don't have a type for ConsPair diff --git a/racket/typed/list.rkt b/racket/typed/list.rkt index 6728fed..7071b4c 100644 --- a/racket/typed/list.rkt +++ b/racket/typed/list.rkt @@ -24,7 +24,7 @@ [⊢ e ≫ e- ⇒ τ] ... #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" ------------------- - [⊢ (list- e- ...) ⇒ (List (U τ ...))]) + [⊢ (#%app- list- e- ...) ⇒ (List (U τ ...))]) (define- (member?- v l) - (and- (member- v l) #t)) + (and- (#%app- member- v l) #t)) diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt index 0a1b782..1ea499b 100644 --- a/racket/typed/prim.rkt +++ b/racket/typed/prim.rkt @@ -26,6 +26,8 @@ (define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns)))) (define-primop even? (→fn Int Bool)) (define-primop odd? (→fn Int Bool)) +(define-primop add1 (→fn Int Int)) +(define-primop sub1 (→fn Int Int)) (define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns)))) (define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns)))) @@ -39,7 +41,7 @@ #:fail-unless (pure? #'e1-) "expression not allowed to have effects" #:fail-unless (pure? #'e2-) "expression not allowed to have effects" ------------------------ - [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)]) + [⊢ (#%app- exact-truncate- (#%app- /- e1- e2-)) (⇒ : Int)]) ;; for some reason defining `and` as a prim op doesn't work (define-typed-syntax (and e ...) ≫ @@ -56,26 +58,26 @@ #:fail-unless (pure? #'e1-) "expression not allowed to have effects" #:fail-unless (pure? #'e2-) "expression not allowed to have effects" --------------------------------------------------------------------------- - [⊢ (equal?- e1- e2-) (⇒ : Bool)]) + [⊢ (#%app- equal?- e1- e2-) (⇒ : Bool)]) (define-typed-syntax (displayln e:expr) ≫ [⊢ e ≫ e- (⇒ : τ)] #:fail-unless (pure? #'e-) "expression not allowed to have effects" --------------- - [⊢ (displayln- e-) (⇒ : ★/t)]) + [⊢ (#%app- displayln- e-) (⇒ : ★/t)]) (define-typed-syntax (printf e ...+) ≫ [⊢ e ≫ e- (⇒ : τ)] ... #:fail-unless (stx-andmap pure? #'(e- ...)) "expression not allowed to have effects" --------------- - [⊢ (printf- e- ...) (⇒ : ★/t)]) + [⊢ (#%app- printf- e- ...) (⇒ : ★/t)]) (define-typed-syntax (~a e ...) ≫ [⊢ e ≫ e- (⇒ : τ)] ... #:fail-unless (stx-andmap flat-type? #'(τ ...)) "expressions must be string-able" -------------------------------------------------- - [⊢ (~a- e- ...) (⇒ : String)]) + [⊢ (#%app- ~a- e- ...) (⇒ : String)]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Basic Values diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 42cfb5d..d15e7a4 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -1,7 +1,7 @@ #lang turnstile (provide #%module-begin - (rename-out [typed-app #%app]) + #%app (rename-out [typed-quote quote]) #%top-interaction require only-in @@ -11,7 +11,7 @@ Tuple Bind Discard → ∀ Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop FacetName Field ★/t - Observe Inbound Outbound Actor U + Observe Inbound Outbound Actor U ⊥ Computation Value Endpoints Roles Spawns →fn ;; Statements @@ -33,6 +33,8 @@ bind discard ;; primitives (all-from-out "prim.rkt") + ;; expressions + (all-from-out "core-expressions.rkt") ;; lists (all-from-out "list.rkt") ;; sets @@ -54,6 +56,7 @@ require-struct ) (require "core-types.rkt") +(require "core-expressions.rkt") (require "list.rkt") (require "set.rkt") (require "prim.rkt") @@ -64,13 +67,9 @@ (require (prefix-in syndicate: syndicate/actor-lang)) (require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base)) -(require (for-syntax turnstile/examples/util/filter-maximal)) -(require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) -(require (for-syntax racket/struct-info)) (require macrotypes/postfix-in) (require (postfix-in - racket/list)) (require (postfix-in - racket/set)) -(require (postfix-in - racket/match)) (module+ test (require rackunit) @@ -104,7 +103,7 @@ ;; τ-m ... τ-r ...)) -------------------------------------------------------------- - [⊢ (syndicate:react (let- ([#,name-- (syndicate:current-facet-id)]) + [⊢ (syndicate:react (let- ([#,name-- (#%app- syndicate:current-facet-id)]) #,@ep-...)) (⇒ : ★/t) (⇒ ν-f (τ))]) @@ -203,57 +202,12 @@ (⇒ : ★/t) (⇒ ν-ep (τ-r))]) -;; pat -> ([Id Type] ...) -(define-for-syntax (pat-bindings stx) - (syntax-parse stx - #:datum-literals (bind tuple) - [(bind x:id τ:type) - #'([x τ])] - [(tuple p ...) - #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) - #'([x τ] ... ...)] - [(k:kons1 p) - (pat-bindings #'p)] - [(~constructor-exp cons p ...) - #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) - #'([x τ] ... ...)] - [_ - #'()])) - -;; TODO - figure out why this needs different list identifiers -(define-for-syntax (compile-pattern pat list-binding bind-id-transformer exp-transformer) - (define (l-e stx) (local-expand stx 'expression '())) - (let loop ([pat pat]) - (syntax-parse pat - #:datum-literals (tuple discard bind) - [(tuple p ...) - #`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))] - [(k:kons1 p) - #`(#,(kons1->constructor #'k) #,(loop #'p))] - [(bind x:id τ:type) - (bind-id-transformer #'x)] - [discard - #'_] - [(~constructor-exp ctor p ...) - (define/with-syntax uctor (untyped-ctor #'ctor)) - #`(uctor #,@(stx-map loop #'(p ...)))] - [_ - ;; local expanding "expression-y" syntax allows variable references to transform - ;; according to the mappings set up by turnstile. - (exp-transformer (l-e pat))]))) - (define-for-syntax (compile-syndicate-pattern pat) (compile-pattern pat #'list- (lambda (id) #`($ #,id)) identity)) -(define-for-syntax (compile-match-pattern pat) - (compile-pattern pat - #'list - identity - (lambda (exp) #`(==- #,exp)))) - (define-typed-syntax (spawn τ-c:type s) ≫ #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order" ;; TODO: check that each τ-f is a Role @@ -292,7 +246,7 @@ [⊢ x ≫ x- (⇒ : (~Field τ-x:type))] #:fail-unless (<: #'τ #'τ-x) "Ill-typed field write" ---------------------------------------------------- - [⊢ (x- e-) (⇒ : ★/t)]) + [⊢ (#%app- x- e-) (⇒ : ★/t)]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Derived Forms @@ -356,215 +310,7 @@ (define-typed-syntax (ref x:id) ≫ [⊢ x ≫ x- ⇒ (~Field τ)] ------------------------ - [⊢ (x-) (⇒ : τ)]) - -(define-typed-syntax typed-app - ;; Polymorphic, Pure Function - Perform Local Inference - [(_ e_fn e_arg ...) ≫ - ;; compute fn type (ie ∀ and →) - [⊢ e_fn ≫ e_fn- ⇒ (~∀ Xs (~→fn tyX_in ... tyX_out))] - ;; successfully matched a polymorphic fn type, don't backtrack - #:cut - #:with tyX_args #'(tyX_in ... tyX_out) - ;; solve for type variables Xs - #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax) - ;; instantiate polymorphic function type - #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) - #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) - ;; arity check - #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) - (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) - ;; purity check - #:fail-unless (all-pure? #'(e_fn- e_arg- ...)) "expressions must be pure" - ;; compute argument types - #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...)) - ;; typecheck args - [τ_arg τ⊑ τ_in #:for e_arg] ... - #:with τ_out* (if (stx-null? #'(unsolved-X ...)) - #'τ_out - (syntax-parse #'τ_out - [(~?∀ (Y ...) τ_out) - #:fail-unless (→? #'τ_out) - (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) - (for ([X (in-list (syntax->list #'(unsolved-X ...)))]) - (unless (covariant-X? X #'τ_out) - (raise-syntax-error - #f - (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn) - this-syntax))) - (mk-∀- #'(unsolved-X ... Y ...) #'(τ_out))])) - -------- - [⊢ (#%plain-app- e_fn- e_arg- ...) ⇒ τ_out*]] - ;; All Other Functions - [(_ e_fn e_arg ...) ≫ - [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in ... (~Computation (~Value τ-out) - (~Endpoints τ-ep ...) - (~Roles τ-f ...) - (~Spawns τ-s ...))))] - #:fail-unless (pure? #'e_fn-) "expression not allowed to have effects" - #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) - (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) - [⊢ e_arg ≫ e_arg- (⇐ : τ_in)] ... - #:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects" - ------------------------------------------------------------------------ - [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-out) - (⇒ ν-ep (τ-ep ...)) - (⇒ ν-s (τ-s ...)) - (⇒ ν-f (τ-f ...))]]) - -(begin-for-syntax - ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id) - ;; finds the free Xs in the type - (define (find-free-Xs Xs ty) - (for/list ([X (in-stx-list Xs)] - #:when (stx-contains-id? ty X)) - X)) - - ;; Type -> Bool - ;; checks if the type contains any unions - (define (contains-union? ty) - (syntax-parse ty - [(~U* _ ...) - #t] - [(~Base _) #f] - [X:id #f] - [(~Any/bvs _ _ τ ...) - (stx-ormap contains-union? #'(τ ...))] - [_ - (type-error #:src (get-orig ty) - #:msg "contains-union?: unrecognized-type: ~a" - ty)])) - - ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args - ;; stx = the application stx = (#%app e_fn e_arg ...) - ;; tyXs = input and output types from fn type - ;; ie (typeof e_fn) = (-> . tyXs) - ;; It infers the types of arguments from left-to-right, - ;; and it expands and returns all of the arguments. - ;; It returns list of 3 values if successful, else throws a type error - ;; - a list of all the arguments, expanded - ;; - a list of all the type variables - ;; - the constraints for substituting the types - (define (solve Xs tyXs stx) - (syntax-parse tyXs - [(τ_inX ... τ_outX) - ;; generate initial constraints with expected type and τ_outX - #:with (~?∀ Vs expected-ty) - (and (get-expected-type stx) - ((current-type-eval) (get-expected-type stx))) - (define initial-cs - (if (and (syntax-e #'expected-ty) (stx-null? #'Vs)) - (add-constraints Xs '() (list (list #'expected-ty #'τ_outX))) - '())) - (syntax-parse stx - [(_ e_fn . args) - (define-values (as- cs) - (for/fold ([as- null] [cs initial-cs]) - ([a (in-stx-list #'args)] - [tyXin (in-stx-list #'(τ_inX ...))]) - (define ty_in (inst-type/cs/orig Xs cs tyXin datum=?)) - (when (contains-union? ty_in) - (type-error #:src a - #:msg (format "can't infer types with unions: ~a\nraw: ~a" - (type->str ty_in) ty_in))) - (define/with-syntax [a- ty_a] - (infer+erase (if (null? (find-free-Xs Xs ty_in)) - (add-expected-type a ty_in) - a))) - (when (contains-union? #'ty_a) - (type-error #:src a - #:msg (format "can't infer types with unions: ~a\nraw: ~a" - (type->str #'ty_a) #'ty_a))) - (values - (cons #'a- as-) - (add-constraints Xs cs (list (list ty_in #'ty_a)) - (list (list (inst-type/cs/orig - Xs cs ty_in - datum=?) - #'ty_a)))))) - - (list (reverse as-) Xs cs)])])) - - (define (mk-app-poly-infer-error stx expected-tys given-tys e_fn) - (format (string-append - "Could not infer instantiation of polymorphic function ~s.\n" - " expected: ~a\n" - " given: ~a") - (syntax->datum (get-orig e_fn)) - (string-join (stx-map type->str expected-tys) ", ") - (string-join (stx-map type->str given-tys) ", "))) - - ;; covariant-Xs? : Type -> Bool - ;; Takes a possibly polymorphic type, and returns true if all of the - ;; type variables are in covariant positions within the type, false - ;; otherwise. - (define (covariant-Xs? ty) - (syntax-parse ((current-type-eval) ty) - [(~?∀ Xs ty) - (for/and ([X (in-stx-list #'Xs)]) - (covariant-X? X #'ty))])) - - ;; find-X-variance : Id Type [Variance] -> Variance - ;; Returns the variance of X within the type ty - (define (find-X-variance X ty [ctxt-variance covariant]) - (car (find-variances (list X) ty ctxt-variance))) - - ;; covariant-X? : Id Type -> Bool - ;; Returns true if every place X appears in ty is a covariant position, false otherwise. - (define (covariant-X? X ty) - (variance-covariant? (find-X-variance X ty covariant))) - - ;; contravariant-X? : Id Type -> Bool - ;; Returns true if every place X appears in ty is a contravariant position, false otherwise. - (define (contravariant-X? X ty) - (variance-contravariant? (find-X-variance X ty covariant))) - - ;; find-variances : (Listof Id) Type [Variance] -> (Listof Variance) - ;; Returns the variances of each of the Xs within the type ty, - ;; where it's already within a context represented by ctxt-variance. - (define (find-variances Xs ty [ctxt-variance covariant]) - (syntax-parse ty - [A:id - (for/list ([X (in-list Xs)]) - (cond [(free-identifier=? X #'A) ctxt-variance] - [else irrelevant]))] - [(~Any tycons) - (stx-map (λ _ irrelevant) Xs)] - [(~?∀ () (~Any tycons τ ...)) - #:when (get-arg-variances #'tycons) - #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons)) - (define τ-ctxt-variances - (for/list ([arg-variance (in-list (get-arg-variances #'tycons))]) - (variance-compose ctxt-variance arg-variance))) - (for/fold ([acc (stx-map (λ _ irrelevant) Xs)]) - ([τ (in-stx-list #'[τ ...])] - [τ-ctxt-variance (in-list τ-ctxt-variances)]) - (map variance-join - acc - (find-variances Xs τ τ-ctxt-variance)))] - [ty - #:when (not (for/or ([X (in-list Xs)]) - (stx-contains-id? #'ty X))) - (stx-map (λ _ irrelevant) Xs)] - [_ (stx-map (λ _ invariant) Xs)]))) - -(define-typed-syntax (tuple e:expr ...) ≫ - [⊢ e ≫ e- (⇒ : τ)] ... - #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects" - ----------------------- - [⊢ (list- 'tuple e- ...) (⇒ : (Tuple τ ...))]) - -(define-typed-syntax (select n:nat e:expr) ≫ - [⊢ e ≫ e- (⇒ : (~Tuple τ ...))] - #:fail-unless (pure? #'e-) "expression not allowed to have effects" - #:do [(define i (syntax->datum #'n))] - #:fail-unless (< i (stx-length #'(τ ...))) "index out of range" - #:with τr (list-ref (stx->list #'(τ ...)) i) - -------------------------------------------------------------- - [⊢ (tuple-select n e-) (⇒ : τr)]) - -(define- (tuple-select n t) - (list-ref- t (add1 n))) + [⊢ (#%app- x-) (⇒ : τ)]) ;; it would be nice to abstract over these three (define-typed-syntax (observe e:expr) ≫ @@ -604,127 +350,6 @@ -------------------- [⊢ (error- 'discard "escaped") (⇒ : Discard)]]) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Core-ish forms -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; copied from stlc -(define-typed-syntax (ann e (~optional (~datum :)) τ:type) ≫ - [⊢ e ≫ e- (⇐ : τ.norm)] - #:fail-unless (pure? #'e-) "expression must be pure" - ------------------------------------------------ - [⊢ e- (⇒ : τ.norm) ]) - -;; copied from ext-stlc -(define-typed-syntax if - [(_ e_tst e1 e2) ⇐ τ-expected ≫ - [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. - #:fail-unless (pure? #'e_tst-) "expression must be pure" - [⊢ e1 ≫ e1- (⇐ : τ-expected) - (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))] - [⊢ e2 ≫ e2- (⇐ : τ-expected) - (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))] - -------- - [⊢ (if- e_tst- e1- e2-) - (⇒ ν-ep (eps1 ... eps2 ...)) - (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) - (⇒ ν-s (ss1 ... ss2 ...))]] - [(_ e_tst e1 e2) ≫ - [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. - #:fail-unless (pure? #'e_tst-) "expression must be pure" - [⊢ e1 ≫ e1- (⇒ : τ1) - (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))] - [⊢ e2 ≫ e2- (⇒ : τ2) - (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))] - #:with τ (type-eval #'(U τ1 τ2)) - -------- - [⊢ (if- e_tst- e1- e2-) (⇒ : τ) - (⇒ ν-ep (eps1 ... eps2 ...)) - (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) - (⇒ ν-s (ss1 ... ss2 ...))]]) - -(define-typed-syntax (when e s ...+) ≫ - ------------------------------------ - [≻ (if e (begin s ...) #f)]) - -(define-typed-syntax (unless e s ...+) ≫ - ------------------------------------ - [≻ (if e #f (begin s ...))]) - -;; copied from ext-stlc -(define-typed-syntax let - [(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫ - [⊢ e ≫ e- ⇒ : τ_x] ... - #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" - [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected) - (⇒ ν-ep (~effs eps ...)) - (⇒ ν-f (~effs fs ...)) - (⇒ ν-s (~effs ss ...))] - ---------------------------------------------------------- - [⊢ (let- ([x- e-] ...) e_body-) - (⇒ ν-ep (eps ...)) - (⇒ ν-f (fs ...)) - (⇒ ν-s (ss ...))]] - [(_ ([x e] ...) e_body ...) ≫ - [⊢ e ≫ e- ⇒ : τ_x] ... - #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure" - [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body) - (⇒ ν-ep (~effs eps ...)) - (⇒ ν-f (~effs fs ...)) - (⇒ ν-s (~effs ss ...))] - ---------------------------------------------------------- - [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body) - (⇒ ν-ep (eps ...)) - (⇒ ν-f (fs ...)) - (⇒ ν-s (ss ...))]]) - -;; copied from ext-stlc -(define-typed-syntax let* - [(_ () e_body ...) ≫ - -------- - [≻ (begin e_body ...)]] - [(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫ - -------- - [≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) - -(define-typed-syntax (cond [pred:expr s ...+] ...+) ≫ - [⊢ pred ≫ pred- (⇐ : Bool)] ... - #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure" - [⊢ (begin s ...) ≫ s- (⇒ : τ-s) - (⇒ ν-ep (~effs eps ...)) - (⇒ ν-f (~effs fs ...)) - (⇒ ν-s (~effs ss ...))] ... - ------------------------------------------------ - [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...)) - (⇒ ν-ep (eps ... ...)) - (⇒ ν-f #,(make-Branch #'((fs ...) ...))) - (⇒ ν-s (ss ... ...))]) - -(define-typed-syntax (match e [p s ...+] ...+) ≫ - [⊢ e ≫ e- (⇒ : τ-e)] - #:fail-unless (pure? #'e-) "expression must be pure" - #:with (([x τ] ...) ...) (stx-map pat-bindings #'(p ...)) - [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s) - (⇒ ν-ep (~effs eps ...)) - (⇒ ν-f (~effs fs ...)) - (⇒ ν-s (~effs ss ...))] ... - ;; REALLY not sure how to handle p/p-/p.match-pattern, - ;; particularly w.r.t. typed terms that appear in p.match-pattern - [⊢ p ≫ p-- ⇒ τ-p] ... - #:fail-unless (project-safe? #'τ-e (type-eval #'(U τ-p ...))) "possibly unsafe pattern match" - #:fail-unless (stx-andmap pure? #'(p-- ...)) "patterns must be pure" - #:with (p- ...) (stx-map (lambda (p x-s xs) (substs x-s xs (compile-match-pattern p))) - #'(p ...) - #'((x- ...) ...) - #'((x ...) ...)) - -------------------------------------------------------------- - [⊢ (match- e- [p- s-] ... - [_ (error "incomplete pattern match")]) - (⇒ : (U τ-s ...)) - (⇒ ν-ep (eps ... ...)) - (⇒ ν-f #,(make-Branch #'((fs ...) ...))) - (⇒ ν-s (ss ... ...))]) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Ground Dataspace ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -734,7 +359,7 @@ (define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫ [⊢ (dataspace τ-c s ...) ≫ ((~literal erased) ((~literal syndicate:dataspace) s- ...)) (⇒ : t)] ----------------------------------------------------------------------------------- - [⊢ (syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))]) + [⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/set.rkt b/racket/typed/set.rkt index 3bfc84b..a911c1a 100644 --- a/racket/typed/set.rkt +++ b/racket/typed/set.rkt @@ -19,11 +19,6 @@ (require (postfix-in - racket/set)) -(module+ test - (require rackunit) - (require rackunit/turnstile) - ) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Sets ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -34,13 +29,13 @@ [⊢ e ≫ e- ⇒ τ] ... #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" --------------- - [⊢ (set- e- ...) ⇒ (Set (U τ ...))]) + [⊢ (#%app- set- e- ...) ⇒ (Set (U τ ...))]) (define-typed-syntax (set-count e) ≫ [⊢ e ≫ e- ⇒ (~Set _)] #:fail-unless (pure? #'e-) "expression must be pure" ---------------------- - [⊢ (set-count- e-) ⇒ Int]) + [⊢ (#%app- set-count- e-) ⇒ Int]) (define-typed-syntax (set-add st v) ≫ [⊢ st ≫ st- ⇒ (~Set τs)] @@ -48,7 +43,7 @@ [⊢ v ≫ v- ⇒ τv] #:fail-unless (pure? #'v-) "expression must be pure" ------------------------- - [⊢ (set-add- st- v-) ⇒ (Set (U τs τv))]) + [⊢ (#%app- set-add- st- v-) ⇒ (Set (U τs τv))]) (define-typed-syntax (set-remove st v) ≫ [⊢ st ≫ st- ⇒ (~Set τs)] @@ -56,7 +51,7 @@ [⊢ v ≫ v- ⇐ τs] #:fail-unless (pure? #'v-) "expression must be pure" ------------------------- - [⊢ (set-remove- st- v-) ⇒ (Set τs)]) + [⊢ (#%app- set-remove- st- v-) ⇒ (Set τs)]) (define-typed-syntax (set-member? st v) ≫ [⊢ st ≫ st- ⇒ (~Set τs)] @@ -66,7 +61,7 @@ #:fail-unless (<: #'τv #'τs) "type mismatch" ------------------------------------- - [⊢ (set-member?- st- v-) ⇒ Bool]) + [⊢ (#%app- set-member?- st- v-) ⇒ Bool]) (define-typed-syntax (set-union st0 st ...) ≫ [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] @@ -74,7 +69,7 @@ [⊢ st ≫ st- ⇒ (~Set τ-st)] ... #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" ------------------------------------- - [⊢ (set-union- st0- st- ...) ⇒ (Set (U τ-st0 τ-st ...))]) + [⊢ (#%app- set-union- st0- st- ...) ⇒ (Set (U τ-st0 τ-st ...))]) (define-typed-syntax (set-intersect st0 st ...) ≫ [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] @@ -83,7 +78,7 @@ #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" #:with τr (∩ #'τ-st0 (type-eval #'(U τ-st ...))) ------------------------------------- - [⊢ (set-intersect- st0- st- ...) ⇒ (Set τr)]) + [⊢ (#%app- set-intersect- st0- st- ...) ⇒ (Set τr)]) (define-typed-syntax (set-subtract st0 st ...) ≫ [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] @@ -91,37 +86,16 @@ [⊢ st ≫ st- ⇒ (~Set _)] ... #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" ------------------------------------- - [⊢ (set-subtract- st0- st- ...) ⇒ (Set τ-st0)]) + [⊢ (#%app- set-subtract- st0- st- ...) ⇒ (Set τ-st0)]) (define-typed-syntax (list->set l) ≫ [⊢ l ≫ l- ⇒ (~List τ)] #:fail-unless (pure? #'l-) "expression must be pure" ----------------------- - [⊢ (list->set- l-) ⇒ (Set τ)]) + [⊢ (#%app- list->set- l-) ⇒ (Set τ)]) (define-typed-syntax (set->list s) ≫ [⊢ s ≫ s- ⇒ (~Set τ)] #:fail-unless (pure? #'s-) "expression must be pure" ----------------------- - [⊢ (set->list- s-) ⇒ (List τ)]) - -(module+ test - (require "prim.rkt") - (check-type (set 1 2 3) - : (Set Int) - -> (set- 2 3 1)) - (check-type (set 1 "hello" 3) - : (Set (U Int String)) - -> (set- "hello" 3 1)) - (check-type (set-count (set 1 "hello" 3)) - : Int - -> 3) - (check-type (set-union (set 1 2 3) (set "hello" "world")) - : (Set (U Int String)) - -> (set- 1 2 3 "hello" "world")) - (check-type (set-intersect (set 1 2 3) (set "hello" "world")) - : (Set ⊥) - -> (set-)) - (check-type (set-intersect (set 1 "hello" 3) (set #t "world" #f "hello")) - : (Set String) - -> (set- "hello"))) + [⊢ (#%app- set->list- s-) ⇒ (List τ)]) diff --git a/racket/typed/tests/for-loops.rkt b/racket/typed/tests/for-loops.rkt index d7793b7..8332877 100644 --- a/racket/typed/tests/for-loops.rkt +++ b/racket/typed/tests/for-loops.rkt @@ -71,3 +71,20 @@ (check-type (zip-even (list 1 2 3) (list 5 6 7)) : (List (Tuple Int Int)) ⇒ (list (tuple 2 6))) + +(check-type (for/list ([x (list 1 2 3 4 5 6)] + #:when (even? x)) + (add1 x)) + : (List Int) + ⇒ (list 3 5 7)) + +(check-type (for/set ([x (set 1 2 3 4 5 6)] + #:when (even? x)) + (add1 x)) + : (Set Int) + ⇒ (set 5 3 7)) + +(check-type (for/sum ([x (set 8 7 2)]) + (* x 2)) + : Int + ⇒ 34) diff --git a/racket/typed/tests/sets.rkt b/racket/typed/tests/sets.rkt new file mode 100644 index 0000000..ecd89e1 --- /dev/null +++ b/racket/typed/tests/sets.rkt @@ -0,0 +1,22 @@ +#lang typed/syndicate/roles + +(require rackunit/turnstile) + +(check-type (set 1 2 3) + : (Set Int) + -> (set 2 3 1)) +(check-type (set 1 "hello" 3) + : (Set (U Int String)) + -> (set "hello" 3 1)) +(check-type (set-count (set 1 "hello" 3)) + : Int + -> 3) +(check-type (set-union (set 1 2 3) (set "hello" "world")) + : (Set (U Int String)) + -> (set 1 2 3 "hello" "world")) +(check-type (set-intersect (set 1 2 3) (set "hello" "world")) + : (Set ⊥) + -> (set)) +(check-type (set-intersect (set 1 "hello" 3) (set #t "world" #f "hello")) + : (Set String) + -> (set "hello"))