internal events for typed lang

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 '())

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))
+      (define-values (i o i/i o/i s) (analyze-role-input/output r))
-      (values (cons i is) (cons o os) (cons s ss))))
+      (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 ... ...))
+     #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-r ... ...))
-     (values #'τi #'τo #'τa)]
+     (values #'τ-i #'τ-o #'τ-i/i #'τ-o/i #'τ-a)]
     [(~Stop name:id τ-r ...)
-     #:with (τi τo τa) (analyze-roles #'(τ-r ...))
+     #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-r ...))
-     (values #'τi #'τo #'τa)]
+     (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))
+         (define-values (i o i/i o/i s) (analyze-role-input/output t))
-         (values (cons i ins) (cons o outs) (cons s spawns))))
+         (values (cons i ins) (cons o outs) (cons i/i ins/int) (cons o/i outs/int) (cons s spawns))))
-     (define pat-types (stx-map event-desc-type #'(τ-if ...)))
+     (define-values (ifs/ext ifs/int) (partition external-evt? (stx->list #'(τ-if ...))))
-     (values (mk-U- #`(#,@is #,@pat-types))
+     (define pat-types/ext (map event-desc-type ifs/ext))
-             (mk-U- #`(τ-s ... msg ... #,@os #,@(stx-map pattern-sub-type pat-types)))
+     (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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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)))))))))))))))))
+)

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)))))
+)

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))))

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
+  (define-syntax-class event-cons
-    #:datum-literals (asserted retracted message)
+    #: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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;