Store mutation is the boundary: the choke points everything that stores or removes a
sentex passes through, so exceptWhen's re-check queue is never skipped. The table of what
each special predicate means is in vaelii.impl.special.
sentex-added integrate through the table and queue the re-check: the assert
path's reflection of a sentex that just landed
sentex-removed! disintegrate, unindex, delete the record and queue the re-check: the
one teardown, shared by retract! and the excepted-conclusion sweep
symmetrize- re-spell the rows stored before a late (symmetric P) mark, folding
existing a mirrored pair into one; moves a record without moving a handle
special/derived-sentex-added is the derivation path's twin. Triggers that are not store
mutations (a taxonomy edge change, rule indexing, recover) post their re-checks at their
own sites. See docs/exceptions.md and docs/canonicalization.md.
Store mutation is the boundary: the choke points everything that stores or removes a
sentex passes through, so exceptWhen's re-check queue is never skipped. The table of what
each special predicate means is in `vaelii.impl.special`.
sentex-added integrate through the table and queue the re-check: the assert
path's reflection of a sentex that just landed
sentex-removed! disintegrate, unindex, delete the record and queue the re-check: the
one teardown, shared by `retract!` and the excepted-conclusion sweep
symmetrize- re-spell the rows stored before a late `(symmetric P)` mark, folding
existing a mirrored pair into one; moves a record without moving a handle
`special/derived-sentex-added` is the derivation path's twin. Triggers that are not store
mutations (a taxonomy edge change, rule indexing, `recover`) post their re-checks at their
own sites. See docs/exceptions.md and docs/canonicalization.md.A volatile holding a vector of the sentexes that have left the store, or nil (the default:
the removal choke point records nothing). Callers that act on the region a teardown
touched read it, such as core's reified-NAT orphan sweep. Every removal passes the
choke point, so the narrowed question equals the whole-KB one (docs/nat.md). A volatile
because the engine is single-writer.
A volatile holding a vector of the sentexes that have left the store, or nil (the default: the removal choke point records nothing). Callers that act on the region a teardown touched read it, such as `core`'s reified-NAT orphan sweep. Every removal passes the choke point, so the narrowed question equals the whole-KB one (docs/nat.md). A volatile because the engine is single-writer.
(apply-removals! kb {:keys [removed-sentexes removed-justifications] :as r})Delete from the stores what a network removal r swept (swept-records), and tear
each deleted record down through sentex-removed!: r is a jtms/retract!,
jtms/sweep! or jtms/drop-justification! result.
Delete from the stores what a network removal `r` swept (`swept-records`), and tear each deleted record down through `sentex-removed!`: `r` is a `jtms/retract!`, `jtms/sweep!` or `jtms/drop-justification!` result.
(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 it puts every
later one in. Returns commute-predicate's result (the rows whose spelling moved, which
are new content to every rule reading the canonical one, and the mints their spellings
drew), or nil when sentence moves no spelling. The storage migrates rather than an alias
recording that two rows mean one. The extent is P's own stored rows and the rows applying
P below the literal (rows-spelled-by), not its spec subtree. Read from storage, never
belief. Linear in the facts it reaches. See docs/canonicalization.md.
When a declaration that re-spells arrives (`symmetric`, or either commutativity relation), bring the named predicate's already stored facts into the argument order it puts every later one in. Returns `commute-predicate`'s result (the rows whose spelling moved, which are new content to every rule reading the canonical one, and the mints their spellings drew), or nil when `sentence` moves no spelling. The storage migrates rather than an alias recording that two rows mean one. The extent is `P`'s own stored rows and the rows applying `P` below the literal (`rows-spelled-by`), not its spec subtree. Read from storage, never belief. Linear in the facts it reaches. See docs/canonicalization.md.
(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] :violations [v]}, the moved rows and the mints their new
spellings drew, 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] :violations [v]}`, the moved rows and the mints their new
spellings drew, 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.
The marks are read unscoped, a superset that witness-among narrows to a believed
statement.
A believed statement of a permuting mark on `pred` (`witness-among`), for `commute-predicate`. The marks are read unscoped, a superset that `witness-among` narrows to a believed statement.
(move-row! kb sx want witness rewrite)Bring one stored row sx to the spelling want: {:at handle :new [handle …] :violations [v …]}, the handle the row ends up at, followed in :new by the mints its
new spelling drew (redraw-mints!), 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`: `{:at handle :new [handle …]
:violations [v …]}`, the handle the row ends up at, followed in `:new` by the mints its
new spelling drew (`redraw-mints!`), 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-sentence? kb sentence)Does a stored mark permute the arguments of sentence's literal, or of a compound
below it (sx/compound-functors)? Read unscoped, as permuting? is.
Does a stored mark permute the arguments of `sentence`'s literal, or of a compound below it (`sx/compound-functors`)? Read unscoped, as `permuting?` is.
(permuting? kb pred)Does a stored mark permute pred's arguments — symmetric, or a commuting group — or
reshape its applications below the literal — associative, idempotent, or a
meetFunctionOf order?
Read unscoped: the fold decides the stored key, which every reader shares.
Does a stored mark permute `pred`'s arguments — `symmetric`, or a commuting group — or reshape its applications below the literal — `associative`, `idempotent`, or a `meetFunctionOf` order? Read unscoped: the fold decides the stored key, which every reader shares.
(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, so a nested teardown appends to the record its caller is reading.
want? false answers nil, which records nothing. The record retains every removed sentex
for the teardown's length, so the caller passes the presence check its readers consult
(nat/any-reified-constants?, a stored defeat).
The sink to record a teardown's removals into: the bound one when there is one, a fresh volatile otherwise, so a nested teardown appends to the record its caller is reading. `want?` false answers nil, which records nothing. The record retains every removed sentex for the teardown's length, so the caller passes the presence check its readers consult (`nat/any-reified-constants?`, a stored `defeat`).
(rows-spelled-by idx pred)The stored rows whose spelling pred's permuting marks decide, sorted: pred's own
rows, and the rows the term index keys by pred, a candidate set holding every row with
an application of pred below its literal. A candidate whose spelling the marks do not
move is left where it lies by the caller's re-spell.
The stored rows whose spelling `pred`'s permuting marks decide, sorted: `pred`'s own rows, and the rows the term index keys by `pred`, a candidate set holding every row with an application of `pred` below its literal. A candidate whose spelling the marks do not move is left where it lies by the caller's re-spell.
(sentex-added kb sentex handle)Reflect a sentex that just landed as a premise into the caches through the
special-predicate table, and queue the exception re-check its arrival may flip. Returns
the table walk's result: the {:new :superseded :violations} migration map for an
equality sentex, nil otherwise. Runs whether or not the sentex is new, since
re-asserting adds premise support.
Reflect a sentex that just landed as a premise into the caches through the
special-predicate table, and queue the exception re-check its arrival may flip. Returns
the table walk's result: the `{:new :superseded :violations}` migration map for an
equality sentex, nil otherwise. Runs whether or not the sentex is new, since
re-asserting adds premise support.(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.
(swept-records kb removed-sentexes)(swept-records kb removed-sentexes retracted)The stored records of a network removal's removed-sentexes, in the removal's order and
read before any is deleted, less each record carrying the :inert provenance mark
assert-inert writes. A derivation concluding an inert record's sentence gives the
record a node and a justification, and the sweep that drops them leaves the record as
assert-inert stored it. retracted, the handle a retract! names, is kept in the
result even when it carries the mark.
The stored records of a network removal's `removed-sentexes`, in the removal's order and read before any is deleted, less each record carrying the `:inert` provenance mark `assert-inert` writes. A derivation concluding an inert record's sentence gives the record a node and a justification, and the sweep that drops them leaves the record as `assert-inert` stored it. `retracted`, the handle a `retract!` names, is kept in the result even when it carries the mark.
(take-out! kb h)Take stored row h out of the network and the store: drop its premise mark and every
justification concluding it, retract it, remove what that swept, then the row itself when
still stored (an inert sentex is no network datum). core/retract!'s storage half. The
justifications go first, so no node or justification names a handle with no record.
Take stored row `h` out of the network and the store: drop its premise mark and every justification concluding it, retract it, remove what that swept, then the row itself when still stored (an inert sentex is no network datum). `core/retract!`'s storage half. The justifications go first, so no node or justification names a handle with no record.
(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 |