internal events for typed lang
This commit is contained in:
Sam Caldwell
parent
963676c0c6
commit
f597fdc499
|
|
@ -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 '())
|
||||
|
|
|
|||
|
|
@ -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
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
|
|||
|
|
@ -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)))))))))))))))))
|
||||
)
|
||||
|
|
@ -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)))))
|
||||
)
|
||||
|
|
@ -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))))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
|
|||
Loading…
Reference in New Issue