vaelii.impl.special — com.vaelii/vaelii 0.29.0

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.

*entail-moves?* clj

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.

*recheck-reads* clj

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.

*release-withheld?* clj

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.

*seed-moves?* clj

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! clj

(advance-refusal-generations! kb {:keys [taxonomy gens conviction]})

Record the generations now on the :constraint and :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 clj

(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.

antisym-equate-under-context-edge clj

(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.

antisym-equate-under-edge clj

(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.

argument-refusals? clj

(argument-refusals? kb)

Does the refusal record hold a refused firing or a refused lift, each waiting on an argument conviction? Two map reads (:kinds).

arrival-releasable-rule? clj

(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.

bearing-equalities clj

(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.

believed-again-sweeps clj

(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.

check-declarations clj

(check-declarations entries)

(check-declarations entries arm-functors)

Refuse a table whose arms and declarations disagree — the cross-layer half of check-entries, which sees only the arms and so can only check that they mirror each other. Three disagreements are refused, all at namespace load:

• a functor with arms and no declaration, or a declaration and no arms. The two are one enumeration now, and a functor in only one of them is a predicate the engine either interprets without saying so or says something about and does nothing with. arm-functors is the set of functors the arms map keys, read before entries filters to pr/in-special-table — so an arm keyed on a functor no declaration places in the table is refused here rather than left out of the join unreported. The one-argument arity reads the functors off entries itself, for a caller driving the validator over a hand-built table.
• a :cached declaration whose arms have no cache triple, or the reverse.
• a :checked declaration whose arms have no :wff, or the reverse.

check-entries catches a missing arm; neither validator can catch an arm attached to the wrong functor, which is what special_table_test and predicates_test are for. Two validators at two layers, each checking what it can see: they are not to be merged.

One :type between them — :bad-table-entry, discriminated by :mismatch — for the reason check-entries already gives itself two shapes under one word: whichever way the table is bad, the caller catching it is the namespace load, and there is nothing a second keyword would let that caller do.

check-entries clj

(check-entries entries)

Refuse an ill-formed table at namespace load, so add/remove symmetry is a structural property rather than a review item.

Two shapes are refused. An entry with some of the cache arms — an :integrate whose :disintegrate or :rebuild is missing (or any other partial triple) is exactly the mirrored-cond drift this table exists to end: the cache would fill on assert and leak on retract, or come back wrong after recover. And an entry with no arm at all, which is a typo. :mismatch says which — :partial-cache-triple or :no-arm — the same discriminant every other :bad-table-entry in the tree carries, so a caller reads one key rather than guessing from the message. Returns entries unchanged so it can wrap the def.

class-moved-merges clj

(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".

clear-except-moves! clj

(clear-except-moves! kb)

Empty :except-moves outright — a rebuild reconciles every supersession from scratch.

closure-edge-relation clj

(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.

computed-reading-rules clj

(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). A rule whose computed antecedents only other provers answer rests on no answer the datum moves.

Nothing connects the two predicates: a (conversionFactor Gram Kilogram 0.001) decides whether (quantityGreaterThan ?q (QuantityFn 1 Kilogram)) holds of a mass in grams, the trigger index keys on the antecedent's own functor, and the facts that would have triggered the rule have already arrived. bfn is the functor of the sentence's underlying body, so a believed (not (conversionFactor …)) reaches here too: it defeats the positive row and so moves the reading exactly as removing it would.

The rules stated in every context are read, since the re-join and the re-check place each firing from its antecedents' contexts. One map lookup for every datum that is not one of these. For one that is, the stored rules' antecedent keys are read once, and the rules only for the answers some rule takes. s is the sentence: a genl edge moves only the expression kinds at or above its upper end (provers/support-answers-reading).

context-move clj

(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.

conviction-generations clj

(conviction-generations kb)

taxonomy-generations with the separations (tax/separation-inputs): the value an argument conviction is decided under, a refused lift's and (as chain/constraint-generations) a refused firing's. A conviction reads a type the taxonomy separates from the declared one, so a separation moving re-asks it.

declared-type-informant clj

The informant of the justification of (unary_predicate T) by an argument declaration naming T (unary-entailments). No mint informant (mint-informant?): the membership enters no mint family, and only a conflicting length withdraws it (withdrawn-type-entailments).

deduce-arg-types clj

(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 both stores of new content — assert and forward chaining's place-conclusion — because what a declaration says about an argument is a claim about the predicate, not about how a particular sentence arrived. Entailing only what a caller asserted would make belief depend on arrival order, exactly as lifting only asserted content would.

pre-checked? says these entailments already passed the definitional constraint check, so each mint's admissibility test skips it (inadmissible). Only the assert path passes true, and only for its first level: checks/entailment-check validated those before the trigger was stored. The default is false, which every other caller takes and which the cascade the materializer walks itself takes — a mint drawn one level down was not on entailment-check's pre-store list, so it is checked in full.

deduce-below clj

(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.

deduce-lifts clj

(deduce-lifts kb sentence handle context)

Deduce sentence (stored at handle in context) into CxUniverse if its predicate is decontextualized or is a permuting mark — {:new [handles] :violations [v]}, nil when neither holds. Called by assert and by forward chaining's place-conclusion. A permuting mark (inherit/permuting-marks) is lifted on its statement alone, whatever the KB declares; any other is lifted once per declaring sentex. The declaration is read unscoped (docs/contexts.md#decontextualized_predicate-a-fact-that-belongs-to-the-kb-not-to-one-theory).

defer-first-release! clj

(defer-first-release! kb)

Make kb's next settle run with *release-withheld?* false (take-first-deferral!).

departed-edge-seeds clj

(departed-edge-seeds kb handles)

The chaining seeds a settle owes the records among handles that hold closure edges (closure-edge-relation: a genl or genlCx edge, or a cover) and went IN ⇒ OUT in it — resubsumption-seeds for an edge that lost belief rather than its record.

A defeat sweeps nothing: the firings that named the edge as a witness go OUT with it and are retained for revival, so the retraction path's re-join never runs, and a reachability that outlives the edge over a second route never re-derives them. The same three sentences then leave a conclusion believed where the negation arrived first and withdrawn where it arrived last (docs/nmtms.md, "Where the layer stops").

This runs per edge only when a dependent is now OUT, the defeat's counterpart of resubsumption-seeds' condition on the sweep having taken something: an edge nothing rests on, or whose dependents all kept another justification, owes no re-join. The spec subtree is read with the edge already OUT, which changes no answer: specs of the edge's own sub is what lies below sub, and the edge runs above it.

derive-antisymmetric-equalities clj

(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-functional-equalities clj

(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 (tax/context-down), since a reader below two blind siblings sees a clash neither sibling sees. readers, when given, narrows that set; only equate-under-context-edge-via passes it, with the contexts the edge widened (genlcx_sweep_test, genlcx_sweep_cost_test).

Two presence checks run before context-down is read: the KB-wide tax/functional-family-declared?, one map read, and functional-mark-relevant? of the functor, so a fact no mark reaches pays for no reader sweep.

derived-sentex-added clj

(derived-sentex-added kb sentex handle)

The derivation-path add choke point: everything that must happen because a derived sentex landed in the store — the integration arms a derived sentex may reach, and the exception re-check post, since a derived fact is a re-check trigger like an asserted one (an exception may be stated over a predicate that only ever arrives by inference — the cried-wolf case, where liar is concluded by another rule).

The dispatch is run-integrate-arms's, narrowed. A functor the table keys runs its :integrate arm iff the entry is flagged :derived? (integrate-transitive); a functor it does not key runs the structural walk, minus the rule arm the caller posts by name (structural-integrate's derived?). Both halves have to be here or the derivation path reaches a strictly smaller set of caches than recover's rebuild does, and the running KB and the restarted one then disagree about one store: a rule concluding a disjoint metatype's member separated nothing until a restart replayed it, and a rule-derived (except (sentexHandle H)) hid its target from the reads — the index holds it from the store primitive (kb/create-sentex) — while no firing that used H was ever queued for the sweep.

The except arm's reconcile-belief-change is called inline, mid-fixpoint, and that is safe. It does not re-enter chaining or settling: tax/refresh-beliefs is a swap! over the taxonomy that reads jtms/in? and writes cache entries — no assert, no chain, no settle, and no relabel. It is scoped to the arriving except and the handle it hides, so it costs two handles' worth of edge lookups rather than the vocabulary's. recheck-except beside it only pushes rule handles onto the re-check queue, which is what the settle around this drains; that is exactly what the assert path does from inside its own integrate-sentex.

The one ordering difference from the assert path is that mark-premise runs before integrate/sentex-added, where two of this fn's four callers run it before the justification — so the except is stored and indexed a few lines ahead of being believed. Nothing reads a scoped taxonomy answer between the store and the justification (the callers write a justification and nothing else), and the JTMS labels the region as the justification lands, so the first read after it recomputes against settled belief.

Lives here rather than beside sentex-added in vaelii.impl.integrate because the equality arms are themselves derivation sites: a migrated twin and a functional-inferred equals are derived sentexes, and hand-rolling this pair at those sites is exactly the copy-paste the choke points exist to end. Callers: forward chaining's place-conclusion, the decontextualized_predicate lift, the argument-constraint entailment, and derive-equality.

descent-surplus-placements clj

(descent-surplus-placements kb moved)

The mint justifications, in id order, that a record among moved left at a context that is no longer a placement of their fact and declaration (pair-placements): a genl route or a trigger membership stated in a more general context than the one a placement descended to places the pair above it, and the placement below goes, as surplus-placements drops one a genlCx edge displaced.

• A record that installs genl edges (tax/installed-edges) whose super reaches a declaration (super-reaches-declaration?) reads the facts of its subs' spec subtrees, the extent entail-under-edge drew over.
• A membership (T x) whose T reaches a trigger type (trigger-types) reads the facts naming x, the facts trigger-entailments drew over.

Each fact's mint justifications are read off the network (jtms/dependents). The trigger types are reached through tax/genls-global (E17), as trigger-entailments reaches them: the facts are read across every context, and each justification is asked its own pair's placements, so the unscoped presence check only reads more facts.

disintegrate-sentex! clj

(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.

drain-context-moves! clj

(drain-context-moves! kb read rebuilding?)

Once a settle pass: read the genlCx moves since the placement cursor (decide/take-edge-cursor!, register J6 over J5), compute each one's context-move once, and hand it to every row of move-families the move reads. The edges are the ones moved-edges names; the placement families read :reach, a delay of {:under :below} over every lower end moved and each active edge up from it ({:all? true} when the relation was rebuilt), read over the unscoped closures: a superset over every reader, where no reader exists, as the candidate rows are (decide/unscoped-closures). The active edges an except that moved reaches are moves of their own (excepted-edges), read by the effective rows. read is the settle's volatile of supporter labels drained. Returns {:reach :first? :seeds :mig}. A rebuild takes the departures, leaves the cursor for the first pass that places, and runs no row. See docs/contexts.md, "One context move".

drain-departures! clj

(drain-departures! kb)

The records note-departure! queued since the last drain, and the queue emptied.

drain-except-moves! clj

(drain-except-moves! kb sweep?)

Take the pending handles off :except-moves, sweep them (except-move-sweeps, with sweep?), and keep 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.

drop-kinds clj

(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.

drop-replaced-routes! clj

(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 from it only in genl / genlCx edges that are all believed. route is just's own route handles; nil reads them off the antecedents by shape. The consequence keeps just, whose antecedents are groundable, so the sweep collects nothing just does not hold up.

An edge of the older route that is OUT keeps its justification: a route a defeat took away comes back when the defeat lifts, and the store then holds both (docs/nmtms.md, "Where the layer stops").

edge-descended-justifications clj

(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 justification records, since the records are what name the fact and the declaration to derive from again. This runs only when gone holds a route edge, or a membership while a trigger declaration is stored, so a removal that took neither fetches no justification record.

An entailment qualifies when a removed antecedent is past its fact and declaration (past-the-pair?) and neither of those two is removed; a descended equality, when one of its antecedents is a removed route edge and no removed antecedent is anything else; a restatement (:migration) the same way, with a removed equality counted as a route edge. A removed fact or declaration withdraws the derivation, and re-deriving it would undo the removal.

entail-existing clj

(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 — so a declaration arriving after the facts reaches them exactly as one arriving before reaches the facts that follow. Same {:new :violations} result, so the types it mints are chaining seeds like any other new content. nil when sentence is not an argument constraint.

triggered-mints reaches a conditional form's trigger arriving after both the fact and the declaration, in the settle.

Sweeps what is stored, not what is believed, for lift-existing's reason: a type minted off a defeated fact is justified by that fact and so is defeated too — the JTMS already says what a disbelieved antecedent means — whereas skipping it would leave the type missing when the fact revives, which is belief depending on the order the defeat and the declaration arrived in.

An inert sentex draws nothing (retroactive-mints).

The extent is read off the predicate extents of P's whole spec subtree, which is the precise answer to "every stored tuple this declaration constrains": a declaration on P binds every predicate beneath it (res/constraining-predicates), so an extent read off P alone would mint over (parentOf …) and not over (fatherOf …) — a type the same three sentences produce in one arrival order and not the other. subtree-sentexes reads it, and snapshots it before the first mint. A (resultArg F n) binds the stored 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 reads no extent and records nothing: every arm asks arity/mintable-type? of that type before it draws, so no fact would yield an entailment, and mints-on-lengths runs the sweep once the type's length admits one. A declaration whose every type is thing reads none either. A declaration that mints entails its types' unary_predicate memberships (unary-entailments).

entail-under-context-edge clj

(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 of an entailment through an inherited declaration, beside the fact, the declaration and the genl edge. Each derivation names the genlCx edges it sees its declaration through (checks/entailment-support), so retracting this edge takes back what rests on it, and rederive-descended draws again what a second route still reaches.

The edge also gives a fact and a declaration a new common descendant, under sub, when one of them is stated where super sees it and the other in a context a context under sub sees and super does not (below: context-move's :under and :below). The facts are read from every context of below, and each draws at its placements (deduce-placed); the declarations stated in below draw over the facts stated in a context a reader under sub sees through the edge alone (:moved), since a fact the reader already saw has its placements already (declarations-meeting). A placement the edge leaves below a more general one is dropped by the settle (surplus-placements).

Off unless *assertive-arg-types?* and *entail-moves?* hold and some predicate declares. Off too when no context of m's :moved stores a sentex older than the :floor (any sentex, without one): every reader under sub then sees the content it saw before the move, so no fact meets a new ingredient (lein perf's genlcx-edge-showing-an-empty-context). The facts are read from the smaller of two sides, compared by index counts: the facts stored in the contexts of below, kept when a declaration reaches their functor, or the extent in below of each functor a declaration reaches (reads/as-stored-with-functor-in), priced at the lesser of the declared extent and one probe per functor and context. So the fact half costs the lesser of the edge's extent and the declared extent, and a context holding many undeclared facts or a KB holding many declared ones elsewhere costs only the other. Snapshotted before the first mint. With m's :floor (seed-floor), a fact or a declaration stored at or above it arrived with the edge in the taxonomy and drew its entailments then (deduce-arg-types, entail-existing), so neither half reads it. With m's :entailed (a volatile set of handles, one per drain, drain-moves!), a fact an earlier move of the drain drew is not drawn again: every move of a drain reads one taxonomy, and deduce-placed reads no move.

entail-under-edge clj

(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 of the same three ingredients, and there for the reason subsumption-seeds beside it is. A covering, separating or partition installs an edge per part (tax/installed-edges), and each of those edges is read as an arriving genl edge.

A constraint descends the predicate hierarchy, so the fact, the declaration and the edge are all ingredients of one entailment. deduce-arg-types covers the fact arriving last and entail-existing the declaration arriving last; without this, the edge arriving last mints nothing and the same three sentences leave the KB holding a type in two orders out of three. nil when sentence installs no edge.

The whole spec subtree of sub, because subsumption is transitive: an edge at the top of a predicate hierarchy brings every predicate below it under the declarations above it. Each stored sentex is put back through checks/constraint-entailments in its own context — the same function the other two directions ask, so the three cannot disagree — and the mints deduplicate on content, so a fact whose type was already entailed by a route that survives contributes a justification and no second record.

Three checks in front of the subtree, because this arm fires on a genl edge — the commonest thing an ontology says, where the other two fire on a declaration. Off unless *assertive-arg-types?*, since with the entailment off there is nothing to mint and the edge's other consequences are subsumption-seeds'; off unless some predicate carries an entailing declaration (any-declaring?, the taxonomy's :props sets, no index read); and off unless a genl-ancestor of super carries one (super-reaches-declaration?). The first two keep an edge under a predicate nobody constrained from reading a subtree's extent to discover there was nothing to draw; the third keeps an edge whose sub is constrained but whose super reaches no declaration from reading it, since every mint this arm draws cites the arriving edge and so reaches its declaring predicate through super. The extent itself is subtree-sentexes, filtered by cardinality for the same reason one step further in.

entries clj

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 an entry for. post-taxonomy-supporters! replays it top to bottom and a rebuild arm may read what an earlier one wrote (metatype membership reads the marks; nothing else is order-sensitive today, and keeping the assert path's traditional order adds no work), so the order is content and belongs with the other content.

This vector is the functor enumeration the four walks use: integrate, disintegrate, rebuild and wff all walk it, so a predicate declared and armed is added to all four at once, check-entries refuses it half-armed and check-declarations refuses it armed without being declared — the latter reading the arms map keys, which hold every armed functor, not this filtered vector, which by construction holds only the declared ones. table below is the lookup table.

equate-existing clj

(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.

equate-under-context-edge clj

(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 fourth arrival order of the three ingredients, and the context twin of equate-under-edge. Sweeps the stored facts the readers under sub see (context-move's :seen), kept when functional-mark-relevant? admits their functor, and hands each to derive-functional-equalities at its own context, which sweeps the readers below it. Free for a KB that declares nothing functional. Budgeted (budgeted-context-edge-candidates), and idempotent: a pair same-class-in? holds is skipped. An equality derived here rests on the genlCx edges its reader sees each fact and the declaration through (pair-antecedents), so retracting the edge un-merges.

equate-under-edge clj

(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.

except-move-region clj

(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}}.

A supersession is decided at the datum's own context from the equalities that context sees (displacement), and an except changes that only for the contexts that read it and only for the equalities it withdraws, so this set is the whole of what the settle's reconcile re-examines for it. Each candidate costs a term-index lookup per term, the same lookups the arrival sweep makes, and a KB superseding nothing costs one deref.

except-move-sweeps clj

(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. Returns one {:new :superseded :violations :removed}, or nil when handles is empty.

An equality restates a fact for the readers that see it, and an except changes which readers those are without the equality arriving, leaving or changing label. A fact stored while the except hid the equality from the fact's context was stored as spelled, with no twin, and every goal from that context is normalized under the equality the moment the except goes — so without this sweep the fact is believed and answered by no read (docs/equational.md, "An except of an equation"). The sweeps are the arrival ones and idempotent, so a twin already made gains nothing, and a handle that is no longer stored, or restates nothing, costs a record fetch. The handles are walked in content order.

The argument-type derivations move the same way (docs/argtypes.md, "An except of an ingredient"): with sweep?, the ones 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. For a handle in whole, whose except itself moved, that is every context and the record's own arrival sweep (revealed-entailments). For one only in scoped, {handle #{[sub super]}}, moved by genlCx edges, it is the contexts under each sub and the edge's own sweep over them (entail-under-context-edge).

except-moved clj

(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!).

forget-kinds clj

(forget-kinds m k)

Refusal record m with handle k named under no kind: its entries left together.

inadmissible clj

(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, as one value.

These hold of any content the engine mints on its own behalf: a (T x) can clash with a disjoint membership, a (genl X T) edge can close a taxonomy cycle or a cycle through negation, and a type used at the wrong arity is not a type membership at all. Three callers ask it — the argument-type entailment below, the computed genlCx edge of a context-valued function (context-nat), and abduction, which asks it before minting a hypothesis so that a sentence no assertion could legally make is never one the search assumes. Forward chaining runs the same four over a rule's conclusion in chain/place-conclusion, the naming arm only where a consequent literal's functor is a variable.

A value, never a throw. Two of its callers run after their triggering sentex is stored (that is what gives them a handle to be justified by), and neither may abort halfway; the third would rather refuse a hypothesis than fail the query that wanted it.

constraint-arm is the definitional-constraint check, checks/constraint-violation by default, which refuses every violation. The argument-type mint passes checks/derivation-violation instead: a mint that clashes with a believed membership is placed, and settle weighs the pair as it weighs a rule's conclusion that clashes (docs/argtypes.md).

A nil constraint-arm omits the arm, for a caller that has already run it against this exact content. The assert path's first-level argument-type mints are the one such caller: checks/entailment-check runs constraint-problem (and cascade-clash, which reads the source's own membership) over every mint of the cascade before the trigger is stored, and refuses the trigger if any mint fails — so a first-level mint reaching the materializer has passed the constraint check already, and storing the trigger and the mints beside it only adds memberships, which cannot turn a passing args/disjoint/arity check into a failing one (each convicts on an absent type, never a present one). Naming, well-formedness and edge stratification are not what entailment-check runs, so they are asked here whether or not the arm is. Every other caller — forward chaining, the retroactive sweeps, and the cascade's own deeper levels, none of which entailment-check pre-validates — leaves it false and pays the full check.

index-exceptWhen-meta clj

(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!).

index-rule-sentex clj

(index-rule-sentex kb handle rule-sentex)

Index a rule handle by all of its predicates — both sets are complete, so reads/as-stored-rules-by-consequent-in answers "what could conclude P?" for a forward-only rule too. A rule whose consequent functor is a variable is filed under the p/var-consequent-key catch-all instead of a canonical ?var0 (see rules/consequent-index-pred); completeness of the consequent read is then the concrete bucket unioned with that catch-all, which resolution/concluding-rule-handles does.

Only the predicates are indexed. The record is the source of truth for what a rule may do: a set/*Rule wrapper canonicalizes into the sentex (see vaelii.impl.sentex), and :engines / :defeasible are read off it by every consumer. Nothing enumerates rules by defeasibility — defaults fire from the same agenda as strict rules — so there is no default-rule index to maintain.

A rule is not a table entry: its trigger is the shape of the sentence (any functor can head an implication), so it is the structural arm of the integrate-sentex walk below, and this is its add half.

integrate-equality-sentex clj

(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).

integrate-sentex clj

(integrate-sentex kb sentex handle)

Reflect a newly stored sentex into the taxonomy / rule index / disjointness — the :integrate column of the table, walked, plus the structural arms above.

Returns {:new [handles] :superseded [[datum reason]] :violations [v]} for an equality sentex — the twins it created are chaining seeds and the violations are the caller's to report — and nil for everything else. (Only the equality arm has anything to say; every other arm mutates a cache and its return value is whatever that mutator handed back, so the result is normalized here rather than left for the caller to sort out.)

integrate-transitive clj

(integrate-transitive kb sentex handle)

The table half of derived-sentex-added: for a functor the table keys, only the arms flagged :derived? — the genl / genlCx closure edges, and the marks that carry the flag for their own reasons — run for a rule-derived conclusion, because the rest of integration either does not apply to a derived sentex or would re-enter assert from inside forward chaining. Without this on the derivation path, a rule concluding (genl a b) stored and believed the sentex while the taxonomy never learned the edge — and recover, which reads the store, then disagreed with the running KB about what the KB entailed. (A derived equality is not reached from here: chain/place-fact-conclusion calls integrate-equality-sentex by name, because this fn discards what an arm returns and there the return value is the work — the twins and the violations.) A functor the table does not key is the structural walk's, not this one's.

integrate-twin clj

(integrate-twin kb sentex handle)

Full integration for a migrated twin — a restated declaration or fact the equality migration derives (migrate-sentex). A twin must reach the same caches an asserted declaration would, or its class-representative spelling is stored and believed while the taxonomy never learns what it declares: a merged (disjoint dog cat) twin (disjoint canine cat) must reach add-disjoint, a (transitive containedBy) twin must reach mark-prop, and a migrated rule twin must reach the rule index or it never fires. So this runs the same arms integrate-sentex does, where derived-sentex-added (the forward-chaining conclusion path) narrows the table half to the :derived? entries and drops the rule arm its own caller posts by name.

The equality arm is skipped: a twin is never an equality sentex (those are held back from migration, kb/rewritable-sentex?), and running migrate-class from inside a migration would recurse. Then the same re-check post every derived sentex gets — a migrated fact / declaration arriving is a trigger like an asserted one.

Migration can run inside a forward-chaining pass (derive-functional-equalities infers an equality from a derived fact), so the table/structural arms can fire mid-fixpoint. That is safe: none of them re-enter assert or chain — they add cache entries, justifications, and re-check queue items — and the common functional merge is of two individual values, whose twins are facts that match no declaration arm at all.

kind-entries clj

(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.

lift-refusals clj

(lift-refusals kb)

The lifts waiting on an argument conviction, as [source-handle entry] pairs in handle order.

lost-descended-derivations clj

(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 fact and the declaration (past-the-pair?), such as a trigger membership, or an equality a restatement rests on.

Two settle arms read it. A genl edge that went IN ⇒ OUT takes the derivation naming it OUT, where a second route to the declaration still licenses it; a defeat deletes nothing, so the justification stays and nothing else draws the derivation again. And a spelling an un-merge gives back is a fact the derivation could not be drawn from while the merge superseded it: an equality over two spellings of one merged pair is found by matching both, so it is drawn only once both are believed again.

Only a justification whose conclusion is OUT, or withdrawn at its own context (exc/believed-own?), qualifies: one that kept another support owes nothing to belief, and asking it again every pass of the settle would re-read a conclusion that cannot move. The dependents are a network read and the record a store fetch, so the filter that drops nearly every handle runs first.

materialize-defn-rules clj

(materialize-defn-rules kb sentence defn-handle context)

Materialize the forward rule(s) 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]} — the new rule handles the caller seeds chaining with (so a rule fires over the facts already stored), and any rule that could not be admitted.

Called from assert-one once the defn* fact has a handle to be justified by. A non-defn* sentence returns the empty result, so the caller pays one defn-sentence? read and stops — the presence check that keeps every ordinary assert free of it.

migrate-handle-metas clj

(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 equalities that migrated the sentex, under rewriteOf.

Public for integrate/commute-existing: a (symmetric P) mark folding two mirrored rows into one carries the dropped row's metas, with the declaration as the single witness.

migrate-meta-onto-twins clj

(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.

migrate-sentex clj

(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.

migrate-under-context-edge clj

(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.

mint-informant? clj

(mint-informant? informant)

Is informant one an argument declaration's mint is justified under?

minted-seeds clj

(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.

mints-on-lengths clj

(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 own arity bindings moved to those bindings' #{[kind value]} (arity/drain!'s :bound). A type's mintability reads its own bindings alone, and only a binding admitting a length other than one moves it, so a type whose moved bindings all bind one is not read, nor is any type no write bound. A declaration arriving while its type was bound to another length minted nothing and recorded nothing (entail-existing), and this is where it mints.

For each mintable type t of bound, in content order:

• each stored entailing declaration naming t with no declaredType justification of (unary_predicate t) (declared-type-justifications) runs its sweep (entail-existing). That justification stands for every declaration whose sweep ran while t was mintable, so a declaration that already minted reads no extent;
• each stored fact naming t where an argArg names its type at the fact's own argument, and each natFormula fact naming t in the expression of a function a resultArg declares, draws what its arrival draws (deduce-placed), deduplicated on content.

Reads, per type of bound, its arity bindings, then for a mintable one the declaration postings naming it and its (unary_predicate t) justifications, and the slot or term postings only when an argArg or resultArg is stored. The predicates an argArg is declared of are read KB-wide (tax/props-over with no context), a superset: each fact found draws through its own context's declarations. An inert declaration sweeps nothing.

move-seeds clj

(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), and fresh the contexts some reader below sub sees through the edge alone (:moved). The facts of fresh are seeded when seen states a rule, the facts of seen when fresh states a rule or a genl edge, the smaller side when only the rest of up states a rule, the facts of up under a genl edge seen states (under-seen-edges), and, when seen states a rule, the facts of up under a genl edge fresh states. A fact is read under an antecedent key fanned by genl or a licensing functor (seeds-in). The unfiltered arity, departed-edge-seeds' re-join, seeds every such fact of up and seen.

With m's :floor (seed-floor), the move is read as of the edge's arrival: a rule, a genl edge or a fact of seen, or a seed, stored at a handle at or above the floor arrived after the edge and was chained or joined with the edge in the taxonomy, so the checks on seen read and the seeds keep only those below it. See docs/contexts.md, "A genlCx edge owes the same debt".

naming-violation clj

(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.

note-departure! clj

(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.

note-except-move! clj

(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!).

note-kind clj

(note-kind m k e)

Refusal record m with handle k named under entry e's kind.

note-unpremised! clj

(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.

offer-marked-existing clj

(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.

offer-marked-under-edge clj

(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.

owed-releases clj

(owed-releases kb)

How many departures and arrivals withheld-releases left owed (*release-withheld?*).

pair-placements clj

(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"). The fact's context when it sees them all, else the maximal common descendants of the ingredients' contexts (tax/maximal-common-descendant-contexts, the placement of a forward firing and of a placed nogood), and empty when no context sees them.

The ingredients beyond the fact and the declaration join them as a firing's do (chain's descent placement): a declaration written of a predicate the fact's functor descends to over genl edges adds one route's supporters (tax/general-reach-supports), for each route no other covers, and a trigger declaration adds one trigger's (trigger-alternatives), for each. The placements are taken over each combination and the most general kept. While an except hides an ingredient somewhere (exc/closure-excepted-anywhere?), each combination is placed past it (res/exception-aware-placements).

pending-supersession-moves clj

(pending-supersession-moves kb)

The datums whose supersession entry changed since the last take-supersession-moves!, read without emptying them.

post-mint! clj

(post-mint! index sentence context h)

File record h, holding sentence in context and concluded by a stored justification 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! clj

(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. reindex's share of the index that its per-record pass cannot post, since the key a declaration installs is the table's to say. kb's own taxonomy is not touched, and the equality relations, whose partition keeps its own supporters, post nothing.

A stored genl / genlCx declaration whose positional read is not a well-formed edge is dropped rather than posted (replay-edge), and the count is warned once — the same discipline rebuild-tms follows for a justification the store cannot root. A well-formed store never has one; a store an older or foreign writer left a non-edge sentex in the genl / genlCx predicate extent does, and posting it would seed a null closure node that crashes restore-depths.

reader-contexts-at clj

(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.

rebuild-pending! clj

(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. The refusal record is in-memory state no store holds, and chain/rerecord-refusals! rebuilds only the rules' half of it. The lift sweep is lift-existing's, which over copies already stored adds nothing and so only re-notes the refused ones.

The marks are read unscoped: the rebuild covers every stored mark, whichever reader sees it.

rebuild-taxonomy clj

(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, reading the network's labels), and the equality partition and rewrite rules, which keep their own supporters, replayed from their stored declarations by the :rebuild column. Reads no other record.

Drops every cache first: a rebuild that merged into the existing one could only ever add, so an entry whose sentex is gone would survive the recovery that was supposed to re-derive it.

recheck-defeat-target clj

(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.

recheck-every-exception clj

(recheck-every-exception kb)

Queue :all every rule carrying a re-check condition. recover takes it.

recheck-except clj

(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, so settle sweeps a conclusion now resting on an invisible antecedent and re-derives one the fact can be seen for again.

• The firings that rest on H through any chain (the justifications of H's consequence closure, jtms/consequence-closure) are queued under a {::except-closure c} marker, so the settle re-decides those firings and not the extent of their rules (recheck/except-candidates).
• The firings the except refused or swept are gone from dependents, so the drain re-joins from the closure and from the antecedents of the justifications resting on it (note-except-move!, drain-except-moves!).
• H itself, when H is a rule, is queued :all: a firing rests on its rule as it rests on its antecedents, and no fact of the closure keys the rule's own sentence.
• H's own target, when H is an except, is re-checked the same way, down the cascade: H's force moved, so what rests on its target moves.

H goes on :except-moves with edge, which also re-runs H's arrival sweep for the restatements the move reaches: an equality or a merge mark H restates facts only where it is visible.

recheck-except-ancestors clj

(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).

recheck-on-lengths clj

(recheck-on-lengths kb moved)

The settle pass moved the length of the relations moved (arity/drain!'s :moved, a set or :all): queue every rule carrying an antecedent a relation's length can move (provers/relation-moved-answers) for a re-check of every firing and a fresh join in this pass (:all-rejoin). A binding, a genl edge and a relabel each move a length with no datum on a functor the prover reads, so no write-time re-join (computed-reading-rules) takes these. Reads nothing while moved is empty, then the term index for a stored quoted form (provers/quoted-anywhere?), then, for a set, the term index for a stored quoted application headed by a member of moved (provers/quoted-head?), and when one is stored, the stored rule keys once.

recheck-on-sentence clj

(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.

recheck-subjects clj

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 clj

(reconcile-belief-change kb)

(reconcile-belief-change kb moved)

Reconcile every belief-derived taxonomy cache after moved may have changed truth.

Bare, like recover and every other recompute: it rebuilds caches from what the KB currently believes and stores nothing of its own, so re-running it is the whole of taking it back.

This is the engine-level choke point above tax/refresh-beliefs: ordinary JTMS defeat/revival/supersession and visibility except both change whether a stored declaration currently has force. moved may name either declaration handles or except handles; the latter are expanded to their targets before the scoped refresh.

The caches read the network (jtms/in?); a scoped read filters a supporter through the read walk (res/supporter-believed?) and is keyed on the change clock, which every write moves, so nothing here retires one.

reconcile-removed-supersession! clj

(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.

record-arg-types clj

(record-arg-types kb)

Record the argument-type entailments every stored fact draws, over a store whose facts were written without them: {:facts n :new [handle …] :violations [v …]}.

assert draws them as each fact arrives. A store loaded around that path — a dump import, *bulk-load?*, bulk-assert-facts! — holds the facts and none of their derived memberships and edges, and recover rebuilds belief from the stored justifications without drawing any. This is the one pass that records them, so the store then holds what a per-fact load of the same facts holds. Run it once, after the load and after the store is recovered or reindexed, since the declarations and the hierarchy they name are read from the taxonomy.

Facts are read per declared functor, every predicate under an entailing declaration in content order, and each fact is asked once whatever number of declarations reach it. Idempotent: a derivation already recorded adds nothing (has-justification?).

rederive-descended clj

(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. The violations are reported and the spellings a merge displaces are refreshed here, as the arrival path does for the same derivations.

Each derivation is asked for through the function its arrival arms ask: the entailment through retroactive-mints, narrowed to the declaration the removed justification named; a descended equality through derive-functional-equalities or derive-antisymmetric-equalities over the fact at the head of its antecedents. So where a second route survives, the derivation comes back resting on it, and where none does, nothing is drawn. A conclusion that kept another justification takes the surviving route's as well, which is the justification the same content loaded without the edge records. A restatement is drawn again by migrate-sentex over the original at the head of its antecedents, or over the target a restated meta names.

An entailment's antecedents lead with the fact and the declaration, in that order (entail-arg-type). An equality's are in content order (derive-equality), so its facts are read off by functor: every antecedent that is neither a genl or genlCx edge nor a mark declaration. Each task is drawn once however many of the removed justifications name it.

redraw-mints clj

(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).

refile-mint! clj

(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!).

refresh-supersessions clj

(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).

release-lift! clj

(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.

release-withheld! clj

(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.

restrength-firings! clj

(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.

resubsumption-seeds clj

(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 firing names one witness for each reachability it rests on: the genl path a subsumed match climbed, and the genlCx path its placement saw each ingredient context over (taxonomy/reach-support, chain/visibility-support). So removing an edge on one of those paths invalidates the justification and the dependency-directed sweep collects the conclusion. A reachability can outlive one of its supporters — the same edge asserted from a second context, or a second path around the one that went — and then the firing is still licensed and must come back, as a re-derivation at a fresh handle (docs/contexts.md, "A genlCx edge owes the same debt").

A departing genl edge seeds its spec subtree (each part's, for a cover), read before the teardown while specs still names the facts that subsumed through it, and the rules with an antecedent on the edge's own relation (closure-reader-rules). Both run only when the sweep has taken something besides the records asked for, not counting an argument-type mint of the edge itself (edge-own-mints). A departing genlCx edge seeds the antecedents of the firings that named it (sighting-seeds), unconditionally, and its closure-reading rules under the same condition. Whether a surviving route still licenses a firing is place-conseq's question, so most of what this seeds places nothing, and that pass files no :no-placement (chain/*report-no-placement?*).

retire-mint! clj

(retire-mint! kb sentex)

Take the departing sentex out of the mint family, when it is filed there.

retire-unjustified-mints! clj

(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.

revived-declaration-sweeps clj

(revived-declaration-sweeps kb handles)

Run, for each sentex in handles the settle just brought back OUT ⇒ 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, and 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, which costs one map read per kind.

The sweeps read what is stored and are idempotent, and the handles are walked in content order. A revived permuting mark re-spells its rows through chain/reconcile-spellings! instead.

signed-all clj

(signed-all tax dir p)

p's global genl closure in direction dir, with every predicate genlInverse edges reach either way round (tax/signed-closure) — what the matching fan meets from p. The plain closure on a KB declaring no genlInverse.

subsumed-mint-blocks clj

(subsumed-mint-blocks kb moved was-in asked believed? routes? whole)

The justifications to block because the records they hold up are redundant, and the records — {:blocked #{jid} :withdrawn #{handle}} over the records the sentexes in moved can have displaced.

Every justification of a withdrawn record, because a record survives on any one of them: two facts can entail the same type, and blocking one would leave the record standing on the other, so how many facts happened to entail it would decide whether it stayed.

moved is a delay over the region's records, and the checks in front of it decide whether it is ever forced: off unless the entailment is on, off unless the mint is prunable, and off while the mint family is empty. A KB holding no mint therefore fetches no record here however much it asserts, which is what record_fetch_cost_test counts. Forced, the region is filtered by shape (subsumer-shaped?) and the candidates are the mint family's (withdrawal-candidates per record, edge-route-candidates once for all the genl edges the records install), so a membership about a term holding no mint reads nothing.

Only a record that became believed is asked, which is what keeps this off the price of a settle that relabels a large region without moving much of it — a qualitative network relabels its whole network per fact and moves a handful of nodes.

The records a retraction left standing on a derivation alone (note-unpremised!) are asked too, each the whole question.

A genlCx edge among the moved records is also asked which mint placements it displaced (surplus-placements), with pruning on or off; those justifications are returned under :surplus, for the settle to drop.

asked is the settle's own record of which of them it has already put this question to, and a record is asked once per settle however many passes relabel it. Nothing is missed by that: a mint stored after a pass examined its subsumer never reaches the store, since entail-arg-type asks the same question of every mint it is about to write. believed? is belief now, jtms/in? or own-context belief. With routes?, a genl edge or a trigger membership among them is asked the same of the placements it displaced (descent-surplus-placements).

whole is the region's size when the region is the whole store (a recover), else nil. With fewer mints stored than that, moved is never forced: each stored mint is asked the whole question, and the genlCx edges are read off the index.

subsumption-seeds clj

(subsumption-seeds kb sentence)

The stored facts the genl edges sentence installs newly make matchable, as chaining seeds — the taxonomy twin of lift-existing, and there for exactly the same reason. The edges are tax/installed-edges': a (genl sub super) edge, or one per part of a cover, whose edges subsume exactly as a stated one does.

Matching fans an antecedent's functor over its genl spec closure, so an edge arriving after the facts changes which antecedents they satisfy: (dog Muffet) stored, then (genl dog animal), and a rule on (animal ?x) should fire. The semi-naive agenda never sees it — the arriving datum is the edge, and firing the rules keyed on genl is not the same thing as re-firing the rules the edge just connected. Without this the same three sentences derive a conclusion in one order and not the other, which is the one thing belief may not depend on (docs/nmtms.md).

The seeds are sub's whole spec subtree, because subsumption is transitive: an edge at the top of a hierarchy makes every fact below it matchable at the new supertype. Believed only — a disbelieved fact matches nothing, and it will seed the agenda itself when it revives. This runs per edge only when rule-reads-above? holds: a fact below the edge newly reaches the terms at or above super and no other, so where no rule reads one the subtree is not read. Every functor of the subtree reaches the same terms, so the check decides for all of its facts at once. Sound on a departing edge for negative-subsumption-seeds' reason: a firing that climbed it read a term at or above super.

A negated antecedent is answered contravariantly, so the facts an edge newly offers it sit on the other side of the edge entirely: negative-subsumption-seeds above reads them up super's genl closure.

The removal side is resubsumption-seeds below: a firing names the genl edges it subsumed through, so dropping one withdraws what it licensed — and the facts have to go back on the agenda when the reachability outlives the supporter that left.

surplus-placements clj

(surplus-placements kb edges)

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). An edge arriving can give the two a more general common descendant, and the placement under it then goes, so the store holds the same mints in every arrival order. Every placement an edge can displace lies under its sub, and the mints stated there are read off the mint family (withdrawal-candidates). A justification at its fact's own context is not asked: that context sees the declaration while the genlCx edges the justification names hold. The caller checks the two preconditions: the entailment on and the mint family holding a record.

table clj

entries as the lookup map the walks below dispatch through.

take-except-moves! clj

(take-except-moves! kb)

Empty :except-moves and return what the settle's supersession reconcile owes it: {:extra [[datum reason]] :region #{datum} :full? bool} — the supersessions except-move-sweeps found, the superseded data an except that moved can change (except-move-region), and whether a move is still pending undrained, which leaves the reconcile nothing narrower than a full pass. nil when nothing moved.

take-first-deferral! clj

(take-first-deferral! kb)

Whether defer-first-release! marked this settle, with the mark cleared.

take-supersession-moves! clj

(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.

taxonomy-generations clj

(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.

transitive-rule-seeds clj

(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' three ingredients, and there for the reason the other two are.

A rule seeded on its own handle is joined over the stored facts, and that join reaches the closure only from whichever side it leads: led from the transitive antecedent it enumerates the STORED links and nothing else, since the closure is answered rather than stored and an open goal on it yields no record to lead from. So a rule arriving after its facts derives the direct pairs and stops, where the same rule arriving before them derives the closure — the same sentences, two answer sets, decided by which came last.

Seeding the partner facts fixes it the way it fixes the other two arms: each becomes a trigger, and a trigger binds the shared variable before the transitive antecedent is asked, which is the direction that reaches the closure.

Off unless an antecedent is actually declared transitive, so an ordinary rule assert pays one property lookup per antecedent and reads nothing.

The mark is read unscoped, for transitive-seeds' reason.

transitive-seeds clj

(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 above, and there for exactly the same reason.

A declared-transitive predicate's closure is answered, never stored. (causes E0 E2) is provable the moment both links are in and is never a record — so it is never a datum, never on the agenda, and never a trigger. A rule joined to that predicate, [(does ?a ?act) (causes ?act ?e)], can reach a closure pair only from its OTHER antecedent's trigger; and when the closure grows, nothing puts that trigger back. Assert the does before the second link and the firing has already run against a shorter closure; assert it after and the join reaches the whole of it. Same four sentences, two answer sets, which is the one thing belief may not depend on (docs/nmtms.md). subsumption-seeds states the principle for the taxonomy: firing the rules keyed on the arriving predicate is not the same thing as re-firing the rules the arrival just connected. This is that, one closure over.

Two arrival orders, because the closure has two ingredients — the links and the declaration — and either can come last. deduce-arg-types / entail-existing / entail-under-edge are the same three-cornered shape for an argument type:

• a link (pred a b), with pred already transitive: the reach that grew is a's and that of everything behind it (transitive-left-ends), so the seeds are the believed facts mentioning one of those.
• the declaration (transitive pred), over links already stored: every pair of the closure appears at once, so every believed fact on a partner functor goes back. This is the arm a (transitive …) asserted after its links needs, and without it a KB that declares its properties at the end of a file answers differently from one that declares them at the start.

The seeds are the partner triggers, not the links. Re-seeding the pred facts themselves buys nothing: their own trigger position joins the other antecedent at the term the link already names, which is the pair the run made anyway.

The presence checks keep an ordinary assert free. Both arms are off unless some rule takes a pred antecedent — with no such rule there is no join to re-drive — and the link arm reads the inverted index's posting per left end rather than any functor extent, so a KB whose transitive facts feed no rule pays two lookups and reads nothing.

The removal side needs no twin: a retracted link withdraws the closure pairs that rested on it through the justifications the firings recorded, which is the TMS's ordinary business and not a reachability question.

The mark is read unscoped: a seed over-approximates, and each seeded fact is joined from the rule's own context.

triggered-mints clj

(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.

unindex-exceptWhen-meta clj

(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!).

universal-context clj

unpost-mint! clj

(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.

visibility-seeds clj

(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.

wff-problems clj

(wff-problems tax sentence context)

Structural well-formedness problems for sentence (empty if OK) — the :wff column of the table, walked. A sentence whose functor has no entry (or no :wff arm) is structurally unconstrained here; its argument types are still checked by the arg constraints.

context is the asserting (or, on the derivation path, the landing) context, passed to every arm. Every arm is a context-free structural check and ignores it. A nil tax skips the checks that read stored content: the genl, genlCx, cover and rewriteOf cycles and the transitivity a preservation names. An import reads it so, since the content a check reads can arrive in a later frame.

A not over a pr/query-only term, at any depth of nots, is checked by that term's arm, so (not (unknown S)) is refused as (unknown S) is: the negation of a query is a query too.

wff-violation clj

(wff-violation kb sentence context)

The same check as a value, for content a rule derived rather than one a caller asserted: nil when sentence is well-formed, else a violation map in the shape checks/constraint-violation returns.

assert checks this on the way in, but a rule may conclude a special predicate — (implies (relates ?x ?y) (genl ?x ?y)) derives taxonomy edges — and the derivation path had no such check. A derived edge reaches the closure through integrate-transitive, so a rule could close a genl cycle that the same edge asserted directly would have been refused for, leaving genls/specs cyclic — and those are what matching, placement and stratification all read.

Dropped and reported rather than thrown, like every check on that path: chaining is a fixpoint and must not abort halfway through one.

with-recheck-reads clj macro

(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.

withdrawn-edge-seeds clj

(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 for each of its twins (handle-twins). The closure holds a retired edge's twin in place of the edge, so the re-join over the twin draws the firing the merge-first order makes.

The firing is what is owed, not the conclusion. A genl mint is withdrawn because a stated route now reaches as far as it did, so every firing that climbed it has a surviving route, and the same content loaded with the stated route first stores that firing over it. Its conclusion keeping another firing says nothing about this one, so the condition is a dependent justification whose informant is a rule, read before the sweep deletes it, and not a dependent conclusion that went OUT. Without the re-join the store keeps whichever firings the arrival order happened to draw, and a later full join — a re-join, forward-chain — draws the rest at fresh handles.

withdrawn-type-entailments clj

(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.

withdrawn-type-mints clj

(withdrawn-type-mints kb bound)

The mint justifications to drop for each type t of bound (arity/drain!'s :bound) whose moved bindings admit another length and whose length no longer admits one (arity/mintable-type?): those concluding a membership (t x) or an edge (genl x t). A declaration meeting its fact while t is bound to another length mints nothing, so the store then holds what the order with the binding first holds; 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, so a binary predicate's extent is not read. Every context, since t's length holds at every context (arity/relation-length).

withheld-releases clj

(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 are kept owed (owe-releases!) and nothing is drawn.

The departures are the records note-departure! queued as they left the store, and the records in moved (a delay over the settle's region) that went IN ⇒ OUT against was-in; the arrivals are the ones that came IN. believed? is belief now. withdrawn holds the mints this settle withdrew, which release nothing. asked holds what this settle has already asked, so each record is asked once per settle however many passes relabel it. The queue is drained whether or not the checks pass.

A departure is read again when its term's turn comes, and a term whose departures are all stored as they were and believed again is not re-drawn: re-drawing the terms before it adds justifications, and the relabel that follows can bring a departure back IN, so that what it subsumed is withheld still. A term is re-drawn only for the mints one of its departures out could have withheld (may-release): a membership leaving releases the memberships of its type and the types above it, and no other mint about its term.