From 19f915620e99c7007c6866690708cbb7f796e9d6 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Thu, 28 Mar 2019 14:53:25 -0400 Subject: [PATCH] Keep track of branches for role effects in turnstile lang --- racket/typed/roles.rkt | 31 ++++++++++++++++++++++++++----- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 7ad63cd..6db5bb9 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -80,7 +80,7 @@ ;; ν-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 a facet) as `Role`s and message sends, `Sends` +;; ν-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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -97,6 +97,11 @@ (define-type-constructor Message #: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) @@ -394,6 +399,19 @@ ;; 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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -506,6 +524,9 @@ ;; 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)] @@ -1570,7 +1591,7 @@ -------- [⊢ (if- e_tst- e1- e2-) (⇒ ν-ep (eps1 ... eps2 ...)) - (⇒ ν-f (fs1 ... fs2 ...)) + (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) (⇒ ν-s (ss1 ... ss2 ...))]] [(_ e_tst e1 e2) ≫ [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. @@ -1583,7 +1604,7 @@ -------- [⊢ (if- e_tst- e1- e2-) (⇒ : τ) (⇒ ν-ep (eps1 ... eps2 ...)) - (⇒ ν-f (fs1 ... fs2 ...)) + (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...)))) (⇒ ν-s (ss1 ... ss2 ...))]]) (define-typed-syntax (when e s ...+) ≫ @@ -1651,7 +1672,7 @@ ------------------------------------------------ [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...)) (⇒ ν-ep (eps ... ...)) - (⇒ ν-f (fs ... ...)) + (⇒ ν-f #,(make-Branch #'((fs ...) ...))) (⇒ ν-s (ss ... ...))]) (define-typed-syntax (match e [p s ...+] ...+) ≫ @@ -1676,7 +1697,7 @@ [_ (error "incomplete pattern match")]) (⇒ : (U τ-s ...)) (⇒ ν-ep (eps ... ...)) - (⇒ ν-f (fs ... ...)) + (⇒ ν-f #,(make-Branch #'((fs ...) ...))) (⇒ ν-s (ss ... ...))]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;