vaelii.impl.nat-maintenance — com.vaelii/vaelii 0.24.0

The reified-NAT maintenance the write paths run once their own work is done — docs/nat.md, docs/context-nat.md.

Three entry points, one per site in vaelii.core:

• reconcile-assert, after a sentence is stored: the collision merge an equality may have caused, the correspondence reconciliation, the structural genlCx edges the new fact entails, and the merges those edges license.
• reconcile-revivals!, after a teardown has settled: the edges the producer could not build while their declaration was OUT, and the merges they license.
• collect-orphans!, on the same teardown: the reified constants no live use references any more, removed to a fixpoint.

Sits above both vaelii.impl.nat and vaelii.impl.context-nat, because the assert-path sequencing spans the two, and above vaelii.impl.settle, because a computed genlCx edge owes a chain and a settle of its own.

The teardown entry point is an argument, not a require: the orphan sweep retracts through vaelii.core/retract!, and the engine never requires the API namespace (docs/namespaces.md, "The layering"). vaelii.core hands its own retract! in.

collect-orphans! clj

(collect-orphans! kb retract!)

(collect-orphans! kb sink retract!)

Sweep a reified NAT orphaned by a teardown — its termOfUnit map and materialized types would dangle a raw nat/ symbol (docs/nat.md), and an emptied cx/ context would be a place nothing can reach and nothing is in (docs/context-nat.md). Gated on the KB declaring a reifiable function at all — context_denoting_function is one — and suppressed while already removing orphans. retract! is the teardown entry point the sweep takes each bookkeeping handle out with.

Two arms, and which one a caller takes turns on whether it can name the region the teardown touched:

• retract! and edit! pass their removal record — every sentex that left the store while they ran, collected at the removal choke point (integrate/*removed-sink*), the settle's own sweep included. A constant no removal named is not a candidate, at the cost of the region instead of the cost of the KB's whole NAT population; remove-orphaned-nats! says why a merely defeated use is not a use that went, and why collecting on one would be the dangling symbol rather than the fix for it.
• rollback-batch! for a batch passes nothing and asks the whole KB. It is putting a KB back rather than taking something out of one, so the claim it owes — the KB is as it was found — is about all of it rather than about one teardown's region; and a preview's batch reached this sweep at no point, having run with the settle sweep off (settle/*sweep?*). A rollback runs once per batch, and only for a preview or a batch that refused, so the whole-KB cost is one it can carry. The rollback of a single refused assert passes its removal record, since its settles ran with the sweep on.

The two arms therefore ask different questions, not one question at two costs. The region arm asks what a teardown's removals orphaned; the whole-KB arm asks which constants are orphaned now, which is the stronger reading and the one a restore owes.

reconcile-assert clj

(reconcile-assert kb sentence opts)

The reified-NAT maintenance a just-stored sentence calls for, run after the sentence is in and its own chaining has settled. opts is the assert's, carried through to the chain a computed genlCx edge's merges run.

Two questions in order, behind one gate:

• nat/reconcile-nats! — the collision merge a rename may have caused, and the correspondence a value, an application or a declaration arriving last leaves to settle (docs/nat.md).
• context-nat/reconcile-genlCx — the structural genlCx edges a context's mint, a contextArgSubrelation declaration or an R-evidence fact entails; materialized justified so they belief-follow (docs/context-nat.md). A computed edge widens which merges a context can see exactly as a stated one does, so apply-computed-edge-merges gives it the same follow-through — nil, and one test, whenever it merged nothing (vaelii#56).

The gate covers all of it. A context_denoting_function is a reify-kind, so any KB with a context NAT to order already passes nat/any-reifiable-functions? — a free in-memory read — and one that declares no reifiable function has no cx/ context and nothing to reconcile. So a KB that reifies nothing pays neither the any-context-subrelations? index read nor the correspondence count (assert_cost_test).

reconcile-revivals! clj

(reconcile-revivals! kb)

Rebuild the structural genlCx edges a teardown revived the premises of, and apply the merges they license.

A teardown can put a contextArgSubrelation declaration or a stored R-evidence fact back IN by retracting a monotonic defeater above it, and the producer runs on the assert path only — so an edge never built while the declaration was OUT would stay absent with nothing for the JTMS to revive. context-nat/reconcile-revivals rebuilds it against the settled belief, and an edge built here widens an ancestor set the moment it is built, whichever entry point built it — so it takes the same follow-through the assert path gives a computed edge.

Gated internally on the KB declaring a context function.