4.5 KiB
Syntax
Just a sketch, at the moment.
Instantaneous actions, I := (actor I ...)
(network 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 ...)
(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 (final-values-of B)]))
(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 of the final I
from the E
exit branch that was chosen.
There are four kinds of actor-spawning I
s: actor
, network
,
state
and background
. Neither actor
, network
nor background
yield a value; only state
does so. However, both state
and
background
link to their invoking contexts, because state
may
return a value 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 network 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.
Examples
#lang prospect/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))))))