Store mutation is the boundary: the two choke points everything that stores or removes a sentex must pass through.
Fourth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): the table of what each special predicate means lives below in
vaelii.impl.special; what lives here is the guarantee that its arms — and the
exception re-check queue they feed — are never skipped. exceptWhen correctness
depends on every mutation path posting a re-check. Scattering that call across the
mutation sites makes a missed one invisible — the failure mode is stale excepted
conclusions, silently, and the next mutation path (a bulk load, a new merge) is one
forgotten call from that bug. So the sequence is stated once per direction:
sentex-added integrate through the table + queue the re-check — the assert
path's reflection of a sentex that just landed (storage and
indexing having happened in kb/create-sentex, which is the
store-side half of the same boundary)
sentex-removed! disintegrate + unindex + delete the record + queue the
re-check — the one teardown, shared by retract! and the
excepted-conclusion sweep
symmetrize- the third direction, and the only one that moves a record
existing without moving a handle: a late (symmetric P) mark re-spelling
the rows stored before it and folding a mirrored pair into one
(see the section at the foot of this namespace)
The derivation path's twin (special/derived-sentex-added) sits beside the table
instead, because the equality arms are themselves derivation sites and must reach
it from below. The triggers that are not store mutations stay explicit at
their own sites: a taxonomy edge change (posted inside the genl / genlCx
arms — the trigger is the closure moving, not the sentex), rule indexing (posted
in special/index-rule-sentex — the trigger is the rule gaining an exception to
evaluate), and recover (nothing about blocking survives a restart, so it
re-queues everything wholesale).
Store mutation is the boundary: the two choke points everything that stores or
removes a sentex must pass through.
Fourth layer of the engine stack (kb <- checks <- special <- integrate <- chain
<- settle): the table of what each special predicate *means* lives below in
`vaelii.impl.special`; what lives here is the guarantee that its arms — and the
exception re-check queue they feed — are never skipped. exceptWhen correctness
depends on every mutation path posting a re-check. Scattering that call across the
mutation sites makes a missed one invisible — the failure mode is stale excepted
conclusions, silently, and the next mutation path (a bulk load, a new merge) is one
forgotten call from that bug. So the sequence is stated once per direction:
sentex-added integrate through the table + queue the re-check — the assert
path's reflection of a sentex that just landed (storage and
indexing having happened in `kb/create-sentex`, which is the
store-side half of the same boundary)
sentex-removed! disintegrate + unindex + delete the record + queue the
re-check — the one teardown, shared by `retract!` and the
excepted-conclusion sweep
symmetrize- the third direction, and the only one that moves a record
existing without moving a handle: a late `(symmetric P)` mark re-spelling
the rows stored before it and folding a mirrored pair into one
(see the section at the foot of this namespace)
The derivation path's twin (`special/derived-sentex-added`) sits beside the table
instead, because the equality arms are themselves derivation sites and must reach
it from below. The triggers that are *not* store mutations stay explicit at
their own sites: a taxonomy edge change (posted inside the genl / genlCx
arms — the trigger is the closure moving, not the sentex), rule indexing (posted
in `special/index-rule-sentex` — the trigger is the rule gaining an exception to
evaluate), and `recover` (nothing about blocking survives a restart, so it
re-queues everything wholesale).A volatile holding a vector of the sentexes that have left the store, or nil — the default, and the removal choke point records nothing.
What a caller needs when it must act on the region a teardown touched rather than
on the whole KB. core's reified-NAT orphan sweep is the one that does: an orphaned
constant is one some departing sentex stopped referencing, so the constants those
sentexes named are the whole of what it has to ask about. The removals are not all in
one place — the dependency-directed sweep produces some, the settle that follows
produces more (settle/sweep-excepted!), and the sweep's own retractions produce more
again — so recording them where every removal already passes is what makes the
narrowed question equal to the whole-KB one.
A volatile rather than an atom: the engine is single-writer, and this sits on the teardown path.
A volatile holding a vector of the sentexes that have left the store, or nil — the default, and the removal choke point records nothing. What a caller needs when it must act on **the region a teardown touched** rather than on the whole KB. `core`'s reified-NAT orphan sweep is the one that does: an orphaned constant is one some departing sentex stopped referencing, so the constants those sentexes named are the whole of what it has to ask about. The removals are not all in one place — the dependency-directed sweep produces some, the settle that follows produces more (`settle/sweep-excepted!`), and the sweep's own retractions produce more again — so recording them where every removal already passes is what makes the narrowed question equal to the whole-KB one. A volatile rather than an atom: the engine is single-writer, and this sits on the teardown path.
(removal-sink)(removal-sink want?)The sink to record a teardown's removals into: the bound one when there is one, a fresh volatile otherwise. Reused rather than shadowed, so a nested teardown appends to the record its caller is still reading — which is what lets the orphan sweep see what its own retractions removed, and so find a cascade.
want? false answers nil, and a nil sink is the one that records nothing. The
record is the reified-NAT sweep's and only that sweep's, so a KB declaring no
reifiable function has nothing to do with it — and the record is not free: it retains
every sentex a teardown removes for as long as the teardown runs, which on a cascade
is the whole cascade held in a vector nobody reads. The caller passes the gate it was
going to consult anyway (nat/any-reifiable-functions?), so the KBs that never reify
pay the retention of nothing at all.
The sink to record a teardown's removals into: the bound one when there is one, a fresh volatile otherwise. **Reused rather than shadowed**, so a nested teardown appends to the record its caller is still reading — which is what lets the orphan sweep see what its own retractions removed, and so find a cascade. `want?` false answers **nil**, and a nil sink is the one that records nothing. The record is the reified-NAT sweep's and only that sweep's, so a KB declaring no reifiable function has nothing to do with it — and the record is not free: it retains every sentex a teardown removes for as long as the teardown runs, which on a cascade is the whole cascade held in a vector nobody reads. The caller passes the gate it was going to consult anyway (`nat/any-reifiable-functions?`), so the KBs that never reify pay the retention of nothing at all.
(sentex-added kb sentex handle)Everything that must happen because a sentex just landed in the store as a
premise: reflect it into the caches through the special-predicate table, and
queue the exception re-check its arrival may have flipped. Returns what the
table walk returns — the {:new :superseded :violations} migration map for an
equality sentex, nil otherwise.
Runs whether or not the sentex is newly created: re-asserting an existing sentence re-adds premise support, which can flip belief, so the re-check must be posted either way (the cache adds are refcounted and idempotent).
Everything that must happen because a sentex just landed in the store as a
premise: reflect it into the caches through the special-predicate table, and
queue the exception re-check its arrival may have flipped. Returns what the
table walk returns — the `{:new :superseded :violations}` migration map for an
equality sentex, nil otherwise.
Runs whether or not the sentex is newly created: re-asserting an existing
sentence re-adds premise support, which can flip belief, so the re-check must be
posted either way (the cache adds are refcounted and idempotent).(sentex-removed! kb sentex)Everything that must happen because a sentex is leaving the store: reverse its cache effects through the table, drop it from every index, delete the record, and queue the exception re-check — a fact leaving is as much a re-check trigger as one arriving, since its departure may be exactly what releases some rule's exception.
Records the sentex into *removed-sink* when one is bound, which is how a caller
learns the region a teardown removed without every removal path having to report it.
Everything that must happen because a sentex is leaving the store: reverse its cache effects through the table, drop it from every index, delete the record, and queue the exception re-check — a fact *leaving* is as much a re-check trigger as one arriving, since its departure may be exactly what releases some rule's exception. Records the sentex into `*removed-sink*` when one is bound, which is how a caller learns the region a teardown removed without every removal path having to report it.
(symmetrize-existing kb sentence witness)When a (symmetric P) declaration arrives, bring P's already stored facts into
the argument order the declaration puts every later one in. {:new [handles]} — the
rows whose spelling moved, which are new content to every rule that reads the canonical
one — or nil when sentence declares nothing symmetric.
A declaration has to reach the facts already stored exactly as it reaches the facts that
follow, which is equate-existing's rule and holds here for a blunter reason: the entry point
sorts a symmetric literal's arguments, so a declaration arriving second leaves the KB
holding (P b a) where a KB told the same things in the other order holds (P a b) —
and if both spellings were written, two rows for one proposition, each retractable
without the other (vaelii#61). Written the ordinary way — declaration first, then the
facts — this finds an empty extent and costs one index cardinality read.
Shape: the storage migrates, rather than an alias recording that two rows mean one.
Both answer the issue; they differ in what a restart sees. An alias is derived state,
so it has to be rebuilt on every recover from records that still spell the fact two
ways, and every reader — matching, retraction, the TMS, the handle entry points — has to
consult it for ever after. Migrating instead leaves the records themselves canonical,
so recover reads a store that needs no reconciling and no reader learns a new rule.
The price is that it is a write and therefore not undone by retracting the mark: the
declaration going away leaves P's facts spelled the way the declaration had them
spelled, which is a spelling and not a belief, and sort-symmetric-args never claimed
the two orders were different propositions to begin with.
The extent is P's own stored rows, not its spec subtree. res/kb-sentex reads
the mark off the literal's exact functor — a genl edge below a symmetric predicate
does not make the sub-predicate symmetric, and constraint_descension_test holds that
line — so a row this arm re-spelled at a sub-predicate would be one the entry point stores the
other way round on the very next assertion.
Stored, never believed. A mirrored pair whose rows are currently defeated merges
exactly as a believed one does, for equate-existing's reason: a spelling is not a
claim, and reading belief here would leave the migration missing when the defeat lifts
— belief depending on the order the defeat and the declaration arrived in.
On a KB with a large extent under the newly marked predicate this costs one posting-list
read plus a record fetch and a canonicalization per row, and a store probe per row that
is out of order. That is the same shape equate-existing pays and the same bound: it
is a declaration reaching the facts, so it is linear in the facts it reaches, and a
predicate marked before it has any is free.
When a `(symmetric P)` declaration arrives, bring `P`'s **already stored** facts into
the argument order the declaration puts every later one in. `{:new [handles]}` — the
rows whose spelling moved, which are new content to every rule that reads the canonical
one — or nil when `sentence` declares nothing symmetric.
A declaration has to reach the facts already stored exactly as it reaches the facts that
follow, which is `equate-existing`'s rule and holds here for a blunter reason: the entry point
*sorts* a symmetric literal's arguments, so a declaration arriving second leaves the KB
holding `(P b a)` where a KB told the same things in the other order holds `(P a b)` —
and if both spellings were written, two rows for one proposition, each retractable
without the other (vaelii#61). Written the ordinary way — declaration first, then the
facts — this finds an empty extent and costs one index cardinality read.
**Shape: the storage migrates, rather than an alias recording that two rows mean one.**
Both answer the issue; they differ in what a *restart* sees. An alias is derived state,
so it has to be rebuilt on every `recover` from records that still spell the fact two
ways, and every reader — matching, retraction, the TMS, the handle entry points — has to
consult it for ever after. Migrating instead leaves the records themselves canonical,
so `recover` reads a store that needs no reconciling and no reader learns a new rule.
The price is that it is a write and therefore not undone by retracting the mark: the
declaration going away leaves `P`'s facts spelled the way the declaration had them
spelled, which is a spelling and not a belief, and `sort-symmetric-args` never claimed
the two orders were different propositions to begin with.
**The extent is `P`'s own stored rows, not its spec subtree.** `res/kb-sentex` reads
the mark off the literal's exact functor — a `genl` edge below a symmetric predicate
does not make the sub-predicate symmetric, and `constraint_descension_test` holds that
line — so a row this arm re-spelled at a sub-predicate would be one the entry point stores the
other way round on the very next assertion.
**Stored, never believed.** A mirrored pair whose rows are currently defeated merges
exactly as a believed one does, for `equate-existing`'s reason: a spelling is not a
claim, and reading belief here would leave the migration missing when the defeat lifts
— belief depending on the order the defeat and the declaration arrived in.
On a KB with a large extent under the newly marked predicate this costs one posting-list
read plus a record fetch and a canonicalization per row, and a store probe per row that
is out of order. That is the same shape `equate-existing` pays and the same bound: it
is a declaration reaching the facts, so it is linear in the facts it reaches, and a
predicate marked before it has any is free.cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |