Add a typed during/spawn and checks for overly broad interests
This commit is contained in:
parent
c3559f1611
commit
98c58d3e6f
|
@ -26,8 +26,7 @@
|
||||||
|
|
||||||
(spawn chat-ds
|
(spawn chat-ds
|
||||||
(start-facet chat-server
|
(start-facet chat-server
|
||||||
;; TODO - should be during/spawn
|
(during/spawn (tcp-connection (bind id Symbol) (tcp-listener 5999))
|
||||||
(during (tcp-connection (bind id Symbol) (tcp-listener 5999))
|
|
||||||
(assert (tcp-accepted id))
|
(assert (tcp-accepted id))
|
||||||
(let ([me (gensym 'user)])
|
(let ([me (gensym 'user)])
|
||||||
(assert (present me))
|
(assert (present me))
|
||||||
|
|
|
@ -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))))))
|
|
@ -1112,6 +1112,13 @@
|
||||||
(reassemble-type #'τ-cons subitems)]
|
(reassemble-type #'τ-cons subitems)]
|
||||||
[_ t]))
|
[_ 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
|
;; Type -> String
|
||||||
(define-for-syntax (type->strX ty)
|
(define-for-syntax (type->strX ty)
|
||||||
;; Identifier -> String
|
;; Identifier -> String
|
||||||
|
|
|
@ -22,7 +22,7 @@
|
||||||
→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
|
||||||
when unless send! realize! define
|
when unless send! realize! define during/spawn
|
||||||
;; Derived Forms
|
;; Derived Forms
|
||||||
during During
|
during During
|
||||||
define/query-value
|
define/query-value
|
||||||
|
@ -182,6 +182,26 @@
|
||||||
(⇒ : ★/t)
|
(⇒ : ★/t)
|
||||||
(⇒ ν-f (τ))]])
|
(⇒ ν-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
|
(define-typed-syntax field
|
||||||
[(_ [x:id τ-f:type e:expr] ...) ≫
|
[(_ [x:id τ-f:type e:expr] ...) ≫
|
||||||
#:cut
|
#:cut
|
||||||
|
@ -204,6 +224,7 @@
|
||||||
(define-typed-syntax (assert e:expr) ≫
|
(define-typed-syntax (assert e:expr) ≫
|
||||||
[⊢ e ≫ e- (⇒ : τ)]
|
[⊢ e ≫ e- (⇒ : τ)]
|
||||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||||
|
#:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed"
|
||||||
#:with τs (mk-Shares- #'(τ))
|
#:with τs (mk-Shares- #'(τ))
|
||||||
-------------------------------------
|
-------------------------------------
|
||||||
[⊢ (syndicate:assert e-) (⇒ : ★/t)
|
[⊢ (syndicate:assert e-) (⇒ : ★/t)
|
||||||
|
@ -315,6 +336,7 @@
|
||||||
#:with p/e (if msg? (stx-cadr elab) elab)
|
#:with p/e (if msg? (stx-cadr elab) elab)
|
||||||
[⊢ p/e ≫ p-- (⇒ : τp)]
|
[⊢ p/e ≫ p-- (⇒ : τp)]
|
||||||
#:fail-unless (pure? #'p--) "pattern not allowed to have effects"
|
#: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)
|
#:with ([x:id τ:type] ...) (pat-bindings #'p/e)
|
||||||
[[x ≫ x- : τ] ... ⊢ (block s ...) ≫ s-
|
[[x ≫ x- : τ] ... ⊢ (block s ...) ≫ s-
|
||||||
(⇒ ν-ep (~effs))
|
(⇒ ν-ep (~effs))
|
||||||
|
|
|
@ -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")
|
Loading…
Reference in New Issue