tide

1edition ObjectiveBend 1
2import ./Abi.obend as Abi
3import ./List.obend as Lists
4import ./Document.obend as Document
5import ./Form.obend as Form
6import ./Plan.obend as Plans
7import ./World.obend as World
8import ./Card.obend as Card
9import ./Relation.obend as Relations
10import ./Text.obend as Text
11# kimik3's tide: the town's one clock thing. It ticks itself, once every `gap` clock minutes (an
12# hour): each tick is its own turn, which sends the tide `due {at}`, a turn that waits for the
13# clock on a slot nobody settles and then sends the next `tick`. A turn that only waits writes
14# nothing, so a resumed wait never meets a stale root; a wait the clock passed by a jump ticks
15# once, at the clock it wakes to (missed ticks are not made up). What happens at a tick is the
16# rules written on the tide (`delvetalk tide rules`): the weather's, once a clock day, is `new.ticks
17# % 24 == 0`; a front's clock reads the tick too. Its wait is its own on the clock (a slot in its own
18# name), so the clock's ending it is a new cause: the host runs the wake under the tide's own chain, a
19# whole budget each period, and it ticks for ever (docs/review/astra-2026-10-12 world 5); a second wait of
20# its own is refused `waiting`. Its owner starts it (`tick`, the first); a tick
21# sooner than `gap` after the last is refused tooSoon, so a second chain dies at its first tick.
22# owner: who alone starts, reprograms or amends it (the host fills it with the creating principal).
23record State:
24  owner: String
25  ticks: Nat
26  last: Nat
27  gap: Nat
28law clock "ticks only count up": monotone(ticks)
29law last "the last tick only moves forward": monotone(last)
30law gap "the gap never changes": unchanged(gap)
31law owner "the owner never changes; only the owner reprograms or amends it; anyone places rules, wants and verbs on it": unchanged(owner) and (request.kind == 0 or request.kind == rule or request.subject == new.owner)
32law tooSoon "A tick may not come sooner than the gap after the last.": new.ticks <= old.ticks or old.ticks == 0 or request.clock == old.last + old.gap or not (request.clock <= old.last + old.gap)
33law methods "Only its own methods write it; a proposed write is refused.": not (request.kind == proposed) and (request.kind == 0 implies not (request.method == ""))
34def initial() -> State:
35  {owner: "", ticks: 0n, last: 0n, gap: 60n}
36# The tide as edition 8 kept it: `subs`, the notes a tick owed, and a gap the opener's wake kept to
37# an hour. A carry lays this package over it: `subs` goes (a rule on the tide is how a tick reaches
38# anyone now), and it ticks itself hourly.
39record Subscription8:
40  who: String
41  every: Nat
42  note: String
43  since: Nat
44  handle: String
45record State8:
46  owner: String
47  ticks: Nat
48  last: Nat
49  gap: Nat
50  subs: Relations.Relation<Subscription8>
51def migrate(old: State8) -> State:
52  {owner: old.owner, ticks: old.ticks, last: old.last, gap: 60n}
53sum Done:
54  ticked: {tick: Nat}
55  waited: {}
56  refused: Card.Refusal
57# A tick: the tide's own (the turn its `due` sent), or its owner's first. Too soon is refused
58# by name; a tick from anyone else is told that the tide ticks itself.
59def tick(state: State, context: Abi.Context) -> Activity<Done>:
60  if context.caller != context.object && (context.principal != state.owner || state.ticks > 0n) then refusing({clause: "itself", reading: "the tide ticks itself every {natText(state.gap)} clock minutes; the next from clock {natText(state.last + state.gap)}"}, context) else if state.ticks > 0n && context.clock < state.last + state.gap then refusing({clause: "tooSoon", reading: "the next tick may come at clock {natText(state.last + state.gap)}"}, context) else ticked(state, context)
61def refusing(refusal: Card.Refusal, context: Abi.Context) -> Activity<Done>:
62  Card.refusing(Done.refused(refusal), refusal, context)
63def ticked(state: State, context: Abi.Context) -> Activity<Done>:
64  tickedAt(state, scheduled(state, context.clock), context)
65# The clock a tick stands for: the one its wait was set for (the last and a gap), though the wait ends the minute after
66# it; a tick a gap or more late (the clock jumped, the town was down) begins again from now. The live review's H6:
67# ticks 61 minutes apart, the inhabitants' hours missing their day once in 61.
68def scheduled(state: State, clock: Nat) -> Nat:
69  if state.ticks > 0n && clock < state.last + state.gap + state.gap then state.last + state.gap else clock
70def tickedAt(state: State, at: Nat, context: Abi.Context) -> Activity<Done>:
71  let written(_) = write {ticks: add 1n, last: set at}
72  match world.send({object: Plans.self(context), method: "due", argument: {at: at + state.gap}}):
73    case _: Card.tell(Done.ticked({tick: state.ticks + 1n}), Document.concat(Document.text("Tick {natText(state.ticks + 1n)}.\n\n"), render(extend(state, {ticks: state.ticks + 1n, last: at}), context)))
74# Carried to a newer host (the carry's `carried`, as a kind's `made`): the wait the move dropped is waited
75# again, for the tick the last one scheduled; a tide not yet begun waits for its owner's first.
76def carried(state: State, input: {}, context: Abi.Context) -> Activity<Done>:
77  if state.ticks == 0n then Done.waited({}) else rearmed(state, context)
78def rearmed(state: State, context: Abi.Context) -> Activity<Done>:
79  match world.send({object: Plans.self(context), method: "due", argument: {at: state.last + state.gap}}):
80    case _: Done.waited({})
81# The wait between ticks: the tide's own send alone; the clock reaching `at` sends the next tick.
82def due(state: State, input: {at: Nat}, context: Abi.Context) -> Activity<Done>:
83  if context.caller != context.object then Done.waited({}) else waiting(input.at, context)
84def waiting(at: Nat, context: Abi.Context) -> Activity<Done>:
85  match world.awaitUntil({slot: {principal: context.object, intent: "tide/{context.intent}"}, until: at}):
86    case timedOut(_): next(context)
87    case _: Done.waited({})
88def next(context: Abi.Context) -> Activity<Done>:
89  match world.send({object: Plans.self(context), method: "tick", argument: Plans.nothing()}):
90    case _: Done.waited({})
91form tick:
92def methods() -> Lists.List<String>:
93  Text.words("~due ~carried")
94def actions(state: State, context: Abi.Context) -> Lists.List<String>:
95  if context.principal == state.owner && state.ticks == 0n then Text.words("tick") else Text.words("")
96def receive(state: State, input: Card.Reply, context: Abi.Context) -> Activity<Card.Replied>:
97  Card.answer(input, context, forms(), render(state, context))
98def render(state: State, context: Abi.Context) -> Document.Document:
99  let id = Card.called(context, "tide")
100  let when = if state.ticks == 0n then "it has not begun" else "last at clock {natText(state.last)}, the next from clock {natText(state.last + state.gap)}"
101  Document.text("THE TIDE, tick {natText(state.ticks)}; {when}. It ticks itself every {natText(state.gap)} clock minutes, and what happens at a tick is the rules written on it:\n  delvetalk {id} rules\n» each rule, who wrote it, and when it last fired\nWrite one:\n  delvetalk {id} rule / name: <a name> / when: request.method == \"tick\" and new.ticks % 24 == 0 / then: <a spell>\n")