The special-predicate dispatch table: what each functor the engine interprets does to the derived state around the store, stated once, with every half of every behaviour side by side.
A special predicate needs behaviour in four places — reflecting a stored sentex
into the caches, the removal mirror, recover's cache-only replay, and wff's
per-functor well-formedness check — and the compiler cross-checks none of them, so
the arms live once here, in arms, keyed by functor:
:integrate (fn [kb sentex handle]) reflect a newly stored sentex into the caches
:disintegrate (fn [kb sentex]) the mirror, reference-counted on (:id sentex)
:rebuild (fn [tax sentex]) recover's cache-only replay — no re-check
posting, no migration, no universal lifting,
because the store already holds what those
side effects produced
:wff (fn [tax sentence context]) structural well-formedness (vaelii.impl.wff
keeps the check fns; the table points at them.
context scopes the arms that read it — today
only disjoint-problems)
and check-entries refuses an asymmetric entry at namespace load, so an
add-side arm without its removal and rebuild halves is a build failure rather
than a cache that drifts on the first retraction or restart.
The enumeration is not here. Which functors the engine interprets, in what
order, what each one says — its sentence shape, the :props kind it maintains,
whether its arms run on the derivation path — is one entry per term in
vaelii.impl.predicates, which requires nothing and so can be read by taxonomy,
wff and provers, none of which can read this namespace. That split is what
lifts the four-place ceiling above: the arms need functions from four layers and
can only ever live at layer three, while what a predicate says is needed at every
layer there is. entries joins the two, check-declarations refuses a
disagreement, and predicates_test checks the join against the live tables.
structural-integrate stays outside that framework permanently and no declaration
can name its arms: they dispatch on a sentence's shape rather than on its functor
— a rule, an exceptWhen meta, a visibility except, and a disjoint metatype's
member, whose functor is the metatype and so is data rather than vocabulary.
What this namespace still owns is everything the arms are and everything they need:
all four arm columns, the five walks over them, the exception re-check queue the
taxonomy arms post to, the universal-predicate lifting, and the equality migration.
Third layer of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle): everything here reads kb and checks, and the store-mutation choke points in
vaelii.impl.integrate sit directly above.
The special-predicate dispatch table: what each functor the engine interprets
*does* to the derived state around the store, stated once, with every half of every
behaviour side by side.
A special predicate needs behaviour in four places — reflecting a stored sentex
into the caches, the removal mirror, `recover`'s cache-only replay, and `wff`'s
per-functor well-formedness check — and the compiler cross-checks none of them, so
the arms live once here, in `arms`, keyed by functor:
:integrate (fn [kb sentex handle]) reflect a newly stored sentex into the caches
:disintegrate (fn [kb sentex]) the mirror, reference-counted on (:id sentex)
:rebuild (fn [tax sentex]) recover's cache-only replay — no re-check
posting, no migration, no universal lifting,
because the store already holds what those
side effects produced
:wff (fn [tax sentence context]) structural well-formedness (vaelii.impl.wff
keeps the check fns; the table points at them.
`context` scopes the arms that read it — today
only `disjoint-problems`)
and `check-entries` refuses an asymmetric entry **at namespace load**, so an
add-side arm without its removal and rebuild halves is a build failure rather
than a cache that drifts on the first retraction or restart.
**The enumeration is not here.** Which functors the engine interprets, in what
order, what each one *says* — its sentence shape, the `:props` kind it maintains,
whether its arms run on the derivation path — is one entry per term in
`vaelii.impl.predicates`, which requires nothing and so can be read by `taxonomy`,
`wff` and `provers`, none of which can read this namespace. That split is what
lifts the four-place ceiling above: the arms need functions from four layers and
can only ever live at layer three, while what a predicate *says* is needed at every
layer there is. `entries` joins the two, `check-declarations` refuses a
disagreement, and `predicates_test` checks the join against the live tables.
`structural-integrate` stays outside that framework permanently and no declaration
can name its arms: they dispatch on a sentence's *shape* rather than on its functor
— a rule, an `exceptWhen` meta, a visibility `except`, and a disjoint metatype's
member, whose functor is the metatype and so is data rather than vocabulary.
What this namespace still owns is everything the arms are and everything they need:
all four arm columns, the five walks over them, the exception re-check queue the
taxonomy arms post to, the universal-predicate lifting, and the equality migration.
Third layer of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle): everything here reads kb and checks, and the store-mutation choke points in
`vaelii.impl.integrate` sit directly above.False while a *bulk-load?* write settles: the drain draws no argument types over the
facts a genlCx move shows (entail-under-context-edge). record-arg-types draws them
after the load.
False while a `*bulk-load?*` write settles: the drain draws no argument types over the facts a `genlCx` move shows (`entail-under-context-edge`). `record-arg-types` draws them after the load.
A volatile of {:edges #{[sub super]} :arrived #{handle} :derived {functor #{handle}}},
or nil: the belief moves a write's settles make that the structural genlCx producer
reads once the write has settled (context-nat/reconcile-moves). A write entry point
binds it to producer-moves. The context-move drain adds the edges it read, a settle
pass the datums it revived, and derived-sentex-added each derivation.
A volatile of `{:edges #{[sub super]} :arrived #{handle} :derived {functor #{handle}}}`,
or nil: the belief moves a write's settles make that the structural genlCx producer
reads once the write has settled (`context-nat/reconcile-moves`). A write entry point
binds it to `producer-moves`. The context-move drain adds the edges it read, a settle
pass the datums it revived, and `derived-sentex-added` each derivation.nil, or a volatile {key rule-handles} of the watched rules a re-check trigger reads
for one predicate, which recheck-read answers from. A sweep that mints many
memberships of few types binds one (with-recheck-reads), as does
chain/sync-arity-classes! placing class memberships: each placement posts the trigger
of its type, and the rules read for a type are the same for every placement of it. The key
carries the genl generation, since a sweep can mint a genl edge (genlArg); the
sweeps store no rule and no declaration a read here names.
nil, or a volatile `{key rule-handles}` of the watched rules a re-check trigger reads
for one predicate, which `recheck-read` answers from. A sweep that mints many
memberships of few types binds one (`with-recheck-reads`), as does
`chain/sync-arity-classes!` placing class memberships: each placement posts the trigger
of its type, and the rules read for a type are the same for every placement of it. The key
carries the `genl` generation, since a sweep can mint a `genl` edge (`genlArg`); the
sweeps store no rule and no declaration a read here names.False under *bulk-load?* and in the settles an open, a recover or an upgrade runs,
the first settle after a trusted image install among them (defer-first-release!):
withheld-releases then draws nothing and keeps the departures and arrivals it would
have read owed (:owed in mint-queues, which the image carries), and
release-withheld! draws them.
False under `*bulk-load?*` and in the settles an open, a recover or an upgrade runs, the first settle after a trusted image install among them (`defer-first-release!`): `withheld-releases` then draws nothing and keeps the departures and arrivals it would have read owed (`:owed` in `mint-queues`, which the image carries), and `release-withheld!` draws them.
False while a write asserted with {:chain? false} settles: the drain re-checks what a
genlCx move moves and seeds no chaining from it (drain-context-moves!).
False while a write asserted with `{:chain? false}` settles: the drain re-checks what a
`genlCx` move moves and seeds no chaining from it (`drain-context-moves!`).(advance-refusal-generations! kb {:keys [taxonomy gens conviction]})Record the generations now on the :lift entries recorded under the
generations before held (its :taxonomy, :gens and :conviction, read before a
batch), when a rollback has put the relations and the separations back as they were
(tax/relations-match?). Generations only grow, so without it the next settle re-asks
every entry the batch found settled (docs/preview.md, "What the rollback restores").
An entry recorded under other generations stays owed its re-ask.
Record the generations now on the `:lift` entries recorded under the generations `before` held (its `:taxonomy`, `:gens` and `:conviction`, read before a batch), when a rollback has put the relations and the separations back as they were (`tax/relations-match?`). Generations only grow, so without it the next settle re-asks every entry the batch found settled (docs/preview.md, "What the rollback restores"). An entry recorded under other generations stays owed its re-ask.
(antisym-equate-existing kb sentence)When an (anti_symmetric P) declaration arrives, hand every stored fact of P's spec
subtree to derive-antisymmetric-equalities, as equate-existing does for the
functional family. nil when sentence declares nothing antisymmetric.
When an `(anti_symmetric P)` declaration arrives, hand every stored fact of `P`'s spec subtree to `derive-antisymmetric-equalities`, as `equate-existing` does for the functional family. nil when `sentence` declares nothing antisymmetric.
(antisym-equate-under-context-edge kb m)When a (genlCx sub super) edge arrives, derive the equalities an (anti_symmetric …)
mark licenses over the facts the widened ancestor set newly makes jointly visible: the
twin of equate-under-context-edge, over derive-antisymmetric-equalities.
When a `(genlCx sub super)` edge arrives, derive the equalities an `(anti_symmetric …)` mark licenses over the facts the widened ancestor set newly makes jointly visible: the twin of `equate-under-context-edge`, over `derive-antisymmetric-equalities`.
(antisym-equate-under-edge kb sentence)When a (genl sub super) edge arrives, derive the equalities an (anti_symmetric …)
mark above super now licenses over the (sub …) facts already stored — the twin of
equate-under-edge. Free for an edge no anti_symmetric mark stands above, decided
before the subtree is read. nil when sentence is not a genl edge.
When a `(genl sub super)` edge arrives, derive the equalities an `(anti_symmetric …)` mark above `super` now licenses over the `(sub …)` facts already stored — the twin of `equate-under-edge`. Free for an edge no `anti_symmetric` mark stands above, decided before the subtree is read. nil when `sentence` is not a `genl` edge.
(arg-type-extents kb)The facts the argument-type pass draws, as [[functor handles] …]: every functor an
entailing declaration reaches, in content order (declared-functors), with the handles
stored now. Empty under VAELII_ASSERTIVE_ARG_TYPES=0. A store loaded around assert
(a dump import, *bulk-load?*, bulk-assert-facts!) holds no derived memberships; the
pass draws them per fact (draw-fact).
The facts the argument-type pass draws, as `[[functor handles] …]`: every functor an entailing declaration reaches, in content order (`declared-functors`), with the handles stored now. Empty under `VAELII_ASSERTIVE_ARG_TYPES=0`. A store loaded around `assert` (a dump import, `*bulk-load?*`, `bulk-assert-facts!`) holds no derived memberships; the pass draws them per fact (`draw-fact`).
(argument-refusals? kb)Does the refusal record hold a refused lift, waiting on an argument conviction? One
map read (:kinds).
Does the refusal record hold a refused lift, waiting on an argument conviction? One map read (`:kinds`).
(arrival-releasable-rule? kb rh)Can an arriving fact release a block on the rule stored at rh? True when
rules/arrival-releasable? holds of it, or rules/exception-arrival-releasable? of
its exceptions. The settle loop owes such a rule a re-join, and the two edge triggers
below exempt it from their firing-side narrowing.
Can an arriving fact release a block on the rule stored at `rh`? True when `rules/arrival-releasable?` holds of it, or `rules/exception-arrival-releasable?` of its exceptions. The settle loop owes such a rule a re-join, and the two edge triggers below exempt it from their firing-side narrowing.
(bearing-equalities kb sentence)The handles of every equality edge and schematic rewrite rule that could bear on
sentence: the supporters across the whole class of each merged symbol it names
(docs/equality.md, "The reader is not the fact's own context"), unbelieved ones
included, since each candidate reader re-reads belief and visibility. Empty when no
symbol of sentence is merged and no rule applies, decided before any class walk or
record read: the assert path offers every sentex to migration.
The handles of every equality edge and schematic rewrite rule that could bear on `sentence`: the supporters across the whole **class** of each merged symbol it names (docs/equality.md, "The reader is not the fact's own context"), unbelieved ones included, since each candidate reader re-reads belief and visibility. Empty when no symbol of `sentence` is merged and no rule applies, decided before any class walk or record read: the assert path offers every sentex to migration.
(believed-again-sweeps kb handles)Run, for each symbol-merge supporter in handles that is stored and believed, what
its arrival runs over the stored facts: the re-check of the merged class
(recheck-equality-edge) and the migration (equality-arrival-sweep). Returns one
{:new :superseded :violations}. handles is tax/take-believed-again!'s answer: a
supporter whose firing was held void met its arrival with nothing to restate, and a
relabel brings it IN with no arrival. Walked in content order, and scoped to each
supporter's class.
Run, for each symbol-merge supporter in `handles` that is stored and believed, what
its arrival runs over the stored facts: the re-check of the merged class
(`recheck-equality-edge`) and the migration (`equality-arrival-sweep`). Returns one
`{:new :superseded :violations}`. `handles` is `tax/take-believed-again!`'s answer: a
supporter whose firing was held void met its arrival with nothing to restate, and a
relabel brings it IN with no arrival. Walked in content order, and scoped to each
supporter's class.(call-with-pass-caches kb f)(f) holding, across the facts a pass over kb draws, the admission checks' answers
(*admission-memo*), each context's reader state (exc/with-reader-states) and the
justification dedup index (jtms/with-dedup-cache); the ones already bound are kept.
`(f)` holding, across the facts a pass over `kb` draws, the admission checks' answers (`*admission-memo*`), each context's reader state (`exc/with-reader-states`) and the justification dedup index (`jtms/with-dedup-cache`); the ones already bound are kept.
(check-declarations entries)(check-declarations entries arm-functors)Refuse a table whose arms and declarations disagree, at namespace load, as the
cross-layer half of check-entries: a functor with arms and no declaration or the
reverse (arm-functors is read before entries filters to pr/in-special-table; the
one-argument arity reads the functors off entries); a :cached declaration whose arms
have no cache triple, or the reverse; a :checked declaration whose arms have no
:wff, or the reverse. Throws :bad-table-entry with :mismatch. The two validators
stay separate (docs/predicates.md).
Refuse a table whose arms and declarations disagree, at namespace load, as the cross-layer half of `check-entries`: a functor with arms and no declaration or the reverse (`arm-functors` is read before `entries` filters to `pr/in-special-table`; the one-argument arity reads the functors off `entries`); a `:cached` declaration whose arms have no cache triple, or the reverse; a `:checked` declaration whose arms have no `:wff`, or the reverse. Throws `:bad-table-entry` with `:mismatch`. The two validators stay separate (docs/predicates.md).
(check-entries entries)Refuse an ill-formed table at namespace load: an entry with some of the cache arms
(:integrate, :disintegrate, :rebuild) and not all, or with no arm at all. Throws
:bad-table-entry with :mismatch :partial-cache-triple or :no-arm. Returns
entries unchanged.
Refuse an ill-formed table at namespace load: an entry with some of the cache arms (`:integrate`, `:disintegrate`, `:rebuild`) and not all, or with no arm at all. Throws `:bad-table-entry` with `:mismatch` `:partial-cache-triple` or `:no-arm`. Returns `entries` unchanged.
(class-moved-merges kb region asked drop?)Re-ask the collision merges of the handles in region (a delay over jtms/touched)
whose class can have moved: drop each collision justification whose members are all IN
and one at :default (off when drop? is false), and re-derive from each member IN at
:monotonic but a premise this settle created at that class. asked is the settle's
volatile set of [handle class] asked already. {:new :superseded :violations :removed :members}, :removed the merged removals for the caller's stores and :members the
dropped justifications' members; nil, with region unforced, when no merge mark is
declared. See docs/equality.md, "functional infers equality instead of throwing".
Re-ask the collision merges of the handles in `region` (a delay over `jtms/touched`)
whose class can have moved: drop each collision justification whose members are all IN
and one at `:default` (off when `drop?` is false), and re-derive from each member IN at
`:monotonic` but a premise this settle created at that class. `asked` is the settle's
volatile set of `[handle class]` asked already. `{:new :superseded :violations :removed
:members}`, `:removed` the merged removals for the caller's stores and `:members` the
dropped justifications' members; nil, with `region` unforced, when no merge mark is
declared. See docs/equality.md, "`functional` infers equality instead of throwing".(clear-except-moves! kb)Empty :except-moves outright — a rebuild reconciles every supersession from scratch.
Empty `:except-moves` outright — a rebuild reconciles every supersession from scratch.
(closure-edge-relation sentence)The closure relation sentence puts edges into: its functor for a binary genl or
genlCx edge, genl for a cover (tax/installed-edges), and nil for any other sentence.
The closure relation `sentence` puts edges into: its functor for a binary `genl` or `genlCx` edge, `genl` for a cover (`tax/installed-edges`), and nil for any other sentence.
(computed-reading-rules kb bfn s)The forward rules a datum on bfn re-joins and re-checks because bfn is a
predicate a registered SupportingProver reads: the rules carrying an antecedent that a
prover reading bfn answers (provers/support-answers-reading). bfn is the functor
of the sentence's underlying body, so a believed (not (conversionFactor …)) counts.
Reads the rules stated in every context; one map lookup for a datum no prover reads.
s is the sentence: a genl edge moves only the expression kinds at or above its
upper end.
The forward rules a datum on `bfn` re-joins and re-checks because `bfn` is a predicate a registered `SupportingProver` reads: the rules carrying an antecedent that a prover reading `bfn` answers (`provers/support-answers-reading`). `bfn` is the functor of the sentence's underlying body, so a believed `(not (conversionFactor …))` counts. Reads the rules stated in every context; one map lookup for a datum no prover reads. `s` is the sentence: a `genl` edge moves only the expression kinds at or above its upper end.
(context-move kb sub super)What the move of the genlCx edge [sub super] shows or hides (tax/context-move),
with the reader classes the stored excepts on genlCx supporters' support split the
readers into (exc/genlCx-except-contexts). The walks without the edge do not cross an
edge stored in both polarities, so that edge can only enlarge the answer.
What the move of the `genlCx` edge `[sub super]` shows or hides (`tax/context-move`), with the reader classes the stored `except`s on `genlCx` supporters' support split the readers into (`exc/genlCx-except-contexts`). The walks without the edge do not cross an edge stored in both polarities, so that edge can only enlarge the answer.
(conviction-generations kb)taxonomy-generations with the separations (tax/separation-inputs): the value an
argument conviction is decided under, a refused lift's and an argument hold's
(checks/refresh-argument-holds!). A conviction reads a type the taxonomy separates
from the declared one, so a separation moving re-asks it.
`taxonomy-generations` with the separations (`tax/separation-inputs`): the value an argument conviction is decided under, a refused lift's and an argument hold's (`checks/refresh-argument-holds!`). A conviction reads a type the taxonomy separates from the declared one, so a separation moving re-asks it.
(covered-merges kb moved)The collision justifications, in id order, of every merge copy covered-copies finds
in a class the equality partition moved since the last call (tax/take-equality-moves!
as :covers, every merged term after a recover's replay) or in the class of a merge
of moved (move-covered-merges). A reader that sees a pair in one class derives no
merge of it, so a covered copy is one that an arrival order placing the more general
merges first never stores (docs/equality.md, "A merge copy that a more general merge
covers is dropped"). nil when no merge mark is declared; the moved terms are taken
either way.
The collision justifications, in id order, of every merge copy `covered-copies` finds in a class the equality partition moved since the last call (`tax/take-equality-moves!` as `:covers`, every merged term after a `recover`'s replay) or in the class of a merge of `moved` (`move-covered-merges`). A reader that sees a pair in one class derives no merge of it, so a covered copy is one that an arrival order placing the more general merges first never stores (docs/equality.md, "A merge copy that a more general merge covers is dropped"). nil when no merge mark is declared; the moved terms are taken either way.
The informant of the justification of (unary_predicate T) by an argument declaration
naming T (unary-entailments). No mint informant (kb/mint-informant?): the membership
enters no mint family, and only a conflicting length withdraws it
(withdrawn-type-entailments).
The informant of the justification of `(unary_predicate T)` by an argument declaration naming `T` (`unary-entailments`). No mint informant (`kb/mint-informant?`): the membership enters no mint family, and only a conflicting length withdraws it (`withdrawn-type-entailments`).
(deduce-arg-types kb entailments handle context)(deduce-arg-types kb entailments handle context pre-checked?)Materialize the entailments checks/constraint-entailments drew over a sentence
stored at handle in context: {:new [handles] :violations [v]}. Called from
assert and from forward chaining's place-conclusion. pre-checked? skips the
definitional constraint check of each mint (inadmissible); only the assert path's
first level passes true.
Materialize the entailments `checks/constraint-entailments` drew over a sentence
stored at `handle` in `context`: `{:new [handles] :violations [v]}`. Called from
`assert` and from forward chaining's `place-conclusion`. `pre-checked?` skips the
definitional constraint check of each mint (`inadmissible`); only the assert path's
first level passes true.(deduce-below kb sentence handle context)(deduce-below kb sentence handle context keep?)Materialize what the declarations declarations-below finds say about the fact
sentence stored at handle in context, at each of their placements:
{:new [handles] :violations [v]}. Each mint names the fact, the declaration and the
genlCx edges its placement sees both through (checks/declaration-entailments). The
assert path and chain/place-conclusion call it beside deduce-arg-types. keep?,
when given, takes an entailment and its placement.
Materialize what the declarations `declarations-below` finds say about the fact
`sentence` stored at `handle` in `context`, at each of their placements:
`{:new [handles] :violations [v]}`. Each mint names the fact, the declaration and the
`genlCx` edges its placement sees both through (`checks/declaration-entailments`). The
assert path and `chain/place-conclusion` call it beside `deduce-arg-types`. `keep?`,
when given, takes an entailment and its placement.(deduce-lifts kb sentence handle context)Deduce sentence (stored at handle in context) into CxUniverse when
lifts-to-universe? holds of its predicate — {:new [handles] :violations [v]}, nil
otherwise. Called by assert and by forward chaining's place-conclusion. A
permuting mark is lifted on its statement alone, whatever the KB declares; any other
is lifted once per declaring sentex
(docs/contexts.md#decontextualized_predicate-a-fact-that-belongs-to-the-kb-not-to-one-theory).
Deduce `sentence` (stored at `handle` in `context`) into CxUniverse when
`lifts-to-universe?` holds of its predicate — `{:new [handles] :violations [v]}`, nil
otherwise. Called by `assert` and by forward chaining's `place-conclusion`. A
permuting mark is lifted on its statement alone, whatever the KB declares; any other
is lifted once per declaring sentex
(docs/contexts.md#decontextualized_predicate-a-fact-that-belongs-to-the-kb-not-to-one-theory).(defer-first-release! kb)Make kb's next settle run with *release-withheld?* false (take-first-deferral!).
Make `kb`'s next settle run with `*release-withheld?*` false (`take-first-deferral!`).
(departed-edge-seeds kb handles)The chaining seeds a settle owes the records among handles that hold closure edges
(closure-edge-relation) and went IN to OUT: resubsumption-seeds for an edge that
lost belief rather than its record. Runs per edge only when a dependent is now OUT
(docs/nmtms.md, "Where the layer stops").
The chaining seeds a settle owes the records among `handles` that hold closure edges (`closure-edge-relation`) and went IN to OUT: `resubsumption-seeds` for an edge that lost belief rather than its record. Runs per edge only when a dependent is now OUT (docs/nmtms.md, "Where the layer stops").
(derive-antisymmetric-equalities kb sentence context handle)(derive-antisymmetric-equalities kb sentence context handle readers)derive-antisymmetric-equalities-in run from every reader at or below context, with
the presence checks and the readers narrowing derive-functional-equalities takes.
`derive-antisymmetric-equalities-in` run from every reader at or below `context`, with the presence checks and the `readers` narrowing `derive-functional-equalities` takes.
(derive-functional-equalities kb sentence context handle)(derive-functional-equalities kb sentence context handle readers)derive-functional-equalities-in run from every reader at or below context
(merge-readers). readers, when given, narrows that set; only
equate-under-context-edge-via passes it. Two presence checks precede the reader
sweep: tax/functional-family-declared? and functional-mark-relevant?.
`derive-functional-equalities-in` run from every reader at or below `context` (`merge-readers`). `readers`, when given, narrows that set; only `equate-under-context-edge-via` passes it. Two presence checks precede the reader sweep: `tax/functional-family-declared?` and `functional-mark-relevant?`.
(derive-merge kb sentence context informant antes)Store the equality sentence in context as a derivation from antes under
informant, and merge with it. Returns the migration result. The antecedents are
ordered by content (kb/antecedent-order), so the list why prints does not depend on
which fact arrived first.
Store the equality `sentence` in `context` as a derivation from `antes` under `informant`, and merge with it. Returns the migration result. The antecedents are ordered by content (`kb/antecedent-order`), so the list `why` prints does not depend on which fact arrived first.
(derived-sentex-added kb sentex handle)The derivation-path add choke point: the integration arms a derived sentex may reach
(integrate-transitive for a functor the table keys; the structural walk minus the rule
arm otherwise) and the exception re-check post. The except arm's
reconcile-belief-change runs inline mid-fixpoint: it only swaps the taxonomy and
writes cache entries. mark-premise runs before integrate/sentex-added, with no
read between the store and the justification. Callers: forward chaining's
place-conclusion, the decontextualized_predicate lift, the argument-constraint
entailment and derive-equality. See docs/taxonomy.md and docs/exceptions.md.
The derivation-path add choke point: the integration arms a derived sentex may reach (`integrate-transitive` for a functor the table keys; the structural walk minus the rule arm otherwise) and the exception re-check post. The except arm's `reconcile-belief-change` runs inline mid-fixpoint: it only swaps the taxonomy and writes cache entries. `mark-premise` runs before `integrate/sentex-added`, with no read between the store and the justification. Callers: forward chaining's `place-conclusion`, the `decontextualized_predicate` lift, the argument-constraint entailment and `derive-equality`. See docs/taxonomy.md and docs/exceptions.md.
(descent-surplus-placements kb moved)The mint justifications, in id order, that a record among moved left at a context
no longer a placement of their fact and declaration (pair-placements): a genl route
or trigger membership stated in a more general context places the pair above, and the
placement below goes. A record installing genl edges whose super reaches a
declaration (super-reaches-declaration?) reads its subs' facts; a membership whose
type reaches a trigger type (trigger-types, through tax/genls-global, E17) reads the
facts naming its term.
The mint justifications, in id order, that a record among `moved` left at a context no longer a placement of their fact and declaration (`pair-placements`): a `genl` route or trigger membership stated in a more general context places the pair above, and the placement below goes. A record installing `genl` edges whose `super` reaches a declaration (`super-reaches-declaration?`) reads its `sub`s' facts; a membership whose type reaches a trigger type (`trigger-types`, through `tax/genls-global`, E17) reads the facts naming its term.
(different-rechecked-terms kb rh triggers)The terms a firing or a refusal of the rule at rh must bind for one of its queued
triggers to have flipped it, or nil when the triggers say nothing that narrow. Only
a different-only-rule? narrows, and only when every trigger is a merge's
{::merged class} marker or a sentence sentence-moved-terms reads.
The terms a firing or a refusal of the rule at `rh` must bind for one of its queued
`triggers` to have flipped it, or nil when the triggers say nothing that narrow. Only
a `different-only-rule?` narrows, and only when every trigger is a merge's
`{::merged class}` marker or a sentence `sentence-moved-terms` reads.(disintegrate-sentex! kb sentex)The mirror walk: reverse a departing sentex's cache effects through the
:disintegrate column, or the matching structural arm. Every cache below is
reference-counted on the departing sentex's id, so an entry survives while
another sentex still asserts the same claim.
The mirror walk: reverse a departing sentex's cache effects through the `:disintegrate` column, or the matching structural arm. Every cache below is reference-counted on the departing sentex's id, so an entry survives while another sentex still asserts the same claim.
(drain-context-moves! kb read rebuilding?)Once a settle pass: read the genlCx moves since the placement cursor
(decide/take-edge-cursor!), compute each one's context-move once, and hand it to
every row of move-families the move reads. The edges are moved-edges'; the
placement families read :reach, a delay of {:under :below} over the unscoped
closures (decide/unscoped-closures); the active edges an except that moved reaches
are moves of their own (excepted-edges). read is the settle's volatile of supporter
labels drained. Each row a move runs is a step (dur/check-abort!), and a drain past
progress/first-line-ms logs a line per doubling. Returns {:reach :first? :seeds :covered :mig}. A rebuild takes the departures, leaves the cursor and runs no row. See
docs/contexts.md, "One context move".
Once a settle pass: read the `genlCx` moves since the placement cursor
(`decide/take-edge-cursor!`), compute each one's `context-move` once, and hand it to
every row of `move-families` the move reads. The edges are `moved-edges`'; the
placement families read `:reach`, a delay of `{:under :below}` over the unscoped
closures (`decide/unscoped-closures`); the active edges an `except` that moved reaches
are moves of their own (`excepted-edges`). `read` is the settle's volatile of supporter
labels drained. Each row a move runs is a step (`dur/check-abort!`), and a drain past
`progress/first-line-ms` logs a line per doubling. Returns `{:reach :first? :seeds
:covered :mig}`. A rebuild takes the departures, leaves the cursor and runs no row. See
docs/contexts.md, "One context move".(drain-departures! kb)The records note-departure! queued since the last drain, and the queue emptied.
The records `note-departure!` queued since the last drain, and the queue emptied.
(drain-except-moves! kb sweep?)Take the pending handles off :except-moves, sweep them (except-move-sweeps, with
sweep?), and keep the handles, the supersessions the sweeps found and the region the
moves can change (except-move-region) for take-except-moves!. Returns the sweeps' result,
its :new joined by the believed facts of the targets' consequence closure and of the
antecedents resting on it, to chain from, or nil when nothing was pending.
Take the pending handles off `:except-moves`, sweep them (`except-move-sweeps`, with `sweep?`), and keep the handles, the supersessions the sweeps found and the region the moves can change (`except-move-region`) for `take-except-moves!`. Returns the sweeps' result, its `:new` joined by the believed facts of the targets' consequence closure and of the antecedents resting on it, to chain from, or nil when nothing was pending.
(draw-fact kb h deadline)Draw the argument-type entailments of the stored fact at h, at its placements
(deduce-placed): {:new [h …] :violations [v …]}, nothing for a rule, a negation or a
handle the store no longer holds. A mint the draw would leave as it is
(changed-only) is not asked about, so a violation of one already stored is not
reported again. With deadline, a budget/now instant, a draw whose checks run past
it stops at the next mint and adds :deferred {:phase :transitions}: the part of the
checks that ran out, and every mint it brought IN, whose own entailments the re-run
draws (redraw-deferred). Run under call-with-pass-caches.
Draw the argument-type entailments of the stored fact at `h`, at its placements
(`deduce-placed`): `{:new [h …] :violations [v …]}`, nothing for a rule, a negation or a
handle the store no longer holds. A mint the draw would leave as it is
(`changed-only`) is not asked about, so a violation of one already stored is not
reported again. With `deadline`, a `budget/now` instant, a draw whose checks run past
it stops at the next mint and adds `:deferred {:phase :transitions}`: the part of the
checks that ran out, and every mint it brought IN, whose own entailments the re-run
draws (`redraw-deferred`). Run under `call-with-pass-caches`.(drop-kinds m k gone)Refusal record m, from which the entries gone have left handle k, with k no
longer named under a kind of gone that no entry still under k holds.
Refusal record `m`, from which the entries `gone` have left handle `k`, with `k` no longer named under a kind of `gone` that no entry still under `k` holds.
(drop-replaced-routes! kb just)(drop-replaced-routes! kb just route)Drop the justifications the one just added as just replaces: the same firing over
a route the witness rule no longer names. Returns the merged
jtms/drop-justification! results for the caller to apply to its stores; the dropped
records are deleted here. A justification is replaced when it has just's informant,
consequence, bindings and subsumptions (same-pairing?), holds every antecedent of
just outside route, and differs only in believed genl / genlCx edges. route
is just's route handles; nil reads them off the antecedents. An edge that is OUT
keeps its justification (docs/nmtms.md, "Where the layer stops").
Drop the justifications the one just added as `just` replaces: the same firing over a route the witness rule no longer names. Returns the merged `jtms/drop-justification!` results for the caller to apply to its stores; the dropped records are deleted here. A justification is replaced when it has `just`'s informant, consequence, bindings and subsumptions (`same-pairing?`), holds every antecedent of `just` outside `route`, and differs only in believed `genl` / `genlCx` edges. `route` is `just`'s route handles; nil reads them off the antecedents. An edge that is OUT keeps its justification (docs/nmtms.md, "Where the layer stops").
(edge-descended-justifications kb gone removed-jids)The justifications among removed-jids that a departing route edge (route-functors)
or trigger membership invalidated while the fact and the declaration survive, as
records: the derivations a teardown owes a re-derivation (rederive-descended).
gone is the sentexes the sweep removed. Read before the teardown deletes the
records. Runs only when gone holds a route edge, or a membership while a trigger
declaration is stored. An entailment qualifies when a removed antecedent is past its
fact and declaration (past-the-pair?) and neither is removed; a descended equality
or a restatement (:migration) when a removed route edge is its only removed
antecedent (a removed equality counts as one).
The justifications among `removed-jids` that a departing route edge (`route-functors`) or trigger membership invalidated while the fact and the declaration survive, as records: the derivations a teardown owes a re-derivation (`rederive-descended`). `gone` is the sentexes the sweep removed. Read before the teardown deletes the records. Runs only when `gone` holds a route edge, or a membership while a trigger declaration is stored. An entailment qualifies when a removed antecedent is past its fact and declaration (`past-the-pair?`) and neither is removed; a descended equality or a restatement (`:migration`) when a removed route edge is its only removed antecedent (a removed equality counts as one).
(entail-existing kb sentence dh)When an (arg P n T) / (genlArg P n T) / (interArg P n T m U) declaration
arrives, draw what it now says about the (P …) sentexes already stored. Same
{:new :violations} result; nil when sentence is not an argument constraint. Sweeps
what is stored, not believed, over P's whole spec subtree (subtree-sentexes,
snapshotted before the first mint); (resultArg F n) reads the natFormula facts of
F's applications (result-arg-extent) and an interArgEqual the tuples holding its
value at its trigger position (trigger-extent). A declaration whose type is not
mintable (arity/mintable-type?) or whose every type is thing reads no extent;
mints-on-lengths runs it later. An inert sentex or computed genlCx edge draws
nothing (retroactive-mints). A declaration that mints entails its types'
unary_predicate memberships (unary-entailments). triggered-mints reaches a trigger
arriving last. See docs/argtypes.md.
When an `(arg P n T)` / `(genlArg P n T)` / `(interArg P n T m U)` declaration
arrives, draw what it now says about the `(P …)` sentexes already stored. Same
`{:new :violations}` result; nil when `sentence` is not an argument constraint. Sweeps
what is stored, not believed, over `P`'s whole spec subtree (`subtree-sentexes`,
snapshotted before the first mint); `(resultArg F n)` reads the `natFormula` facts of
`F`'s applications (`result-arg-extent`) and an `interArgEqual` the tuples holding its
value at its trigger position (`trigger-extent`). A declaration whose type is not
mintable (`arity/mintable-type?`) or whose every type is `thing` reads no extent;
`mints-on-lengths` runs it later. An inert sentex or computed `genlCx` edge draws
nothing (`retroactive-mints`). A declaration that mints entails its types'
`unary_predicate` memberships (`unary-entailments`). `triggered-mints` reaches a trigger
arriving last. See docs/argtypes.md.(entail-under-context-edge kb m)When the genlCx move m (context-move) shows contexts, draw what the declarations
it makes visible say about the facts already stored in sub and every context under
it, the fourth arrival order beside the fact, the declaration and the genl edge. Each
derivation names the genlCx edges it sees its declaration through
(checks/entailment-support). Facts and declarations stated in below draw at their
new common placements (deduce-placed, declarations-meeting); the settle drops a
placement left below a more general one (surplus-placements). Off unless
*assertive-arg-types?* and *entail-moves?* hold, some predicate declares, and a
context of :moved stores a sentex older than :floor. Per group of readers
(move-groups) one side is read (move-entail-side, trigger-named-facts,
declared-facts-in). :floor (seed-floor) excludes content that arrived with the
edge; :entailed (a volatile set, one per drain) excludes facts an earlier move drew.
When the `genlCx` move `m` (`context-move`) shows contexts, draw what the declarations it makes visible say about the facts already stored in `sub` and every context under it, the fourth arrival order beside the fact, the declaration and the `genl` edge. Each derivation names the `genlCx` edges it sees its declaration through (`checks/entailment-support`). Facts and declarations stated in `below` draw at their new common placements (`deduce-placed`, `declarations-meeting`); the settle drops a placement left below a more general one (`surplus-placements`). Off unless `*assertive-arg-types?*` and `*entail-moves?*` hold, some predicate declares, and a context of `:moved` stores a sentex older than `:floor`. Per group of readers (`move-groups`) one side is read (`move-entail-side`, `trigger-named-facts`, `declared-facts-in`). `:floor` (`seed-floor`) excludes content that arrived with the edge; `:entailed` (a volatile set, one per drain) excludes facts an earlier move drew.
(entail-under-edge kb sentence)When a (genl sub super) edge arrives, draw what the declarations on super now say
about the (sub …) sentexes already stored, the third arrival order beside
deduce-arg-types and entail-existing. A covering, separating or partition
installs an edge per part (tax/installed-edges), each read as an arriving edge. nil
when sentence installs no edge. Covers the whole spec subtree of sub
(subtree-sentexes), each sentex put back through checks/constraint-entailments in
its own context. Off unless *assertive-arg-types?*, some predicate carries an
entailing declaration (any-declaring?) and a genl-ancestor of super does
(super-reaches-declaration?).
When a `(genl sub super)` edge arrives, draw what the declarations on `super` now say about the `(sub …)` sentexes already stored, the third arrival order beside `deduce-arg-types` and `entail-existing`. A `covering`, `separating` or `partition` installs an edge per part (`tax/installed-edges`), each read as an arriving edge. nil when `sentence` installs no edge. Covers the whole spec subtree of `sub` (`subtree-sentexes`), each sentex put back through `checks/constraint-entailments` in its own context. Off unless `*assertive-arg-types?*`, some predicate carries an entailing declaration (`any-declaring?`) and a genl-ancestor of `super` does (`super-reaches-declaration?`).
The special-predicate dispatch table: an ordered vector of [functor spec] pairs,
joined from the arms above and the declarations in vaelii.impl.predicates. The order
is the declaration's (predicates/entries filtered to the functors this table holds),
and post-taxonomy-supporters! replays it top to bottom. The four walks (integrate,
disintegrate, rebuild, wff) all walk this vector; table is the lookup table.
The special-predicate dispatch table: an ordered vector of `[functor spec]` pairs, joined from the arms above and the declarations in `vaelii.impl.predicates`. The order is the declaration's (`predicates/entries` filtered to the functors this table holds), and `post-taxonomy-supporters!` replays it top to bottom. The four walks (integrate, disintegrate, rebuild, wff) all walk this vector; `table` is the lookup table.
(equate-existing kb sentence)When a (functional P) or (functionalInArg P n) declaration arrives, derive the
equalities the stored facts of P's spec subtree license, each handed to
derive-functional-equalities (docs/equality.md, "Four directions"). nil when
sentence declares neither.
When a `(functional P)` or `(functionalInArg P n)` declaration arrives, derive the equalities the stored facts of `P`'s spec subtree license, each handed to `derive-functional-equalities` (docs/equality.md, "Four directions"). nil when `sentence` declares neither.
(equate-under-context-edge kb m)When a (genlCx sub super) edge arrives, derive the equalities a (functional …)
mark licenses over facts the readers under sub newly see together: the context twin
of equate-under-edge. Hands each stored fact of :seen that
functional-mark-relevant? admits to derive-functional-equalities at its own context.
Free for a KB that declares nothing functional. Budgeted
(budgeted-context-edge-candidates) and idempotent. The equality rests on the genlCx
edges its reader sees each fact and the declaration through (pair-antecedents).
When a `(genlCx sub super)` edge arrives, derive the equalities a `(functional …)` mark licenses over facts the readers under `sub` newly see together: the context twin of `equate-under-edge`. Hands each stored fact of `:seen` that `functional-mark-relevant?` admits to `derive-functional-equalities` at its own context. Free for a KB that declares nothing functional. Budgeted (`budgeted-context-edge-candidates`) and idempotent. The equality rests on the `genlCx` edges its reader sees each fact and the declaration through (`pair-antecedents`).
(equate-under-edge kb sentence)When a (genl sub super) edge arrives, derive the equalities a functional or
functionalInArg mark at or above super now licenses over the stored facts of sub's
spec subtree (equate-under-edge-via). nil when sentence is not a genl edge, and
no subtree read when no mark of the family stands over super.
When a `(genl sub super)` edge arrives, derive the equalities a `functional` or `functionalInArg` mark at or above `super` now licenses over the stored facts of `sub`'s spec subtree (`equate-under-edge-via`). nil when `sentence` is not a `genl` edge, and no subtree read when no mark of the family stands over `super`.
(except-move-region kb pending)The superseded data whose supersession an except that moved can change: the ones
naming a term an equality in the excepted handles' reach re-spells
(except-move-terms), stored in a context that sees one of the contexts the moving
excepts are stated in. pending is {target #{except-context}}.
The superseded data whose supersession an `except` that moved can change: the ones
naming a term an equality in the excepted handles' reach re-spells
(`except-move-terms`), stored in a context that sees one of the contexts the moving
`except`s are stated in. `pending` is `{target #{except-context}}`.(except-move-sweeps kb handles sweep? whole scoped)Run, for each handle in handles whose visibility an except moved, the sweep its
arrival runs over the facts already stored: the equality migration for an equality
sentex (equality-arrival-sweep) and revived-declaration-sweeps' for a merge or lift
mark (docs/equational.md, "An except of an equation"). Returns one {:new :superseded :violations :removed}, or nil when handles is empty. With sweep?, the
argument-type derivations resting on a record an except now hides are dropped
(drop-hidden-mints!, :removed for the caller to apply) and the records it stopped
hiding draw again (docs/argtypes.md, "An except of an ingredient"): for a handle in
whole, every context and the record's own arrival sweep (revealed-entailments); for
one only in scoped, {handle #{[sub super]}}, the contexts under each sub
(entail-under-context-edge).
Run, for each handle in `handles` whose visibility an `except` moved, the sweep its
arrival runs over the facts already stored: the equality migration for an equality
sentex (`equality-arrival-sweep`) and `revived-declaration-sweeps`' for a merge or lift
mark (docs/equational.md, "An except of an equation"). Returns one `{:new :superseded
:violations :removed}`, or nil when `handles` is empty. With `sweep?`, the
argument-type derivations resting on a record an `except` now hides are dropped
(`drop-hidden-mints!`, `:removed` for the caller to apply) and the records it stopped
hiding draw again (docs/argtypes.md, "An except of an ingredient"): for a handle in
`whole`, every context and the record's own arrival sweep (`revealed-entailments`); for
one only in `scoped`, `{handle #{[sub super]}}`, the contexts under each `sub`
(`entail-under-context-edge`).(except-moved kb)The handles an except of which arrived, left or flipped since the last
drain-except-moves!, read without emptying the queue (note-except-move!).
The handles an `except` of which arrived, left or flipped since the last `drain-except-moves!`, read without emptying the queue (`note-except-move!`).
(exception-recheck-predicates tx meta)The re-check keys of the exceptWhen meta-sentence meta, read against the taxonomy
tx: the predicates its query mentions, the types a separation's denial and the
predicates a negates denial move a negated conjunct of it on
(rules/separation-denial-predicates, rules/negates-denial-predicates), and the
predicates of its closed-extent negatives (rules/closed-extent-query-predicates).
The re-check keys of the exceptWhen meta-sentence `meta`, read against the taxonomy `tx`: the predicates its query mentions, the types a separation's denial and the predicates a `negates` denial move a negated conjunct of it on (`rules/separation-denial-predicates`, `rules/negates-denial-predicates`), and the predicates of its closed-extent negatives (`rules/closed-extent-query-predicates`).
(firing-informant? kb informant)Is informant a rule a forward or backward run fired: a rule handle that is not one of
kv/mint-rules, which no engine runs.
Is `informant` a rule a forward or backward run fired: a rule handle that is not one of `kv/mint-rules`, which no engine runs.
(firing-seeds kb js edge? gone?)The antecedents of the rule firings (firing-informant?) among the justification
records js that name a handle edge? holds as an antecedent, less the handles gone?
holds, as chaining seeds. The re-chain a departing edge owes a firing that named it as
its witness: sighting-seeds here, and vaelii.impl.record-edit/sweep! for the firings
a record edit left to its settle.
The antecedents of the rule firings (`firing-informant?`) among the justification records `js` that name a handle `edge?` holds as an antecedent, less the handles `gone?` holds, as chaining seeds. The re-chain a departing edge owes a firing that named it as its witness: `sighting-seeds` here, and `vaelii.impl.record-edit/sweep!` for the firings a record edit left to its settle.
(forget-kinds m k)Refusal record m with handle k named under no kind: its entries left together.
Refusal record `m` with handle `k` named under no kind: its entries left together.
(inadmissible kb sentence context)(inadmissible kb sentence context constraint-arm)The violation that stops sentence from being stored in context, or nil: naming,
the definitional constraints, well-formedness and edge stratification. Returns a
value and never throws, since its callers run after their triggering sentex is stored
(argument-type entailment, the computed genlCx edge of context-nat) or must refuse a
hypothesis without failing the query (abduction).
constraint-arm is checks/constraint-violation by default; a nil arm omits the
definitional-constraint check for a caller that already ran it. See docs/argtypes.md.
The violation that stops `sentence` from being stored in `context`, or nil: naming, the definitional constraints, well-formedness and edge stratification. Returns a value and never throws, since its callers run after their triggering sentex is stored (argument-type entailment, the computed `genlCx` edge of `context-nat`) or must refuse a hypothesis without failing the query (abduction). `constraint-arm` is `checks/constraint-violation` by default; a nil arm omits the definitional-constraint check for a caller that already ran it. See docs/argtypes.md.
(index-exceptWhen-meta kb meta-sentex)Register the exceptWhen meta-sentex meta-sentex in the re-check index: post the
rule it names under its keys (exception-recheck-predicates) and into the :rules
set, queue the rule for a blanket re-check (a fact may already have arrived that its
new exception blocks), lower the rule's firings to :default
(restrength-firings!), and hold void the firings of a forced-monotonic rule it convicts
(checks/force-sentexes!).
Register the exceptWhen meta-sentex `meta-sentex` in the re-check index: post the rule it names under its keys (`exception-recheck-predicates`) and into the `:rules` set, queue the rule for a blanket re-check (a fact may already have arrived that its new exception blocks), lower the rule's firings to `:default` (`restrength-firings!`), and hold void the firings of a forced-monotonic rule it convicts (`checks/force-sentexes!`).
(index-rule-sentex kb handle rule-sentex)Index a rule handle by all of its predicates (antecedent and consequent), so
reads/as-stored-rules-by-consequent-in answers "what could conclude P?" for a
forward-only rule too, and in the re-check index under the keys rule-recheck-keys
names. A variable consequent functor is filed under p/var-consequent-key
(rules/consequent-index-pred); resolution/concluding-rule-handles unions that
bucket. The record holds :engines and :defeasible; no rule index keys on them.
This is the add half of the structural arm of integrate-sentex.
Index a rule handle by all of its predicates (antecedent and consequent), so `reads/as-stored-rules-by-consequent-in` answers "what could conclude P?" for a forward-only rule too, and in the re-check index under the keys `rule-recheck-keys` names. A variable consequent functor is filed under `p/var-consequent-key` (`rules/consequent-index-pred`); `resolution/concluding-rule-handles` unions that bucket. The record holds `:engines` and `:defeasible`; no rule index keys on them. This is the add half of the structural arm of `integrate-sentex`.
(integrate-equality-sentex kb sentex handle)The three equality relations' add arm on every entry point, asserted or derived.
Returns the migration result {:new :superseded :violations}, which the derivation
path seeds chaining with and files (docs/equality.md, "A rule concluding one of the
three relations merges"). A schematic (equals L R) goes to
integrate-rewrite-rule, and a (rewriteOf T E) with a compound E is a NAT
reify-to-term declaration the partition holds no part of (equality-entry).
The three equality relations' add arm on every entry point, asserted or derived.
Returns the migration result `{:new :superseded :violations}`, which the derivation
path seeds chaining with and files (docs/equality.md, "A rule concluding one of the
three relations merges"). A schematic `(equals L R)` goes to
`integrate-rewrite-rule`, and a `(rewriteOf T E)` with a compound `E` is a NAT
reify-to-term declaration the partition holds no part of (`equality-entry`).(integrate-sentex kb sentex handle)Reflect a newly stored sentex into the taxonomy, rule index and disjointness: the
:integrate column of the table, walked, plus the structural arms. Returns
{:new [handles] :superseded [[datum reason]] :violations [v]} for an equality sentex,
whose twins are chaining seeds, and nil for everything else.
Reflect a newly stored sentex into the taxonomy, rule index and disjointness: the
`:integrate` column of the table, walked, plus the structural arms. Returns
`{:new [handles] :superseded [[datum reason]] :violations [v]}` for an equality sentex,
whose twins are chaining seeds, and nil for everything else.(integrate-transitive kb sentex handle)The table half of derived-sentex-added: for a functor the table keys, only the arms
flagged :derived? run for a rule-derived conclusion. A derived equality is reached
through integrate-equality-sentex by name, since this fn discards what an arm returns.
A functor the table does not key is the structural walk's. See docs/taxonomy.md.
The table half of `derived-sentex-added`: for a functor the table keys, only the arms flagged `:derived?` run for a rule-derived conclusion. A derived equality is reached through `integrate-equality-sentex` by name, since this fn discards what an arm returns. A functor the table does not key is the structural walk's. See docs/taxonomy.md.
(integrate-twin kb sentex handle)Full integration for a migrated twin (migrate-sentex): the same arms
integrate-sentex runs, so a twin reaches the same caches an asserted declaration
does. derived-sentex-added narrows the table half to the :derived? entries. The
equality arm is skipped (kb/rewritable-sentex? holds equalities back from migration),
then the re-check post every derived sentex gets. Migration can run inside a
forward-chaining pass; none of the arms re-enter assert or chain.
Full integration for a migrated twin (`migrate-sentex`): the same arms `integrate-sentex` runs, so a twin reaches the same caches an asserted declaration does. `derived-sentex-added` narrows the table half to the `:derived?` entries. The equality arm is skipped (`kb/rewritable-sentex?` holds equalities back from migration), then the re-check post every derived sentex gets. Migration can run inside a forward-chaining pass; none of the arms re-enter `assert` or `chain`.
(kind-entries m kind)Every entry of kind in refusal record m, as [handle entry] pairs, read off the
sets of the handles the kind index names under kind.
Every entry of `kind` in refusal record `m`, as `[handle entry]` pairs, read off the sets of the handles the kind index names under `kind`.
(lift-refusals kb)The lifts waiting on an argument conviction, as [source-handle entry] pairs in
handle order.
The lifts waiting on an argument conviction, as `[source-handle entry]` pairs in handle order.
(lifts-to-universe? kb pred)Does deduce-lifts deduce a sentence on pred into CxUniverse: is pred a permuting
mark (inherit/permuting-marks), or a predicate the KB declares decontextualized? The
declaration is read unscoped: a decontextualized predicate's facts belong to the KB, not
to the context that declares it.
Does `deduce-lifts` deduce a sentence on `pred` into CxUniverse: is `pred` a permuting mark (`inherit/permuting-marks`), or a predicate the KB declares decontextualized? The declaration is read unscoped: a decontextualized predicate's facts belong to the KB, not to the context that declares it.
(lost-descended-derivations kb handles edges-only?)The edge-descended derivations among the dependents of handles whose conclusion is
OUT, as justification records: edge-descended-justifications for an ingredient that
lost belief rather than its record. edges-only? keeps a dependent only where its
handle is a route edge (route-functors), an entailment antecedent past the pair
(past-the-pair?), or an equality a restatement rests on. Only a justification whose
conclusion is OUT, or withdrawn at its own context (exc/believed-own?), qualifies.
The network filter runs before the record fetch.
The edge-descended derivations among the dependents of `handles` whose conclusion is OUT, as justification records: `edge-descended-justifications` for an ingredient that lost belief rather than its record. `edges-only?` keeps a dependent only where its handle is a route edge (`route-functors`), an entailment antecedent past the pair (`past-the-pair?`), or an equality a restatement rests on. Only a justification whose conclusion is OUT, or withdrawn at its own context (`exc/believed-own?`), qualifies. The network filter runs before the record fetch.
(materialize-defn-rules kb sentence defn-handle context)Materialize the forward rules a defn* fact stored at defn-handle in context
expands into (sx/defn-companion-rules), each a derived rule sentex justified by the
defn* fact alone: {:new [handles] :violations [v]}. Called from assert-one. A
non-defn* sentence returns the empty result after one defn-sentence? read.
Materialize the forward rules a `defn*` fact stored at `defn-handle` in `context`
expands into (`sx/defn-companion-rules`), each a derived rule sentex justified by the
`defn*` fact alone: `{:new [handles] :violations [v]}`. Called from `assert-one`. A
non-`defn*` sentence returns the empty result after one `defn-sentence?` read.(migrate-handle-metas kb orig twin eqs reader)(migrate-handle-metas kb orig twin informant witnesses reader)Carry every believed handle-naming meta of sentex orig onto its migrated twin twin
(docs/equality.md, "Handle-naming metas travel with their target"): each meta gets a
twin naming twin, its terms rewritten to reader's representatives, registered through
integrate-twin and justified by the meta and each of witnesses under informant
(justify-twin!). The 5-arity takes eqs, the migrating equalities, under rewriteOf.
Public for integrate/commute-existing.
Carry every believed handle-naming meta of sentex `orig` onto its migrated twin `twin` (docs/equality.md, "Handle-naming metas travel with their target"): each meta gets a twin naming `twin`, its terms rewritten to `reader`'s representatives, registered through `integrate-twin` and justified by the meta and each of `witnesses` under `informant` (`justify-twin!`). The 5-arity takes `eqs`, the migrating equalities, under `rewriteOf`. Public for `integrate/commute-existing`.
(migrate-meta-onto-twins kb sentex)The handle-naming meta sentex was just stored: when its target already has twins, the
merge ran before the meta existed, so replay migrate-handle-metas onto each twin.
Idempotent for the metas already carried. nil, and a no-op when sentex names nothing
or its target has no twin.
The handle-naming meta `sentex` was just stored: when its target already has twins, the merge ran before the meta existed, so replay `migrate-handle-metas` onto each twin. Idempotent for the metas already carried. nil, and a no-op when `sentex` names nothing or its target has no twin.
(migrate-sentex kb sentex)Restate one stored sentex under its terms' representatives, once per reader whose
election differs (reader-contexts-at; docs/equality.md, "What a merge does").
{:new [handles] :superseded [[datum reason]] :violations [v]}.
Each twin is re-canonicalized through find-or-create rather than substituted, justified
by the original and the equalities of one path per displaced term (migrate-into),
placed in the reader that elected it, and checked as a derivation
(checks/derivation-violation). Only the fact's own context supersedes. An
inadmissible twin is dropped into :violations, and its original stays believed.
Restate one stored sentex under its terms' representatives, once per reader whose
election differs (`reader-contexts-at`; docs/equality.md, "What a merge does").
`{:new [handles] :superseded [[datum reason]] :violations [v]}`.
Each twin is re-canonicalized through find-or-create rather than substituted, justified
by the original and the equalities of one path per displaced term (`migrate-into`),
placed in the reader that elected it, and checked as a derivation
(`checks/derivation-violation`). Only the fact's own context supersedes. An
inadmissible twin is dropped into `:violations`, and its original stays believed.(migrate-under-context-edge kb m)When the genlCx move m (context-move) shows contexts, restate the sentexes the
widened ancestor set newly exposes to a merge: the edge-arriving-last order
(docs/equality.md, "A late genlCx edge is a third arrival order"). Both halves
run: a merge in the shown contexts meets the facts the readers already saw, and a fact
there meets the merges they already saw. Each half is enumerated from the merges
through the term index.
When the `genlCx` move `m` (`context-move`) shows contexts, restate the sentexes the widened ancestor set newly exposes to a merge: the edge-arriving-last order (docs/equality.md, "A late `genlCx` edge is a third arrival order"). Both halves run: a merge in the shown contexts meets the facts the readers already saw, and a fact there meets the merges they already saw. Each half is enumerated from the merges through the term index.
(mint-rule-retraction-problem kb handle where)The :mint-rule refusal of retracting the sentex at handle, as a value, or nil: the
handle stores a rule of kv/mint-rules, which the mints of its kind rest on and the engine
stores again at the next mint (mint-rule-handle!). where names the entry point.
The `:mint-rule` refusal of retracting the sentex at `handle`, as a value, or nil: the handle stores a rule of `kv/mint-rules`, which the mints of its kind rest on and the engine stores again at the next mint (`mint-rule-handle!`). `where` names the entry point.
(minted-seeds kb handles)handles — sentexes an entailment minted — as chaining seeds, followed by the
subsumption-seeds of each one that is a genl edge. A genlArg mint is an edge
like an asserted one, and the facts under it become matchable at the new supertype
whichever of the two stored it: seeding the handle alone fires the rules keyed on
genl, not the rules the edge connected, so (wolf Rex) and a rule on (animal ?x)
stored before a minted (genl wolf animal) would derive nothing in that order only.
`handles` — sentexes an entailment minted — as chaining seeds, followed by the `subsumption-seeds` of each one that is a `genl` edge. A `genlArg` mint is an edge like an asserted one, and the facts under it become matchable at the new supertype whichever of the two stored it: seeding the handle alone fires the rules keyed on `genl`, not the rules the edge connected, so `(wolf Rex)` and a rule on `(animal ?x)` stored before a minted `(genl wolf animal)` would derive nothing in that order only.
(mints-on-lengths kb bound)The mints the stored content naming a type of bound owes now that the type's own
length admits one (arity/mintable-type?), as one {:new :violations}. bound maps
each relation whose arity bindings moved to those bindings' #{[kind value]}
(arity/drain!'s :bound). Per mintable type t, in content order: each stored
entailing declaration naming t with no declaredType justification of
(unary_predicate t) (declared-type-justifications) runs entail-existing; each stored
fact naming t where an argArg names its type, and each natFormula fact naming t
under a resultArg function, draws through deduce-placed. The argArg predicates are
read KB-wide. An inert declaration sweeps nothing.
The mints the stored content naming a type of `bound` owes now that the type's own
length admits one (`arity/mintable-type?`), as one `{:new :violations}`. `bound` maps
each relation whose arity bindings moved to those bindings' `#{[kind value]}`
(`arity/drain!`'s `:bound`). Per mintable type `t`, in content order: each stored
entailing declaration naming `t` with no `declaredType` justification of
`(unary_predicate t)` (`declared-type-justifications`) runs `entail-existing`; each stored
fact naming `t` where an `argArg` names its type, and each `natFormula` fact naming `t`
under a `resultArg` function, draws through `deduce-placed`. The `argArg` predicates are
read KB-wide. An inert declaration sweeps nothing.(move-seeds kb m filtered?)The stored facts the genlCx move m (context-move) newly makes matchable, as
chaining seeds: the context twin of subsumption-seeds. up is super's ancestor
set (:up), seen what the contexts below sub that gain a context see beside it
(:gained-below; :below in the unfiltered arity), fresh the contexts some reader
below sub sees through the edge alone (:moved). The unfiltered arity seeds every
such fact of up and seen. With m's :floor (seed-floor), content stored at or
above the floor arrived after the edge and is excluded. See docs/contexts.md, "A
genlCx edge owes the same debt".
The stored facts the `genlCx` move `m` (`context-move`) newly makes matchable, as chaining seeds: the context twin of `subsumption-seeds`. `up` is `super`'s ancestor set (`:up`), `seen` what the contexts below `sub` that gain a context see beside it (`:gained-below`; `:below` in the unfiltered arity), `fresh` the contexts some reader below `sub` sees through the edge alone (`:moved`). The unfiltered arity seeds every such fact of `up` and `seen`. With `m`'s `:floor` (`seed-floor`), content stored at or above the floor arrived after the edge and is excluded. See docs/contexts.md, "A `genlCx` edge owes the same debt".
(names-any? terms b)Does the binding map b of a firing or a refusal bind a variable to one of terms,
at any depth?
Does the binding map `b` of a firing or a refusal bind a variable to one of `terms`, at any depth?
(naming-violation kb sentence context)The :naming violation sentence in context carries under kb's naming policy, or
nil: nm/blocking-problems as the value a caller that may not throw drops a sentence
for. Nil under :warn and :off.
The `:naming` violation `sentence` in `context` carries under `kb`'s naming policy, or nil: `nm/blocking-problems` as the value a caller that may not throw drops a sentence for. Nil under `:warn` and `:off`.
(note-departure! kb sentex)Queue sentex, leaving the store, when it is a genlCx edge, whose [sub super] the
context-move drain reads (drain-context-moves!), or a record that can have subsumed a
mint (subsumer-shaped?) with pruning on, for withheld-releases. Called from
integrate/sentex-removed!, the one place a record leaves.
Queue `sentex`, leaving the store, when it is a `genlCx` edge, whose `[sub super]` the context-move drain reads (`drain-context-moves!`), or a record that can have subsumed a mint (`subsumer-shaped?`) with pruning on, for `withheld-releases`. Called from `integrate/sentex-removed!`, the one place a record leaves.
(note-except-move! kb h context edge)Queue handle h on :except-moves: an except of it stated in context arrived,
left or flipped, so what h restates or merges is visible to a different set of
readers there and below. edge, a (genlCx sub super) edge's [sub super], says the
move is that edge's and reaches the contexts under sub alone (:scoped); nil says the
except itself moved (:whole). The settle drains the queue (drain-except-moves!,
take-except-moves!).
Queue handle `h` on `:except-moves`: an `except` of it stated in `context` arrived, left or flipped, so what `h` restates or merges is visible to a different set of readers there and below. `edge`, a `(genlCx sub super)` edge's `[sub super]`, says the move is that edge's and reaches the contexts under `sub` alone (`:scoped`); nil says the `except` itself moved (`:whole`). The settle drains the queue (`drain-except-moves!`, `take-except-moves!`).
(note-kind m k e)Refusal record m with handle k named under entry e's kind.
Refusal record `m` with handle `k` named under entry `e`'s kind.
(note-producer-moves! k xs)Add xs under k of *producer-moves*, when it is bound.
Add `xs` under `k` of `*producer-moves*`, when it is bound.
(note-unpremised! kb h)Queue the record at h, whose premise mark a retraction removed while a derivation
still holds it up, for the settle's withdrawal question: a record an author stated
beside a mint of the same sentence is not the entailment's to withdraw, and once the
statement goes it is (mint-only?), so a believed record that says it more
specifically withdraws it as it withdraws a mint it meets on arrival.
Queue the record at `h`, whose premise mark a retraction removed while a derivation still holds it up, for the settle's withdrawal question: a record an author stated beside a mint of the same sentence is not the entailment's to withdraw, and once the statement goes it is (`mint-only?`), so a believed record that says it more specifically withdraws it as it withdraws a mint it meets on arrival.
(offer-marked-existing kb sentence)When a functional, functionalInArg, asymmetric, anti_transitive or negates
mark arrives, offer every stored fact of the spec subtree of each predicate it names
(the first argument, both of a negates) to decide/offer!, which reads the nogoods
each forms under the mark. nil.
When a `functional`, `functionalInArg`, `asymmetric`, `anti_transitive` or `negates` mark arrives, offer every stored fact of the spec subtree of each predicate it names (the first argument, both of a `negates`) to `decide/offer!`, which reads the nogoods each forms under the mark. nil.
(offer-marked-under-edge kb sentence)When a (genl sub super) edge arrives under an offered-marks mark on super or
above it, offer the stored facts of sub's spec subtree to decide/offer!. nil, and
free for a KB declaring none of the marks.
When a `(genl sub super)` edge arrives under an `offered-marks` mark on `super` or above it, offer the stored facts of `sub`'s spec subtree to `decide/offer!`. nil, and free for a KB declaring none of the marks.
(owed-releases kb)How many departures and arrivals withheld-releases left owed (*release-withheld?*).
How many departures and arrivals `withheld-releases` left owed (`*release-withheld?*`).
(pair-placements kb fsx dsx)The contexts a mint drawn over the fact fsx through the declaration dsx (sentexes)
is placed in, in content order: each maximal context that sees every ingredient of the
derivation where no except hides one (docs/argtypes.md, "Where a mint is placed").
Empty when no context sees them all. Ingredients beyond the fact and declaration are a
genl route's supporters (tax/general-reach-supports) and a trigger's
(trigger-alternatives); placements are taken per combination and the most general
kept. Past an except, res/exception-aware-placements places each combination.
The contexts a mint drawn over the fact `fsx` through the declaration `dsx` (sentexes) is placed in, in content order: each maximal context that sees every ingredient of the derivation where no `except` hides one (docs/argtypes.md, "Where a mint is placed"). Empty when no context sees them all. Ingredients beyond the fact and declaration are a `genl` route's supporters (`tax/general-reach-supports`) and a trigger's (`trigger-alternatives`); placements are taken per combination and the most general kept. Past an `except`, `res/exception-aware-placements` places each combination.
(pending-supersession-moves kb)The datums whose supersession entry changed since the last take-supersession-moves!,
read without emptying them.
The datums whose supersession entry changed since the last `take-supersession-moves!`, read without emptying them.
(post-mint! index sentence context h)File record h, holding sentence in context and concluded by a stored justification
kb/mint-informant? accepts, in index's mint family, when the sentence has a
mint-term. Posted from the sentence in hand: entail-arg-type as it stores the
justification, and reindex from the record it is indexing.
File record `h`, holding `sentence` in `context` and concluded by a stored justification `kb/mint-informant?` accepts, in `index`'s mint family, when the sentence has a `mint-term`. Posted from the sentence in hand: `entail-arg-type` as it stores the justification, and `reindex` from the record it is indexing.
(post-taxonomy-supporters! kb)Post the taxonomy's supporter families (tax/post!) for every stored declaration in
kb: the :rebuild column replayed in entry order over a scratch taxonomy whose index
store is kb's, then each stored disjoint metatype's members, then the re-check keys of
every stored rule and exceptWhen (post-recheck-keys!). kb's own taxonomy is
untouched and the equality relations post nothing. A malformed genl / genlCx row is
dropped (replay-edge) and the count warned once.
Post the taxonomy's supporter families (`tax/post!`) for every stored declaration in `kb`: the `:rebuild` column replayed in entry order over a scratch taxonomy whose index store is `kb`'s, then each stored disjoint metatype's members, then the re-check keys of every stored rule and `exceptWhen` (`post-recheck-keys!`). `kb`'s own taxonomy is untouched and the equality relations post nothing. A malformed `genl` / `genlCx` row is dropped (`replay-edge`) and the count warned once.
(producer-moves)A fresh value for a write entry point to bind *producer-moves* to.
A fresh value for a write entry point to bind `*producer-moves*` to.
(reader-contexts-at kb pctx sentence)The contexts whose election could restate sentence, stated in pctx, differently:
pctx, and every context where it meets an equality that bears on sentence or an
except of one. Migration passes a stored sentex's own; a guard passes its placement
and its substituted condition (chain/guard-solutions).
The reader is not the fact's own context. A merge holds where it is visible, and
who reads the fact is any context below it — each electing a representative over a
different set of visible edges (tax/scoped-class). A single normal form computed
at the fact's context serves only that one reader; one computed globally serves none
reliably, since it can be elected by an edge no reader of the fact inherits. So the
parties are tax/meet-closure of the fact's context with the equalities' — the same
enumeration a qualitative network takes (docs/qcn.md) and for the same reason. The
contexts holding an except of one of those equalities are parties too: a reader
below the fact that reads the except sees less than the fact's context, and
migrate-into stores the fact's spelling there when the fact's context supersedes it.
Filtered to contexts that see the fact: a context the fact is invisible from has nothing of it to restate. Ordered most-general first, by the size of the context's own up-closure and then by name — a content-keyed order, so which twin a duplicate form collapses into cannot depend on arrival. The fact's own context leads explicitly rather than by that key: it is the only reader that supersedes, and two mutually-visible contexts have up-closures of a size that would otherwise let a name decide which of them is the fact's.
No equality bearing on the sentence means no reader, and that is the presence check:
nothing can restate it, so migration reads no closure and runs no rewrite. One equality
context closes almost as fast — meet-closure of a comparable pair is the pair, and
the filter leaves the fact's own context alone.
The contexts whose election could restate `sentence`, stated in `pctx`, differently: `pctx`, and every context where it meets an equality that bears on `sentence` or an `except` of one. Migration passes a stored sentex's own; a guard passes its placement and its substituted condition (`chain/guard-solutions`). **The reader is not the fact's own context.** A merge holds where it is visible, and who reads the fact is any context below it — each electing a representative over a different set of visible edges (`tax/scoped-class`). A single normal form computed at the fact's context serves only that one reader; one computed globally serves none reliably, since it can be elected by an edge no reader of the fact inherits. So the parties are `tax/meet-closure` of the fact's context with the equalities' — the same enumeration a qualitative network takes (docs/qcn.md) and for the same reason. The contexts holding an `except` of one of those equalities are parties too: a reader below the fact that reads the except sees less than the fact's context, and `migrate-into` stores the fact's spelling there when the fact's context supersedes it. Filtered to contexts that **see** the fact: a context the fact is invisible from has nothing of it to restate. Ordered most-general first, by the size of the context's own up-closure and then by name — a content-keyed order, so which twin a duplicate form collapses into cannot depend on arrival. The fact's own context leads explicitly rather than by that key: it is the only reader that supersedes, and two mutually-visible contexts have up-closures of a size that would otherwise let a name decide which of them is the fact's. **No equality bearing on the sentence means no reader**, and that is the presence check: nothing can restate it, so migration reads no closure and runs no rewrite. One equality context closes almost as fast — `meet-closure` of a comparable pair is the pair, and the filter leaves the fact's own context alone.
(rebuild-pending! kb)Rebuild the engine's own waiting lifts after recover: every decontextualized lift an
argument conviction refuses (a permuting mark's included), re-noted as its arrival
noted it, by lift-existing's sweep. chain/rerecord-refusals! rebuilds only the
rules' half of the refusal record. The marks are read unscoped.
Rebuild the engine's own waiting lifts after `recover`: every decontextualized lift an argument conviction refuses (a permuting mark's included), re-noted as its arrival noted it, by `lift-existing`'s sweep. `chain/rerecord-refusals!` rebuilds only the rules' half of the refusal record. The marks are read unscoped.
(rebuild-taxonomy kb)Rebuild the in-memory taxonomy over a cleared one: the believed side of every key the
index's supporter families hold (tax/refresh-beliefs with no region), and the equality
partition and rewrite rules replayed from their stored declarations by the :rebuild
column. Drops every cache first.
Rebuild the in-memory taxonomy over a cleared one: the believed side of every key the index's supporter families hold (`tax/refresh-beliefs` with no region), and the equality partition and rewrite rules replayed from their stored declarations by the `:rebuild` column. Drops every cache first.
(recheck-defeat-target kb sx)Post the re-check a (defeat (sentexHandle H)) sentex sx owes H's watchers when it is
stored, removed or relabelled: the defeat moves H's belief at the contexts that see it
with no relabel of H, so H's sentence posts what its own arrival posts
(recheck-on-sentence), and a permuting mark resting on H re-spells its facts
(note-mark-reach!). A no-op for any other sentex, and for an H no longer stored.
Post the re-check a `(defeat (sentexHandle H))` sentex `sx` owes H's watchers when it is stored, removed or relabelled: the defeat moves H's belief at the contexts that see it with no relabel of H, so H's sentence posts what its own arrival posts (`recheck-on-sentence`), and a permuting mark resting on H re-spells its facts (`note-mark-reach!`). A no-op for any other sentex, and for an H no longer stored.
(recheck-every-exception kb)Queue :all every rule carrying a re-check condition. recover takes it.
Queue `:all` every rule carrying a re-check condition. `recover` takes it.
(recheck-except kb except-sentex)(recheck-except kb except-sentex edge)An (except (sentexHandle H)) fact arrived or left, or the genlCx edge edge, a
[sub super], moved which contexts see it: queue what the visibility change touches.
jtms/consequence-closure) are queued
under {::except-closure c}.:except-moves records H with edge, and the drain re-joins from the closure
(note-except-move!, drain-except-moves!).:all; an except H re-checks its own target down the cascade.
Re-runs H's arrival sweep for the restatements the move reaches. See docs/exceptions.md,
"Five channels".An `(except (sentexHandle H))` fact arrived or left, or the `genlCx` edge `edge`, a
`[sub super]`, moved which contexts see it: queue what the visibility change touches.
* The firings resting on H through any chain (`jtms/consequence-closure`) are queued
under `{::except-closure c}`.
* `:except-moves` records H with `edge`, and the drain re-joins from the closure
(`note-except-move!`, `drain-except-moves!`).
* A rule H is queued `:all`; an except H re-checks its own target down the cascade.
Re-runs H's arrival sweep for the restatements the move reaches. See docs/exceptions.md,
"Five channels".(recheck-except-ancestors kb {:keys [edge raw]})Re-check each except the genlCx move m (context-move) moves (recheck-except,
over its target's consequence closure): one stated in a context of the move's raw stratum
(:raw), where the excepts in force at a reader under the edge's sub are read, and
the except each of those names, whose cascade moves with it. An edge whose sub
already sees every context stating an except re-checks none (lein perf's
genlcx-edge-beside-excepted-declarations, genlcx-edge-beside-seen-excepts).
Re-check each `except` the `genlCx` move `m` (`context-move`) moves (`recheck-except`, over its target's consequence closure): one stated in a context of the move's raw stratum (`:raw`), where the excepts in force at a reader under the edge's `sub` are read, and the `except` each of those names, whose cascade moves with it. An edge whose `sub` already sees every context stating an `except` re-checks none (`lein perf`'s `genlcx-edge-beside-excepted-declarations`, `genlcx-edge-beside-seen-excepts`).
(recheck-on-lengths kb moved)The settle pass moved the length of the relations moved (arity/drain!'s :moved,
a set or :all): queue :all-rejoin every rule carrying an antecedent a relation's
length can move (provers/relation-moved-answers). Reads nothing while moved is
empty.
The settle pass moved the length of the relations `moved` (`arity/drain!`'s `:moved`, a set or `:all`): queue `:all-rejoin` every rule carrying an antecedent a relation's length can move (`provers/relation-moved-answers`). Reads nothing while `moved` is empty.
(recheck-on-sentence kb sentence)The re-check trigger for a whole sentence: post it under its functor and, for a
negation, under the functor of its underlying-body, both with the whole sentence as
the narrowing trigger; then post the declaration, qualitative, computed, separation,
preservation and closed-extent grant triggers on the body, and for a unary body the
typed-admission trigger. underlying-body rather than positive-body, because a
(not (penguin X)) arriving defeats a believed (penguin X) and moves a condition that
reads belief with no fact stored or removed.
The re-check trigger for a whole sentence: post it under its functor and, for a negation, under the functor of its `underlying-body`, both with the whole sentence as the narrowing trigger; then post the declaration, qualitative, computed, separation, preservation and closed-extent grant triggers on the body, and for a unary body the typed-admission trigger. `underlying-body` rather than `positive-body`, because a `(not (penguin X))` arriving defeats a believed `(penguin X)` and moves a condition that reads belief with no fact stored or removed.
declaration-subjects' functors as a set — which declarations post to the exception
re-check queue through the shared path rather than from arms of their own.
Public because predicates/check-facets holds every declaration that answers goals
about a predicate to posting by one route or the other, and the two routes live in
different namespaces: a :retriggers facet says the arms do it, this says
recheck-declaration does. A declaration in neither decides by arrival order, which
is what that rule refuses at load.
`declaration-subjects`' functors as a set — which declarations post to the exception re-check queue through the shared path rather than from arms of their own. Public because `predicates/check-facets` holds every declaration that answers goals about a predicate to posting by one route or the other, and the two routes live in different namespaces: a `:retriggers` facet says the arms do it, this says `recheck-declaration` does. A declaration in neither decides by arrival order, which is what that rule refuses at load.
(reconcile-belief-change kb)(reconcile-belief-change kb moved)Reconcile every belief-derived taxonomy cache after moved may have changed truth.
Stores nothing; re-running it recomputes from current belief. moved may name
declaration handles or except handles (expanded to their targets by
belief-change-region). The scoped read filters through res/supporter-believed? and
is keyed on the change clock, which every write moves.
Reconcile every belief-derived taxonomy cache after `moved` may have changed truth. Stores nothing; re-running it recomputes from current belief. `moved` may name declaration handles or except handles (expanded to their targets by `belief-change-region`). The scoped read filters through `res/supporter-believed?` and is keyed on the change clock, which every write moves.
(reconcile-removed-supersession! kb sentex)The supersession reconcile sentex leaving the store owes, from the removal choke
point: the full pass for a genlCx edge or a schematic rewrite rule while any spelling
is superseded, and the narrowed one over sentex and the classes it moved for a
superseded datum or an equality sentence. A superseded datum leaving drops its entry,
and an equality leaving gives back the spellings its class displaced.
The supersession reconcile `sentex` leaving the store owes, from the removal choke point: the full pass for a `genlCx` edge or a schematic rewrite rule while any spelling is superseded, and the narrowed one over `sentex` and the classes it moved for a superseded datum or an equality sentence. A superseded datum leaving drops its entry, and an equality leaving gives back the spellings its class displaced.
(rederive-descended kb justs)Draw each of justs (edge-descended-justifications) again from the taxonomy as it
now stands, and return the handles it created as chaining seeds. Violations are
reported and displaced spellings refreshed, as the arrival path does. An entailment is
asked through retroactive-mints narrowed to its declaration; a descended equality
through derive-functional-equalities or derive-antisymmetric-equalities over the
fact at the head of its antecedents (read off by functor); a restatement through
migrate-sentex over its original or the target a restated meta names. Each task is
drawn once.
Draw each of `justs` (`edge-descended-justifications`) again from the taxonomy as it now stands, and return the handles it created as chaining seeds. Violations are reported and displaced spellings refreshed, as the arrival path does. An entailment is asked through `retroactive-mints` narrowed to its declaration; a descended equality through `derive-functional-equalities` or `derive-antisymmetric-equalities` over the fact at the head of its antecedents (read off by functor); a restatement through `migrate-sentex` over its original or the target a restated meta names. Each task is drawn once.
(redraw-deferred kb h transitions deadline)Draw again what draw-fact set aside for h: the fact, then each mint of
transitions it brought IN, whose entailments are drawn and, for one it created, its
restatement at a merged term (restate-retired), as the cascade it stopped in
would have. The answer is draw-fact's; a draw deferred again names the transitions of
both attempts.
Draw again what `draw-fact` set aside for `h`: the fact, then each mint of `transitions` it brought IN, whose entailments are drawn and, for one it created, its restatement at a merged term (`restate-retired`), as the cascade it stopped in would have. The answer is `draw-fact`'s; a draw deferred again names the transitions of both attempts.
(redraw-mints kb h)Draw the argument-type entailments of the stored literal fact at h over the spelling
it holds now, after a store mutation moved that spelling (integrate/move-row!):
[drawn stale]. drawn is deduce-placed's {:new :violations}. stale holds the
ids of the mint justifications h triggers that this spelling does not draw, for the
caller to drop. A declaration reads the argument at its own position, so a mint drawn
over the spelling the row held before can name the declaration of another position
(docs/canonicalization.md).
Draw the argument-type entailments of the stored literal fact at `h` over the spelling
it holds now, after a store mutation moved that spelling (`integrate/move-row!`):
`[drawn stale]`. `drawn` is `deduce-placed`'s `{:new :violations}`. `stale` holds the
ids of the mint justifications `h` triggers that this spelling does not draw, for the
caller to drop. A declaration reads the argument at its own position, so a mint drawn
over the spelling the row held before can name the declaration of another position
(docs/canonicalization.md).(refile-mint! kb old h)Bring record h's entry in the mint family to its stored spelling: out from under the
filing term of old, the record h held before (nil when its spelling did not move),
and under the current one while a mint justification concludes it. The callers are the
store mutations that move a record's spelling (integrate/respell!) or the
justifications concluding it (integrate/fold-row!).
Bring record `h`'s entry in the mint family to its stored spelling: out from under the filing term of `old`, the record `h` held before (nil when its spelling did not move), and under the current one while a mint justification concludes it. The callers are the store mutations that move a record's spelling (`integrate/respell!`) or the justifications concluding it (`integrate/fold-row!`).
(refresh-supersessions kb)(refresh-supersessions kb extra)(refresh-supersessions kb extra region)Reconcile the superseded set with the equality closure (supersession-map), on the
write path: where a migration hands over extra (the two-arity, which examines extra
and the moved classes), where a sentence leaves the store
(reconcile-removed-supersession!), and at recover, which passes nil for the full
pass. The settle calls it for a genlCx move that shows contexts (reconcile-move,
from drain-context-moves!), for an except that moved and for an equality edge that
moved in belief (settle/settle-finish).
Reconcile the superseded set with the equality closure (`supersession-map`), on the write path: where a migration hands over `extra` (the two-arity, which examines `extra` and the moved classes), where a sentence leaves the store (`reconcile-removed-supersession!`), and at `recover`, which passes nil for the full pass. The settle calls it for a `genlCx` move that shows contexts (`reconcile-move`, from `drain-context-moves!`), for an `except` that moved and for an equality edge that moved in belief (`settle/settle-finish`).
(release-lift! kb src-handle entry gens)Re-ask the lift of the fact at src-handle under declaration (:dh entry), or on
the statement alone where that is nil (a permuting mark's):
{:new [handle …]} when it is admitted now, the entry re-recorded under gens and the
term of the conviction read now (checks/conviction-watch) when the conviction still
holds, and retired when the fact or the declaration has left. An admitted lift
withdraws the ledger entry its refusal filed, since the order that brought the type
first would have filed none.
Re-ask the lift of the fact at `src-handle` under declaration `(:dh entry)`, or on
the statement alone where that is nil (a permuting mark's):
`{:new [handle …]}` when it is admitted now, the entry re-recorded under `gens` and the
term of the conviction read now (`checks/conviction-watch`) when the conviction still
holds, and retired when the fact or the declaration has left. An admitted lift
withdraws the ledger entry its refusal filed, since the order that brought the type
first would have filed none.(release-withheld! kb)Draw what the departures and arrivals withheld-releases left owed can have withheld
(owed-releases), and empty the debt: {:terms n :released n :new [handle …]}, the
terms the owed rows release and the records drawn. The caller settles.
Draw what the departures and arrivals `withheld-releases` left owed can have withheld
(`owed-releases`), and empty the debt: `{:terms n :released n :new [handle …]}`, the
terms the owed rows release and the records drawn. The caller settles.(restate-retired kb sx)Restate the derived row sx just stored (a mint entail-arg-type draws, or a
correspondence derivation chain/sync-values! places) when its sentence names a term
the equality closure already displaces, as assert-one restates an asserted fact
(docs/equality.md, "What a merge does"): sx is superseded and its twin under the
representative is stored (migrate-sentex). {:new [twin handles] :violations [v]},
empty when nothing in the sentence merged.
Restate the derived row `sx` just stored (a mint `entail-arg-type` draws, or a
correspondence derivation `chain/sync-values!` places) when its sentence names a term
the equality closure already displaces, as `assert-one` restates an asserted fact
(docs/equality.md, "What a merge does"): `sx` is superseded and its twin under the
representative is stored (`migrate-sentex`). `{:new [twin handles] :violations [v]}`,
empty when nothing in the sentence merged.(restrength-firings! kb rh)(restrength-firings! kb rh dropping-id)Set the strength of every justification rule rh informs to the rule's current
provers/firing-strength, in both copies: the record store's justification records
(what supporting-justifications shows and what recover rebuilds the network from)
and the network's (jtms/restrength-informant, which relabels the region). A rule's
firing strength moves when its defeasibility resolves or an exceptWhen arrives or
leaves; dropping-id is the exception meta-sentex leaving, if any.
Set the strength of every justification rule `rh` informs to the rule's current `provers/firing-strength`, in both copies: the record store's justification records (what `supporting-justifications` shows and what `recover` rebuilds the network from) and the network's (`jtms/restrength-informant`, which relabels the region). A rule's firing strength moves when its defeasibility resolves or an `exceptWhen` arrives or leaves; `dropping-id` is the exception meta-sentex leaving, if any.
(resubsumption-seeds kb removed removed-jids)The chaining seeds a teardown owes, given the removed sentexes its sweep collected
and the removed-jids justifications: subsumption-seeds and visibility-seeds in
the retraction direction. A departing genl edge seeds its spec subtree, read before
the teardown, and the rules with an antecedent on the edge's own relation
(closure-reader-rules), both only when the sweep took something besides the records
asked for (edge-own-mints excluded). A departing genlCx edge seeds the antecedents
of the firings that named it (sighting-seeds) and its closure-reading rules. See
docs/contexts.md, "A genlCx edge owes the same debt".
The chaining seeds a teardown owes, given the `removed` sentexes its sweep collected and the `removed-jids` justifications: `subsumption-seeds` and `visibility-seeds` in the retraction direction. A departing `genl` edge seeds its spec subtree, read before the teardown, and the rules with an antecedent on the edge's own relation (`closure-reader-rules`), both only when the sweep took something besides the records asked for (`edge-own-mints` excluded). A departing `genlCx` edge seeds the antecedents of the firings that named it (`sighting-seeds`) and its closure-reading rules. See docs/contexts.md, "A `genlCx` edge owes the same debt".
(retire-mint! kb sentex)Take the departing sentex out of the mint family, when it is filed there.
Take the departing `sentex` out of the mint family, when it is filed there.
(retire-unjustified-mints! kb removals)Take out of the mint family each record a mint justification removed in removals
concluded, once no other mint justification concludes it. removals is a
jtms/retract!-shaped result, whose :removed-supports names each removed
justification's consequence and informant, read off the network before the removal. A
consequence the removal swept leaves through retire-mint!; one still in the network
is retired here, and its record is the one fetch.
Take out of the mint family each record a mint justification removed in `removals` concluded, once no other mint justification concludes it. `removals` is a `jtms/retract!`-shaped result, whose `:removed-supports` names each removed justification's consequence and informant, read off the network before the removal. A consequence the removal swept leaves through `retire-mint!`; one still in the network is retired here, and its record is the one fetch.
(revived-declaration-sweeps kb handles)Run, for each sentex in handles the settle just brought back OUT to IN, the sweeps
its arrival runs over the facts already stored: equate-existing and
antisym-equate-existing for a merge mark, revived-edge-sweep for a genl edge under
one, lift-existing for a decontextualized_predicate (docs/equality.md, "A mark that
revives runs its arrival sweep again"). Returns one {:new :superseded :violations}, or
nil when the KB declares no merge, nogood-candidate or lift mark. The sweeps read
stored content and are idempotent; handles are walked in content order.
Run, for each sentex in `handles` the settle just brought back OUT to IN, the sweeps
its arrival runs over the facts already stored: `equate-existing` and
`antisym-equate-existing` for a merge mark, `revived-edge-sweep` for a `genl` edge under
one, `lift-existing` for a `decontextualized_predicate` (docs/equality.md, "A mark that
revives runs its arrival sweep again"). Returns one `{:new :superseded :violations}`, or
nil when the KB declares no merge, nogood-candidate or lift mark. The sweeps read
stored content and are idempotent; handles are walked in content order.(rule-recheck-keys tx rule-sentex)The keys the re-check index posts the rule rule-sentex under, read against the
taxonomy tx: rules/recheck-predicates, the closed-extent, separation-denial and
negates-denial keys of its sentence, and rules/nonempty-recheck-predicates. Nil when
the rule carries none of them and no re-check condition (rules/rechecked?); a rule
with a condition and no key answers an empty vector, which posts it into the :rules
set alone.
The keys the re-check index posts the rule `rule-sentex` under, read against the taxonomy `tx`: `rules/recheck-predicates`, the closed-extent, separation-denial and negates-denial keys of its sentence, and `rules/nonempty-recheck-predicates`. Nil when the rule carries none of them and no re-check condition (`rules/rechecked?`); a rule with a condition and no key answers an empty vector, which posts it into the `:rules` set alone.
(subsumed-mint-blocks kb moved was-in asked believed? routes? whole)The justifications to block because the records they hold up are redundant:
{:blocked #{jid} :withdrawn #{handle}}, plus :surplus (surplus-placements) for the
settle to drop, over the records the sentexes in moved can have displaced. Blocks
every justification of a withdrawn record. moved is a delay, forced only when the
entailment is on, the mint is prunable and the mint family is non-empty; forced, it is
filtered by subsumer-shaped? and read through withdrawal-candidates and
edge-route-candidates. Only a record that became believed is asked, and also each
record a retraction left standing on a derivation alone (note-unpremised!). asked
is the settle's record of the records already asked, so each is asked once per settle.
believed? is belief now. With routes?, descent-surplus-placements is asked too.
whole is the region's size for a recover, else nil; with fewer mints stored than
that, moved is never forced. See docs/argtypes.md.
The justifications to block because the records they hold up are redundant:
`{:blocked #{jid} :withdrawn #{handle}}`, plus `:surplus` (`surplus-placements`) for the
settle to drop, over the records the sentexes in `moved` can have displaced. Blocks
every justification of a withdrawn record. `moved` is a delay, forced only when the
entailment is on, the mint is prunable and the mint family is non-empty; forced, it is
filtered by `subsumer-shaped?` and read through `withdrawal-candidates` and
`edge-route-candidates`. Only a record that became believed is asked, and also each
record a retraction left standing on a derivation alone (`note-unpremised!`). `asked`
is the settle's record of the records already asked, so each is asked once per settle.
`believed?` is belief now. With `routes?`, `descent-surplus-placements` is asked too.
`whole` is the region's size for a `recover`, else nil; with fewer mints stored than
that, `moved` is never forced. See docs/argtypes.md.(subsumption-seeds kb sentence)The stored facts the genl edges sentence installs newly make matchable, as
chaining seeds: the taxonomy twin of lift-existing. The edges are
tax/installed-edges' (a genl edge, or one per part of a cover). The seeds are
sub's whole spec subtree, believed only, and per edge only when rule-reads-above?
holds. The negated half is negative-subsumption-seeds; the removal side is
resubsumption-seeds. See docs/inference.md and docs/taxonomy.md.
The stored facts the `genl` edges `sentence` installs newly make matchable, as chaining seeds: the taxonomy twin of `lift-existing`. The edges are `tax/installed-edges`' (a `genl` edge, or one per part of a cover). The seeds are `sub`'s whole spec subtree, believed only, and per edge only when `rule-reads-above?` holds. The negated half is `negative-subsumption-seeds`; the removal side is `resubsumption-seeds`. See docs/inference.md and docs/taxonomy.md.
(surplus-placements kb edges)(surplus-placements kb edges plans)The mint justifications, in id order, that a genlCx edge among edges (sentexes)
left at a context that is no longer a placement of their fact and declaration
(pair-placements). plans maps an edge record to its edge-mint-plan, whose
:displaced contexts are the only ones read. The caller checks that the entailment is
on and the mint family holds a record.
The mint justifications, in id order, that a `genlCx` edge among `edges` (sentexes) left at a context that is no longer a placement of their fact and declaration (`pair-placements`). `plans` maps an edge record to its `edge-mint-plan`, whose `:displaced` contexts are the only ones read. The caller checks that the entailment is on and the mint family holds a record.
entries as the lookup map the walks below dispatch through.
`entries` as the lookup map the walks below dispatch through.
(take-except-moves! kb)Empty :except-moves and return what the settle owes it:
{:extra [[datum reason]] :region #{datum} :full? bool :moved #{h}} — the
supersessions except-move-sweeps found, the superseded data an except that moved
can change (except-move-region), whether a move is still pending undrained, which
leaves the supersession reconcile nothing narrower than a full pass, and the handles
the drained moves hid or showed. nil when nothing moved.
Empty `:except-moves` and return what the settle owes it:
`{:extra [[datum reason]] :region #{datum} :full? bool :moved #{h}}` — the
supersessions `except-move-sweeps` found, the superseded data an `except` that moved
can change (`except-move-region`), whether a move is still pending undrained, which
leaves the supersession reconcile nothing narrower than a full pass, and the handles
the drained moves hid or showed. nil when nothing moved.(take-first-deferral! kb)Whether defer-first-release! marked this settle, with the mark cleared.
Whether `defer-first-release!` marked this settle, with the mark cleared.
(take-producer-moves!)*producer-moves*' moves, emptied, or nil when it is unbound.
`*producer-moves*`' moves, emptied, or nil when it is unbound.
(take-supersession-moves! kb){:moved #{datum} :was {datum entry}}: the datums whose supersession entry changed
since the last call, each with its entry before the first change (nil when it was not
superseded), emptied; nil when the KB keeps no supersession moves. settle-finish
reads it once per settle: a supersession moves belief with no relabel, so
jtms/touched does not name these.
`{:moved #{datum} :was {datum entry}}`: the datums whose supersession entry changed
since the last call, each with its entry before the first change (nil when it was not
superseded), emptied; nil when the KB keeps no supersession moves. `settle-finish`
reads it once per settle: a supersession moves belief with no relabel, so
`jtms/touched` does not name these.(taxonomy-generations kb)The genl and genlCx generations with the rebuild epoch (tax/relation-epoch), the
value conviction-generations extends with the separations. settle re-asks an entry only when this moves
from the value the entry records, so the recorded value and the comparison are this one
function. The epoch moves at every recover, which restarts the generations at 0.
The `genl` and `genlCx` generations with the rebuild epoch (`tax/relation-epoch`), the value `conviction-generations` extends with the separations. `settle` re-asks an entry only when this moves from the value the entry records, so the recorded value and the comparison are this one function. The epoch moves at every `recover`, which restarts the generations at 0.
(transitive-rule-seeds kb rule-sentex)The stored facts a newly forward-capable rule needs back on the agenda when one of its
antecedents reads a declared-transitive predicate: the third arrival order of
transitive-seeds. Off unless an antecedent is declared transitive. Read unscoped.
The stored facts a newly forward-capable rule needs back on the agenda when one of its antecedents reads a declared-transitive predicate: the third arrival order of `transitive-seeds`. Off unless an antecedent is declared transitive. Read unscoped.
(transitive-seeds kb sentence)The stored facts a declared-transitive predicate's closure makes newly matchable, as
chaining seeds: the TransitivePredicateProver's twin of subsumption-seeds. Two
arrival orders: a link (pred a b) with pred already transitive seeds the believed
facts mentioning a left end (transitive-left-ends); a declaration (transitive pred)
over stored links seeds every believed fact on a partner functor. Off unless some rule
takes a pred antecedent. The removal side needs no twin. The mark is read unscoped.
See docs/inference.md, "Seeding a transitive closure".
The stored facts a declared-transitive predicate's closure makes newly matchable, as chaining seeds: the `TransitivePredicateProver`'s twin of `subsumption-seeds`. Two arrival orders: a link `(pred a b)` with `pred` already transitive seeds the believed facts mentioning a left end (`transitive-left-ends`); a declaration `(transitive pred)` over stored links seeds every believed fact on a partner functor. Off unless some rule takes a `pred` antecedent. The removal side needs no twin. The mark is read unscoped. See docs/inference.md, "Seeding a transitive closure".
(triggered-mints kb moved was-in asked believed?)Draw what the memberships and genl edges among moved that came IN this settle
trigger (trigger-entailments): {:new [handle …] :violations [v …]}. A membership
(T x) arriving after a fact and an interArg or homogeneity declaration over it is
the trigger's arrival order, which the fact and the declaration cannot reach because
the trigger did not hold when each arrived. was-in and believed? are belief before
the settle and now; asked holds the records this settle has asked.
Draw what the memberships and `genl` edges among `moved` that came IN this settle
trigger (`trigger-entailments`): `{:new [handle …] :violations [v …]}`. A membership
`(T x)` arriving after a fact and an `interArg` or homogeneity declaration over it is
the trigger's arrival order, which the fact and the declaration cannot reach because
the trigger did not hold when each arrived. `was-in` and `believed?` are belief before
the settle and now; `asked` holds the records this settle has asked.(unindex-exceptWhen-meta kb meta-sentex)The mirror of index-exceptWhen-meta: withdraw the departing exceptWhen
meta-sentex's postings, then re-post the rule from the predicates its remaining
exceptions and NAF antecedents still need — a set re-add restores any shared
predicate the blanket withdraw over-removed, and leaves the rule out of the :rules
set exactly when nothing watches it any more. Queues the rule for re-check, since
losing an exception may revive what it was blocking, restores the rule's firing
strength when no guard remains (restrength-firings!), and releases the firings of a
forced-monotonic rule no exception convicts any more (checks/force-sentexes!).
The mirror of `index-exceptWhen-meta`: withdraw the departing exceptWhen meta-sentex's postings, then re-post the rule from the predicates its *remaining* exceptions and NAF antecedents still need — a set re-add restores any shared predicate the blanket withdraw over-removed, and leaves the rule out of the `:rules` set exactly when nothing watches it any more. Queues the rule for re-check, since losing an exception may revive what it was blocking, restores the rule's firing strength when no guard remains (`restrength-firings!`), and releases the firings of a forced-monotonic rule no exception convicts any more (`checks/force-sentexes!`).
(unpost-mint! index sentence context h)The mirror of post-mint!: take record h, holding sentence in context, out of
index's mint family, when the sentence has a mint-term.
The mirror of `post-mint!`: take record `h`, holding `sentence` in `context`, out of `index`'s mint family, when the sentence has a `mint-term`.
(visibility-seeds kb sentence)(visibility-seeds kb sentence filtered?)move-seeds for sentence, a genlCx edge between two symbols, and nil for any other
sentence.
`move-seeds` for `sentence`, a `genlCx` edge between two symbols, and nil for any other sentence.
(wff-problems tax sentence context)Structural well-formedness problems for sentence (empty if OK): the :wff column of
the table, walked. A functor with no entry or no :wff arm is structurally
unconstrained here. context is passed to every arm. A nil tax skips the checks that
read stored content (the genl, genlCx, cover and rewriteOf cycles and the
transitivity a preservation names), as an import does. A not over a pr/query-only
term, at any depth, is checked by that term's arm.
Structural well-formedness problems for `sentence` (empty if OK): the `:wff` column of the table, walked. A functor with no entry or no `:wff` arm is structurally unconstrained here. `context` is passed to every arm. A nil `tax` skips the checks that read stored content (the `genl`, `genlCx`, cover and `rewriteOf` cycles and the transitivity a preservation names), as an import does. A `not` over a `pr/query-only` term, at any depth, is checked by that term's arm.
(wff-violation kb sentence context)wff-problems as a value, for content a rule derived: nil when sentence is
well-formed, else a violation map in the shape checks/constraint-violation returns.
Dropped and reported rather than thrown, since chaining is a fixpoint.
`wff-problems` as a value, for content a rule derived: nil when `sentence` is well-formed, else a violation map in the shape `checks/constraint-violation` returns. Dropped and reported rather than thrown, since chaining is a fixpoint.
(with-recheck-reads & body)Run body with a *recheck-reads* memo, the one already bound if there is one. The
caller's body stores no rule and no declaration.
Run `body` with a `*recheck-reads*` memo, the one already bound if there is one. The caller's body stores no rule and no declaration.
(withdrawn-edge-seeds kb handles)The chaining seeds a settle owes the closure edges among handles, mints it is about
to withdraw as redundant (subsumed-mint-blocks) or spellings a merge retired
(settle/withdraw-retired-firings!), that a rule firing names as its witness:
departed-edge-rejoin's facts and rules for each such edge and each of its twins
(handle-twins). The condition is a dependent justification whose informant is a rule,
read before the sweep deletes it. See docs/argtypes.md.
The chaining seeds a settle owes the closure edges among `handles`, mints it is about to withdraw as redundant (`subsumed-mint-blocks`) or spellings a merge retired (`settle/withdraw-retired-firings!`), that a rule firing names as its witness: `departed-edge-rejoin`'s facts and rules for each such edge and each of its twins (`handle-twins`). The condition is a dependent justification whose informant is a rule, read before the sweep deletes it. See docs/argtypes.md.
(withdrawn-type-entailments kb bound)The declaredType justifications of (unary_predicate T) to drop for each relation
T of bound (the relations whose own arity bindings moved, the keys of
arity/drain!'s :bound) whose length no longer admits one alone (arity/mintable-type?): an arity
statement binding T to another length arrived after a declaration naming T minted.
withdrawn-type-mints drops what it minted. When the length admits one again,
mints-on-lengths sweeps the declaration. Returns the justification ids, for the
caller to drop. The stored entailment is read before the length, so a binding of a
relation no declaration names reads no length.
The `declaredType` justifications of `(unary_predicate T)` to drop for each relation `T` of `bound` (the relations whose own arity bindings moved, the keys of `arity/drain!`'s `:bound`) whose length no longer admits one alone (`arity/mintable-type?`): an arity statement binding `T` to another length arrived after a declaration naming `T` minted. `withdrawn-type-mints` drops what it minted. When the length admits one again, `mints-on-lengths` sweeps the declaration. Returns the justification ids, for the caller to drop. The stored entailment is read before the length, so a binding of a relation no declaration names reads no length.
(withdrawn-type-mints kb bound)The mint justifications to drop for each type t of bound (arity/drain!'s
:bound) with a moved binding that refuses a mint (binds-another-length?) and an IN
length that does not admit one (arity/mintable-type?), whether or not a length of one
is IN beside it: those concluding a membership (t x) or an edge (genl x t). A
record with other support stays. Returns the justification ids, for the caller to
drop. Reads nothing more while the mint family is empty, and reads t's one-argument
tuples alone. Every context, since t's length holds at every context
(arity/relation-length).
The mint justifications to drop for each type `t` of `bound` (`arity/drain!`'s `:bound`) with a moved binding that refuses a mint (`binds-another-length?`) and an IN length that does not admit one (`arity/mintable-type?`), whether or not a length of one is IN beside it: those concluding a membership `(t x)` or an edge `(genl x t)`. A record with other support stays. Returns the justification ids, for the caller to drop. Reads nothing more while the mint family is empty, and reads `t`'s one-argument tuples alone. Every context, since `t`'s length holds at every context (`arity/relation-length`).
(withheld-releases kb moved was-in asked withdrawn believed?)The mints no longer withheld because a record that subsumed them left, and the
justifications a withheld mint owes a record of its sentence that arrived:
{:new [handle …]}, drawn by rederive-mints (docs/argtypes.md, "Nothing records a
withheld mint"). Pruning only; a genlCx edge's departure is the drain's
(departed-context-edge-mints). Under *release-withheld?* false the departures and
arrivals stay owed (owe-releases!) and nothing is drawn. Departures are the records
note-departure! queued and the records in moved (a delay) that went IN to OUT against
was-in; arrivals came IN. withdrawn holds the mints this settle withdrew, which
release nothing; asked holds the records already asked, so each is asked once per
settle. A term is re-drawn only for the mints one of its departures could have
withheld (may-release).
The mints no longer withheld because a record that subsumed them left, and the
justifications a withheld mint owes a record of its sentence that arrived:
`{:new [handle …]}`, drawn by `rederive-mints` (docs/argtypes.md, "Nothing records a
withheld mint"). Pruning only; a `genlCx` edge's departure is the drain's
(`departed-context-edge-mints`). Under `*release-withheld?*` false the departures and
arrivals stay owed (`owe-releases!`) and nothing is drawn. Departures are the records
`note-departure!` queued and the records in `moved` (a delay) that went IN to OUT against
`was-in`; arrivals came IN. `withdrawn` holds the mints this settle withdrew, which
release nothing; `asked` holds the records already asked, so each is asked once per
settle. A term is re-drawn only for the mints one of its departures could have
withheld (`may-release`).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 |