diff --git a/racket/typed/examples/chat-tcp2.rkt b/racket/typed/examples/chat-tcp2.rkt index 913bf7d..9e9112c 100644 --- a/racket/typed/examples/chat-tcp2.rkt +++ b/racket/typed/examples/chat-tcp2.rkt @@ -26,8 +26,7 @@ (spawn chat-ds (start-facet chat-server - ;; TODO - should be during/spawn - (during (tcp-connection (bind id Symbol) (tcp-listener 5999)) + (during/spawn (tcp-connection (bind id Symbol) (tcp-listener 5999)) (assert (tcp-accepted id)) (let ([me (gensym 'user)]) (assert (present me)) diff --git a/racket/typed/examples/simple-during-spawn.rkt b/racket/typed/examples/simple-during-spawn.rkt new file mode 100644 index 0000000..8874809 --- /dev/null +++ b/racket/typed/examples/simple-during-spawn.rkt @@ -0,0 +1,33 @@ +#lang typed/syndicate + +;; Expected Output +;; +parent +;; +GO +;; +ready +;; -parent +;; -GO +;; -ready + +(define-type-alias ds-type + (U (Tuple String) (Observe (Tuple ★/t)))) + +(run-ground-dataspace ds-type + (spawn ds-type + (start-facet parent + (assert (tuple "parent")) + (during/spawn (tuple "GO") + (assert (tuple "ready"))) + (on (asserted (tuple "ready")) + (stop parent)))) + (spawn ds-type + (start-facet flag + (assert (tuple "GO")) + (on (retracted (tuple "parent")) + (stop flag)))) + (spawn ds-type + (start-facet obs + (during (tuple (bind s String)) + (on start + (printf "+~a\n" s)) + (on stop + (printf "-~a\n" s)))))) diff --git a/racket/typed/syndicate/core-types.rkt b/racket/typed/syndicate/core-types.rkt index f9f8937..0d97e7b 100644 --- a/racket/typed/syndicate/core-types.rkt +++ b/racket/typed/syndicate/core-types.rkt @@ -1112,6 +1112,13 @@ (reassemble-type #'τ-cons subitems)] [_ t])) +;; Type -> Bool +;; to prevent observing the linkage assertions used by during/spawn, +;; disallow ?★ and ??★ +(define-for-syntax (allowed-interest? t) + (not (or (<: (type-eval #'(Observe ★/t)) t) + (<: (type-eval #'(Observe (Observe ★/t))) t)))) + ;; Type -> String (define-for-syntax (type->strX ty) ;; Identifier -> String diff --git a/racket/typed/syndicate/roles.rkt b/racket/typed/syndicate/roles.rkt index 4a4b084..d19069e 100644 --- a/racket/typed/syndicate/roles.rkt +++ b/racket/typed/syndicate/roles.rkt @@ -22,7 +22,7 @@ →fn proc ;; Statements let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do - when unless send! realize! define + when unless send! realize! define during/spawn ;; Derived Forms during During define/query-value @@ -182,6 +182,26 @@ (⇒ : ★/t) (⇒ ν-f (τ))]]) +(define-typed-syntax (during/spawn pat bdy ...+) ≫ + #:with pat+ (elaborate-pattern/with-com-ty #'pat) + [⊢ pat+ ≫ pat-- (⇒ : τp)] + #:fail-unless (pure? #'pat--) "pattern not allowed to have effects" + #:fail-unless (allowed-interest? (pattern-sub-type #'τp)) "overly broad interest, ?̱̱★ and ??★ not allowed" + #:with ([x:id τ:type] ...) (pat-bindings #'pat+) + [[x ≫ x- : τ] ... ⊢ (block bdy ...) ≫ bdy- + (⇒ ν-ep (~effs τ-ep ...)) + (⇒ ν-f (~effs)) + (⇒ ν-s (~effs))] + #:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat+)) + #:with τc:type (current-communication-type) + #:with τ-facet (type-eval #'(Role (_) τ-ep ...)) + #:with τ-spawn (mk-ActorWithRole- #'(τc.norm τ-facet)) + #:with τ-endpoint (type-eval #'(Reacts (Asserted τp) τ-spawn)) + ------------------------------ + [⊢ (syndicate:during/spawn pat- bdy-) + (⇒ : ★/t) + (⇒ ν-ep (τ-endpoint))]) + (define-typed-syntax field [(_ [x:id τ-f:type e:expr] ...) ≫ #:cut @@ -204,6 +224,7 @@ (define-typed-syntax (assert e:expr) ≫ [⊢ e ≫ e- (⇒ : τ)] #:fail-unless (pure? #'e-) "expression not allowed to have effects" + #:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed" #:with τs (mk-Shares- #'(τ)) ------------------------------------- [⊢ (syndicate:assert e-) (⇒ : ★/t) @@ -315,6 +336,7 @@ #:with p/e (if msg? (stx-cadr elab) elab) [⊢ p/e ≫ p-- (⇒ : τp)] #:fail-unless (pure? #'p--) "pattern not allowed to have effects" + #:fail-unless (allowed-interest? (pattern-sub-type #'τp)) "overly broad interest, ?̱̱★ and ??★ not allowed" #:with ([x:id τ:type] ...) (pat-bindings #'p/e) [[x ≫ x- : τ] ... ⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs)) diff --git a/racket/typed/tests/overly-broad-interests.rkt b/racket/typed/tests/overly-broad-interests.rkt new file mode 100644 index 0000000..2d8f58e --- /dev/null +++ b/racket/typed/tests/overly-broad-interests.rkt @@ -0,0 +1,22 @@ +#lang typed/syndicate + +(require rackunit/turnstile) + +(typecheck-fail (spawn ⊥ + (start-facet x + (on (asserted $x:Int) + #f))) + #:with-msg "overly broad interest") + +(typecheck-fail (spawn ⊥ + (start-facet x + (on (asserted (observe $x:Int)) + #f))) + #:with-msg "overly broad interest") + +;; TODO - but this one seems fine? +(typecheck-fail (spawn ⊥ + (start-facet x + (on (asserted _) + #f))) + #:with-msg "overly broad interest")