From f597fdc499e36c99c36696d6c583271bbe6f798b Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Fri, 14 Jun 2019 11:43:15 -0400 Subject: [PATCH] internal events for typed lang --- racket/syndicate/actor.rkt | 8 +- racket/typed/core-types.rkt | 137 +++++++----------- .../examples/roles/internal-knowledge.rkt | 88 +++++++++++ racket/typed/examples/roles/realize.rkt | 27 ++++ racket/typed/prim.rkt | 1 + racket/typed/roles.rkt | 97 ++++++++++--- 6 files changed, 253 insertions(+), 105 deletions(-) create mode 100644 racket/typed/examples/roles/internal-knowledge.rkt create mode 100644 racket/typed/examples/roles/realize.rkt diff --git a/racket/syndicate/actor.rkt b/racket/syndicate/actor.rkt index a5be9f7..fea168c 100644 --- a/racket/syndicate/actor.rkt +++ b/racket/syndicate/actor.rkt @@ -1212,7 +1212,7 @@ (lambda () (define a (current-actor-state)) (define new-knowledge - (update-interests (actor-state-knowledge a) internal)) + (apply-patch (actor-state-knowledge a) internal)) (current-actor-state (struct-copy actor-state a [knowledge new-knowledge])))) @@ -1295,6 +1295,10 @@ (define a (current-actor-state)) (for* ([e (in-list pending)] [(fid f) (in-hash (actor-state-facets a))]) + (when (patch? e) + (define a (current-actor-state)) + (current-actor-state (struct-copy actor-state a + [knowledge (apply-patch (actor-state-knowledge a) e)]))) (facet-handle-event! fid f e #f))) (define (refresh-facet-assertions!) @@ -1332,7 +1336,7 @@ (if (patch? e) (struct-copy actor-state a [previous-knowledge (actor-state-knowledge a)] - [knowledge (update-interests (actor-state-knowledge a) e)]) + [knowledge (apply-patch (actor-state-knowledge a) e)]) a)) (current-pending-patch patch-empty) (current-pending-actions '()) diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt index c8e59e1..957b3f7 100644 --- a/racket/typed/core-types.rkt +++ b/racket/typed/core-types.rkt @@ -201,9 +201,13 @@ (define-binding-type Role #:arity >= 0 #:bvs = 1) (define-type-constructor Shares #:arity = 1) (define-type-constructor Sends #:arity = 1) +(define-type-constructor Realizes #:arity = 1) (define-type-constructor Reacts #:arity >= 1) (define-type-constructor Asserted #:arity = 1) (define-type-constructor Retracted #:arity = 1) +(define-type-constructor Know #:arity = 1) +(define-type-constructor Forget #:arity = 1) +(define-product-type Realize #:arity = 1) (define-type-constructor Stop #:arity >= 1) (define-type-constructor Field #:arity = 1) (define-type-constructor Bind #:arity = 1) @@ -660,6 +664,9 @@ (define-for-syntax (bot? t) ((current-typecheck-relation) t (mk-U*- '()))) +(define-for-syntax bot + (mk-U*- '())) + (define-for-syntax (flat-type? τ) (syntax-parse τ [(~→ τ ...) #f] @@ -701,7 +708,6 @@ (define-for-syntax (relay-interests t) (syntax-parse t - ;; TODO: probably need to `normalize` the result [(~U* τ ...) (mk-U- (stx-map relay-interests #'(τ ...)))] [~★/t (type-eval #'★/t)] [(~Observe (~Inbound τ)) (mk-Observe- #'(τ))] @@ -709,15 +715,19 @@ ;; (SyntaxOf RoleType ...) -> (Syntaxof InputType OutputType SpawnType) (define-for-syntax (analyze-roles rs) - (define-values (lis los lss) + (define-values (lis los lis/i los/i lss) (for/fold ([is '()] [os '()] + [is/i '()] + [os/i '()] [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)))) + (define-values (i o i/i o/i s) (analyze-role-input/output r)) + (values (cons i is) (cons o os) (cons i/i is/i) (cons o/i os/i) (cons s ss)))) #`(#,(mk-U- lis) #,(mk-U- los) + #,(mk-U- lis/i) + #,(mk-U- los/i) #,(mk-U- lss))) ;; Wanted test case, but can't use it bc it uses things defined for-syntax @@ -727,50 +737,77 @@ [(τ-i τ-o) (check-true (type=? #'τ-o (type-eval #'Int)))]))) -;; RoleType -> (Values InputType OutputType SpawnType) +;; RoleType -> (Values ExternalInputType ExternalOutputType +;; InternalInputType InternalOutputType +;; 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)] + #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-r ... ...)) + (values #'τ-i #'τ-o #'τ-i/i #'τ-o/i #'τ-a)] [(~Stop name:id τ-r ...) - #:with (τi τo τa) (analyze-roles #'(τ-r ...)) - (values #'τi #'τo #'τa)] + #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-r ...)) + (values #'τ-i #'τ-o #'τ-i/i #'τ-o/i #'τ-a)] [(~Actor τc) - (values (mk-U*- '()) (mk-U*- '()) t)] + (values bot bot bot bot t)] [(~Sends τ-m) - (values (mk-U*- '()) (mk-Message- #'(τ-m)) (mk-U*- '()))] + (values bot (mk-Message- #'(τ-m)) bot bot bot)] + [(~Realizes τ-m) + (values bot bot bot (mk-Realize- #'(τ-m)) bot)] [(~Role (name:id) (~or (~Shares τ-s) + (~Know τ-k) (~Sends τ-m) + (~Realizes τ-rlz) (~Reacts τ-if τ-then ...)) ... (~and (~Role _ ...) sub-role) ...) #:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))]) (mk-Message- (list m))) - (define-values (is os ss) + #:with (rlz ...) (for/list ([r (in-syntax #'(τ-rlz ...))]) + (mk-Realize- (list r))) + (define-values (is/e os/e is/i os/i ss) (for/fold ([ins '()] [outs '()] + [ins/int '()] + [outs/int '()] [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 (mk-U- #`(#,@is #,@pat-types)) - (mk-U- #`(τ-s ... msg ... #,@os #,@(stx-map pattern-sub-type pat-types))) + (define-values (i o i/i o/i s) (analyze-role-input/output t)) + (values (cons i ins) (cons o outs) (cons i/i ins/int) (cons o/i outs/int) (cons s spawns)))) + (define-values (ifs/ext ifs/int) (partition external-evt? (stx->list #'(τ-if ...)))) + (define pat-types/ext (map event-desc-type ifs/ext)) + (define pat-types/int (map event-desc-type ifs/int)) + (values (mk-U- #`(#,@is/e #,@pat-types/ext)) + (mk-U- #`(τ-s ... msg ... #,@os/e #,@(map pattern-sub-type pat-types/ext))) + (mk-U- #`(#,@is/i #,@pat-types/int)) + (mk-U- #`(τ-k ... rlz ... #,@os/i #,@(map pattern-sub-type pat-types/int))) (mk-U- ss))])) +;; EventType -> Bool +;; recognize external events (assertions and messages) +(define-for-syntax (external-evt? evt) + (syntax-parse evt + [(~Asserted τ) #t] + [(~Retracted τ) #t] + [(~Message τ) #t] + [_ #f])) + ;; EventDescriptorType -> Type (define-for-syntax (event-desc-type desc) (syntax-parse desc [(~Asserted τ) #'τ] [(~Retracted τ) #'τ] [(~Message τ) desc] + [(~Know τ) #'τ] + [(~Forget τ) #'τ] + [(~Realize τ) desc] [_ (mk-U*- '())])) ;; PatternType -> Type (define-for-syntax (pattern-sub-type pt) (syntax-parse pt - [(~Message τ) + [(~or (~Message τ) + (~Realize τ)) (define t (replace-bind-and-discard-with-★ #'τ)) (mk-Observe- (list t))] [τ @@ -957,7 +994,6 @@ ;; first type is the contents of the set/dataspace ;; second type is the type of a pattern (define-for-syntax (project-safe? t1 t2) - ;; TODO - not sure how to handle type variables (define (project-safe* t1 t2) (syntax-parse #`(#,t1 #,t2) [(_ (~Bind τ2)) @@ -994,7 +1030,6 @@ [~★/t #f] [(~U* τ:type ...) (stx-andmap finite? #'(τ ...))] - ;; TODO - this is questionable. maybe need a kind for assertions? [X:id #t] [(~Base _) #t] @@ -1017,68 +1052,6 @@ (reassemble-type #'τ-cons 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) - [((~Asserted τ1) (~Asserted τ2)) - (<: (pattern-matching-assertions #'τ2) - (pattern-matching-assertions #'τ1))] - [((~Retracted τ1) (~Retracted τ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)])) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Effect Checking ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/examples/roles/internal-knowledge.rkt b/racket/typed/examples/roles/internal-knowledge.rkt new file mode 100644 index 0000000..65c6cf8 --- /dev/null +++ b/racket/typed/examples/roles/internal-knowledge.rkt @@ -0,0 +1,88 @@ +#lang typed/syndicate/roles + +;; Expected Output: +#| +balance = 0 +balance = 5 +balance = 0 +JEEPERS +know overdraft! +balance = -1 +balance = -2 +no longer in overdraft +balance = 8 +|# + +(assertion-struct balance : Balance (v)) +(message-struct deposit : Deposit (v)) + +;; Internal Events +(message-struct new-transaction : NewTransaction (old new)) +(assertion-struct overdraft : Overdraft ()) + +(define-type-alias τc/external + (U (Balance Int) + (Message (Deposit Int)) + (Observe ★/t))) + +(define-type-alias τc/internal + (U (Message (NewTransaction Int Int)) + (Overdraft) + (Observe ★/t))) + +(define-type-alias τc + (U τc/external + τc/internal)) + +(run-ground-dataspace τc/external + +(spawn + (begin + (start-facet bank + (field [account Int 0]) + + (assert (balance (ref account))) + + (on (message (deposit $v)) + (define prev (ref account)) + (set! account (+ v prev)) + (realize! (new-transaction prev (ref account)))) + + (on (realize (new-transaction $old:Int $new:Int)) + (when (and (negative? new) + (not (negative? old))) + (start-facet neg + ;; (this print is to make sure only one of these facets is created) + (printf "JEEPERS\n") + (know (overdraft)) + (on (realize (new-transaction _ $new:Int)) + (when (not (negative? new)) + (stop neg)))))) + + (during (know (overdraft)) + (on-start (printf "know overdraft!\n")) + (on-stop (printf "no longer in overdraft\n")))))) + +(spawn + (start-facet obs + (on (asserted (balance $v)) + (printf "balance = ~a\n" v)))) + +(spawn + (start-facet _ + (on start + (send! (deposit 5)) + (spawn + (start-facet _ + (on start + (send! (deposit -5)) + (spawn + (start-facet _ + (on start + (send! (deposit -1)) + (spawn + (start-facet _ + (on start + (send! (deposit -1)) + (spawn (start-facet _ (on start (send! (deposit 10))))))))))))))))) +) diff --git a/racket/typed/examples/roles/realize.rkt b/racket/typed/examples/roles/realize.rkt new file mode 100644 index 0000000..d11a04d --- /dev/null +++ b/racket/typed/examples/roles/realize.rkt @@ -0,0 +1,27 @@ +#lang typed/syndicate/roles + +;; Expected Output: +#| +received message bad +realized good +|# + +(message-struct ping : Ping (v)) + +(define-type-alias τc + (U (Message (Ping Symbol)) + (Observe ★/t))) + +(run-ground-dataspace τc +(spawn + (start-facet _ + (on (realize (ping $v:Symbol)) + (printf "realized ~a\n" v)) + (on (message (ping $v)) + (printf "received message ~a\n" v) + (realize! (ping 'good))))) + +(spawn + (start-facet _ + (on start (send! (ping 'bad))))) +) diff --git a/racket/typed/prim.rkt b/racket/typed/prim.rkt index 8c45ccc..940a875 100644 --- a/racket/typed/prim.rkt +++ b/racket/typed/prim.rkt @@ -32,6 +32,7 @@ (define-primop min (→fn Int Int Int)) (define-primop zero? (→fn Int Bool)) (define-primop positive? (→fn Int Bool)) +(define-primop negative? (→fn Int Bool)) (define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns)))) (define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns)))) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 49635b2..a8431d5 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -10,6 +10,7 @@ ;; Types Tuple Bind Discard → ∀ Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop + Know Forget Realize Branch Effs FacetName Field ★/t Observe Inbound Outbound Actor U ⊥ @@ -17,20 +18,22 @@ →fn proc ;; Statements let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do - when unless send! define + when unless send! realize! define ;; Derived Forms during During define/query-value define/query-set define/query-hash + on-start on-stop ;; endpoints - assert on field + assert know on field ;; expressions tuple select lambda ref observe inbound outbound Λ inst call/inst ;; making types define-type-alias assertion-struct + message-struct define-constructor define-constructor* ;; values #%datum @@ -95,6 +98,9 @@ (define-simple-macro (assertion-struct name:id (~datum :) Name:id (slot:id ...)) (define-constructor* (name : Name slot ...))) +(define-simple-macro (message-struct name:id (~datum :) Name:id (slot:id ...)) + (define-constructor* (name : Name slot ...))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Compile-time State ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -129,6 +135,7 @@ (unless (and (stx-null? facet-effects) (stx-null? spawn-effects)) (type-error #:src #'(ep ...) #:msg "only endpoint effects allowed"))] #:with ((~or (~and τ-a (~Shares _)) + (~and τ-k (~Know _)) ;; untyped syndicate might allow this - TODO #;(~and τ-m (~Sends _)) (~and τ-r (~Reacts _ ...)) @@ -137,6 +144,7 @@ ep-effects #:with τ (type-eval #`(Role (#,name--) τ-a ... + τ-k ... ;; τ-m ... τ-r ...)) -------------------------------------------------------------- @@ -165,6 +173,14 @@ [⊢ (syndicate:assert e-) (⇒ : ★/t) (⇒ ν-ep (τs))]) +(define-typed-syntax (know e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ)] + #:fail-unless (pure? #'e-) "expression not allowed to have effects" + #:with τs (mk-Know- #'(τ)) + ------------------------------------- + [⊢ (syndicate:know e-) (⇒ : ★/t) + (⇒ ν-ep (τs))]) + (define-typed-syntax (send! e:expr) ≫ [⊢ e ≫ e- (⇒ : τ)] #:fail-unless (pure? #'e-) "expression not allowed to have effects" @@ -173,6 +189,14 @@ [⊢ (#%app- syndicate:send! e-) (⇒ : ★/t) (⇒ ν-f (τm))]) +(define-typed-syntax (realize! e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ)] + #:fail-unless (pure? #'e-) "expression not allowed to have effects" + #:with τm (mk-Realizes- #'(τ)) + -------------------------------------- + [⊢ (#%app- syndicate:realize! e-) (⇒ : ★/t) + (⇒ ν-f (τm))]) + (define-typed-syntax (stop facet-name:id cont ...) ≫ [⊢ facet-name ≫ facet-name- (⇐ : FacetName)] [⊢ (begin #f cont ...) ≫ cont- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))] @@ -182,17 +206,27 @@ (⇒ ν-f (τ))]) (begin-for-syntax - (define-syntax-class asserted/retracted/message - #:datum-literals (asserted retracted message) + (define-syntax-class event-cons + #:attributes (syndicate-kw ty-cons) + #:datum-literals (asserted retracted message know forget realize) (pattern (~or (~and asserted (~bind [syndicate-kw #'syndicate:asserted] - [react-con #'Asserted])) + [ty-cons #'Asserted])) (~and retracted (~bind [syndicate-kw #'syndicate:retracted] - [react-con #'Retracted])) + [ty-cons #'Retracted])) (~and message (~bind [syndicate-kw #'syndicate:message] - [react-con #'Message]))))) + [ty-cons #'Message])) + (~and know + (~bind [syndicate-kw #'syndicate:know] + [ty-cons #'Know])) + (~and forget + (~bind [syndicate-kw #'syndicate:forget] + [ty-cons #'Forget])) + (~and realize + (~bind [syndicate-kw #'syndicate:realize] + [ty-cons #'Realize]))))) (define-syntax-class priority-level #:literals (*query-priority-high* *query-priority* @@ -216,7 +250,8 @@ ) (define-typed-syntax on - [(on (~literal start) s ...) ≫ + #:datum-literals (start stop) + [(on start s ...) ≫ [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))] @@ -224,7 +259,7 @@ ----------------------------------- [⊢ (syndicate:on-start s-) (⇒ : ★/t) (⇒ ν-ep (τ-r))]] - [(on (~literal stop) s ...) ≫ + [(on stop s ...) ≫ [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))] @@ -232,10 +267,10 @@ ----------------------------------- [⊢ (syndicate:on-stop s-) (⇒ : ★/t) (⇒ ν-ep (τ-r))]] - [(on (a/r/m:asserted/retracted/message p) + [(on (evt:event-cons p) priority:priority s ...) ≫ - #:do [(define msg? (free-identifier=? #'syndicate:message (attribute a/r/m.syndicate-kw))) + #:do [(define msg? (free-identifier=? #'syndicate:message (attribute evt.syndicate-kw))) (define elab (elaborate-pattern/with-com-ty (if msg? #'(message p) #'p)))] #:with p/e (if msg? (stx-cadr elab) elab) @@ -247,9 +282,9 @@ (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))] #:with p- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'p/e)) - #:with τ-r (type-eval #'(Reacts (a/r/m.react-con τp) τ-f ... τ-s ...)) + #:with τ-r (type-eval #'(Reacts (evt.ty-cons τp) τ-f ... τ-s ...)) ----------------------------------- - [⊢ (syndicate:on (a/r/m.syndicate-kw p-) + [⊢ (syndicate:on (evt.syndicate-kw p-) #:priority priority.level s-) (⇒ : ★/t) @@ -282,7 +317,7 @@ [⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))] ] ;; TODO: s shouldn't refer to facets or fields! - #:with (τ-i τ-o τ-a) (analyze-roles #'(τ-f ...)) + #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...)) #:fail-unless (<: #'τ-o #'τ-c.norm) (format "Output ~a not valid in dataspace ~a" (type->str #'τ-o) (type->str #'τ-c.norm)) #:with τ-final (mk-Actor- #'(τ-c.norm)) @@ -291,6 +326,8 @@ #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm) #'τ-i) "Not prepared to handle all inputs" + #:fail-unless (project-safe? #'τ-o/i #'τ-i/i) + "Not prepared to handle internal events" -------------------------------------------------------------------------------------------- [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t) (⇒ ν-s (τ-final))]] @@ -328,21 +365,33 @@ ;; Derived Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(define-typed-syntax (during p s ...) ≫ +(define-typed-syntax during + #:literals (know) + [(_ (~or (~and k (know p)) p) s ...) ≫ #:with p+ (elaborate-pattern/with-com-ty #'p) #:with inst-p (instantiate-pattern #'p+) + #:with start-e (if (attribute k) #'know #'asserted) + #:with stop-e (if (attribute k) #'forget #'retracted) + #:with res #'(on (start-e p+) + (start-facet during-inner + (on (stop-e inst-p) + (stop during-inner)) + s ...)) ---------------------------------------- - [≻ (on (asserted p+) + [≻ (on (start-e p+) (start-facet during-inner - (on (retracted inst-p) + (on (stop-e inst-p) (stop during-inner)) - s ...))]) + s ...))]]) -(define-simple-macro (During τ:type EP ...) +(define-simple-macro (During (~or (~and K ((~literal Know) τ:type)) τ:type) + EP ...) #:with τ/inst (instantiate-pattern-type #'τ.norm) - (Reacts (Asserted τ) + #:with start-e (if (attribute K) #'Know #'Asserted) + #:with stop-e (if (attribute K) #'Forget #'Retracted) + (Reacts (start-e τ) (Role (during-inner) - (Reacts (Retracted τ/inst) + (Reacts (stop-e τ/inst) (Stop during-inner)) EP ...))) @@ -458,6 +507,12 @@ (set! x (hash-remove (ref x) e-key)) remove.expr))]) +(define-simple-macro (on-start e ...) + (on start e ...)) + +(define-simple-macro (on-stop e ...) + (on stop e ...)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Expressions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;