5.5 KiB
Syntax
Just a sketch, at the moment.
Instantaneous actions, I := (actor I ...)
(dataspace I ...)
(state [B O ...] [E I ...] ...)
(background I ...)
(assert! P)
(retract! P)
(send! P)
(flush!) ;; ???
expr
Optional Bindings, B := ;; nothing, or
#:collect [(id I) ...]
Ongoing actions, O := (on E I ...)
(during P O ...)
(once E I ...) ;; ???
(assert P)
(assert #:when Pred P)
(track [x Agg] I ...)
(begin O ...) ;; ??? begin isn't quite right
Predicates, Pred := (not Pred) ;; -- NOT YET IMPLEMENTED
(exists P Pred) ;; -- NOT YET IMPLEMENTED
(forall P Pred) ;; -- NOT YET IMPLEMENTED
expr
Events, E := (asserted P)
(retracted P)
(message P)
(rising-edge Pred)
(falling-edge Pred)
Aggregates, Agg := (count expr P)
(set expr P)
(hash k_expr v_expr P)
(project P)
(single-value expr P)
(single-value expr P #:default def_expr)
Pred
Patterns, P := ... ;; uses $var as binder
(define-syntax-rule (until B E O ...)
(state [B O ...] [E (values)]))
(define-syntax-rule (forever B O ...)
(state [B O ...]))
Note also that falling-edge
is encodable using rising-edge
and
not
, and that forall
is encodable using exists
and not
.
state
has the B
bindings visible in the I
s, and returns the
value(s) of the final I
from the E
exit branch that was chosen
prepended to the values of the calling actor's variables at the time
of state
termination.
There are four kinds of actor-spawning I
s: actor
, dataspace
,
state
and background
. Neither actor
, dataspace
nor background
yield a value; only state
does so. However, both state
and
background
link to their invoking contexts, because state
may
return values or crash, and background
may crash. Actors using
state
and background
must therefore have a special continuation
table in their private state to link them to their state
and
background
logical-children-but-physical-siblings. The link
communicates values (on success) and crashes (on failure).
Q: Should exception values be transmitted on state
failure? I think
no, but I am not sure there's a good reason why not.
Of the events, asserted
, retracted
and message
require no
private-state, since the dataspace does the book-keeping for us.
rising-edge
, however, needs to track the state of its predicate. If
the predicate happens to involve an exists
, then an assertion set
must be maintained, like for a track
.
This is leading me to believe that the order of operations is:
- Given a patch,
- update
track
s and assertion-sets related torising-edge
. - handle
on
forasserted
,retracted
andrising-edge
, in order of appearance - check termination conditions
- maintain
assert
s and subscriptions foron
s
- update
- Given a message,
- handle
on
formessage
andrising-edge
, in order of appearance - check termination conditions
- maintain
assert
s and subscriptions foron
s
- handle
Actually, I'm not sure falling-edge
is encodable using
rising-edge
, since the initial state might be different. Do we
assume that the level is high when the level is unknown for a
falling-edge? I think it likely, given I think it likely that we
assume the level is low when the level is unknown for a rising-edge.
when
is a bit tricky, because it should clearly apply to on
and
assert
, but it is not clear that it should apply to track
.
Furthermore, what should happen if, mid-way through some interaction
involving assertions, the when
predicate goes false? Should the
subscription be retracted? On balance, I'm starting to think that
when
is a bad idea. In my sketches so far, there's only one place
it's used, to conditionally assert
a set, so I've added #:when
to
assert
instead.
Note that exists
(and so forall
) are tricky because of the nested
Pred
. For now, I'm not implementing them -- we'll see how painful it
is to use track
and plain-old expr
Pred
s instead.
during
is a quasi-macro, with defining equation
(during P O ...) === (on (asserted P)
(until (retracted P')
O ...))
where P'
is like P
but with all the binders in P
instantiated
with their values at the time the until
is started.
Examples
#lang syndicate/actor
;; Simple mutable box and count-to-infinity box client.
(struct set-box (new-value) #:transparent)
(struct box-state (value) #:transparent)
(actor (forever #:collect [(value 0)]
(assert (box-state value))
(on (message (set-box $new-value))
new-value)))
(actor (forever
(on (asserted (box-state $value))
(send! (set-box (+ value 1))))))