Belief settling: the pass that relabels the TMS and runs the exceptWhen re-check
queue to a joint fixpoint with belief (pass-work, block-work, apply-pass!), the
seed readers a pass gathers, settle-finish and settle. A pass calls
readings and recheck; what a reader reads of the
clashes is vaelii.impl.clashes. The top engine layer, below vaelii.core. See
docs/nmtms.md.
Belief settling: the pass that relabels the TMS and runs the `exceptWhen` re-check queue to a joint fixpoint with belief (`pass-work`, `block-work`, `apply-pass!`), the seed readers a pass gathers, `settle-finish` and `settle`. A pass calls `readings` and `recheck`; what a reader reads of the clashes is `vaelii.impl.clashes`. The top engine layer, below `vaelii.core`. See docs/nmtms.md.
A volatile holding the reading a with-deferred-settle batch took before its first
write (reading-before), or nil. The batch does not name its writes in advance, so
the reading covers every standing defeat's reach. A settle inside the batch takes it
again once it has reported, and the batch's closing settle diffs against it.
A volatile holding the reading a `with-deferred-settle` batch took before its first write (`reading-before`), or nil. The batch does not name its writes in advance, so the reading covers every standing defeat's reach. A settle inside the batch takes it again once it has reported, and the batch's closing settle diffs against it.
{handle hidden?} read before a write (reading-before), or nil: the own-context belief
a write's report diffs against for the handles the defeats its sentences can move reach.
Bound by the write entry points, and by settle when none is bound.
`{handle hidden?}` read before a write (`reading-before`), or nil: the own-context belief
a write's report diffs against for the handles the defeats its sentences can move reach.
Bound by the write entry points, and by `settle` when none is bound.True while recover's settles restore a KB rather than react to a change. The passes
that report or re-derive what a change moved read it and stand aside, among them the
cut notices, the revival and un-merge re-seeds, the refusal re-asks
and the second-route re-derivations. A rebuild relabels the whole graph, so its region
is every stored sentex, and the replayed justifications already carry every
derivation. The definitional nogood sweep does not read it (docs/taxonomy.md, "What a
declaration reaches back over").
True while `recover`'s settles restore a KB rather than react to a change. The passes that report or re-derive what a change moved read it and stand aside, among them the cut notices, the revival and un-merge re-seeds, the refusal re-asks and the second-route re-derivations. A rebuild relabels the whole graph, so its region is every stored sentex, and the replayed justifications already carry every derivation. The definitional nogood sweep does not read it (docs/taxonomy.md, "What a declaration reaches back over").
True when labels flipped before the settle by a path that is neither a defeat, a
block nor a write: core/preview's jtms/suspend-premise and its rollback's
add-premise, and settle's drop of a firing over a retired spelling
(withdraw-retired-firings!). It opens the belief-moved? gate (docs/nmtms.md, "What
settle-finish reconciles"). A flag the caller binds, rather than a gate that tests
the region for a taxonomy sentex, because that test would cost a record read per region
member on every settle for a path only preview takes.
True when labels flipped before the settle by a path that is neither a defeat, a block nor a write: `core/preview`'s `jtms/suspend-premise` and its rollback's `add-premise`, and `settle`'s drop of a firing over a retired spelling (`withdraw-retired-firings!`). It opens the `belief-moved?` gate (docs/nmtms.md, "What `settle-finish` reconciles"). A flag the caller binds, rather than a gate that tests the region for a taxonomy sentex, because that test would cost a record read per region member on every settle for a path only `preview` takes.
Does a settle delete what a newly-blocked justification solely supported? False only
inside core/preview, which must hand the KB back at the same handles
(docs/preview.md).
Does a settle delete what a newly-blocked justification solely supported? False only inside `core/preview`, which must hand the KB back at the same handles (docs/preview.md).
An atom holding a set, or nil: the companion of *touched-sink*, collecting which
handles of that region were believed before the settle (jtms/touched-in).
core/edit-with-consequences! binds both.
An atom holding a set, or nil: the companion of `*touched-sink*`, collecting which handles of that region were believed before the settle (`jtms/touched-in`). `core/edit-with-consequences!` binds both.
An atom holding a set, or nil. When bound, every settle adds the handles of its
relabelled region before clearing them. core/preview and
core/edit-with-consequences! bind it (docs/preview.md).
An atom holding a set, or nil. When bound, every settle adds the handles of its relabelled region before clearing them. `core/preview` and `core/edit-with-consequences!` bind it (docs/preview.md).
(belief-before kb writes){handle hidden?} for every handle what writes can move reaches: kb/moved-reach of
their seeds (write-seeds). For a write no seed set places, or a reach a handle of which
moves a placement or queues a watched rule (special/posts-recheck?), the reach is that
of every standing defeat's target and every placed contradicts' members. The value is
whether the handle's own context does not believe it now (exc/own-hidden-fn); a handle
the reading does not hold was hidden by no defeat and no conflict.
`{handle hidden?}` for every handle what `writes` can move reaches: `kb/moved-reach` of
their seeds (`write-seeds`). For a write no seed set places, or a reach a handle of which
moves a placement or queues a watched rule (`special/posts-recheck?`), the reach is that
of every standing defeat's target and every placed `contradicts`' members. The value is
whether the handle's own context does not believe it now (`exc/own-hidden-fn`); a handle
the reading does not hold was hidden by no defeat and no conflict.predicates/entries, having passed the facet contract at this namespace's load, which
throws on a violation. A var rather than a bare call so predicates_test can prove
the check runs here on the live inputs.
`predicates/entries`, having passed the facet contract at this namespace's load, which throws on a violation. A var rather than a bare call so `predicates_test` can prove the check runs here on the live inputs.
The cross-layer facts predicates/check-facets cannot read for itself. A var so
that this call site and predicates_test check the same arguments.
:recheck-subjects — the functors posting exception re-checks through the shared
path (special/declaration-subjects) rather than from an arm of their own.:family-rosters — family -> {roster-name functors}, every roster that reads a
mark family as a family (predicates_test/a-roster-that-enumerates-a-family-is-named-here).The cross-layer facts `predicates/check-facets` cannot read for itself. A var so
that this call site and `predicates_test` check the same arguments.
* `:recheck-subjects` — the functors posting exception re-checks through the shared
path (`special/declaration-subjects`) rather than from an arm of their own.
* `:family-rosters` — `family -> {roster-name functors}`, every roster that reads a
mark family as a family (`predicates_test/a-roster-that-enumerates-a-family-is-named-here`).(reading-before kb writes)What a write that reports binds *belief-before* to before it writes: the binding in
force, or belief-before over writes when a sink is bound or a listener registered,
else nil. A defeat moves belief with no relabel, and a retraction moves a defeat before
its settle opens, so the reading precedes the write (docs/nmtms.md, "The published
window").
What a write that reports binds `*belief-before*` to before it writes: the binding in force, or `belief-before` over `writes` when a sink is bound or a listener registered, else nil. A defeat moves belief with no relabel, and a retraction moves a defeat before its settle opens, so the reading precedes the write (docs/nmtms.md, "The published window").
(rechain-exception-rules kb rule-handles)Re-chain the stored, believed forward rules among rule-handles over their whole
extent, to re-derive what a released exception suppressed. A firing whose conclusion
stands or whose exception still holds places nothing. Each rule costs one join over its
extent, so callers pass the released rules rather than the queued ones
(docs/exceptions.md). Uses chain, not chain-all: the violations ledger is scoped to
the caller's run.
Re-chain the stored, believed forward rules among `rule-handles` over their whole extent, to re-derive what a released exception suppressed. A firing whose conclusion stands or whose exception still holds places nothing. Each rule costs one join over its extent, so callers pass the released rules rather than the queued ones (docs/exceptions.md). Uses `chain`, not `chain-all`: the violations ledger is scoped to the caller's run.
(rechain-owed kb queued)The rules of the re-check queue queued a teardown re-chains over their extent
(rechain-exception-rules): every one but a rule queued only for an except's move,
whose re-derivations chain from the moved target's consequence closure
(special/drain-except-moves!), and a rule queued only for sentences and except moves
that the settle releases narrowly (released-narrowly?): a firing its block refused or
swept is in the refusal record (chain/record-swept-firing!).
The rules of the re-check queue `queued` a teardown re-chains over their extent (`rechain-exception-rules`): every one but a rule queued only for an `except`'s move, whose re-derivations chain from the moved target's consequence closure (`special/drain-except-moves!`), and a rule queued only for sentences and except moves that the settle releases narrowly (`released-narrowly?`): a firing its block refused or swept is in the refusal record (`chain/record-swept-firing!`).
(rechain-seeds kb seeds)Re-chain from seeds, the datum handles something put back on the agenda, filtered to
what is still stored and believed. One join per rule keyed by each datum's predicate,
as an assert pays (docs/nmtms.md, "A revived datum is a datum the agenda has not
seen"). Uses chain, not chain-all, as rechain-exception-rules does.
Re-chain from `seeds`, the datum handles something put back on the agenda, filtered to what is still stored and believed. One join per rule keyed by each datum's predicate, as an assert pays (docs/nmtms.md, "A revived datum is a datum the agenda has not seen"). Uses `chain`, not `chain-all`, as `rechain-exception-rules` does.
(settle kb)Settle belief (settle*) under a belief hold, re-settle while an un-merge gives
spellings back or a merge retires spellings that fired (at most max-unmerge-rounds
rounds), then deliver the moved region to the feed listeners, outside the relabel so a
listener's write starts a fresh settle. Returns nil. The rounds: docs/nmtms.md,
"The other half: a spelling an un-merge gives back".
Settle belief (`settle*`) under a belief hold, re-settle while an un-merge gives spellings back or a merge retires spellings that fired (at most `max-unmerge-rounds` rounds), then deliver the moved region to the feed listeners, outside the relabel so a listener's write starts a fresh settle. Returns nil. The rounds: docs/nmtms.md, "The other half: a spelling an un-merge gives back".
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 |