A held namespace (vaelii.impl.types.prover states what that means): the Tms
protocol alone, no implementation, in its own file apart from vaelii.impl.jtms and
vaelii.impl.dense-jtms. Its forty-odd methods make the generated protocol map large
enough that re-evaluating the form, as cloverage does to instrument a namespace,
overflows the JVM's 64 KB per-method limit; isolated here, the protocol is loaded and not
instrumented while vaelii.impl.jtms still is (scripts/coverage.sh). It requires no vaelii
namespace, so the development browser's reloader never re-evaluates it and an edit takes a
restart.
A **held namespace** (`vaelii.impl.types.prover` states what that means): the `Tms` protocol alone, no implementation, in its own file apart from `vaelii.impl.jtms` and `vaelii.impl.dense-jtms`. Its forty-odd methods make the generated protocol map large enough that re-evaluating the form, as cloverage does to instrument a namespace, overflows the JVM's 64 KB per-method limit; isolated here, the protocol is loaded and not instrumented while `vaelii.impl.jtms` still is (scripts/coverage.sh). It requires no vaelii namespace, so the development browser's reloader never re-evaluates it and an edit takes a restart.
Which role each Tms method is in, as {role #{method-name}}: the protocol docstring's
seven roles as data. A partition of what a method touches, not of what an implementation
may omit, since every mutation relabels. -believed? and -defeat-class read across
roles and say so in their own docstrings. jtms_protocol_test fails on a method in no
role, a method in two, and a name here that the protocol does not define.
Which role each `Tms` method is in, as `{role #{method-name}}`: the protocol docstring's
seven roles as data. A partition of what a method touches, not of what an implementation
may omit, since every mutation relabels. `-believed?` and `-defeat-class` read across
roles and say so in their own docstrings. `jtms_protocol_test` fails on a method in no
role, a method in two, and a name here that the protocol does not define.What a truth-maintenance network must answer, independent of how it stores the graph.
RefTms (vaelii.impl.jtms) and vaelii.impl.dense-jtms implement it, selected by
open-kb's :tms. Both run the same least-fixpoint relabel over the same affected region;
they differ in where a node's premise flag, depth and adjacency live. The obligations an
implementation owes, each with its enforcing test, are in docs/nmtms.md, What a second
network owes.
The network computes one function:
label(graph, attributes, blocked) -> (in, classes)
believed = in - superseded - held
graph is the nodes and justifications. attributes are the per-element strengths the
class fixpoint reads and the four forced sets the caller decides from stored content
(docs/nmtms.md, "The forced-monotonic set"): :mono, :out, :void and :held.
blocked and superseded are caller-computed sets replaced whole every settle, because
the network holds no KB. blocked enters inside valid? and moves in; superseded is
subtracted at the read and moves nothing. A reader's verdict and a visibility except are
applied per reading context by vaelii.impl.resolution, not on this protocol.
roles assigns every method one of seven roles (:graph :attribute :blocked
:superseded :output :touched :hold), and jtms_protocol_test fails on a method in
none or in two. Every method is named with a leading -; the plain names (in?,
add-premise, …) are the public functions in vaelii.impl.jtms, which dispatch here.
What a truth-maintenance network must answer, independent of how it stores the graph.
`RefTms` (`vaelii.impl.jtms`) and `vaelii.impl.dense-jtms` implement it, selected by
`open-kb`'s `:tms`. Both run the same least-fixpoint relabel over the same affected region;
they differ in where a node's premise flag, depth and adjacency live. The obligations an
implementation owes, each with its enforcing test, are in docs/nmtms.md, What a second
network owes.
The network computes one function:
label(graph, attributes, blocked) -> (in, classes)
believed = in - superseded - held
`graph` is the nodes and justifications. `attributes` are the per-element strengths the
class fixpoint reads and the four forced sets the caller decides from stored content
(docs/nmtms.md, "The forced-monotonic set"): `:mono`, `:out`, `:void` and `:held`.
`blocked` and `superseded` are caller-computed sets replaced whole every settle, because
the network holds no KB. `blocked` enters inside `valid?` and moves `in`; `superseded` is
subtracted at the read and moves nothing. A reader's verdict and a visibility `except` are
applied per reading context by `vaelii.impl.resolution`, not on this protocol.
`roles` assigns every method one of seven roles (`:graph` `:attribute` `:blocked`
`:superseded` `:output` `:touched` `:hold`), and `jtms_protocol_test` fails on a method in
none or in two. Every method is named with a leading `-`; the plain names (`in?`,
`add-premise`, …) are the public functions in `vaelii.impl.jtms`, which dispatch here.(-node? tms datum)Is there a node for datum?
Is there a node for `datum`?
(-superseded tms)The datum -> reason supersession map.
The `datum -> reason` supersession map.
(-supersede tms m)Replace the supersession map. No relabel, and the one
override mutation that walks no region: supersession subtracts reported belief
after the fixpoint, so no label moves. The caller computes m from the equality
closure. A map m is installed as it is, in O(1); any other collection of entries
costs its size.
Replace the supersession map. No relabel, and the one override mutation that walks no region: supersession subtracts *reported* belief after the fixpoint, so no label moves. The caller computes `m` from the equality closure. A map `m` is installed as it is, in O(1); any other collection of entries costs its size.
(-touch-mark tms)A mark of this point in the touched sets, which
-touched-since reads: every datum they record after this call is in it.
A mark of this point in the touched sets, which `-touched-since` reads: every datum they record after this call is in it.
(-held tms)The hold open on this network, or nil.
The hold open on this network, or nil.
(-justifications tms)Every live graph justification.
Every live graph justification.
(-justification tms jid)The graph justification (graph-just — no bindings), or nil.
The graph justification (`graph-just` — no bindings), or nil.
(-defeat-class tms datum)Defeat-class of an IN datum, nil when OUT. Reads
:graph-resident IN-ness too: :classes holds only the datums above the lattice's
bottom, so being IN is what separates OUT from IN at the default class.
Defeat-class of an IN datum, nil when OUT. Reads `:graph`-resident IN-ness too: `:classes` holds only the datums above the lattice's bottom, so being IN is what separates OUT from IN at the default class.
(-sweep tms seeds)Sweep the consequence closure of seeds.
Sweep the consequence closure of `seeds`.
(-reset-touched tms)Clear the touched sets, and outdate every mark.
Clear the touched sets, and outdate every mark.
(-touched-out tms)Datums a forced-set change (-set-forced) took from IN
to OUT since the reset.
Datums a forced-set change (`-set-forced`) took from IN to OUT since the reset.
(-restrength-informant tms informant strength)Set strength as the rule-contribution slot of every justification whose
informant is informant, and relabel the region their consequences span. Cost is
that region, plus the scan for the informant's justifications.
Set `strength` as the rule-contribution slot of every justification whose informant is `informant`, and relabel the region their consequences span. Cost is that region, plus the scan for the informant's justifications.
(-add-premise tms datum strength)Mark datum a premise at strength, and
relabel its region. Writes :attribute as well as :graph — strength is the
premise strength -premise-strength answers.
Mark `datum` a premise at `strength`, and relabel its region. Writes `:attribute` as well as `:graph` — `strength` is the premise strength `-premise-strength` answers.
(-touched tms)Datums whose region was relabelled since the reset.
Datums whose region was relabelled since the reset.
(-forced? tms kind x)Is x a member of forced set kind? A set lookup,
read on the relabel path.
Is `x` a member of forced set `kind`? A set lookup, read on the relabel path.
(-drop-justification tms jid)Remove the one justification jid, relabel what it
supported, and sweep what that leaves OUT; return the removals.
Remove the one justification `jid`, relabel what it supported, and sweep what that leaves OUT; return the removals.
(-datums tms)Seq of every datum with a node.
Seq of every datum with a node.
(-retract tms datum)Drop the premise, relabel, sweep; return the removals.
Drop the premise, relabel, sweep; return the removals.
(-snapshot tms)The whole network as one canonical persistent map — :nodes :justs :in :blocked :superseded :classes. The only method that spans
every role, and the comparison shape the differential oracle checks; it is the
shape RefTms happens to store, and a dense implementation materializes it, so it
is a debugging and testing surface, never something an engine path calls.
The whole network as one canonical persistent map — `:nodes :justs :in :blocked :superseded :classes`. The only method that spans every role, and the *comparison* shape the differential oracle checks; it is the shape `RefTms` happens to store, and a dense implementation materializes it, so it is a debugging and testing surface, never something an engine path calls.
(-blocked tms)The blocked justification-id set.
The blocked justification-id set.
(-any-node? tms)Is there any node at all? A boolean that must not
materialize the datum seq — (first (-datums …)) drains the whole dense bitmap
into boxed Longs, so callers on a render/poll path use this instead.
Is there any node at all? A boolean that must not materialize the datum seq — `(first (-datums …))` drains the whole dense bitmap into boxed Longs, so callers on a render/poll path use this instead.
(-relabel tms)Whole-graph relabel — no engine path calls it; see
vaelii.impl.jtms/relabel. The one method whose cost is the graph rather than a
region, which is why nothing on the engine path may acquire the habit.
Whole-graph relabel — no engine path calls it; see `vaelii.impl.jtms/relabel`. The one method whose cost is the graph rather than a region, which is why nothing on the engine path may acquire the habit.
(-dependents tms datum)Justification ids using datum as an antecedent.
Justification ids using `datum` as an antecedent.
(-premise? tms datum)Is datum a premise?
Is `datum` a premise?
(-hold tms h)Open hold h (vaelii.impl.observe/new-hold) on this
network, and answer true, or answer false when a hold is open on it already. From this
call until -release, every relabel records the labels it moves as they were before
the first move, and a read on a thread other than h's owner answers from those while
vaelii.impl.observe/reads-held? is true of h.
Open hold `h` (`vaelii.impl.observe/new-hold`) on this network, and answer true, or answer false when a hold is open on it already. From this call until `-release`, every relabel records the labels it moves as they were before the first move, and a read on a thread other than `h`'s owner answers from those while `vaelii.impl.observe/reads-held?` is true of `h`.
(-ensure-node tms datum depth)Create the node if absent; lower its depth and the
depths below it (jtms/lowered-depths). The one graph mutation that relabels
nothing: a node with no premise mark and no justification is OUT either way.
Create the node if absent; lower its depth and the depths below it (`jtms/lowered-depths`). The one graph mutation that relabels nothing: a node with no premise mark and no justification is OUT either way.
(-set-forced tms kind xs on?)Add each of xs to forced set kind (on?
true) or take it out, and relabel the region of the members that moved: the datums
themselves for :mono and :out, the consequences for :void, and none for :held,
whose IN members -touched and -touched-in record as a relabel would. A member need not
have a node or a justification yet, so a caller writes it before the element it
governs and the element never holds a label the set rules out.
Add each of `xs` to forced set `kind` (`on?` true) or take it out, and relabel the region of the members that moved: the datums themselves for `:mono` and `:out`, the consequences for `:void`, and none for `:held`, whose IN members `-touched` and `-touched-in` record as a relabel would. A member need not have a node or a justification yet, so a caller writes it before the element it governs and the element never holds a label the set rules out.
(-believed? tms datum)Is datum believed (IN, minus supersession and the
:held forced set)? Reads :superseded and :attribute as well as :output,
because believed = in - superseded - held is the definition rather than a filter
over it. An empty :held set costs one emptiness check.
Is `datum` believed (IN, minus supersession and the `:held` forced set)? Reads `:superseded` and `:attribute` as well as `:output`, because `believed = in - superseded - held` is the definition rather than a filter over it. An empty `:held` set costs one emptiness check.
(-suspend-premise tms datum)Drop datum's premise mark and relabel — no sweep.
Drop `datum`'s premise mark and relabel — no sweep.
(-depth tms datum)Derivation depth, 0 when unknown.
Derivation depth, 0 when unknown.
(-believed tms)Seq of the believed datums, or nil when none.
Seq of the believed datums, or nil when none.
(-add-justification tms just)Record just and relabel what it moves. just carries
its own strength, so this writes :attribute too.
Record `just` and relabel what it moves. `just` carries its own strength, so this writes `:attribute` too.
(-touched-new tms)Datums whose node was created since the reset.
Datums whose node was created since the reset.
(-touched-since tms mark)The datums the touched sets recorded after mark, a datum
relabelled again since included; the whole -touched set for a mark taken before the
last -reset-touched, or nil.
The datums the touched sets recorded after `mark`, a datum relabelled again since included; the whole `-touched` set for a mark taken before the last `-reset-touched`, or nil.
(-set-blocked tms jids)Replace the blocked set and relabel what moved.
Blocking enters through valid?, so an excepted conclusion goes OUT and is swept
rather than retained. An id with no justification is not kept. The caller
evaluates the exceptions and hands jids in — the network holds no KB and cannot run
the query — so the cost here is the region seeded by the justifications whose blocked
status changed, never the cost of deciding which those are.
Replace the blocked set and relabel what moved. Blocking enters through `valid?`, so an excepted conclusion goes OUT and is swept rather than retained. An id with no justification is not kept. The caller evaluates the exceptions and hands `jids` in — the network holds no KB and cannot run the query — so the cost here is the region seeded by the justifications whose blocked status changed, never the cost of deciding which those are.
(-supports tms datum)Justification ids concluding datum.
Justification ids concluding `datum`.
(-touched-in tms)Of those, the ones already believed when first relabelled.
Of those, the ones already believed when first relabelled.
(-any-belief? tms)Is any datum believed (IN, minus supersession and :held)? Like
-any-node?, terminates at the first believed datum rather than draining -believed.
Is any datum believed (IN, minus supersession and `:held`)? Like `-any-node?`, terminates at the first believed datum rather than draining `-believed`.
(-premise-strength tms datum)Its assumption strength, or nil. Read once per in-region node by the class fixpoint, which is what obligation 4 requires to be a memory read on every representation.
Its assumption strength, or nil. Read once per in-region node by the class fixpoint, which is what obligation 4 requires to be a memory read on every representation.
(-release tms h)Close hold h on this network, when it is the one open.
Close hold `h` on this network, when it is the one open.
(-forced-members tms kind)Every member of forced set kind, as a set. Read by a
diagnostic that enumerates the set (vaelii.core/violations); no relabel path calls it.
Every member of forced set `kind`, as a set. Read by a diagnostic that enumerates the set (`vaelii.core/violations`); no relabel path calls it.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |