syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

work towards using typedefs, debugging

This commit is contained in:
Sam Caldwell 2020-09-17 15:11:34 -04:00
parent 8d6a037841
commit 0a8e400f63
2 changed files with 142 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

185
racket/typed/core-types.rkt
View File

@ -1,11 +1,13 @@
#lang turnstile #lang turnstile
(provide (except-out (all-defined-out) → ∀) (provide (except-out (all-defined-out) → ∀ Role)
(rename-out [→+ →] (rename-out [→+ →]
[∀+ ∀]) [∀+ ∀]
(for-syntax (except-out (all-defined-out) ~→ ~∀) [Role+Body Role])
(for-syntax (except-out (all-defined-out) ~→ ~∀ ~Role)
(rename-out [~→+ ~→] (rename-out [~→+ ~→]
[~∀+ ~∀])) [~∀+ ~∀]
[~Role+Body ~Role]))
(for-meta 2 (all-defined-out))) (for-meta 2 (all-defined-out)))
(require (only-in turnstile (require (only-in turnstile
[define-type-constructor define-type-constructor-] [define-type-constructor define-type-constructor-]
@ -15,13 +17,15 @@
(require turnstile/typedefs) (require turnstile/typedefs)
(begin-for-syntax (begin-for-syntax
;; turnstile/typedefs sets it to #t, which breaks things ;; turnstile/typedefs sets it to #t, which breaks things
(current-use-stop-list? #t)) (current-use-stop-list? #f))
(require (prefix-in syndicate: syndicate/actor-lang)) (require (prefix-in syndicate: syndicate/actor-lang))
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base)) (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 turnstile/examples/util/filter-maximal))
(require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) (require (for-syntax (prefix-in ttc: turnstile/type-constraints)
(prefix-in mtc: macrotypes/type-constraints)
(prefix-in mvc: macrotypes/variance-constraints)))
#;(require (only-in (for-syntax macrotypes/typecheck-core) get-orig)) #;(require (only-in (for-syntax macrotypes/typecheck-core) get-orig))
(require (for-syntax racket/struct-info (require (for-syntax racket/struct-info
syntax/id-table)) syntax/id-table))
@ -76,7 +80,10 @@
(define (un- id) (define (un- id)
(define match? (define match?
(regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id)))) (regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
(string->symbol (second match?))) (if match?
(string->symbol (second match?))
(begin (printf "no match! ~a\n" id)
match?)))
;; Identifier -> (U #f type-metadata) ;; Identifier -> (U #f type-metadata)
(define (get-type-info ty-cons) (define (get-type-info ty-cons)
@ -224,24 +231,11 @@
(define (new-type? t) (define (new-type? t)
(or (type?- t) (or (type?- t)
(Type? (detach t ':)))) (Type? (detach t ':))))
#;(require racket/trace)
#;(trace new-type?)
(current-type? new-type?)) (current-type? new-type?))
(begin-for-syntax
;; won't work for binding types
(define-syntax ~Any/new
(pattern-expander
(syntax-parser
[(_ tycons . rst)
#'((~literal #%plain-app)
tycons
(~and
(~or* (~seq ty (... ...) ((~literal #%plain-app) (~literal list) . more-tys))
(~seq ty (... ...)))
(~parse rst (if (attribute more-tys)
#'(ty (... ...) . more-tys)
#'(ty (... ...))))))]))))
(begin-for-syntax (begin-for-syntax
(define-generic-type-method get-arg-variances-data #:default #f) (define-generic-type-method get-arg-variances-data #:default #f)
(define-generic-type-method get-extra-info-data #:default #f) (define-generic-type-method get-extra-info-data #:default #f)
@ -318,9 +312,15 @@
(define-simple-macro (define-base-types Name:id ...) (define-simple-macro (define-base-types Name:id ...)
(begin- (define-base-type Name) ...)) (begin- (define-base-type Name) ...))
(define-base-types Discard ★/t)
(define-type FacetName : FacetName)
#;(define-type-constructor? Shares #:arity = 1) #;(define-type-constructor? Shares #:arity = 1)
(define-binding-type Role #:arity >= 0 #:bvs = 1) #;(define-binding-type Role #:arity >= 0 #:bvs = 1)
(define-type Role #:with-binders [X : FacetName] : Type -> Type)
(define-type RoleBody : Type * -> Type)
(define-type-constructor Shares #:arity = 1) (define-type-constructor Shares #:arity = 1)
(define-type-constructor Sends #:arity = 1) (define-type-constructor Sends #:arity = 1)
(define-type-constructor Realizes #:arity = 1) (define-type-constructor Realizes #:arity = 1)
@ -330,7 +330,8 @@
(define-type-constructor Know #:arity = 1) (define-type-constructor Know #:arity = 1)
(define-type-constructor Forget #:arity = 1) (define-type-constructor Forget #:arity = 1)
(define-product-type Realize #:arity = 1) (define-product-type Realize #:arity = 1)
(define-type-constructor Stop #:arity >= 1) #;(define-type-constructor Stop #:arity >= 1)
(define-type Stop : FacetName Type * -> Type)
(define-type-constructor Field #:arity = 1) (define-type-constructor Field #:arity = 1)
(define-type-constructor Bind #:arity = 1) (define-type-constructor Bind #:arity = 1)
;; keep track of branches for facet effects ;; keep track of branches for facet effects
@ -392,6 +393,21 @@
TY TY
(~parse (vars-pat ty-pat) (flatten-∀ #'TY)))])))) (~parse (vars-pat ty-pat) (flatten-∀ #'TY)))]))))
(define-simple-macro (Role+Body (x:id) ty ...)
(Role (x : FacetName)
(RoleBody ty ...)))
(begin-for-syntax
(define-syntax ~Role+Body
(pattern-expander
(syntax-parser
[(_ var-pat . ty-pat)
(syntax/loc this-syntax
(~and (~Role (internal-name : _)
(~RoleBody . tys))
(~parse var-pat #'(internal-name))
(~parse ty-pat #'tys)))]))))
;; for describing the RHS ;; for describing the RHS
;; a value and a description of the effects ;; a value and a description of the effects
@ -402,7 +418,6 @@
(define-type-constructor Spawns #:arity >= 0) (define-type-constructor Spawns #:arity >= 0)
(define-base-types Discard ★/t FacetName)
(define-for-syntax (type-eval t) (define-for-syntax (type-eval t)
((current-type-eval) t)) ((current-type-eval) t))
@ -415,15 +430,17 @@
;; (copied from ext-stlc example) ;; (copied from ext-stlc example)
(define-syntax define-type-alias (define-syntax define-type-alias
(syntax-parser (syntax-parser
[(_ alias:id τ) [(_ alias:id τ:type)
#:with kind (detach #'τ.norm ':)
#'(define-syntax- alias #'(define-syntax- alias
(make-variable-like-transformer #'τ))] (make-variable-like-transformer (attach #'τ ': #'kind)))]
[(_ (f:id x:id ...) ty) [(_ (f:id x:id ...) ty)
#'(define-syntax- (f stx) #'(define-syntax- (f stx)
(syntax-parse stx (syntax-parse stx
[(_ x ...) [(_ x ...)
#:with τ:any-type #'ty #'ty
#'τ.norm]))])) ;; #:with τ:any-type #'ty
#;#'τ.norm]))]))
(define-type-alias ⊥ (U*)) (define-type-alias ⊥ (U*))
(define-type-alias Unit (Tuple)) (define-type-alias Unit (Tuple))
@ -686,7 +703,7 @@
#'(~and it #'(~and it
(~fail #:unless (user-defined-type? #'it)) (~fail #:unless (user-defined-type? #'it))
(~parse tag (get-type-tag #'it)) (~parse tag (get-type-tag #'it))
(~Any _ . rst))]))) (~Any/new _ . rst))])))
(define-syntax ~constructor-exp (define-syntax ~constructor-exp
(pattern-expander (pattern-expander
@ -756,11 +773,25 @@
#:datum-literals (:) #:datum-literals (:)
[(_ lib [name:id : ty:type] ...) [(_ lib [name:id : ty:type] ...)
#:with (name- ...) (format-ids "~a-" #'(name ...)) #:with (name- ...) (format-ids "~a-" #'(name ...))
#:with (kind ...) (for/list ([t (in-syntax #'(ty.norm ...))])
(detach t ':))
(define nm1 (syntax-e (first (syntax->list #'(name ...)))))
(define kind1 (first (syntax->list #'(kind ...))))
(when (equal? nm1 'identity)
(printf "require/typed: ~a\n" nm1)
(syntax-parse kind1
[(~Base t)
(define t-i (syntax-local-introduce #'t))
(pretty-print (syntax-debug-info t-i))
(pretty-print (identifier-binding t-i))]))
(syntax/loc stx (syntax/loc stx
(begin- (begin-
(require (only-in lib [name name-] ...)) (require (only-in lib [name name-] ...))
(define-syntax name (define-syntax name
(make-variable-like-transformer (add-orig (assign-type #'name- #'ty #:wrap? #f) #'name))) (make-variable-like-transformer
(add-orig (assign-type #'name-
(attach #'ty ': ((current-type-eval) #'Type))
#:wrap? #f) #'name)))
...))])) ...))]))
;; Format identifiers in the same way ;; Format identifiers in the same way
@ -843,9 +874,9 @@
(define-for-syntax (flat-type? τ) (define-for-syntax (flat-type? τ)
(syntax-parse τ (syntax-parse τ
[(~→+ τ ...) #f] [(~→+ i ... o) #f]
[(~Actor τ) #f] [(~Actor τ) #f]
[(~Role (_) _ ...) #f] [(~Role+Body (_) _ ...) #f]
[_ #t])) [_ #t]))
(define-for-syntax (strip-? t) (define-for-syntax (strip-? t)
@ -906,7 +937,7 @@
;; Wanted test case, but can't use it bc it uses things defined for-syntax ;; Wanted test case, but can't use it bc it uses things defined for-syntax
#;(module+ test #;(module+ test
(let ([r (type-eval #'(Role (x) (Shares Int)))]) (let ([r (type-eval #'(Role+Body (x) (Shares Int)))])
(syntax-parse (analyze-role-input/output r) (syntax-parse (analyze-role-input/output r)
[(τ-i τ-o) [(τ-i τ-o)
(check-true (type=? #'τ-o (type-eval #'Int)))]))) (check-true (type=? #'τ-o (type-eval #'Int)))])))
@ -928,13 +959,13 @@
(values bot (mk-Message- #'(τ-m)) bot bot bot)] (values bot (mk-Message- #'(τ-m)) bot bot bot)]
[(~Realizes τ-m) [(~Realizes τ-m)
(values bot bot bot (mk-Realize- #'(τ-m)) bot)] (values bot bot bot (mk-Realize- #'(τ-m)) bot)]
[(~Role (name:id) [(~Role+Body (name:id)
(~or (~Shares τ-s) (~or (~Shares τ-s)
(~Know τ-k) (~Know τ-k)
(~Sends τ-m) (~Sends τ-m)
(~Realizes τ-rlz) (~Realizes τ-rlz)
(~Reacts τ-if τ-then ...)) ... (~Reacts τ-if τ-then ...)) ...
(~and (~Role _ ...) sub-role) ...) (~and (~Role+Body _ _ ...) sub-role) ...)
#:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))]) #:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))])
(mk-Message- (list m))) (mk-Message- (list m)))
#:with (rlz ...) (for/list ([r (in-syntax #'(τ-rlz ...))]) #:with (rlz ...) (for/list ([r (in-syntax #'(τ-rlz ...))])
@ -1026,6 +1057,18 @@
(paren-join (cons "U" (stx-map type->strX #'(τ ...))))] (paren-join (cons "U" (stx-map type->strX #'(τ ...))))]
[(~Base x) [(~Base x)
(un-gensym #'x)] (un-gensym #'x)]
[(~Role+Body (x:id) τ ...)
(define nm (un-gensym #'x))
(define body (stx-map type->strX #'(τ ...)))
(paren-join (list* "Role" (format "(~a)" nm) body))]
[(~∀+ (X ...) τ)
(define vars
(paren-join (stx-map type->strX #'(X ...))))
(paren-join (list "∀" vars (type->strX #'τ)))]
[(~Any/new τ-cons τ ...)
(define ctor (un-gensym #'τ-cons))
(define body (stx-map type->strX #'(τ ...)))
(paren-join (cons ctor body))]
[(~Any/bvs τ-cons (X ...) τ ...) [(~Any/bvs τ-cons (X ...) τ ...)
(define ctor (un-gensym #'τ-cons)) (define ctor (un-gensym #'τ-cons))
(define body (stx-map type->strX #'(τ ...))) (define body (stx-map type->strX #'(τ ...)))
@ -1059,7 +1102,7 @@
(flat-type? t1)] (flat-type? t1)]
[((~U* τ1 ...) _) [((~U* τ1 ...) _)
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))] (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
[(_ (~U* τ2:type ...)) [(_ (~U* τ2 ...))
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))] (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
[((~Actor τ1) (~Actor τ2)) [((~Actor τ1) (~Actor τ2))
(and (<: #'τ1 #'τ2) (and (<: #'τ1 #'τ2)
@ -1083,9 +1126,13 @@
#t] #t]
[(X:id Y:id) [(X:id Y:id)
(or (free-identifier=? #'X #'Y) (or (free-identifier=? #'X #'Y)
(let () #;(let ()
#;(displayln (identifier-binding #'X)) (printf "X:\n")
#;(displayln (identifier-binding #'Y)) (pretty-print (syntax-debug-info (values #;syntax-local-introduce #'X)))
(pretty-print (identifier-binding #'X))
(printf ":\n")
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'Y)))
(pretty-print (identifier-binding #'Y))
#f))] #f))]
[((~∀+ (X:id ...) τ1) (~∀+ (Y:id ...) τ2)) [((~∀+ (X:id ...) τ1) (~∀+ (Y:id ...) τ2))
#:when (stx-length=? #'(X ...) #'(Y ...)) #:when (stx-length=? #'(X ...) #'(Y ...))
@ -1094,8 +1141,16 @@
;; (displayln #'τ2-X/Y)] ;; (displayln #'τ2-X/Y)]
(<: #'τ1 #'τ2-X/Y)] (<: #'τ1 #'τ2-X/Y)]
[((~Base τ1:id) (~Base τ2:id)) [((~Base τ1:id) (~Base τ2:id))
(free-identifier=? #'τ1 #'τ2)] (or (free-identifier=? #'τ1 #'τ2)
[((~Role (x) _ ...) (~Role (y) _ ...)) (let ()
(printf "τ1:\n")
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ1)))
(pretty-print (identifier-binding #'τ1))
(printf "τ2:\n")
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ2)))
(pretty-print (identifier-binding #'τ2))
#f))]
[((~Role+Body (x) _ ...) (~Role+Body (y) _ ...))
;; Extremely Coarse subtyping for Role types ;; Extremely Coarse subtyping for Role types
(type=? t1 t2)] (type=? t1 t2)]
;; TODO: clauses for Roles, effectful functions, and so on ;; TODO: clauses for Roles, effectful functions, and so on
@ -1118,7 +1173,7 @@
[(== irrelevant) [(== irrelevant)
#t]))] #t]))]
[_ [_
#f])) (type=? t1 t2)]))
;; shortcuts for mapping ;; shortcuts for mapping
(define ((<:l l) r) (define ((<:l l) r)
@ -1132,7 +1187,8 @@
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
(begin-for-syntax (begin-for-syntax
(current-typecheck-relation <:)) (current-typecheck-relation <:)
(current-check-relation <:))
;; Flat-Type Flat-Type -> Type ;; Flat-Type Flat-Type -> Type
;; Intersection ;; Intersection
@ -1305,6 +1361,10 @@
(and (flat-type? ty) (and (flat-type? ty)
(finite? ty)))) (finite? ty))))
#;(begin-for-syntax
(require racket/trace)
(trace instantiable?))
(begin-for-syntax (begin-for-syntax
;; CONVENTION: Type variables for effects are prefixed with ρ ;; CONVENTION: Type variables for effects are prefixed with ρ
(define (row-variable? x) (define (row-variable? x)
@ -1431,15 +1491,17 @@
[(_ [x:id x-:id τ e-] ...) [(_ [x:id x-:id τ e-] ...)
#'(syndicate:field [x- e-] ...)])) #'(syndicate:field [x- e-] ...)]))
(define-for-syntax KIND-TAG ':)
(define-syntax (define/intermediate stx) (define-syntax (define/intermediate stx)
(syntax-parse stx (syntax-parse stx
[(_ x:id x-:id τ e) [(_ x:id x-:id τ e)
;; including a syntax binding for x allows for module-top-level references ;; including a syntax binding for x allows for module-top-level references
;; (where walk/bind won't replace further uses) and subsequent provides ;; (where walk/bind won't replace further uses) and subsequent provides
#:with kind (detach #'τ ':)
#'(begin- #'(begin-
(define-syntax x (define-syntax x
(make-variable-like-transformer (add-orig (attach #'x- ': #'τ) #'x))) (make-variable-like-transformer (add-orig (attach #'x- ': (attach #'τ ': #'kind)) #'x)))
(define- x- e))])) (define- x- e))]))
;; copied from ext-stlc ;; copied from ext-stlc
@ -1569,13 +1631,13 @@
;; solve for type variables Xs ;; solve for type variables Xs
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax) #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
;; make sure types are legal ;; make sure types are legal
#:with tyXs (inst-types/cs #'Xs* #'cs #'Xs) #:with tyXs (ttc:inst-types/cs #'Xs* #'cs #'Xs)
#:fail-unless (for/and ([ty (in-syntax #'tyXs)] #:fail-unless (for/and ([ty (in-syntax #'tyXs)]
[x (in-syntax #'Xs)]) [x (in-syntax #'Xs)])
(instantiable? x ty)) (instantiable? x ty))
"type variables must be flat and finite" "type variables must be flat and finite"
;; instantiate polymorphic function type ;; instantiate polymorphic function type
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) #:with [τ_in ... τ_out] (ttc:inst-types/cs #'Xs* #'cs #'tyX_args)
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
;; arity check ;; arity check
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
@ -1665,7 +1727,7 @@
((current-type-eval) (get-expected-type stx))) ((current-type-eval) (get-expected-type stx)))
(define initial-cs (define initial-cs
(if (and (syntax-e #'expected-ty) (stx-null? #'Vs)) (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
(add-constraints Xs '() (list (list #'expected-ty #'τ_outX))) (ttc:add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
'())) '()))
(syntax-parse stx (syntax-parse stx
[(_ e_fn . args) [(_ e_fn . args)
@ -1673,7 +1735,7 @@
(for/fold ([as- null] [cs initial-cs]) (for/fold ([as- null] [cs initial-cs])
([a (in-stx-list #'args)] ([a (in-stx-list #'args)]
[tyXin (in-stx-list #'(τ_inX ...))]) [tyXin (in-stx-list #'(τ_inX ...))])
(define ty_in (inst-type/cs/orig Xs cs tyXin datum=?)) (define ty_in (ttc:inst-type/cs/orig Xs cs tyXin datum=?))
(when (tyvar-under-union? Xs ty_in) (when (tyvar-under-union? Xs ty_in)
(type-error #:src a (type-error #:src a
#:msg (format "can't infer types with unions: ~a\nraw: ~a" #:msg (format "can't infer types with unions: ~a\nraw: ~a"
@ -1688,8 +1750,8 @@
(type->str #'ty_a) #'ty_a))) (type->str #'ty_a) #'ty_a)))
(values (values
(cons #'a- as-) (cons #'a- as-)
(add-constraints Xs cs (list (list ty_in #'ty_a)) (ttc:add-constraints Xs cs (list (list ty_in #'ty_a))
(list (list (inst-type/cs/orig (list (list (ttc:inst-type/cs/orig
Xs cs ty_in Xs cs ty_in
datum=?) datum=?)
#'ty_a)))))) #'ty_a))))))
@ -1739,9 +1801,9 @@
(for/list ([X (in-list Xs)]) (for/list ([X (in-list Xs)])
(cond [(free-identifier=? X #'A) ctxt-variance] (cond [(free-identifier=? X #'A) ctxt-variance]
[else irrelevant]))] [else irrelevant]))]
[(~Any tycons) [(~Any/new tycons)
(stx-map (λ _ irrelevant) Xs)] (stx-map (λ _ irrelevant) Xs)]
[(~?∀ () (~Any tycons τ ...)) [(~?∀ () (~Any/new tycons τ ...))
#:when (get-arg-variances #'tycons) #:when (get-arg-variances #'tycons)
#:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons)) #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
(define τ-ctxt-variances (define τ-ctxt-variances
@ -1750,7 +1812,7 @@
(for/fold ([acc (stx-map (λ _ irrelevant) Xs)]) (for/fold ([acc (stx-map (λ _ irrelevant) Xs)])
([τ (in-stx-list #'[τ ...])] ([τ (in-stx-list #'[τ ...])]
[τ-ctxt-variance (in-list τ-ctxt-variances)]) [τ-ctxt-variance (in-list τ-ctxt-variances)])
(map variance-join (map mvc:variance-join
acc acc
(find-variances Xs τ τ-ctxt-variance)))] (find-variances Xs τ τ-ctxt-variance)))]
[ty [ty
@ -1758,3 +1820,18 @@
(stx-contains-id? #'ty X))) (stx-contains-id? #'ty X)))
(stx-map (λ _ irrelevant) Xs)] (stx-map (λ _ irrelevant) Xs)]
[_ (stx-map (λ _ invariant) Xs)]))) [_ (stx-map (λ _ invariant) Xs)])))
#;(begin-for-syntax
(define t #'Unit)
(define t- ((current-type-eval) t))
(displayln ((current-type?) t-))
(define tt (syntax-parse (detach t- ':)
[(#%plain-app x) #'x]))
(pretty-print (syntax-debug-info tt)))
#;(begin-for-syntax
(define t #'(→ Unit Unit))
#;(define t #'(Actor Unit))
(define t- ((current-type-eval) t))
(values #;displayln ((current-type?) t-))
(printf "flat-type? ~a\n" (flat-type? t-)))

15
racket/typed/roles.rkt
View File

@ -14,7 +14,7 @@
Branch Effs Branch Effs
FacetName Field ★/t FacetName Field ★/t
Observe Inbound Outbound Actor U ⊥ Observe Inbound Outbound Actor U ⊥
Computation Value Endpoints Roles Spawns Computation Value Endpoints Roles Spawns Sends
→fn proc →fn proc
;; Statements ;; Statements
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
@ -84,6 +84,7 @@
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base)) (require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
(require macrotypes/postfix-in) (require macrotypes/postfix-in)
(require (for-syntax turnstile/mode)) (require (for-syntax turnstile/mode))
(require turnstile/typedefs)
(require (postfix-in - racket/list)) (require (postfix-in - racket/list))
(require (postfix-in - racket/set)) (require (postfix-in - racket/set))
@ -139,7 +140,7 @@
(~and τ-k (~Know _)) (~and τ-k (~Know _))
;; untyped syndicate might allow this - TODO ;; untyped syndicate might allow this - TODO
#;(~and τ-m (~Sends _)) #;(~and τ-m (~Sends _))
(~and τ-r (~Reacts _ ...)) (~and τ-r (~Reacts _ _ ...))
~MakesField) ~MakesField)
...) ...)
ep-effects ep-effects
@ -204,7 +205,7 @@
(⇒ ν-ep (~effs)) (⇒ ν-ep (~effs))
(⇒ ν-s (~effs)) (⇒ ν-s (~effs))
(⇒ ν-f (~effs τ-f ...))] (⇒ ν-f (~effs τ-f ...))]
#:with τ (mk-Stop- #`(facet-name- τ-f ...)) #:with τ #'(Stop facet-name- τ-f ...)
--------------------------------------------------------------------------------- ---------------------------------------------------------------------------------
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t) [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
(⇒ ν-f (τ))]) (⇒ ν-f (τ))])
@ -450,7 +451,7 @@
#'τ] #'τ]
[(~U* τ ...) [(~U* τ ...)
(mk-U- (stx-map instantiate-pattern-type #'(τ ...)))] (mk-U- (stx-map instantiate-pattern-type #'(τ ...)))]
[(~Any/bvs τ-cons () τ ...) [(~Any/new τ-cons τ ...)
#:when (reassemblable? #'τ-cons) #:when (reassemblable? #'τ-cons)
(define subitems (for/list ([t (in-syntax #'(τ ...))]) (define subitems (for/list ([t (in-syntax #'(τ ...))])
(instantiate-pattern-type t))) (instantiate-pattern-type t)))
@ -609,6 +610,12 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(module+ test (module+ test
(check-type
(spawn (U (Observe (Tuple Int ★/t)))
(start-facet echo
(on (message (tuple 1 $x))
#f)))
: ★/t)
(check-type (spawn (U (Message (Tuple String Int)) (check-type (spawn (U (Message (Tuple String Int))
(Observe (Tuple String ★/t))) (Observe (Tuple String ★/t)))
(start-facet echo (start-facet echo