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.
(commute-existing kb sentence witness)When a declaration that re-spells arrives — symmetric, or either commutativity
relation — bring the named predicate'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 that moves a spelling.
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 retracting the mark does not undo it by itself:
what makes the mark leaving answerable is the record each moved row keeps of the
spellings it was written in (spellings-key), which chain/reconcile-spellings! reads
to split the rows back apart.
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 declaration that *re-spells* arrives — `symmetric`, or either commutativity
relation — bring the named predicate'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 that moves a spelling.
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 retracting the mark does not undo it by itself:
what makes the mark leaving answerable is the record each moved row keeps of the
spellings it was written in (`spellings-key`), which `chain/reconcile-spellings!` reads
to split the rows back apart.
**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.(commute-predicate kb pred witness)Bring pred's stored rows into the spelling its marks now give them, folding mirrored
pairs — commute-existing's walk, for a caller that knows the predicate rather than
the declaration: a mark revived by a relabel, which no declaration arrives to announce
(chain/reconcile-spellings!). witness is the mark handle a folded row's metas are
carried on. {:new [handles]}, or nil when pred has no stored rows.
Bring `pred`'s stored rows into the spelling its marks now give them, folding mirrored
pairs — `commute-existing`'s walk, for a caller that knows the predicate rather than
the declaration: a mark revived by a relabel, which no declaration arrives to announce
(`chain/reconcile-spellings!`). `witness` is the mark handle a folded row's metas are
carried on. `{:new [handles]}`, or nil when `pred` has no stored rows.(fold-row-home! kb planner sx witness)symmetrize-row! for one row a caller walks itself (chain/respell-rows!).
`symmetrize-row!` for one row a caller walks itself (`chain/respell-rows!`).
(mark-witness kb pred)A believed statement of a permuting mark on pred (witness-among), for
commute-predicate.
A believed statement of a permuting mark on `pred` (`witness-among`), for `commute-predicate`.
(move-row! kb sx want witness rewrite)Bring one stored row sx to the spelling want, and return the handle it ends up at,
or nil when it is spelled want already. symmetrize-row! below states the shape and
the choice of survivor. witness is the mark handle a folded row's metas are carried
on, or nil. rewrite re-spells the row's written spellings (rewritten), nil to keep
them as written.
Bring one stored row `sx` to the spelling `want`, and return the handle it ends up at, or nil when it is spelled `want` already. `symmetrize-row!` below states the shape and the choice of survivor. `witness` is the mark handle a folded row's metas are carried on, or nil. `rewrite` re-spells the row's written spellings (`rewritten`), nil to keep them as written.
(normalized-spellings stored {:keys [premise derived]})rec for a row stored as stored, without what the row's own spelling already says:
a premise map whose one assertion is stored, and every firing written as stored.
`rec` for a row stored as `stored`, without what the row's own spelling already says: a premise map whose one assertion is `stored`, and every firing written as `stored`.
(note-derived-spelling! kb h jid written)Record that justification jid, a rule firing, concluded written onto row h.
Record that justification `jid`, a rule firing, concluded `written` onto row `h`.
(note-premise-spelling! kb h stored written strength prior)Record that written was asserted at strength onto row h, stored as stored.
prior is h's premise class before this assertion, nil when it was none — the
record's premise map is then stale and starts again. Writes nothing while every
premise assertion is spelled as the row is.
Record that `written` was asserted at `strength` onto row `h`, stored as `stored`. `prior` is `h`'s premise class before this assertion, nil when it was none — the record's premise map is then stale and starts again. Writes nothing while every premise assertion is spelled as the row is.
(permuting? kb pred)Does a stored mark permute pred's arguments — symmetric, or a commuting group?
Does a stored mark permute `pred`'s arguments — `symmetric`, or a commuting group?
(premise-spellings kb h stored){written strength} for row h's premise assertions: the record's, or stored at
h's premise class when the record lists none, or {} when h is no premise.
`{written strength}` for row `h`'s premise assertions: the record's, or `stored` at
`h`'s premise class when the record lists none, or `{}` when `h` is no premise.(put-spellings! kb h rec)Record rec as row h's written spellings, dropping empty parts; an empty record
removes the entry (and the provenance map with it, when nothing else is in it).
Record `rec` as row `h`'s written spellings, dropping empty parts; an empty record removes the entry (and the provenance map with it, when nothing else is in it).
(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 read by the reified-NAT sweep, the meta cascade, and a settle reading the
defeats it removed (settle/defeat-moves), and it 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. The caller passes the gate its readers consult
(nat/any-reifiable-functions?, a stored defeat), so a KB with none of them pays 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 read by the reified-NAT sweep, the meta cascade, and a settle reading the defeats it removed (`settle/defeat-moves`), and it 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. The caller passes the gate its readers consult (`nat/any-reifiable-functions?`, a stored `defeat`), so a KB with none of them pays 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.
(spelled pred ctx entries f)Call f with res/*spelled-by* naming pred in ctx with entries, or plainly when
entries is nil, so the store spells pred's literals in ctx by those marks. f's
value is realized inside the binding.
Call `f` with `res/*spelled-by*` naming `pred` in `ctx` with `entries`, or plainly when `entries` is nil, so the store spells `pred`'s literals in `ctx` by those marks. `f`'s value is realized inside the binding.
(spelling-plan kb planner w ctx)[home entries respelled] for a piece of a fact written w in ctx, read through
planner (res/spelling-planner): home, the spelling the piece is stored at, with
entries, the marks that spell it (nil: the store's own marks); and respelled,
{spelling entries} for every other spelling a reader of the fact reads, each stored
justified respell by the home row (chain/respell-rows!). One spelling read: the
piece sits at it. Several: the piece sits at w as written.
`[home entries respelled]` for a piece of a fact written `w` in `ctx`, read through
`planner` (`res/spelling-planner`): `home`, the spelling the piece is stored at, with
`entries`, the marks that spell it (nil: the store's own marks); and `respelled`,
`{spelling entries}` for every other spelling a reader of the fact reads, each stored
justified `respell` by the home row (`chain/respell-rows!`). One spelling read: the
piece sits at it. Several: the piece sits at `w` as written.(spellings kb h)Row h's written-spelling record — {:premise {written strength} :derived {jid written}} — or nil when every piece of it is spelled as the row is.
Row `h`'s written-spelling record — `{:premise {written strength} :derived {jid
written}}` — or nil when every piece of it is spelled as the row is.The provenance key a row's written spellings are recorded under.
The provenance key a row's written spellings are recorded under.
(take-out! kb h)Take stored row h out: drop its premise mark, retract it from the network, and
remove from the store what the retraction swept, then the row itself when it is still
stored (an inert sentex is no network datum). core/retract!'s storage half, for a
caller inside a write or a settle that runs its own follow-through.
Take stored row `h` out: drop its premise mark, retract it from the network, and remove from the store what the retraction swept, then the row itself when it is still stored (an inert sentex is no network datum). `core/retract!`'s storage half, for a caller inside a write or a settle that runs its own follow-through.
(witness-among kb supporters)The believed handle among supporters chosen by content — the handle a fold carries a
folded row's metas on when no declaration arrived to be it. Nil when none is believed.
The believed handle among `supporters` chosen by content — the handle a fold carries a folded row's metas on when no declaration arrived to be it. Nil when none is believed.
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 |