commons

edition ObjectiveBend 1
import ./Abi.obend as Abi
import ./List.obend as Lists
import ./Document.obend as Document
import ./Form.obend as Form
import ./Plan.obend as Plans
import ./World.obend as World
import ./Card.obend as Card
import ./Relation.obend as Relations
import ./Rows.obend as Rows
import ./Text.obend as Text
# The commons (after main's protocols/commons): a bounded place graph, directed paths,
# entry places, gates on paths, and declared presence. A turn moves only its own
# principal; presence is not containment, not read permission and not a connection.
# A gate names a path and who may cross it: anyone, the principals it lists, or only a
# turn the named gate object calls (a door object whose own `cross` decides, then calls
# `move`: context.caller is that object, never a copied reference).
record Place:
  name: String
  title: String
  description: String
record Path:
  from: String
  to: String
sum Rule:
  open: {}
  members: {names: Lists.List<String>}
  object: {object: String}
record Gate:
  from: String
  to: String
  rule: Rule
# Who is where, keyed {who} (Rows.Presence, as a scene keeps it).
type Presence = Rows.Presence
record State:
  owner: String
  places: Lists.List<Place>
  paths: Lists.List<Path>
  entries: Lists.List<String>
  gates: Lists.List<Gate>
  presence: Relations.Relation<Presence>
# Anyone enters, moves and leaves (the code moves only the turn's own principal and
# checks every gate); only the owner changes who a gate admits.
law owner "only the owner changes it; anyone enters, moves and leaves": request.subject == new.owner or (request.kind == 0 and (request.method == "enter" or request.method == "move" or request.method == "leave" or request.method == "receive"))
def initial() -> State:
  {owner: "", places: Lists.List.nil(), paths: Lists.List.nil(), entries: Lists.List.nil(), gates: Lists.List.nil(), presence: Relations.empty()}
def relations() -> Relations.Decls:
  Lists.append(Relations.Decls.nil(), {field: "presence", key: Text.words("who"), limit: presenceMax()})
# Bounds, as main's commons had them: eight places, sixteen paths, sixteen gates; and
# sixteen present, sixteen names on a gate (a seventeenth is refused by name).
def placesMax() -> Nat:
  8n
def pathsMax() -> Nat:
  16n
def gatesMax() -> Nat:
  16n
def presenceMax() -> Nat:
  16n
def namesMax() -> Nat:
  16n
def placeNamed(state: State, name: String) -> Lists.Maybe<Place>:
  Lists.find(state.places, fn(p: Place) -> Bool: p.name == name)
def isPlace(state: State, name: String) -> Bool:
  Lists.any(state.places, fn(p: Place) -> Bool: p.name == name)
# The configuration's own check: bounded, and every path, entry and gate names places.
def problem(state: State) -> String:
  if Lists.length(state.places) > placesMax() then "more than eight places" else if Lists.length(state.paths) > pathsMax() then "more than sixteen paths" else if Lists.length(state.gates) > gatesMax() then "more than sixteen gates" else if Lists.any(state.paths, fn(p: Path) -> Bool: isPlace(state, p.from) == false || isPlace(state, p.to) == false) then "a path names a place that is not here" else if Lists.any(state.entries, fn(e: String) -> Bool: isPlace(state, e) == false) then "an entry is not a place" else if Lists.any(state.gates, fn(g: Gate) -> Bool: pathFrom(state, g.from, g.to) == false) then "a gate is on no path" else ""
def pathFrom(state: State, from: String, to: String) -> Bool:
  Lists.any(state.paths, fn(p: Path) -> Bool: p.from == from && p.to == to)
def here(state: State, context: Abi.Context) -> Lists.Maybe<Presence>:
  Rows.presentAs(state.presence, context.principal)
def gateOn(state: State, from: String, to: String) -> Lists.Maybe<Gate>:
  Lists.find(state.gates, fn(g: Gate) -> Bool: g.from == from && g.to == to)
# Who may cross: "" when the turn may, else why not.
def crossing(rule: Rule, context: Abi.Context) -> String:
  match rule:
    case open(_): ""
    case members(m): if Lists.any(m.names, fn(n: String) -> Bool: n == context.principal) then "" else "the gate does not know you"
    case object(o): if context.caller == o.object then "" else "only {o.object} lets you through"
def gateCheck(found: Lists.Maybe<Gate>, context: Abi.Context) -> String:
  match found:
    case none(_): ""
    case some(g): crossing(g.value.rule, context)
sum Done:
  moved: {from: String, to: String}
  refused: Card.Refusal
def no(clause: String, reading: String) -> Done:
  Done.refused({clause: clause, reading: reading})
def enter(state: State, input: {place: String}, context: Abi.Context) -> Activity<Done>:
  if problem(state) != "" then no("misconfigured", "The commons is misconfigured: {problem(state)}") else entering(here(state, context), input.place, state, context)
def entering(found: Lists.Maybe<Presence>, place: String, state: State, context: Abi.Context) -> Activity<Done>:
  match found:
    case some(p): no("alreadyHere", "Already here, at {p.value.at}")
    case none(_): if Lists.any(state.entries, fn(e: String) -> Bool: e == place) == false then no("noWayIn", "{place} is not a way in") else if Relations.count(state.presence) >= presenceMax() then no("full", "{natText(presenceMax())} are here already.") else arrive(place, context)
def arrive(place: String, context: Abi.Context) -> Activity<Done>:
  let written(_) = write {presence: insert {who: context.principal, at: place}}
  Done.moved({from: "", to: place})
def move(state: State, input: {to: String}, context: Abi.Context) -> Activity<Done>:
  match here(state, context):
    case none(_): no("notHere", "Enter first.")
    case some(p): stepping(p.value, input.to, state, context)
def stepping(me: Presence, to: String, state: State, context: Abi.Context) -> Activity<Done>:
  if pathFrom(state, me.at, to) == false then no("noPath", "No path from {me.at} to {to}") else if gateCheck(gateOn(state, me.at, to), context) != "" then no("gated", "Gated: {gateCheck(gateOn(state, me.at, to), context)}") else crossed(me, to)
def crossed(me: Presence, to: String) -> Activity<Done>:
  let written(_) = write {presence: upsert {who: me.who, at: to}}
  Done.moved({from: me.at, to: to})
def leave(state: State, context: Abi.Context) -> Activity<Done>:
  match here(state, context):
    case none(_): no("notHere", "Not here.")
    case some(p): departing(p.value)
def departing(me: Presence) -> Activity<Done>:
  let written(_) = write {presence: retract {who: me.who}}
  Done.moved({from: me.at, to: ""})
# The owner lets one more principal through a members gate.
def allow(state: State, input: {from: String, to: String, principal: String}, context: Abi.Context) -> Activity<Done>:
  if context.principal != state.owner then no("notOwner", "Only the owner changes a gate; that is {Card.name(state.owner, context)}") else allowedOn(gateOn(state, input.from, input.to), input.principal)
def allowedOn(found: Lists.Maybe<Gate>, principal: String) -> Activity<Done>:
  match found:
    case none(_): no("noGate", "No gate on that path.")
    case some(g): allowing(g.value, principal)
def allowing(gate: Gate, principal: String) -> Activity<Done>:
  match gate.rule:
    case members(m): if Lists.length(m.names) >= namesMax() then no("gateFull", "A gate knows {natText(namesMax())} names.") else if Lists.any(m.names, fn(n: String) -> Bool: n == principal) then no("alreadyAllowed", "Already allowed.") else regated(gate, extend(gate, {rule: Rule.members({names: Lists.append(m.names, principal)})}))
    case _: no("notMembersGate", "Only a members gate lists who may cross.")
def regated(gate: Gate, next: Gate) -> Activity<Done>:
  let written(_) = world.write(extend(keep(), {gates: Plans.Entries.amendItem({item: gate, change: next})}))
  Done.moved({from: next.from, to: next.to})
form enter:
  place: text 1..64
form move:
  to: text 1..64
form leave:
# An action without a form: a gate is opened to a principal by name.
def methods() -> Lists.List<String>:
  Text.words("allow")
def blurb() -> Card.Door:
  {word: "commons", blurb: "Places, paths and gates: enter, walk, and see who may cross."}
def receive(state: State, input: Card.Reply, context: Abi.Context) -> Activity<Card.Replied>:
  Card.answer(input, context, forms(), render(state, context))
def ruleText(rule: Rule, context: Abi.Context) -> String:
  match rule:
    case open(_): ""
    case members(m): if Lists.any(m.names, fn(n: String) -> Bool: n == context.principal) then " (gated; you may cross)" else " (gated; you may not cross)"
    case object(o): " (gated by {o.object})"
def exitLine(state: State, from: String, context: Abi.Context) -> Path -> Document.Document:
  fn(path: Path) -> Document.Document: Document.text("  to {path.to}{gated(gateOn(state, from, path.to), context)}\n")
def gated(found: Lists.Maybe<Gate>, context: Abi.Context) -> String:
  match found:
    case none(_): ""
    case some(g): ruleText(g.value.rule, context)
def standing(state: State, me: Presence, context: Abi.Context) -> Document.Document:
  match placeNamed(state, me.at):
    case none(_): Document.text("You are at {me.at}, which is gone.\n")
    case some(p): Document.Document.sequence({items: Document.Documents.cons({head: Document.text("COMMONS: you are at {p.value.title}.\n{p.value.description}\n{others(state, me.at, context)}Paths:\n"), tail: Card.clipped(Lists.map(Lists.filter(state.paths, fn(path: Path) -> Bool: path.from == me.at), exitLine(state, me.at, context)), 8n)})})
def others(state: State, at: String, context: Abi.Context) -> String:
  counted(Lists.length(Lists.filter(Relations.rows(state.presence), fn(p: Presence) -> Bool: besides(p, at, context.principal))))
def besides(p: Presence, place: String, who: String) -> Bool:
  p.at == place && p.who != who
def counted(n: Nat) -> String:
  if n == 0n then "" else "{natText(n)} others here.\n"
def outside(state: State, context: Abi.Context) -> Document.Document:
  let ways = textJoin(state.entries, ", ")
  Document.text("COMMONS of {Card.name(state.owner, context)}{Card.mine(state.owner, context)}: {natText(Lists.length(state.places))} places, {natText(Relations.count(state.presence))} here. Ways in: {ways}\n")
# The card as the reader in the context sees it: someone here sees their place, who
# else is there and every path out with whether its gate lets them through.
def render(state: State, context: Abi.Context) -> Document.Document:
  match here(state, context):
    case some(p): standing(state, p.value, context)
    case none(_): outside(state, context)