From 3c800a92db03280673016a9fc11a59b6b7cb48d4 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Fri, 26 Apr 2019 15:16:08 -0400 Subject: [PATCH] split out files --- racket/typed/core-types.rkt | 1245 +++++++++++++++++++++++++++++++ racket/typed/list.rkt | 98 +++ racket/typed/roles.rkt | 1409 +---------------------------------- racket/typed/set.rkt | 124 +++ 4 files changed, 1473 insertions(+), 1403 deletions(-) create mode 100644 racket/typed/core-types.rkt create mode 100644 racket/typed/list.rkt create mode 100644 racket/typed/set.rkt diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt new file mode 100644 index 0000000..150ea9c --- /dev/null +++ b/racket/typed/core-types.rkt @@ -0,0 +1,1245 @@ +#lang turnstile + +(provide (all-defined-out) + (for-syntax (all-defined-out)) + (for-meta 2 (all-defined-out))) +(require (only-in turnstile + [define-type-constructor define-type-constructor-])) + +(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 racket/struct-info)) +(require macrotypes/postfix-in) +(require (rename-in racket/math [exact-truncate exact-truncate-])) +(require (postfix-in - racket/list)) +(require (postfix-in - racket/set)) +(require (postfix-in - racket/match)) +(require (postfix-in - (only-in racket/format ~a))) + + +(module+ test + (require rackunit) + (require rackunit/turnstile)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Type Checking Conventions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; : describes the immediate result of evaluation +;; ν-ep key aggregates endpoint affects: +;; `Shares`, `Reacts`, and `MakesField` +;; Note thar MakesField is only an effect, not a type +;; ν-f key aggregates facet effects (starting/stopping a facet) as `Role`s & `Stop`s and message sends, `Sends` +;; ν-s key aggregates spawned actors as `Actor`s + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Types +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; certain metadata needs to be associated with each type, for the purpose of +;; making certain judgments and metafunctions extensible. + +;; a isect-desc describes how a type (constructor) behaves with respect to +;; intersection, and is one of +;; - BASE +;; - CONTAINER-LIKE +;; - PRODUCT-LIKE +(begin-for-syntax + (define BASE 'base) + (define CONTAINER-LIKE 'container-like) + (define PRODUCT-LIKE 'product-like) + + ;; syntax property key + (define isect-desc-key + 'isect-desc-key) + + (define-syntax-class isect-desc + #:attributes (val) + #:datum-literals (BASE CONTAINER-LIKE PRODUCT-LIKE) + (pattern BASE + #:attr val BASE) + (pattern CONTAINER-LIKE + #:attr val CONTAINER-LIKE) + (pattern PRODUCT-LIKE + #:attr val PRODUCT-LIKE)) + + ;; Any -> Bool + ;; recognize isect-descs + (define (isect-desc? x) + (member x (list BASE CONTAINER-LIKE PRODUCT-LIKE))) + + ;; syntax property key + ;; syntax-transformer value + (define type-cons-key + 'type-cons) + + ;; Type -> Bool + ;; check if the type has a syntax property allowing us to create new instances + (define (reassemblable? t) + (and (syntax-property t type-cons-key) #t)) + + ;; Type (Listof Type) -> Type + ;; Create a new instance of the type with the given arguments + ;; needs to have the type-cons-key + (define (reassemble-type ty args) + (define tycons (syntax-property ty type-cons-key)) + (unless tycons + (error "expected to find type-cons-key")) + (type-eval #`(#,tycons #,@args)))) + +(define-syntax (define-type-constructor+ stx) + (syntax-parse stx + [(_ Name:id + #:arity op arity + #:arg-variances variances + #:isect-desc desc:isect-desc + (~optional (~seq #:extra-info extra-info))) + #:with Name- (mk-- #'Name) + #:with NamePat (mk-~ #'Name) + #:with NamePat- (mk-~ #'Name-) + #:with mk (format-id #'Name "mk-~a-" (syntax-e #'Name)) + #:with mk- (format-id #'Name- "mk-~a-" (syntax-e #'Name-)) + (quasisyntax/loc stx + (begin- + (define-type-constructor- Name- + #:arity op arity + #:arg-variances variances + #,@(if (attribute extra-info) + #'(#:extra-info extra-info) + #'())) + (define-syntax (Name stx) + (syntax-parse stx + [(_ t (... ...)) + (set-stx-prop/preserved + (set-stx-prop/preserved + (syntax/loc stx + (Name- t (... ...))) + #,isect-desc-key + '#,(attribute desc.val)) + type-cons-key + #'Name)])) + (begin-for-syntax + (define-syntax NamePat + (pattern-expander + (syntax-parser + [(_ p (... ...)) + #'(NamePat- p (... ...))])))) + (define-for-syntax mk mk-)))])) + +(begin-for-syntax + ;; Syntax -> (Listof Variant) + ;; make a list of the same length as the number of arguments of the given + ;; (type) syntax, all covariant + (define (mk-covariant ts) + (for/list ([_ (sequence-tail (in-syntax ts) 1)]) + covariant))) + +;; Define a type constructor that acts like a container: +;; - covariant +;; - has an empty element (i.e. intersection always non-empty) +(define-syntax (define-container-type stx) + (syntax-parse stx + [(_ Name:id #:arity op arity + (~optional (~seq #:extra-info extra-info))) + (quasisyntax/loc stx + (define-type-constructor+ Name + #:arity op arity + #:arg-variances mk-covariant + #:isect-desc CONTAINER-LIKE + #,@(if (attribute extra-info) + #'(#:extra-info extra-info) + #'())))])) + +;; Define a type constructor that acts like a container: +;; - covariant +;; - does not have an empty element (i.e. intersection may be empty) +(define-syntax (define-product-type stx) + (syntax-parse stx + [(_ Name:id #:arity op arity + (~optional (~seq #:extra-info extra-info))) + (quasisyntax/loc stx + (define-type-constructor+ Name + #:arity op arity + #:arg-variances mk-covariant + #:isect-desc PRODUCT-LIKE + #,@(if (attribute extra-info) + #'(#:extra-info extra-info) + #'())))])) + +(define-binding-type Role #:arity >= 0 #:bvs = 1) +(define-type-constructor Shares #:arity = 1) +(define-type-constructor Sends #:arity = 1) +(define-type-constructor Reacts #:arity >= 1) +(define-type-constructor Know #:arity = 1) +(define-type-constructor ¬Know #:arity = 1) +(define-type-constructor Stop #:arity >= 1) +(define-type-constructor Field #:arity = 1) +(define-type-constructor Bind #:arity = 1) +;; keep track of branches for facet effects +;; (Branch (Listof (Listof Type))) +(define-type-constructor Branch #:arity >= 0) +;; sequence of effects +(define-type-constructor Effs #:arity >= 0) +(define-base-types OnStart OnStop OnDataflow MakesField) +(define-for-syntax field-prop-name 'fields) +(define-type-constructor Actor #:arity = 1) + +(define-product-type Message #:arity = 1) +(define-product-type Tuple #:arity >= 0) +(define-product-type Observe #:arity = 1) +(define-product-type Inbound #:arity = 1) +(define-product-type Outbound #:arity = 1) +(define-container-type AssertionSet #:arity = 1) +(define-container-type Patch #:arity = 2) + +(define-type-constructor → #:arity > 0) +;; for describing the RHS +;; a value and a description of the effects +(define-type-constructor Computation #:arity = 4) +(define-type-constructor Value #:arity = 1) +(define-type-constructor Endpoints #:arity >= 0) +(define-type-constructor Roles #:arity >= 0) +(define-type-constructor Spawns #:arity >= 0) + + +(define-base-types Int Bool String Discard ★/t FacetName ByteString Symbol) + +(define-for-syntax (type-eval t) + ((current-type-eval) t)) + +(define-type-constructor U* #:arity >= 0) + +;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file. +;; however, this version expands the type at every reference, incurring a potentially large +;; overhead---2x in the case of book-club.rkt +;; (copied from ext-stlc example) +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ) + #'(define-syntax- alias + (make-variable-like-transformer #'τ))] + [(_ (f:id x:id ...) ty) + #'(define-syntax- (f stx) + (syntax-parse stx + [(_ x ...) + #:with τ:any-type #'ty + #'τ.norm]))])) + +(define-type-alias ⊥ (U*)) + +(define-for-syntax (prune+sort tys) + (stx-sort + (filter-maximal + (stx->list tys) + typecheck?))) + +(define-syntax (U stx) + (syntax-parse stx + [(_ . tys) + ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys + #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys) + #:with tys- (prune+sort #'(ty1- ... ... ty2- ...)) + (if (= 1 (stx-length #'tys-)) + (stx-car #'tys-) + (syntax/loc stx (U* . tys-)))])) + +;; for looking at the "effects" +(begin-for-syntax + (define-syntax ~effs + (pattern-expander + (syntax-parser + [(_ eff:id ...) + #:with tmp (generate-temporary 'effss) + #'(~and tmp + (~parse (eff ...) (stx-or #'tmp #'())))]))) + + (define (stx-truth? a) + (and a (not (and (syntax? a) (false? (syntax-e a)))))) + (define (stx-or a b) + (cond [(stx-truth? a) a] + [else b]))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Defined Types, aka Constructors +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(begin-for-syntax + (define-splicing-syntax-class type-constructor-decl + (pattern (~seq #:type-constructor TypeCons:id)) + (pattern (~seq) #:attr TypeCons #f)) + + (struct user-ctor (typed-ctor untyped-ctor) + #:property prop:procedure + (lambda (v stx) + (define transformer (user-ctor-typed-ctor v)) + (syntax-parse stx + [(_ e ...) + (quasisyntax/loc stx + (#,transformer e ...))])))) + +(define-syntax (define-constructor* stx) + (syntax-parse stx + #:datum-literals (:) + [(_ (Cons:id : TyCons:id slot:id ...) clause ...) + #'(define-constructor (Cons slot ...) + #:type-constructor TyCons + clause ...)])) + +(define-syntax (define-constructor stx) + (syntax-parse stx + [(_ (Cons:id slot:id ...) + ty-cons:type-constructor-decl + (~seq #:with + Alias AliasBody) ...) + #:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons))) + #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons) + #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons) + #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons) + #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons) + #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons)) + (define arity (stx-length #'(slot ...))) + #`(begin- + (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent) + (define-syntax (TypeConsExtraInfo stx) + (syntax-parse stx + [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) + (define-product-type TypeCons + #:arity = #,arity + #:extra-info 'TypeConsExtraInfo) + (define-syntax (MakeTypeCons stx) + (syntax-parse stx + [(_ t (... ...)) + #:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch" + #'(TypeCons t (... ...))])) + (define-syntax (GetTypeParams stx) + (syntax-parse stx + [(_ (TypeConsExpander t (... ...))) + #'(t (... ...))])) + (define-syntax Cons + (user-ctor #'Cons- #'StructName)) + (define-typed-syntax (Cons- e (... ...)) ≫ + #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch" + [⊢ e ≫ e- (⇒ : τ)] (... ...) + #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure" + ---------------------- + [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))]) + (define-type-alias Alias AliasBody) ...)])) + +;; (require-struct chicken #:as Chicken #:from "some-mod.rkt") will +;; - extract the struct-info for chicken, and ensure that it is immutable, has a set number of fields +;; - determine the number of slots, N, chicken has +;; - define the type constructor (Chicken ...N), with the extra info used by define-constructor above +;; - define chicken+, a turnstile type rule that checks uses of chicken +;; - bind chicken to a user-ctor struct +;; TODO: this implementation shares a lot with that of define-constructor +(define-syntax (require-struct stx) + (syntax-parse stx + [(_ ucons:id #:as ty-cons:id #:from lib) + (with-syntax* ([TypeCons #'ty-cons] + [MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)] + [GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)] + [TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)] + [TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)] + [Cons- (format-id #'ucons "~a/checked" #'ucons)] + [orig-struct-info (generate-temporary #'ucons)] + [type-tag (generate-temporary #'ucons)]) + (quasisyntax/loc stx + (begin- + (require- (only-in- lib [ucons orig-struct-info])) + (begin-for-syntax + (define info (syntax-local-value #'orig-struct-info)) + (unless (struct-info? info) + (raise-syntax-error #f "expected struct" #'#,stx #'ucons)) + (match-define (list desc cons pred accs muts sup) (extract-struct-info info)) + (when (false? (last accs)) + (raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons)) + (unless (equal? #t sup) + (raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons)) + (define arity (length accs))) + (define-syntax (TypeConsExtraInfo stx) + (syntax-parse stx + [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) + (define-type-constructor TypeCons + ;; issue: arity needs to parse as an exact-nonnegative-integer + ;; fix: check arity in MakeTypeCons + #:arity >= 0 + #:extra-info 'TypeConsExtraInfo) + (define-syntax (MakeTypeCons stx) + (syntax-parse stx + [(_ t (... ...)) + #:fail-unless (= arity (stx-length #'(t (... ...)))) "arity mismatch" + #'(TypeCons t (... ...))])) + (define-syntax (GetTypeParams stx) + (syntax-parse stx + [(_ (TypeConsExpander t (... ...))) + #'(t (... ...))])) + (define-typed-syntax (Cons- e (... ...)) ≫ + #:fail-unless (= arity (stx-length #'(e (... ...)))) "arity mismatch" + [⊢ e ≫ e- (⇒ : τ)] (... ...) + #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure" + ---------------------- + [⊢ (#%app- orig-struct-info e- (... ...)) (⇒ : (TypeCons τ (... ...)))]) + (define-syntax ucons + (user-ctor #'Cons- #'orig-struct-info)))))])) + +(begin-for-syntax + (define-syntax ~constructor-extra-info + (pattern-expander + (syntax-parser + [(_ tag mk get) + #'(_ (_ tag) (_ mk) (_ get))]))) + + (define-syntax ~constructor-type + (pattern-expander + (syntax-parser + [(_ tag . rst) + #'(~and it + (~fail #:unless (user-defined-type? #'it)) + (~parse tag (get-type-tag #'it)) + (~Any _ . rst))]))) + + (define-syntax ~constructor-exp + (pattern-expander + (syntax-parser + [(_ cons . rst) + #'(~and (cons . rst) + (~fail #:unless (ctor-id? #'cons)))]))) + + (define (inspect t) + (syntax-parse t + [(~constructor-type tag t ...) + (list (syntax-e #'tag) (stx-map type->str #'(t ...)))])) + + (define (tags-equal? t1 t2) + (equal? (syntax-e t1) (syntax-e t2))) + + (define (user-defined-type? t) + (get-extra-info (type-eval t))) + + (define (get-type-tag t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info tag _ _) + (syntax-e #'tag)])) + + (define (get-type-args t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ _ get) + (define f (syntax-local-value #'get)) + (syntax->list (f #`(get #,t)))])) + + (define (make-cons-type t args) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ mk _) + (define f (syntax-local-value #'mk)) + (type-eval (f #`(mk #,@args)))])) + + (define (ctor-id? stx) + (and (identifier? stx) + (user-ctor? (syntax-local-value stx (const #f))))) + + (define (untyped-ctor stx) + (user-ctor-untyped-ctor (syntax-local-value stx (const #f))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Require & Provide +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Import and ascribe a type from an untyped module +;; TODO: this is where contracts would need to go +(define-syntax (require/typed stx) + (syntax-parse stx + #:datum-literals (:) + [(_ lib [name:id : ty:type] ...) + #:with (name- ...) (format-ids "~a-" #'(name ...)) + (syntax/loc stx + (begin- + (require (only-in lib [name name-] ...)) + (define-syntax name + (make-variable-like-transformer (add-orig (assign-type #'name- #'ty #:wrap? #f) #'name))) + ...))])) + +;; Format identifiers in the same way +;; FormatString (SyntaxListOf Identifier) -> (Listof Identifier) +(define-for-syntax (format-ids fmt ids) + (for/list ([id (in-syntax ids)]) + (format-id id fmt id))) + +;; (SyntaxListof (SyntaxList Identifier Type Identifier)) -> (Listof Identifier) +;; For each triple (name- ty name), +;; assign the ty to name- with the orig name +(define-for-syntax (assign-types los) + (for/list ([iti (in-syntax los)]) + (match-define (list name- ty name) (syntax->list iti)) + (add-orig (assign-type name- ty #:wrap? #f) name))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Conveniences +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; (SyntaxListof (SyntaxListof Type)) -> (U (SyntaxListof Branch) #'()) +(define-for-syntax (make-Branch tys*) + (syntax-parse tys* + [() + #'()] + [(() ...) + #'()] + [((ty ...) ...) + (define effs + (for/list ([tys (in-syntax tys*)]) + (mk-Effs- (syntax->list tys)))) + #`(#,(mk-Branch- effs))])) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Syntax +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(begin-for-syntax + + ;; constructors with arity one + (define-syntax-class kons1 + (pattern (~or (~datum observe) + (~datum inbound) + (~datum outbound) + (~datum message)))) + + (define (kons1->constructor stx) + (syntax-parse stx + #:datum-literals (observe inbound outbound) + [observe #'syndicate:observe] + [inbound #'syndicate:inbound] + [outbound #'syndicate:outbound] + [message #'syndicate:message])) + + (define-syntax-class basic-val + (pattern (~or boolean + integer + string))) + + (define-syntax-class prim-op + (pattern (~or (~literal +) + (~literal -) + (~literal displayln))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilities Over Types +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-for-syntax (bot? t) + ((current-typecheck-relation) t (type-eval #'(U*)))) + +(define-for-syntax (flat-type? τ) + (syntax-parse τ + [(~→ τ ...) #f] + [(~Actor τ) #f] + [_ #t])) + +(define-for-syntax (strip-? t) + (type-eval + (syntax-parse t + [(~U* τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] + [~★/t #'★/t] + ;; since (Observe X) can match (Message X): + ;; doing this specifically for the intersection operation in the spawn rule, need to check other + ;; uses + [(~Observe τ) #'(U τ (Message τ))] + [_ #'(U*)]))) + +;; similar to strip- fns, but leave non-message types as they are +(define-for-syntax (prune-message t) + (type-eval + (syntax-parse t + [(~U* τ ...) #`(U #,@(stx-map prune-message #'(τ ...)))] + [~★/t #'★/t] + [(~Message τ) #'τ] + [_ t]))) + +(define-for-syntax (strip-inbound t) + (type-eval + (syntax-parse t + [(~U* τ ...) #`(U #,@(stx-map strip-inbound #'(τ ...)))] + [~★/t #'★/t] + [(~Inbound τ) #'τ] + [_ #'(U*)]))) + +(define-for-syntax (strip-outbound t) + (type-eval + (syntax-parse t + [(~U* τ ...) #`(U #,@(stx-map strip-outbound #'(τ ...)))] + [~★/t #'★/t] + [(~Outbound τ) #'τ] + [_ #'(U*)]))) + +(define-for-syntax (relay-interests t) + (type-eval + (syntax-parse t + ;; TODO: probably need to `normalize` the result + [(~U* τ ...) #`(U #,@(stx-map relay-interests #'(τ ...)))] + [~★/t #'★/t] + [(~Observe (~Inbound τ)) #'(Observe τ)] + [_ #'(U*)]))) + +;; (SyntaxOf RoleType ...) -> (Syntaxof InputType OutputType SpawnType) +(define-for-syntax (analyze-roles rs) + (define-values (lis los lss) + (for/fold ([is '()] + [os '()] + [ss '()]) + ([r (in-syntax rs)]) + (define-values (i o s) (analyze-role-input/output r)) + (values (cons i is) (cons o os) (cons s ss)))) + #`(#,(type-eval #`(U #,@lis)) + #,(type-eval #`(U #,@los)) + #,(type-eval #`(U #,@lss)))) + +;; Wanted test case, but can't use it bc it uses things defined for-syntax +#;(module+ test + (let ([r (type-eval #'(Role (x) (Shares Int)))]) + (syntax-parse (analyze-role-input/output r) + [(τ-i τ-o) + (check-true (type=? #'τ-o (type-eval #'Int)))]))) + +;; RoleType -> (Values InputType OutputType SpawnType) +(define-for-syntax (analyze-role-input/output t) + (syntax-parse t + [(~Branch (~Effs τ-r ...) ...) + #:with (τi τo τa) (analyze-roles #'(τ-r ... ...)) + (values #'τi #'τo #'τa)] + [(~Stop name:id τ-r ...) + #:with (τi τo τa) (analyze-roles #'(τ-r ...)) + (values #'τi #'τo #'τa)] + [(~Actor τc) + (values (mk-U*- '()) (mk-U*- '()) t)] + [(~Sends τ-m) + (values (mk-U*- '()) (type-eval #'(Message τ-m)) (mk-U*- '()))] + [(~Role (name:id) + (~or (~Shares τ-s) + (~Sends τ-m) + (~Reacts τ-if τ-then ...)) ... + (~and (~Role _ ...) sub-role) ...) + (define-values (is os ss) + (for/fold ([ins '()] + [outs '()] + [spawns '()]) + ([t (in-syntax #'(τ-then ... ... sub-role ...))]) + (define-values (i o s) (analyze-role-input/output t)) + (values (cons i ins) (cons o outs) (cons s spawns)))) + (define pat-types (stx-map event-desc-type #'(τ-if ...))) + (values (type-eval #`(U #,@is #,@pat-types)) + (type-eval #`(U τ-s ... (Message τ-m) ... #,@os #,@(stx-map pattern-sub-type pat-types))) + (type-eval #`(U #,@ss)))])) + +;; EventDescriptorType -> Type +(define-for-syntax (event-desc-type desc) + (syntax-parse desc + [(~Know τ) #'τ] + [(~¬Know τ) #'τ] + [(~Message τ) desc] + [_ (type-eval #'(U*))])) + +;; PatternType -> Type +(define-for-syntax (pattern-sub-type pt) + (syntax-parse pt + [(~Message τ) + (define t (replace-bind-and-discard-with-★ #'τ)) + (type-eval #`(Observe #,t))] + [τ + (define t (replace-bind-and-discard-with-★ #'τ)) + (type-eval #`(Observe #,t))])) + +;; TODO : can potentially use something like `subst` for this +(define-for-syntax (replace-bind-and-discard-with-★ t) + (syntax-parse t + [(~Bind _) + (type-eval #'★/t)] + [~Discard + (type-eval #'★/t)] + [(~U* τ ...) + (type-eval #`(U #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))] + [(~Any/bvs τ-cons () τ ...) + #:when (reassemblable? t) + (define subitems (for/list ([t (in-syntax #'(τ ...))]) + (replace-bind-and-discard-with-★ t))) + (reassemble-type t subitems)] + [_ t])) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Subtyping and Judgments on Types +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(begin-for-syntax + (define-syntax ~Base + (pattern-expander + (syntax-parser + [(_ nm:id) + #'((~literal #%plain-app) nm)]))) + + ;; Type Type -> Bool + ;; subtyping + (define (<: t1 t2) + (syntax-parse #`(#,t1 #,t2) + [(_ ~★/t) + (flat-type? t1)] + [((~U* τ1 ...) _) + (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))] + [(_ (~U* τ2:type ...)) + (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))] + [((~Actor τ1) (~Actor τ2)) + (and (<: #'τ1 #'τ2) + (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))] + [((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2)) + #:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...)) + (and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...)) + (<: #'τ-out1 #'τ-out2))] + [(~Discard _) + #t] + [((~Base τ1:id) (~Base τ2:id)) + (free-identifier=? #'τ1 #'τ2)] + [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) + #:when (free-identifier=? #'τ-cons1 #'τ-cons2) + #:do [(define variances (syntax-property #'τ-cons1 'arg-variances))] + #:when variances + #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) + (for/and ([ty1 (in-syntax #'(τ1 ...))] + [ty2 (in-syntax #'(τ2 ...))] + [var (in-list variances)]) + (match var + [(== covariant) + (<: ty1 ty2)] + [(== contravariant) + (<: ty2 ty1)] + [(== invariant) + (and (<: ty1 ty2) + (<: ty2 ty1))] + [(== irrelevant) + #t]))] + ;; TODO: clauses for Roles, and so on + [_ #f])) + + ;; shortcuts for mapping + (define ((<:l l) r) + (<: l r)) + + (define ((<:r r) l) + (<: l r))) + +;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +;; MODIFYING GLOBAL TYPECHECKING STATE!!!!! +;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + +(begin-for-syntax + (current-typecheck-relation <:)) + +;; Flat-Type Flat-Type -> Type +(define-for-syntax (∩ t1 t2) + (unless (and (flat-type? t1) (flat-type? t2)) + (error '∩ "expected two flat-types")) + (syntax-parse #`(#,t1 #,t2) + [(_ ~★/t) + t1] + [(~★/t _) + t2] + [((~U* τ1:type ...) _) + (type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))] + [(_ (~U* τ2:type ...)) + (type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))] + [((~AssertionSet τ1) (~AssertionSet τ2)) + #:with τ12 (∩ #'τ1 #'τ2) + (type-eval #'(AssertionSet τ12))] + ;; Also, using <: is OK, even though <: refers to ∩, because <:'s use of ∩ is only + ;; in the Actor case. + [((~Base τ1:id) (~Base τ2:id)) + #:when (free-identifier=? #'τ1 #'τ2) + t1] + [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) + #:when (free-identifier=? #'τ-cons1 #'τ-cons2) + #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) + #:do [(define desc (syntax-property t1 isect-desc-key))] + #:when desc + (define slots (stx-map ∩ #'(τ1 ...) #'(τ2 ...))) + (match desc + [(== BASE) + (error "this isn't right")] + [(== CONTAINER-LIKE) + (reassemble-type t1 slots)] + [(== PRODUCT-LIKE) + (if (ormap bot? slots) + (type-eval #'(U)) + (reassemble-type t1 slots))])] + [_ (type-eval #'(U))])) + +;; Type Type -> Bool +;; first type is the contents of the set/dataspace +;; second type is the type of a pattern +(define-for-syntax (project-safe? t1 t2) + (define (project-safe* t1 t2) + (syntax-parse #`(#,t1 #,t2) + [(_ (~Bind τ2:type)) + (and (finite? t1) (<: t1 #'τ2))] + [(_ ~Discard) + #t] + [(_ ~★/t) + #t] + [((~U* τ1:type ...) _) + (stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))] + [(_ (~U* τ2:type ...)) + (stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))] + [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) + #:when (free-identifier=? #'τ-cons1 #'τ-cons2) + #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) + #:do [(define desc (syntax-property t1 isect-desc-key))] + #:when (equal? desc PRODUCT-LIKE) + (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] + [_ #t])) + (if (overlap? t1 t2) + (project-safe* t1 t2) + #t)) + +;; AssertionType PatternType -> Bool +;; Is it possible for things of these two types to match each other? +;; Flattish-Type = Flat-Types + ★/t, Bind, Discard (assertion and pattern types) +(define-for-syntax (overlap? t1 t2) + (define t22 (replace-bind-and-discard-with-★ t2)) + (not (<: (∩ t1 t22) (mk-U*- '())))) + +;; Flattish-Type -> Bool +(define-for-syntax (finite? t) + (syntax-parse t + [~★/t #f] + [(~U* τ:type ...) + (stx-andmap finite? #'(τ ...))] + [(~Base _) #t] + [(~Any/bvs τ-cons () τ ...) + (stx-andmap finite? #'(τ ...))])) + +;; PatternType -> Type +(define-for-syntax (pattern-matching-assertions t) + (syntax-parse t + [(~Bind τ) + #'τ] + [~Discard + (type-eval #'★/t)] + [(~U* τ ...) + (type-eval #`(U #,@(stx-map pattern-matching-assertions #'(τ ...))))] + [(~Any/bvs τ-cons () τ ...) + #:when (reassemblable? t) + (define subitems (for/list ([t (in-syntax #'(τ ...))]) + (pattern-matching-assertions t))) + (reassemble-type t subitems)] + [_ t])) + +;; it's ok for x to respond to strictly more events than y +(define-for-syntax (condition-covers? x y) + (or + ;; covers Start,Stop,Dataflow + (type=? x y) + (syntax-parse #`(#,x #,y) + [((~Know τ1) (~Know τ2)) + (<: (pattern-matching-assertions #'τ2) + (pattern-matching-assertions #'τ1))] + [((~¬Know τ1) (~¬Know τ2)) + (<: (pattern-matching-assertions #'τ2) + (pattern-matching-assertions #'τ1))] + [((~Message τ1) (~Message τ2)) + (<: (pattern-matching-assertions #'τ2) + (pattern-matching-assertions #'τ1))] + [_ #f]))) + +;; RoleType RoleType -> Bool +;; Check that role r implements role spec (possibly does more) +(define-for-syntax (role-implements? r spec) + (syntax-parse #`(#,r #,spec) + ;; TODO: cases for unions, stop + [((~Role (x:id) (~or (~Shares τ-s1) (~Sends τ-m1) (~Reacts τ-if1 τ-then1 ...)) ...) + (~Role (y:id) (~or (~Shares τ-s2) (~Sends τ-m2) (~Reacts τ-if2 τ-then2 ...)) ...)) + #:when (free-identifier=? #'x #'y) + (and + ;; for each assertion in the spec, there must be a suitable assertion in the actual + ;; TODO: this kinda ignores numerosity, can one assertion in r cover multiple assertions in spec? + (for/and [(s2 (in-syntax #'(τ-s2 ...)))] + (stx-ormap (<:l s2) #'(τ-s1 ...))) + ;; similar for messages + (for/and [(m2 (in-syntax #'(τ-m2 ...)))] + (stx-ormap (<:l m2) #'(τ-m1 ...))) + (for/and [(s2 (in-syntax #'((τ-if2 (τ-then2 ...)) ...)))] + (define/syntax-parse (τ-if2 (τ-then2 ...)) s2) + (for/or [(s1 (in-syntax #'((τ-if1 (τ-then1 ...)) ...)))] + (define/syntax-parse (τ-if1 (τ-then1 ...)) s1) + ;; the event descriptors need to line up + (and (condition-covers? #'τ-if1 #'τ-if2) + ;; and for each specified response to the event, there needs to be a similar one in the + ;; the actual + (stx-andmap (lambda (s) (stx-ormap (lambda (r) (role-implements? r s)) #'(τ-then1 ...))) + #'(τ-then2 ...))))))] + [((~Role (x:id) _ ...) + (~Role (y:id) _ ...)) + (role-implements? (subst #'y #'x r) spec)] + [((~Stop x:id τ1 ...) + (~Stop y:id τ2 ...)) + (and + (free-identifier=? #'x #'y) + (for/and ([t2 (in-syntax #'(τ2 ...))]) + (for/or ([t1 (in-syntax #'(τ1 ...))]) + (role-implements? t1 t2))))] + ;; seems like this check might be in the wrong place + [((~Sends τ-m1) + (~Sends τ-m2)) + (<: #'τ-m1 #'τ-m2)] + [((~Actor _) + (~Actor _)) + ;; 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 +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; DesugaredSyntax EffectName -> (Syntaxof Effect ...) +(define-for-syntax (get-effect e- eff) + (or (syntax-property e- eff) #'())) + +;; DesugaredSyntax EffectName -> Bool +(define-for-syntax (effect-free? e- eff) + (define prop (syntax-property e- eff)) + (or (false? prop) (stx-null? prop))) + +;; DesugaredSyntax -> Bool +(define-for-syntax (pure? e-) + (for/and ([key (in-list '(ν-ep ν-f ν-s))]) + (effect-free? e- key))) + +;; (SyntaxOf DesugaredSyntax ...) -> Bool +(define-for-syntax (all-pure? es) + (stx-andmap pure? es)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lambdas +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫ + [[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e) + (⇒ ν-ep (~effs τ-ep ...)) + (⇒ ν-s (~effs τ-s ...)) + (⇒ ν-f (~effs τ-f ...))] + ---------------------------------------- + [⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e) + (Endpoints τ-ep ...) + (Roles τ-f ...) + (Spawns τ-s ...))))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Sequencing & Definitions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; For Debugging +(define-for-syntax DEBUG-BINDINGS? #f) + +(define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx) + (when DEBUG-BINDINGS? + (printf "adding to context ~a\n" (syntax-debug-info x))) + (syntax-local-bind-syntaxes (list x-) #f ctx) + (syntax-local-bind-syntaxes (list x) + #`(make-rename-transformer + (add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x)) + ctx)) + +(define-for-syntax (add-bindings-to-ctx e- def-ctx) + (syntax-parse e- + #:literals (erased field/intermediate define/intermediate begin-) + [(erased (field/intermediate (x:id x-:id τ e-) ...)) + (for ([orig-name (in-syntax #'(x ... ))] + [new-name (in-syntax #'(x- ...))] + [field-ty (in-syntax #'(τ ...))]) + (int-def-ctx-bind-type-rename orig-name new-name field-ty def-ctx))] + [(erased (define/intermediate x:id x-:id τ e-)) + (int-def-ctx-bind-type-rename #'x #'x- #'τ def-ctx)] + #;[(erased (begin- e ...)) + (for ([e (in-syntax #'(e ...))]) + (add-bindings-to-ctx e def-ctx))] + [_ (void)])) + +(define-for-syntax (display-ctx-bindings ctx) + (printf "context:\n") + (for ([x (in-list (internal-definition-context-binding-identifiers ctx))]) + (printf ">>~a\n" (syntax-debug-info x)))) + +;; -> (Values e-... (Listof Type) (Listof EndpointEffects) (Listof FacetEffects) (Listof SpawnEffects)) +;; recognizes local binding forms +;; (field/intermediate [x e] ... +;; (define/intermediate x x- τ e) +(define-for-syntax (walk/bind e... + [def-ctx (syntax-local-make-definition-context)] + [unique (gensym 'walk/bind)]) + (define-values (rev-e-... rev-τ... ep-effects facet-effects spawn-effects) + (let loop ([e... (syntax->list e...)] + [rev-e-... '()] + [rev-τ... '()] + [ep-effects '()] + [facet-effects '()] + [spawn-effects '()]) + (match e... + ['() + (values rev-e-... rev-τ... ep-effects facet-effects spawn-effects)] + [(cons e more) + (when (and DEBUG-BINDINGS? + (identifier? e)) + (display-ctx-bindings def-ctx) + (printf "expanding ~a\n" (syntax-debug-info e))) + (define e- (local-expand e (list unique) (list #'erased #'begin) def-ctx)) + (syntax-parse e- + #:literals (begin) + [(begin e ...) + (loop (append (syntax->list #'(e ...)) more) + rev-e-... + rev-τ... + ep-effects + facet-effects + spawn-effects)] + [_ + (define τ (syntax-property e- ':)) + (define-values (ep-effs f-effs s-effs) + (values (syntax->list (get-effect e- 'ν-ep)) + (syntax->list (get-effect e- 'ν-f)) + (syntax->list (get-effect e- 'ν-s)))) + (add-bindings-to-ctx e- def-ctx) + (loop more + (cons e- rev-e-...) + (cons τ rev-τ...) + (append ep-effs ep-effects) + (append f-effs facet-effects) + (append s-effs spawn-effects))])]))) + (values (reverse rev-e-...) + (reverse rev-τ...) + ep-effects + facet-effects + spawn-effects)) + +(define-syntax (field/intermediate stx) + (syntax-parse stx + [(_ [x:id x-:id τ e-] ...) + #'(syndicate:field [x- e-] ...)])) + + +(define-syntax (define/intermediate stx) + (syntax-parse stx + [(_ x:id x-:id τ e) + ;; including a syntax binding for x allows for module-top-level references + ;; (where walk/bind won't replace further uses) and subsequent provides + #'(begin- + (define-syntax x + (make-variable-like-transformer (add-orig (assign-type #'x- #'τ #:wrap? #f) #'x))) + (define- x- e))])) + +;; copied from ext-stlc +(define-typed-syntax define + [(_ x:id (~datum :) τ:type e:expr) ≫ + [⊢ e ≫ e- ⇐ τ.norm] + #:fail-unless (pure? #'e-) "expression must be pure" + #:with x- (generate-temporary #'x) + #:with x+ (syntax-local-identifier-as-binding #'x) + -------- + [⊢ (define/intermediate x+ x- τ.norm e-) (⇒ : ★/t)]] + [(_ x:id e) ≫ + ;This won't work with mutually recursive definitions + [⊢ e ≫ e- ⇒ τ] + #:fail-unless (pure? #'e-) "expression must be pure" + #:with x- (generate-temporary #'x) + #:with x+ (syntax-local-identifier-as-binding #'x) + -------- + [⊢ (define/intermediate x+ x- τ e-) (⇒ : ★/t)]] + [(_ (f [x (~optional (~datum :)) ty:type] ... + (~or (~datum →) (~datum ->)) ty_out:type) + e ...+) ≫ + [⊢ (lambda ([x : ty] ...) (begin e ...)) ≫ e- (⇒ : (~and fun-ty + (~→ (~not (~Computation _ ...)) ... + (~Computation (~Value τ-v) + _ ...))))] + #:fail-unless (<: #'τ-v #'ty_out.norm) + (format "expected different return type\n got ~a\n expected ~a\n" + #'τ-v #'ty_out + #;(type->str #'τ-v) + #;(type->str #'ty_out)) + #:with f- (add-orig (generate-temporary #'f) #'f) + -------- + [⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]] + [(_ (f [x (~optional (~datum :)) ty] ...) + e ...+) ≫ + ---------------------------- + [≻ (define (f [x ty] ... -> ★/t) e ...)]]) + +(define-typed-syntax begin + [(_ e_unit ... e) ≫ + #:do [(define-values (e-... τ... ep-effs f-effs s-effs) (walk/bind #'(e_unit ... e)))] + #:with τ (last τ...) + -------- + [⊢ (begin- #,@e-...) (⇒ : τ) + (⇒ ν-ep (#,@ep-effs)) + (⇒ ν-f (#,@f-effs)) + (⇒ ν-s (#,@s-effs))]]) diff --git a/racket/typed/list.rkt b/racket/typed/list.rkt new file mode 100644 index 0000000..f5ed0d9 --- /dev/null +++ b/racket/typed/list.rkt @@ -0,0 +1,98 @@ +#lang turnstile + +(provide List + (for-syntax ~List) + list + cons + first + rest + member? + empty? + for + for/fold) + +(require "core-types.rkt") +(require (postfix-in - racket/list)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Lists +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-container-type List #:arity = 1) + +(define-typed-syntax (list e ...) ≫ + [⊢ e ≫ e- ⇒ τ] ... + #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" + ------------------- + [⊢ (list- e- ...) ⇒ (List (U τ ...))]) + +(define-typed-syntax (cons e1 e2) ≫ + [⊢ e1 ≫ e1- ⇒ τ1] + #:fail-unless (pure? #'e1-) "expression must be pure" + [⊢ e2 ≫ e2- ⇒ (~List τ2)] + #:fail-unless (pure? #'e2-) "expression must be pure" + #:with τ-l (type-eval #'(List (U τ1 τ2))) + ---------------------------------------- + [⊢ (cons- e1- e2-) ⇒ τ-l]) + +(define-typed-syntax (for/fold [acc:id e-acc] + [x:id e-list] + e-body ...+) ≫ + [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] + #:fail-unless (pure? #'e-list-) "expression must be pure" + [⊢ e-acc ≫ e-acc- ⇒ τ-a] + #:fail-unless (pure? #'e-acc-) "expression must be pure" + [[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ (begin e-body ...) ≫ e-body- ⇒ τ-b] + #:fail-unless (pure? #'e-body-) "body must be pure" + #:fail-unless (<: #'τ-b #'τ-a) + "loop body doesn't match accumulator" + ------------------------------------------------------- + [⊢ (for/fold- ([acc- e-acc-]) + ([x- (in-list- e-list-)]) + e-body-) + ⇒ τ-b]) + +(define-typed-syntax (for ([x:id e-list] ...) + e-body ...+) ≫ + [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ... + #:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure" + [[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b) + (⇒ ν-ep (~effs eps ...)) + (⇒ ν-f (~effs fs ...)) + (⇒ ν-s (~effs ss ...))] + ------------------------------------------------------- + [⊢ (for- ([x- (in-list- e-list-)] ...) + e-body-) (⇒ : ★/t) + (⇒ ν-ep (eps ...)) + (⇒ ν-f (fs ...)) + (⇒ ν-s (ss ...))]) + +(define-typed-syntax (empty? e) ≫ + [⊢ e ≫ e- ⇒ (~List _)] + #:fail-unless (pure? #'e-) "expression must be pure" + ----------------------- + [⊢ (empty?- e-) ⇒ Bool]) + +(define-typed-syntax (first e) ≫ + [⊢ e ≫ e- ⇒ (~List τ)] + #:fail-unless (pure? #'e-) "expression must be pure" + ----------------------- + [⊢ (first- e-) ⇒ τ]) + +(define-typed-syntax (rest e) ≫ + [⊢ e ≫ e- ⇒ (~List τ)] + #:fail-unless (pure? #'e-) "expression must be pure" + ----------------------- + [⊢ (rest- e-) ⇒ (List τ)]) + +(define-typed-syntax (member? e l) ≫ + [⊢ e ≫ e- ⇒ τe] + #:fail-unless (pure? #'e-) "expression must be pure" + [⊢ l ≫ l- ⇒ (~List τl)] + #:fail-unless (pure? #'l-) "expression must be pure" + #:fail-unless (<: #'τe #'τl) "incompatible list" + ---------------------------------------- + [⊢ (member?- e- l-) ⇒ Bool]) + +(define- (member?- v l) + (and- (member- v l) #t)) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 14e76d9..58c8e11 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -8,7 +8,7 @@ ;; Start dataspace programs run-ground-dataspace ;; Types - Int Bool String Tuple Bind Discard → List ByteString Symbol + Int Bool String Tuple Bind Discard → ByteString Symbol Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop FacetName Field ★/t Observe Inbound Outbound Actor U @@ -34,10 +34,9 @@ gensym symbol->string string->symbol bytes->string/utf-8 string->bytes/utf-8 ~a ;; lists - list cons first rest member? empty? for for/fold + (all-from-out "list.rkt") ;; sets - Set set set-member? set-add set-remove set-count set-union set-subtract set-intersect - list->set set->list + (all-from-out "set.rkt") ;; DEBUG and utilities print-type print-role ;; Extensions @@ -48,8 +47,9 @@ require/typed require-struct ) -(require (only-in turnstile - [define-type-constructor define-type-constructor-])) +(require "core-types.rkt") +(require "list.rkt") +(require "set.rkt") (require (prefix-in syndicate: syndicate/actor-lang)) @@ -68,1153 +68,10 @@ (require rackunit) (require rackunit/turnstile)) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Debugging -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-for-syntax DEBUG-BINDINGS? #f) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Type Checking Conventions -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; : describes the immediate result of evaluation -;; ν-ep key aggregates endpoint affects: -;; `Shares`, `Reacts`, and `MakesField` -;; Note thar MakesField is only an effect, not a type -;; ν-f key aggregates facet effects (starting/stopping a facet) as `Role`s & `Stop`s and message sends, `Sends` -;; ν-s key aggregates spawned actors as `Actor`s - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Types -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; certain metadata needs to be associated with each type, for the purpose of -;; making certain judgments and metafunctions extensible. - -;; a isect-desc describes how a type (constructor) behaves with respect to -;; intersection, and is one of -;; - BASE -;; - CONTAINER-LIKE -;; - PRODUCT-LIKE -(begin-for-syntax - (define BASE 'base) - (define CONTAINER-LIKE 'container-like) - (define PRODUCT-LIKE 'product-like) - - ;; syntax property key - (define isect-desc-key - 'isect-desc-key) - - (define-syntax-class isect-desc - #:attributes (val) - #:datum-literals (BASE CONTAINER-LIKE PRODUCT-LIKE) - (pattern BASE - #:attr val BASE) - (pattern CONTAINER-LIKE - #:attr val CONTAINER-LIKE) - (pattern PRODUCT-LIKE - #:attr val PRODUCT-LIKE)) - - ;; Any -> Bool - ;; recognize isect-descs - (define (isect-desc? x) - (member x (list BASE CONTAINER-LIKE PRODUCT-LIKE))) - - ;; syntax property key - ;; syntax-transformer value - (define type-cons-key - 'type-cons) - - ;; Type -> Bool - ;; check if the type has a syntax property allowing us to create new instances - (define (reassemblable? t) - (and (syntax-property t type-cons-key) #t)) - - ;; Type (Listof Type) -> Type - ;; Create a new instance of the type with the given arguments - ;; needs to have the type-cons-key - (define (reassemble-type ty args) - (define tycons (syntax-property ty type-cons-key)) - (unless tycons - (error "expected to find type-cons-key")) - (type-eval #`(#,tycons #,@args)))) - -(define-syntax (define-type-constructor+ stx) - (syntax-parse stx - [(_ Name:id - #:arity op arity - #:arg-variances variances - #:isect-desc desc:isect-desc - (~optional (~seq #:extra-info extra-info))) - #:with Name- (mk-- #'Name) - #:with NamePat (mk-~ #'Name) - #:with NamePat- (mk-~ #'Name-) - #:with mk (format-id #'Name "mk-~a-" (syntax-e #'Name)) - #:with mk- (format-id #'Name- "mk-~a-" (syntax-e #'Name-)) - (quasisyntax/loc stx - (begin- - (define-type-constructor- Name- - #:arity op arity - #:arg-variances variances - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())) - (define-syntax (Name stx) - (syntax-parse stx - [(_ t (... ...)) - (set-stx-prop/preserved - (set-stx-prop/preserved - (syntax/loc stx - (Name- t (... ...))) - #,isect-desc-key - '#,(attribute desc.val)) - type-cons-key - #'Name)])) - (begin-for-syntax - (define-syntax NamePat - (pattern-expander - (syntax-parser - [(_ p (... ...)) - #'(NamePat- p (... ...))])))) - (define-for-syntax mk mk-)))])) - -(begin-for-syntax - ;; Syntax -> (Listof Variant) - ;; make a list of the same length as the number of arguments of the given - ;; (type) syntax, all covariant - (define (mk-covariant ts) - (for/list ([_ (sequence-tail (in-syntax ts) 1)]) - covariant))) - -;; Define a type constructor that acts like a container: -;; - covariant -;; - has an empty element (i.e. intersection always non-empty) -(define-syntax (define-container-type stx) - (syntax-parse stx - [(_ Name:id #:arity op arity - (~optional (~seq #:extra-info extra-info))) - (quasisyntax/loc stx - (define-type-constructor+ Name - #:arity op arity - #:arg-variances mk-covariant - #:isect-desc CONTAINER-LIKE - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())))])) - -;; Define a type constructor that acts like a container: -;; - covariant -;; - does not have an empty element (i.e. intersection may be empty) -(define-syntax (define-product-type stx) - (syntax-parse stx - [(_ Name:id #:arity op arity - (~optional (~seq #:extra-info extra-info))) - (quasisyntax/loc stx - (define-type-constructor+ Name - #:arity op arity - #:arg-variances mk-covariant - #:isect-desc PRODUCT-LIKE - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())))])) - -(define-binding-type Role #:arity >= 0 #:bvs = 1) -(define-type-constructor Shares #:arity = 1) -(define-type-constructor Sends #:arity = 1) -(define-type-constructor Reacts #:arity >= 1) -(define-type-constructor Know #:arity = 1) -(define-type-constructor ¬Know #:arity = 1) -(define-type-constructor Stop #:arity >= 1) -(define-type-constructor Field #:arity = 1) -(define-type-constructor Bind #:arity = 1) -;; keep track of branches for facet effects -;; (Branch (Listof (Listof Type))) -(define-type-constructor Branch #:arity >= 0) -;; sequence of effects -(define-type-constructor Effs #:arity >= 0) -(define-base-types OnStart OnStop OnDataflow MakesField) -(define-for-syntax field-prop-name 'fields) -(define-type-constructor Actor #:arity = 1) - -(define-product-type Message #:arity = 1) -(define-product-type Tuple #:arity >= 0) -(define-product-type Observe #:arity = 1) -(define-product-type Inbound #:arity = 1) -(define-product-type Outbound #:arity = 1) -(define-container-type AssertionSet #:arity = 1) -(define-container-type Patch #:arity = 2) -(define-container-type List #:arity = 1) -(define-container-type Set #:arity = 1) - -(define-type-constructor → #:arity > 0) -;; for describing the RHS -;; a value and a description of the effects -(define-type-constructor Computation #:arity = 4) -(define-type-constructor Value #:arity = 1) -(define-type-constructor Endpoints #:arity >= 0) -(define-type-constructor Roles #:arity >= 0) -(define-type-constructor Spawns #:arity >= 0) - - -(define-base-types Int Bool String Discard ★/t FacetName ByteString Symbol) - -(define-for-syntax (type-eval t) - ((current-type-eval) t)) - -(define-type-constructor U* #:arity >= 0) - -;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file. -;; however, this version expands the type at every reference, incurring a potentially large -;; overhead---2x in the case of book-club.rkt -;; (copied from ext-stlc example) -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ) - #'(define-syntax- alias - (make-variable-like-transformer #'τ))] - [(_ (f:id x:id ...) ty) - #'(define-syntax- (f stx) - (syntax-parse stx - [(_ x ...) - #:with τ:any-type #'ty - #'τ.norm]))])) - -(define-type-alias ⊥ (U*)) - -(define-for-syntax (prune+sort tys) - (stx-sort - (filter-maximal - (stx->list tys) - typecheck?))) - -(define-syntax (U stx) - (syntax-parse stx - [(_ . tys) - ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys - #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys) - #:with tys- (prune+sort #'(ty1- ... ... ty2- ...)) - (if (= 1 (stx-length #'tys-)) - (stx-car #'tys-) - (syntax/loc stx (U* . tys-)))])) - -;; for looking at the "effects" -(begin-for-syntax - (define-syntax ~effs - (pattern-expander - (syntax-parser - [(_ eff:id ...) - #:with tmp (generate-temporary 'effss) - #'(~and tmp - (~parse (eff ...) (stx-or #'tmp #'())))]))) - - (define (stx-truth? a) - (and a (not (and (syntax? a) (false? (syntax-e a)))))) - (define (stx-or a b) - (cond [(stx-truth? a) a] - [else b]))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; User Defined Types, aka Constructors -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(begin-for-syntax - (define-splicing-syntax-class type-constructor-decl - (pattern (~seq #:type-constructor TypeCons:id)) - (pattern (~seq) #:attr TypeCons #f)) - - (struct user-ctor (typed-ctor untyped-ctor) - #:property prop:procedure - (lambda (v stx) - (define transformer (user-ctor-typed-ctor v)) - (syntax-parse stx - [(_ e ...) - (quasisyntax/loc stx - (#,transformer e ...))])))) - -(define-syntax (define-constructor* stx) - (syntax-parse stx - #:datum-literals (:) - [(_ (Cons:id : TyCons:id slot:id ...) clause ...) - #'(define-constructor (Cons slot ...) - #:type-constructor TyCons - clause ...)])) - -(define-syntax (define-constructor stx) - (syntax-parse stx - [(_ (Cons:id slot:id ...) - ty-cons:type-constructor-decl - (~seq #:with - Alias AliasBody) ...) - #:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons))) - #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons) - #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons) - #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons) - #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons) - #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons)) - (define arity (stx-length #'(slot ...))) - #`(begin- - (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent) - (define-syntax (TypeConsExtraInfo stx) - (syntax-parse stx - [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) - (define-product-type TypeCons - #:arity = #,arity - #:extra-info 'TypeConsExtraInfo) - (define-syntax (MakeTypeCons stx) - (syntax-parse stx - [(_ t (... ...)) - #:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch" - #'(TypeCons t (... ...))])) - (define-syntax (GetTypeParams stx) - (syntax-parse stx - [(_ (TypeConsExpander t (... ...))) - #'(t (... ...))])) - (define-syntax Cons - (user-ctor #'Cons- #'StructName)) - (define-typed-syntax (Cons- e (... ...)) ≫ - #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch" - [⊢ e ≫ e- (⇒ : τ)] (... ...) - #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure" - ---------------------- - [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))]) - (define-type-alias Alias AliasBody) ...)])) - -;; (require-struct chicken #:as Chicken #:from "some-mod.rkt") will -;; - extract the struct-info for chicken, and ensure that it is immutable, has a set number of fields -;; - determine the number of slots, N, chicken has -;; - define the type constructor (Chicken ...N), with the extra info used by define-constructor above -;; - define chicken+, a turnstile type rule that checks uses of chicken -;; - bind chicken to a user-ctor struct -;; TODO: this implementation shares a lot with that of define-constructor -(define-syntax (require-struct stx) - (syntax-parse stx - [(_ ucons:id #:as ty-cons:id #:from lib) - (with-syntax* ([TypeCons #'ty-cons] - [MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)] - [GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)] - [TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)] - [TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)] - [Cons- (format-id #'ucons "~a/checked" #'ucons)] - [orig-struct-info (generate-temporary #'ucons)] - [type-tag (generate-temporary #'ucons)]) - (quasisyntax/loc stx - (begin- - (require- (only-in- lib [ucons orig-struct-info])) - (begin-for-syntax - (define info (syntax-local-value #'orig-struct-info)) - (unless (struct-info? info) - (raise-syntax-error #f "expected struct" #'#,stx #'ucons)) - (match-define (list desc cons pred accs muts sup) (extract-struct-info info)) - (when (false? (last accs)) - (raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons)) - (unless (equal? #t sup) - (raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons)) - (define arity (length accs))) - (define-syntax (TypeConsExtraInfo stx) - (syntax-parse stx - [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) - (define-type-constructor TypeCons - ;; issue: arity needs to parse as an exact-nonnegative-integer - ;; fix: check arity in MakeTypeCons - #:arity >= 0 - #:extra-info 'TypeConsExtraInfo) - (define-syntax (MakeTypeCons stx) - (syntax-parse stx - [(_ t (... ...)) - #:fail-unless (= arity (stx-length #'(t (... ...)))) "arity mismatch" - #'(TypeCons t (... ...))])) - (define-syntax (GetTypeParams stx) - (syntax-parse stx - [(_ (TypeConsExpander t (... ...))) - #'(t (... ...))])) - (define-typed-syntax (Cons- e (... ...)) ≫ - #:fail-unless (= arity (stx-length #'(e (... ...)))) "arity mismatch" - [⊢ e ≫ e- (⇒ : τ)] (... ...) - #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure" - ---------------------- - [⊢ (#%app- orig-struct-info e- (... ...)) (⇒ : (TypeCons τ (... ...)))]) - (define-syntax ucons - (user-ctor #'Cons- #'orig-struct-info)))))])) - -(begin-for-syntax - (define-syntax ~constructor-extra-info - (pattern-expander - (syntax-parser - [(_ tag mk get) - #'(_ (_ tag) (_ mk) (_ get))]))) - - (define-syntax ~constructor-type - (pattern-expander - (syntax-parser - [(_ tag . rst) - #'(~and it - (~fail #:unless (user-defined-type? #'it)) - (~parse tag (get-type-tag #'it)) - (~Any _ . rst))]))) - - (define-syntax ~constructor-exp - (pattern-expander - (syntax-parser - [(_ cons . rst) - #'(~and (cons . rst) - (~fail #:unless (ctor-id? #'cons)))]))) - - (define (inspect t) - (syntax-parse t - [(~constructor-type tag t ...) - (list (syntax-e #'tag) (stx-map type->str #'(t ...)))])) - - (define (tags-equal? t1 t2) - (equal? (syntax-e t1) (syntax-e t2))) - - (define (user-defined-type? t) - (get-extra-info (type-eval t))) - - (define (get-type-tag t) - (syntax-parse (get-extra-info t) - [(~constructor-extra-info tag _ _) - (syntax-e #'tag)])) - - (define (get-type-args t) - (syntax-parse (get-extra-info t) - [(~constructor-extra-info _ _ get) - (define f (syntax-local-value #'get)) - (syntax->list (f #`(get #,t)))])) - - (define (make-cons-type t args) - (syntax-parse (get-extra-info t) - [(~constructor-extra-info _ mk _) - (define f (syntax-local-value #'mk)) - (type-eval (f #`(mk #,@args)))])) - - (define (ctor-id? stx) - (and (identifier? stx) - (user-ctor? (syntax-local-value stx (const #f))))) - - (define (untyped-ctor stx) - (user-ctor-untyped-ctor (syntax-local-value stx (const #f))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Require & Provide -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Import and ascribe a type from an untyped module -;; TODO: this is where contracts would need to go -(define-syntax (require/typed stx) - (syntax-parse stx - #:datum-literals (:) - [(_ lib [name:id : ty:type] ...) - #:with (name- ...) (format-ids "~a-" #'(name ...)) - (syntax/loc stx - (begin- - (require (only-in lib [name name-] ...)) - (define-syntax name - (make-variable-like-transformer (add-orig (assign-type #'name- #'ty #:wrap? #f) #'name))) - ...))])) - -;; Format identifiers in the same way -;; FormatString (SyntaxListOf Identifier) -> (Listof Identifier) -(define-for-syntax (format-ids fmt ids) - (for/list ([id (in-syntax ids)]) - (format-id id fmt id))) - -;; (SyntaxListof (SyntaxList Identifier Type Identifier)) -> (Listof Identifier) -;; For each triple (name- ty name), -;; assign the ty to name- with the orig name -(define-for-syntax (assign-types los) - (for/list ([iti (in-syntax los)]) - (match-define (list name- ty name) (syntax->list iti)) - (add-orig (assign-type name- ty #:wrap? #f) name))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Conveniences -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; (SyntaxListof (SyntaxListof Type)) -> (U (SyntaxListof Branch) #'()) -(define-for-syntax (make-Branch tys*) - (syntax-parse tys* - [() - #'()] - [(() ...) - #'()] - [((ty ...) ...) - (define effs - (for/list ([tys (in-syntax tys*)]) - (mk-Effs- (syntax->list tys)))) - #`(#,(mk-Branch- effs))])) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Syntax -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(begin-for-syntax - - ;; constructors with arity one - (define-syntax-class kons1 - (pattern (~or (~datum observe) - (~datum inbound) - (~datum outbound) - (~datum message)))) - - (define (kons1->constructor stx) - (syntax-parse stx - #:datum-literals (observe inbound outbound) - [observe #'syndicate:observe] - [inbound #'syndicate:inbound] - [outbound #'syndicate:outbound] - [message #'syndicate:message])) - - (define-syntax-class basic-val - (pattern (~or boolean - integer - string))) - - (define-syntax-class prim-op - (pattern (~or (~literal +) - (~literal -) - (~literal displayln))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Utilities Over Types -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-for-syntax (bot? t) - ((current-typecheck-relation) t (type-eval #'(U*)))) - -(define-for-syntax (flat-type? τ) - (syntax-parse τ - [(~→ τ ...) #f] - [(~Actor τ) #f] - [_ #t])) - -(define-for-syntax (strip-? t) - (type-eval - (syntax-parse t - [(~U* τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] - [~★/t #'★/t] - ;; since (Observe X) can match (Message X): - ;; doing this specifically for the intersection operation in the spawn rule, need to check other - ;; uses - [(~Observe τ) #'(U τ (Message τ))] - [_ #'(U*)]))) - -;; similar to strip- fns, but leave non-message types as they are -(define-for-syntax (prune-message t) - (type-eval - (syntax-parse t - [(~U* τ ...) #`(U #,@(stx-map prune-message #'(τ ...)))] - [~★/t #'★/t] - [(~Message τ) #'τ] - [_ t]))) - -(define-for-syntax (strip-inbound t) - (type-eval - (syntax-parse t - [(~U* τ ...) #`(U #,@(stx-map strip-inbound #'(τ ...)))] - [~★/t #'★/t] - [(~Inbound τ) #'τ] - [_ #'(U*)]))) - -(define-for-syntax (strip-outbound t) - (type-eval - (syntax-parse t - [(~U* τ ...) #`(U #,@(stx-map strip-outbound #'(τ ...)))] - [~★/t #'★/t] - [(~Outbound τ) #'τ] - [_ #'(U*)]))) - -(define-for-syntax (relay-interests t) - (type-eval - (syntax-parse t - ;; TODO: probably need to `normalize` the result - [(~U* τ ...) #`(U #,@(stx-map relay-interests #'(τ ...)))] - [~★/t #'★/t] - [(~Observe (~Inbound τ)) #'(Observe τ)] - [_ #'(U*)]))) - -;; (SyntaxOf RoleType ...) -> (Syntaxof InputType OutputType SpawnType) -(define-for-syntax (analyze-roles rs) - (define-values (lis los lss) - (for/fold ([is '()] - [os '()] - [ss '()]) - ([r (in-syntax rs)]) - (define-values (i o s) (analyze-role-input/output r)) - (values (cons i is) (cons o os) (cons s ss)))) - #`(#,(type-eval #`(U #,@lis)) - #,(type-eval #`(U #,@los)) - #,(type-eval #`(U #,@lss)))) - -;; Wanted test case, but can't use it bc it uses things defined for-syntax -#;(module+ test - (let ([r (type-eval #'(Role (x) (Shares Int)))]) - (syntax-parse (analyze-role-input/output r) - [(τ-i τ-o) - (check-true (type=? #'τ-o (type-eval #'Int)))]))) - -;; RoleType -> (Values InputType OutputType SpawnType) -(define-for-syntax (analyze-role-input/output t) - (syntax-parse t - [(~Branch (~Effs τ-r ...) ...) - #:with (τi τo τa) (analyze-roles #'(τ-r ... ...)) - (values #'τi #'τo #'τa)] - [(~Stop name:id τ-r ...) - #:with (τi τo τa) (analyze-roles #'(τ-r ...)) - (values #'τi #'τo #'τa)] - [(~Actor τc) - (values (mk-U*- '()) (mk-U*- '()) t)] - [(~Sends τ-m) - (values (mk-U*- '()) (type-eval #'(Message τ-m)) (mk-U*- '()))] - [(~Role (name:id) - (~or (~Shares τ-s) - (~Sends τ-m) - (~Reacts τ-if τ-then ...)) ... - (~and (~Role _ ...) sub-role) ...) - (define-values (is os ss) - (for/fold ([ins '()] - [outs '()] - [spawns '()]) - ([t (in-syntax #'(τ-then ... ... sub-role ...))]) - (define-values (i o s) (analyze-role-input/output t)) - (values (cons i ins) (cons o outs) (cons s spawns)))) - (define pat-types (stx-map event-desc-type #'(τ-if ...))) - (values (type-eval #`(U #,@is #,@pat-types)) - (type-eval #`(U τ-s ... (Message τ-m) ... #,@os #,@(stx-map pattern-sub-type pat-types))) - (type-eval #`(U #,@ss)))])) - -;; EventDescriptorType -> Type -(define-for-syntax (event-desc-type desc) - (syntax-parse desc - [(~Know τ) #'τ] - [(~¬Know τ) #'τ] - [(~Message τ) desc] - [_ (type-eval #'(U*))])) - -;; PatternType -> Type -(define-for-syntax (pattern-sub-type pt) - (syntax-parse pt - [(~Message τ) - (define t (replace-bind-and-discard-with-★ #'τ)) - (type-eval #`(Observe #,t))] - [τ - (define t (replace-bind-and-discard-with-★ #'τ)) - (type-eval #`(Observe #,t))])) - -;; TODO : can potentially use something like `subst` for this -(define-for-syntax (replace-bind-and-discard-with-★ t) - (syntax-parse t - [(~Bind _) - (type-eval #'★/t)] - [~Discard - (type-eval #'★/t)] - [(~U* τ ...) - (type-eval #`(U #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))] - [(~Any/bvs τ-cons () τ ...) - #:when (reassemblable? t) - (define subitems (for/list ([t (in-syntax #'(τ ...))]) - (replace-bind-and-discard-with-★ t))) - (reassemble-type t subitems)] - [_ t])) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Subtyping and Judgments on Types -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(begin-for-syntax - (define-syntax ~Base - (pattern-expander - (syntax-parser - [(_ nm:id) - #'((~literal #%plain-app) nm)]))) - - ;; Type Type -> Bool - ;; subtyping - (define (<: t1 t2) - (syntax-parse #`(#,t1 #,t2) - [(_ ~★/t) - (flat-type? t1)] - [((~U* τ1 ...) _) - (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))] - [(_ (~U* τ2:type ...)) - (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))] - [((~Actor τ1) (~Actor τ2)) - (and (<: #'τ1 #'τ2) - (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))] - [((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2)) - #:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...)) - (and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...)) - (<: #'τ-out1 #'τ-out2))] - [(~Discard _) - #t] - [((~Base τ1:id) (~Base τ2:id)) - (free-identifier=? #'τ1 #'τ2)] - [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) - #:when (free-identifier=? #'τ-cons1 #'τ-cons2) - #:do [(define variances (syntax-property #'τ-cons1 'arg-variances))] - #:when variances - #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) - (for/and ([ty1 (in-syntax #'(τ1 ...))] - [ty2 (in-syntax #'(τ2 ...))] - [var (in-list variances)]) - (match var - [(== covariant) - (<: ty1 ty2)] - [(== contravariant) - (<: ty2 ty1)] - [(== invariant) - (and (<: ty1 ty2) - (<: ty2 ty1))] - [(== irrelevant) - #t]))] - ;; TODO: clauses for Roles, and so on - [_ #f])) - - ;; shortcuts for mapping - (define ((<:l l) r) - (<: l r)) - - (define ((<:r r) l) - (<: l r))) - -;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! -;; MODIFYING GLOBAL TYPECHECKING STATE!!!!! -;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - -(begin-for-syntax - (current-typecheck-relation <:)) - -;; Flat-Type Flat-Type -> Type -(define-for-syntax (∩ t1 t2) - (unless (and (flat-type? t1) (flat-type? t2)) - (error '∩ "expected two flat-types")) - (syntax-parse #`(#,t1 #,t2) - [(_ ~★/t) - t1] - [(~★/t _) - t2] - [((~U* τ1:type ...) _) - (type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))] - [(_ (~U* τ2:type ...)) - (type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))] - [((~AssertionSet τ1) (~AssertionSet τ2)) - #:with τ12 (∩ #'τ1 #'τ2) - (type-eval #'(AssertionSet τ12))] - ;; Also, using <: is OK, even though <: refers to ∩, because <:'s use of ∩ is only - ;; in the Actor case. - [((~Base τ1:id) (~Base τ2:id)) - #:when (free-identifier=? #'τ1 #'τ2) - t1] - [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) - #:when (free-identifier=? #'τ-cons1 #'τ-cons2) - #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) - #:do [(define desc (syntax-property t1 isect-desc-key))] - #:when desc - (define slots (stx-map ∩ #'(τ1 ...) #'(τ2 ...))) - (match desc - [(== BASE) - (error "this isn't right")] - [(== CONTAINER-LIKE) - (reassemble-type t1 slots)] - [(== PRODUCT-LIKE) - (if (ormap bot? slots) - (type-eval #'(U)) - (reassemble-type t1 slots))])] - [_ (type-eval #'(U))])) - -;; Type Type -> Bool -;; first type is the contents of the set/dataspace -;; second type is the type of a pattern -(define-for-syntax (project-safe? t1 t2) - (define (project-safe* t1 t2) - (syntax-parse #`(#,t1 #,t2) - [(_ (~Bind τ2:type)) - (and (finite? t1) (<: t1 #'τ2))] - [(_ ~Discard) - #t] - [(_ ~★/t) - #t] - [((~U* τ1:type ...) _) - (stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))] - [(_ (~U* τ2:type ...)) - (stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))] - [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...)) - #:when (free-identifier=? #'τ-cons1 #'τ-cons2) - #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) - #:do [(define desc (syntax-property t1 isect-desc-key))] - #:when (equal? desc PRODUCT-LIKE) - (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] - [_ #t])) - (if (overlap? t1 t2) - (project-safe* t1 t2) - #t)) - -;; AssertionType PatternType -> Bool -;; Is it possible for things of these two types to match each other? -;; Flattish-Type = Flat-Types + ★/t, Bind, Discard (assertion and pattern types) -(define-for-syntax (overlap? t1 t2) - (define t22 (replace-bind-and-discard-with-★ t2)) - (not (<: (∩ t1 t22) (mk-U*- '())))) - -;; Flattish-Type -> Bool -(define-for-syntax (finite? t) - (syntax-parse t - [~★/t #f] - [(~U* τ:type ...) - (stx-andmap finite? #'(τ ...))] - [(~Base _) #t] - [(~Any/bvs τ-cons () τ ...) - (stx-andmap finite? #'(τ ...))])) - -;; PatternType -> Type -(define-for-syntax (pattern-matching-assertions t) - (syntax-parse t - [(~Bind τ) - #'τ] - [~Discard - (type-eval #'★/t)] - [(~U* τ ...) - (type-eval #`(U #,@(stx-map pattern-matching-assertions #'(τ ...))))] - [(~Any/bvs τ-cons () τ ...) - #:when (reassemblable? t) - (define subitems (for/list ([t (in-syntax #'(τ ...))]) - (pattern-matching-assertions t))) - (reassemble-type t subitems)] - [_ t])) - -;; it's ok for x to respond to strictly more events than y -(define-for-syntax (condition-covers? x y) - (or - ;; covers Start,Stop,Dataflow - (type=? x y) - (syntax-parse #`(#,x #,y) - [((~Know τ1) (~Know τ2)) - (<: (pattern-matching-assertions #'τ2) - (pattern-matching-assertions #'τ1))] - [((~¬Know τ1) (~¬Know τ2)) - (<: (pattern-matching-assertions #'τ2) - (pattern-matching-assertions #'τ1))] - [((~Message τ1) (~Message τ2)) - (<: (pattern-matching-assertions #'τ2) - (pattern-matching-assertions #'τ1))] - [_ #f]))) - -;; RoleType RoleType -> Bool -;; Check that role r implements role spec (possibly does more) -(define-for-syntax (role-implements? r spec) - (syntax-parse #`(#,r #,spec) - ;; TODO: cases for unions, stop - [((~Role (x:id) (~or (~Shares τ-s1) (~Sends τ-m1) (~Reacts τ-if1 τ-then1 ...)) ...) - (~Role (y:id) (~or (~Shares τ-s2) (~Sends τ-m2) (~Reacts τ-if2 τ-then2 ...)) ...)) - #:when (free-identifier=? #'x #'y) - (and - ;; for each assertion in the spec, there must be a suitable assertion in the actual - ;; TODO: this kinda ignores numerosity, can one assertion in r cover multiple assertions in spec? - (for/and [(s2 (in-syntax #'(τ-s2 ...)))] - (stx-ormap (<:l s2) #'(τ-s1 ...))) - ;; similar for messages - (for/and [(m2 (in-syntax #'(τ-m2 ...)))] - (stx-ormap (<:l m2) #'(τ-m1 ...))) - (for/and [(s2 (in-syntax #'((τ-if2 (τ-then2 ...)) ...)))] - (define/syntax-parse (τ-if2 (τ-then2 ...)) s2) - (for/or [(s1 (in-syntax #'((τ-if1 (τ-then1 ...)) ...)))] - (define/syntax-parse (τ-if1 (τ-then1 ...)) s1) - ;; the event descriptors need to line up - (and (condition-covers? #'τ-if1 #'τ-if2) - ;; and for each specified response to the event, there needs to be a similar one in the - ;; the actual - (stx-andmap (lambda (s) (stx-ormap (lambda (r) (role-implements? r s)) #'(τ-then1 ...))) - #'(τ-then2 ...))))))] - [((~Role (x:id) _ ...) - (~Role (y:id) _ ...)) - (role-implements? (subst #'y #'x r) spec)] - [((~Stop x:id τ1 ...) - (~Stop y:id τ2 ...)) - (and - (free-identifier=? #'x #'y) - (for/and ([t2 (in-syntax #'(τ2 ...))]) - (for/or ([t1 (in-syntax #'(τ1 ...))]) - (role-implements? t1 t2))))] - ;; seems like this check might be in the wrong place - [((~Sends τ-m1) - (~Sends τ-m2)) - (<: #'τ-m1 #'τ-m2)] - [((~Actor _) - (~Actor _)) - ;; 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 - -;; DesugaredSyntax EffectName -> (Syntaxof Effect ...) -(define-for-syntax (get-effect e- eff) - (or (syntax-property e- eff) #'())) - -;; DesugaredSyntax EffectName -> Bool -(define-for-syntax (effect-free? e- eff) - (define prop (syntax-property e- eff)) - (or (false? prop) (stx-null? prop))) - -;; DesugaredSyntax -> Bool -(define-for-syntax (pure? e-) - (for/and ([key (in-list '(ν-ep ν-f ν-s))]) - (effect-free? e- key))) - -;; (SyntaxOf DesugaredSyntax ...) -> Bool -(define-for-syntax (all-pure? es) - (stx-andmap pure? es)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Core forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx) - (when DEBUG-BINDINGS? - (printf "adding to context ~a\n" (syntax-debug-info x))) - (syntax-local-bind-syntaxes (list x-) #f ctx) - (syntax-local-bind-syntaxes (list x) - #`(make-rename-transformer - (add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x)) - ctx)) - -(define-for-syntax (add-bindings-to-ctx e- def-ctx) - (syntax-parse e- - #:literals (erased field/intermediate define/intermediate begin-) - [(erased (field/intermediate (x:id x-:id τ e-) ...)) - (for ([orig-name (in-syntax #'(x ... ))] - [new-name (in-syntax #'(x- ...))] - [field-ty (in-syntax #'(τ ...))]) - (int-def-ctx-bind-type-rename orig-name new-name field-ty def-ctx))] - [(erased (define/intermediate x:id x-:id τ e-)) - (int-def-ctx-bind-type-rename #'x #'x- #'τ def-ctx)] - #;[(erased (begin- e ...)) - (for ([e (in-syntax #'(e ...))]) - (add-bindings-to-ctx e def-ctx))] - [_ (void)])) - -(define-for-syntax (display-ctx-bindings ctx) - (printf "context:\n") - (for ([x (in-list (internal-definition-context-binding-identifiers ctx))]) - (printf ">>~a\n" (syntax-debug-info x)))) - -;; -> (Values e-... (Listof Type) (Listof EndpointEffects) (Listof FacetEffects) (Listof SpawnEffects)) -;; recognizes local binding forms -;; (field/intermediate [x e] ... -;; (define/intermediate x x- τ e) -(define-for-syntax (walk/bind e... - [def-ctx (syntax-local-make-definition-context)] - [unique (gensym 'walk/bind)]) - (define-values (rev-e-... rev-τ... ep-effects facet-effects spawn-effects) - (let loop ([e... (syntax->list e...)] - [rev-e-... '()] - [rev-τ... '()] - [ep-effects '()] - [facet-effects '()] - [spawn-effects '()]) - (match e... - ['() - (values rev-e-... rev-τ... ep-effects facet-effects spawn-effects)] - [(cons e more) - (when (and DEBUG-BINDINGS? - (identifier? e)) - (display-ctx-bindings def-ctx) - (printf "expanding ~a\n" (syntax-debug-info e))) - (define e- (local-expand e (list unique) (list #'erased #'begin) def-ctx)) - (syntax-parse e- - #:literals (begin) - [(begin e ...) - (loop (append (syntax->list #'(e ...)) more) - rev-e-... - rev-τ... - ep-effects - facet-effects - spawn-effects)] - [_ - (define τ (syntax-property e- ':)) - (define-values (ep-effs f-effs s-effs) - (values (syntax->list (get-effect e- 'ν-ep)) - (syntax->list (get-effect e- 'ν-f)) - (syntax->list (get-effect e- 'ν-s)))) - (add-bindings-to-ctx e- def-ctx) - (loop more - (cons e- rev-e-...) - (cons τ rev-τ...) - (append ep-effs ep-effects) - (append f-effs facet-effects) - (append s-effs spawn-effects))])]))) - (values (reverse rev-e-...) - (reverse rev-τ...) - ep-effects - facet-effects - spawn-effects)) - (define-typed-syntax (start-facet name:id ep ...+) ≫ #:with name- (syntax-local-identifier-as-binding (syntax-local-introduce (generate-temporary #'name))) #:with name+ (syntax-local-identifier-as-binding #'name) @@ -1256,11 +113,6 @@ (⇒ : ★/t) (⇒ ν-ep (MF))]) -(define-syntax (field/intermediate stx) - (syntax-parse stx - [(_ [x:id x-:id τ e-] ...) - #'(syndicate:field [x- e-] ...)])) - (define-typed-syntax (assert e:expr) ≫ [⊢ e ≫ e- (⇒ : τ)] #:fail-unless (pure? #'e-) "expression not allowed to have effects" @@ -1498,17 +350,6 @@ ------------------------ [⊢ (x-) (⇒ : τ)]) -(define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫ - [[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e) - (⇒ ν-ep (~effs τ-ep ...)) - (⇒ ν-s (~effs τ-s ...)) - (⇒ ν-f (~effs τ-f ...))] - ---------------------------------------- - [⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e) - (Endpoints τ-ep ...) - (Roles τ-f ...) - (Spawns τ-s ...))))]) - (define-typed-syntax (typed-app e_fn e_arg ...) ≫ [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in ... (~Computation (~Value τ-out) (~Endpoints τ-ep ...) @@ -1592,53 +433,6 @@ ------------------------------------------------ [⊢ e- (⇒ : τ.norm) ]) -(define-syntax (define/intermediate stx) - (syntax-parse stx - [(_ x:id x-:id τ e) - ;; including a syntax binding for x allows for module-top-level references - ;; (where walk/bind won't replace further uses) and subsequent provides - #'(begin- - (define-syntax x - (make-variable-like-transformer (add-orig (assign-type #'x- #'τ #:wrap? #f) #'x))) - (define- x- e))])) - -;; copied from ext-stlc -(define-typed-syntax define - [(_ x:id (~datum :) τ:type e:expr) ≫ - [⊢ e ≫ e- ⇐ τ.norm] - #:fail-unless (pure? #'e-) "expression must be pure" - #:with x- (generate-temporary #'x) - #:with x+ (syntax-local-identifier-as-binding #'x) - -------- - [⊢ (define/intermediate x+ x- τ.norm e-) (⇒ : ★/t)]] - [(_ x:id e) ≫ - ;This won't work with mutually recursive definitions - [⊢ e ≫ e- ⇒ τ] - #:fail-unless (pure? #'e-) "expression must be pure" - #:with x- (generate-temporary #'x) - #:with x+ (syntax-local-identifier-as-binding #'x) - -------- - [⊢ (define/intermediate x+ x- τ e-) (⇒ : ★/t)]] - [(_ (f [x (~optional (~datum :)) ty:type] ... - (~or (~datum →) (~datum ->)) ty_out:type) - e ...+) ≫ - [⊢ (lambda ([x : ty] ...) (begin e ...)) ≫ e- (⇒ : (~and fun-ty - (~→ (~not (~Computation _ ...)) ... - (~Computation (~Value τ-v) - _ ...))))] - #:fail-unless (<: #'τ-v #'ty_out.norm) - (format "expected different return type\n got ~a\n expected ~a\n" - #'τ-v #'ty_out - #;(type->str #'τ-v) - #;(type->str #'ty_out)) - #:with f- (add-orig (generate-temporary #'f) #'f) - -------- - [⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]] - [(_ (f [x (~optional (~datum :)) ty] ...) - e ...+) ≫ - ---------------------------- - [≻ (define (f [x ty] ... -> ★/t) e ...)]]) - ;; copied from ext-stlc (define-typed-syntax if [(_ e_tst e1 e2) ⇐ τ-expected ≫ @@ -1675,17 +469,6 @@ ------------------------------------ [≻ (if e #f (begin s ...))]) - -(define-typed-syntax begin - [(_ e_unit ... e) ≫ - #:do [(define-values (e-... τ... ep-effs f-effs s-effs) (walk/bind #'(e_unit ... e)))] - #:with τ (last τ...) - -------- - [⊢ (begin- #,@e-...) (⇒ : τ) - (⇒ ν-ep (#,@ep-effs)) - (⇒ ν-f (#,@f-effs)) - (⇒ ν-s (#,@s-effs))]]) - ;; copied from ext-stlc (define-typed-syntax let [(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫ @@ -1874,186 +657,6 @@ ---------------------------------- [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))]) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Lists -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-typed-syntax (list e ...) ≫ - [⊢ e ≫ e- ⇒ τ] ... - #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" - ------------------- - [⊢ (list- e- ...) ⇒ (List (U τ ...))]) - -(define-typed-syntax (cons e1 e2) ≫ - [⊢ e1 ≫ e1- ⇒ τ1] - #:fail-unless (pure? #'e1-) "expression must be pure" - [⊢ e2 ≫ e2- ⇒ (~List τ2)] - #:fail-unless (pure? #'e2-) "expression must be pure" - #:with τ-l (type-eval #'(List (U τ1 τ2))) - ---------------------------------------- - [⊢ (cons- e1- e2-) ⇒ τ-l]) - -(define-typed-syntax (for/fold [acc:id e-acc] - [x:id e-list] - e-body ...+) ≫ - [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] - #:fail-unless (pure? #'e-list-) "expression must be pure" - [⊢ e-acc ≫ e-acc- ⇒ τ-a] - #:fail-unless (pure? #'e-acc-) "expression must be pure" - [[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ (begin e-body ...) ≫ e-body- ⇒ τ-b] - #:fail-unless (pure? #'e-body-) "body must be pure" - #:fail-unless (<: #'τ-b #'τ-a) - "loop body doesn't match accumulator" - ------------------------------------------------------- - [⊢ (for/fold- ([acc- e-acc-]) - ([x- (in-list- e-list-)]) - e-body-) - ⇒ τ-b]) - -(define-typed-syntax (for ([x:id e-list] ...) - e-body ...+) ≫ - [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ... - #:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure" - [[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b) - (⇒ ν-ep (~effs eps ...)) - (⇒ ν-f (~effs fs ...)) - (⇒ ν-s (~effs ss ...))] - ------------------------------------------------------- - [⊢ (for- ([x- (in-list- e-list-)] ...) - e-body-) (⇒ : ★/t) - (⇒ ν-ep (eps ...)) - (⇒ ν-f (fs ...)) - (⇒ ν-s (ss ...))]) - -(define-typed-syntax (empty? e) ≫ - [⊢ e ≫ e- ⇒ (~List _)] - #:fail-unless (pure? #'e-) "expression must be pure" - ----------------------- - [⊢ (empty?- e-) ⇒ Bool]) - -(define-typed-syntax (first e) ≫ - [⊢ e ≫ e- ⇒ (~List τ)] - #:fail-unless (pure? #'e-) "expression must be pure" - ----------------------- - [⊢ (first- e-) ⇒ τ]) - -(define-typed-syntax (rest e) ≫ - [⊢ e ≫ e- ⇒ (~List τ)] - #:fail-unless (pure? #'e-) "expression must be pure" - ----------------------- - [⊢ (rest- e-) ⇒ (List τ)]) - -(define-typed-syntax (member? e l) ≫ - [⊢ e ≫ e- ⇒ τe] - #:fail-unless (pure? #'e-) "expression must be pure" - [⊢ l ≫ l- ⇒ (~List τl)] - #:fail-unless (pure? #'l-) "expression must be pure" - #:fail-unless (<: #'τe #'τl) "incompatible list" - ---------------------------------------- - [⊢ (member?- e- l-) ⇒ Bool]) - -(define- (member?- v l) - (and- (member- v l) #t)) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Sets -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(define-typed-syntax (set e ...) ≫ - [⊢ e ≫ e- ⇒ τ] ... - #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" - --------------- - [⊢ (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]) - -(define-typed-syntax (set-add st v) ≫ - [⊢ st ≫ st- ⇒ (~Set τs)] - #:fail-unless (pure? #'st-) "expression must be pure" - [⊢ v ≫ v- ⇒ τv] - #:fail-unless (pure? #'v-) "expression must be pure" - ------------------------- - [⊢ (set-add- st- v-) ⇒ (Set (U τs τv))]) - -(define-typed-syntax (set-remove st v) ≫ - [⊢ st ≫ st- ⇒ (~Set τs)] - #:fail-unless (pure? #'st-) "expression must be pure" - [⊢ v ≫ v- ⇐ τs] - #:fail-unless (pure? #'v-) "expression must be pure" - ------------------------- - [⊢ (set-remove- st- v-) ⇒ (Set τs)]) - -(define-typed-syntax (set-member? st v) ≫ - [⊢ st ≫ st- ⇒ (~Set τs)] - #:fail-unless (pure? #'st-) "expression must be pure" - [⊢ v ≫ v- ⇒ τv] - #:fail-unless (pure? #'v-) "expression must be pure" - #:fail-unless (<: #'τv #'τs) - "type mismatch" - ------------------------------------- - [⊢ (set-member?- st- v-) ⇒ Bool]) - -(define-typed-syntax (set-union st0 st ...) ≫ - [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] - #:fail-unless (pure? #'st0-) "expression must be pure" - [⊢ st ≫ st- ⇒ (~Set τ-st)] ... - #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" - ------------------------------------- - [⊢ (set-union- st0- st- ...) ⇒ (Set (U τ-st0 τ-st ...))]) - -(define-typed-syntax (set-intersect st0 st ...) ≫ - [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] - #:fail-unless (pure? #'st0-) "expression must be pure" - [⊢ st ≫ st- ⇒ (~Set τ-st)] ... - #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" - #:with τr (∩ #'τ-st0 (type-eval #'(U τ-st ...))) - ------------------------------------- - [⊢ (set-intersect- st0- st- ...) ⇒ (Set τr)]) - -(define-typed-syntax (set-subtract st0 st ...) ≫ - [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] - #:fail-unless (pure? #'st0-) "expression must be pure" - [⊢ st ≫ st- ⇒ (~Set _)] ... - #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" - ------------------------------------- - [⊢ (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 τ)]) - -(define-typed-syntax (set->list s) ≫ - [⊢ s ≫ s- ⇒ (~Set τ)] - #:fail-unless (pure? #'s-) "expression must be pure" - ----------------------- - [⊢ (set->list- s-) ⇒ (List τ)]) - -(module+ test - (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"))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Tests ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/set.rkt b/racket/typed/set.rkt new file mode 100644 index 0000000..d96e61e --- /dev/null +++ b/racket/typed/set.rkt @@ -0,0 +1,124 @@ +#lang turnstile + +(provide Set + (for-syntax ~Set) + set + set-member? + set-add + set-remove + set-count + set-union + set-subtract + set-intersect + list->set + set->list) + +(require "core-types.rkt") +(require (only-in "list.rkt" ~List)) + +(require (postfix-in - racket/set)) + +(module+ test + (require rackunit) + (require rackunit/turnstile)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Sets +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-container-type Set #:arity = 1) + +(define-typed-syntax (set e ...) ≫ + [⊢ e ≫ e- ⇒ τ] ... + #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure" + --------------- + [⊢ (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]) + +(define-typed-syntax (set-add st v) ≫ + [⊢ st ≫ st- ⇒ (~Set τs)] + #:fail-unless (pure? #'st-) "expression must be pure" + [⊢ v ≫ v- ⇒ τv] + #:fail-unless (pure? #'v-) "expression must be pure" + ------------------------- + [⊢ (set-add- st- v-) ⇒ (Set (U τs τv))]) + +(define-typed-syntax (set-remove st v) ≫ + [⊢ st ≫ st- ⇒ (~Set τs)] + #:fail-unless (pure? #'st-) "expression must be pure" + [⊢ v ≫ v- ⇐ τs] + #:fail-unless (pure? #'v-) "expression must be pure" + ------------------------- + [⊢ (set-remove- st- v-) ⇒ (Set τs)]) + +(define-typed-syntax (set-member? st v) ≫ + [⊢ st ≫ st- ⇒ (~Set τs)] + #:fail-unless (pure? #'st-) "expression must be pure" + [⊢ v ≫ v- ⇒ τv] + #:fail-unless (pure? #'v-) "expression must be pure" + #:fail-unless (<: #'τv #'τs) + "type mismatch" + ------------------------------------- + [⊢ (set-member?- st- v-) ⇒ Bool]) + +(define-typed-syntax (set-union st0 st ...) ≫ + [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] + #:fail-unless (pure? #'st0-) "expression must be pure" + [⊢ st ≫ st- ⇒ (~Set τ-st)] ... + #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" + ------------------------------------- + [⊢ (set-union- st0- st- ...) ⇒ (Set (U τ-st0 τ-st ...))]) + +(define-typed-syntax (set-intersect st0 st ...) ≫ + [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] + #:fail-unless (pure? #'st0-) "expression must be pure" + [⊢ st ≫ st- ⇒ (~Set τ-st)] ... + #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" + #:with τr (∩ #'τ-st0 (type-eval #'(U τ-st ...))) + ------------------------------------- + [⊢ (set-intersect- st0- st- ...) ⇒ (Set τr)]) + +(define-typed-syntax (set-subtract st0 st ...) ≫ + [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)] + #:fail-unless (pure? #'st0-) "expression must be pure" + [⊢ st ≫ st- ⇒ (~Set _)] ... + #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure" + ------------------------------------- + [⊢ (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 τ)]) + +(define-typed-syntax (set->list s) ≫ + [⊢ s ≫ s- ⇒ (~Set τ)] + #:fail-unless (pure? #'s-) "expression must be pure" + ----------------------- + [⊢ (set->list- s-) ⇒ (List τ)]) + +#;(module+ test + (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")))