Non-atomic terms (NATs): the write-mode reify (mint, materialize result types), the
natFormula map's K → E read, display expansion, the correspondence maintenance, and
the reads the rename, orphan and re-spelling maintenance runs on. The read mode and the
E → K lookups are nat-read's. Stores through wiring/assert-sentence. See
docs/nat.md.
Non-atomic terms (NATs): the write-mode reify (mint, materialize result types), the `natFormula` map's `K → E` read, display expansion, the correspondence maintenance, and the reads the rename, orphan and re-spelling maintenance runs on. The read mode and the `E → K` lookups are `nat-read`'s. Stores through `wiring/assert-sentence`. See docs/nat.md.
(any-reified-constants? kb)Does the KB declare a reifiable_function or store a natFormula map? The presence
check of the maintenance a reified constant owes. The in-memory read first, then one
O(1) functor count, which admits a KB whose only constants are cx/ contexts.
Does the KB declare a `reifiable_function` or store a `natFormula` map? The presence check of the maintenance a reified constant owes. The in-memory read first, then one O(1) functor count, which admits a KB whose only constants are `cx/` contexts.
(any-result-declarations? kb)Does the KB declare any result, genlResult or resultArg? Three O(1) functor
counts.
Does the KB declare any `result`, `genlResult` or `resultArg`? Three O(1) functor counts.
(authoritative-expression exprs)The content-least of exprs: the one expression a reified constant denotes when an
unrepaired collision maps it to several. Every reader of the map takes this one
(docs/nat.md, Rename and remove).
The content-least of `exprs`: the one expression a reified constant denotes when an unrepaired collision maps it to several. Every reader of the map takes this one (docs/nat.md, Rename and remove).
(bookkeeping-handles kb k)The handles of constant k's bookkeeping sentexes, stored, believed or not: its
natFormula map and what minted-for says the mint wrote. A cx/ constant's is its
map alone; the computed genlCx edges go by the dependency-directed sweep. Realized
before it returns, because the caller retracts what it lists and the bookkeeping test
reads k's map (docs/nat.md, Rename and remove).
The handles of constant `k`'s bookkeeping sentexes, stored, believed or not: its `natFormula` map and what `minted-for` says the mint wrote. A `cx/` constant's is its map alone; the computed `genlCx` edges go by the dependency-directed sweep. Realized before it returns, because the caller retracts what it lists and the bookkeeping test reads `k`'s map (docs/nat.md, Rename and remove).
(colliding-constant-groups kb)[survivor [dup …]] per expression more than one believed constant maps. Reads the
whole map in CxUniverse; the maintenance after a write reads merge-colliding-nats!'s rows.
`[survivor [dup …]]` per expression more than one believed constant maps. Reads the whole map in CxUniverse; the maintenance after a write reads `merge-colliding-nats!`'s rows.
(constant-for ns E)The reified constant expression E names in reserved namespace ns (nat or cx),
a function of E's content alone (content-name). A hash collision gives one constant
two expressions, the case authoritative-expression reads.
The reified constant expression `E` names in reserved namespace `ns` (`nat` or `cx`), a function of `E`'s content alone (`content-name`). A hash collision gives one constant two expressions, the case `authoritative-expression` reads.
(context-application? form)True iff form is a ground application headed by a symbol: what a context slot reifies
to a cx/ constant, whatever is declared about the head. Decided by the form alone,
so a write stores the same set in every arrival order (docs/context-nat.md).
True iff `form` is a ground application headed by a symbol: what a context slot reifies to a `cx/` constant, whatever is declared about the head. Decided by the form alone, so a write stores the same set in every arrival order (docs/context-nat.md).
(context-for-check kb context)The context assert stores a sentex in for the slot context, minting nothing: for a
context-application?, its existing-context, else the cx/ constant constant-for
names for the expression, which no stored sentex names. Any other slot passes through.
vaelii.core/check reads the slot through this, so its checks read the context
maybe-reify-context mints.
The context `assert` stores a sentex in for the slot `context`, minting nothing: for a `context-application?`, its `existing-context`, else the `cx/` constant `constant-for` names for the expression, which no stored sentex names. Any other slot passes through. `vaelii.core/check` reads the slot through this, so its checks read the context `maybe-reify-context` mints.
(context-function-believed? kb head)True iff CxUniverse believes a (result head context) declaration: stated in a
context CxUniverse sees and hidden by no except or defeat in force at CxUniverse
(res/supporter-visible?). A read admits a context slot (head a…) on this.
True iff CxUniverse believes a `(result head context)` declaration: stated in a context CxUniverse sees and hidden by no `except` or `defeat` in force at CxUniverse (`res/supporter-visible?`). A read admits a context slot `(head a…)` on this.
The type a (result F context) declaration names (docs/context-nat.md).
The type a `(result F context)` declaration names (docs/context-nat.md).
(corresponded-rules kb f preds spelled?)The stored rules a correspondence of f moving can re-spell back: each rule with an
antecedent on a predicate of a stored correspondence declaration of f, or on one of
preds, whose premise assertions record a written spelling (spelled?). Reads every
context: a stored rule's spelling is one row every reader shares.
The stored rules a correspondence of `f` moving can re-spell back: each rule with an antecedent on a predicate of a stored correspondence declaration of `f`, or on one of `preds`, whose premise assertions record a written spelling (`spelled?`). Reads every context: a stored rule's spelling is one row every reader shares.
(departed-map sentence)[k E] for sentence (natFormula k E) with k an object constant, else nil: the
pair a map leaving the store takes with it.
`[k E]` for `sentence` `(natFormula k E)` with `k` an object constant, else nil: the pair a map leaving the store takes with it.
(existing-context kb form)The cx/ constant (or rewriteOf target) the context application form already
resolves to, or nil when none was minted — the dedup half of maybe-reify-context's
write path, read without any declaration.
The `cx/` constant (or `rewriteOf` target) the context application `form` already resolves to, or nil when none was minted — the dedup half of `maybe-reify-context`'s write path, read without any declaration.
(expand-expression kb form)(expand-expression kb form expand?)form with every reified constant replaced, recursively, by the expression it maps
to. form itself, the same object, when it holds no reified constant. A vector
rebuilds as a vector. expand? narrows which constants are expanded.
`form` with every reified constant replaced, recursively, by the expression it maps to. `form` itself, the same object, when it holds no reified constant. A vector rebuilds as a vector. `expand?` narrows which constants are expanded.
(formula-declared-predicates kb sentences)The predicates whose formula positions (res/formula-position?) the stored or
removed sentences can move, sorted: P of an arg, quotedArg or argN
declaration typed formula or under it, and for a genl edge (genl A B) with B
formula or under it, P of each stored such declaration typed A or under it.
Reads the taxonomy and the declaration index unscoped, as res/formula-position? does.
The predicates whose `formula` positions (`res/formula-position?`) the stored or removed `sentences` can move, sorted: `P` of an `arg`, `quotedArg` or `argN` declaration typed `formula` or under it, and for a `genl` edge `(genl A B)` with `B` `formula` or under it, `P` of each stored such declaration typed `A` or under it. Reads the taxonomy and the declaration index unscoped, as `res/formula-position?` does.
(formula-position-rules kb preds)The stored rules with an antecedent or a consequent on one of preds that name a
variable-functor application (res/names-variable-application?), in content order:
the rules whose hold a formula position of one of preds decides
(held-application?). Reads every context: the hold is one record every reader shares.
The stored rules with an antecedent or a consequent on one of `preds` that name a variable-functor application (`res/names-variable-application?`), in content order: the rules whose hold a `formula` position of one of `preds` decides (`held-application?`). Reads every context: the hold is one record every reader shares.
(genl-result-types kb head)(genl-result-types kb head context)Types T with (genlResult head T): what an application of head is a subtype of.
Globally, or with context through the declarations visible from it. head may be an
application, as result-types takes it.
Types `T` with `(genlResult head T)`: what an application of `head` is a subtype of. Globally, or with `context` through the declarations visible from it. `head` may be an application, as `result-types` takes it.
(held-application-rules kb)The stored rules held-application? holds, read off the rule extent of every context
(the :out forced set is one record every reader shares).
The stored rules `held-application?` holds, read off the rule extent of every context (the `:out` forced set is one record every reader shares).
(held-application? kb sx)Does stored rule sx hold an open application res/respell-applications left as
written, so the rule is held in the :out forced set: one of a reifiable_function
(the mark read unscoped), or a variable-functor application outside a sentence position
(res/holds-variable-application?)? A rule consequent is not read (res/rule-form?).
Does stored rule `sx` hold an open application `res/respell-applications` left as written, so the rule is held in the `:out` forced set: one of a `reifiable_function` (the mark read unscoped), or a variable-functor application outside a sentence position (`res/holds-variable-application?`)? A rule consequent is not read (`res/rule-form?`).
(maybe-reify-context kb context)(maybe-reify-context kb context mint?)Reify a context slot (F …) to its cx/ constant (docs/context-nat.md). With
mint? (the write path) any context-application? reifies, minting as needed.
Without it (a read) only a readable-context-application? does, resolving to an
existing term or no-match. Any other slot passes through unchanged.
Reify a context slot `(F …)` to its `cx/` constant (docs/context-nat.md). With `mint?` (the write path) any `context-application?` reifies, minting as needed. Without it (a read) only a `readable-context-application?` does, resolving to an existing term or `no-match`. Any other slot passes through unchanged.
(maybe-reify-nats kb sentence context)(maybe-reify-nats kb sentence chain? context)Replace every ground reifiable NAT subterm of sentence, written in context
(CxUniverse when nil), with its reified constant, minting as needed. Returns
sentence on a KB declaring no reifiable_function.
Replace every ground reifiable NAT subterm of `sentence`, written in `context` (CxUniverse when nil), with its reified constant, minting as needed. Returns `sentence` on a KB declaring no `reifiable_function`.
(mint-nat! kb E)(mint-nat! kb E ns chain?)Mint the reified constant K for the ground NAT expression E in reify namespace ns
(cx/ for a context slot, nat/ for an argument) and return it. Asserts (natFormula K E) in CxUniverse and, for a nat/ constant, the materialized result types and the
correspondence projection, all :monotonic. The result types and the projection
chain as chain? says; the map chains only when a resultArg of E's function is
declared (docs/defenses.md, The mint's natFormula fact does not chain).
Mint the reified constant `K` for the ground NAT expression `E` in reify namespace `ns` (`cx/` for a context slot, `nat/` for an argument) and return it. Asserts `(natFormula K E)` in CxUniverse and, for a `nat/` constant, the materialized result types and the correspondence projection, all `:monotonic`. The result types and the projection chain as `chain?` says; the map chains only when a `resultArg` of `E`'s function is declared (docs/defenses.md, The mint's natFormula fact does not chain).
(names-open-application? kb form)Does form hold an open application of a reifiable_function (the mark read
unscoped), outside a mention? False on a KB declaring none, with no walk.
Does `form` hold an open application of a `reifiable_function` (the mark read unscoped), outside a mention? False on a KB declaring none, with no walk.
(names-reifiable-nat? kb s)Does sentence s hold a ground reifiable NAT the write-mode reify would replace, at a
position nat-read/reify-in visits? False on a KB declaring no reifiable function, and
otherwise one walk that rebuilds nothing. The modal mark is read KB-wide, as
reify-in reads it.
Does sentence `s` hold a ground reifiable NAT the write-mode reify would replace, at a position `nat-read/reify-in` visits? False on a KB declaring no reifiable function, and otherwise one walk that rebuilds nothing. The modal mark is read KB-wide, as `reify-in` reads it.
(nat-expression kb nat-sym)The NAT expression a reified constant denotes, or nil — the authoritative one where an
unrepaired collision maps it to more than one (authoritative-expression).
The NAT expression a reified constant denotes, or nil — the authoritative one where an unrepaired collision maps it to more than one (`authoritative-expression`).
The one-letter scheme prefix of every content-named reified constant. a is
SHA-256 truncated to 96 bits in base62, so a name is this letter and 17 digits. The
letter keeps the name a readable token and versions the scheme (docs/nat.md, Write
path).
The one-letter scheme prefix of every content-named reified constant. `a` is SHA-256 truncated to 96 bits in base62, so a name is this letter and 17 digits. The letter keeps the name a readable token and versions the scheme (docs/nat.md, Write path).
(orphan? kb k)Is the reified constant k an orphan: is every stored sentex naming it one of its own
(own-sentex-test)? False when no believed natFormula maps k. A cx/ constant
with a non-empty extent is not one, read by one count-in-context before the
term-index read. Uses count by storage; only the map read follows belief. Decided
against the authoritative expression, the one bookkeeping-handles retracts for
(docs/nat.md, Rename and remove).
Is the reified constant `k` an orphan: is every stored sentex naming it one of its own (`own-sentex-test`)? False when no believed `natFormula` maps `k`. A `cx/` constant with a non-empty extent is not one, read by one `count-in-context` before the term-index read. Uses count by storage; only the map read follows belief. Decided against the authoritative expression, the one `bookkeeping-handles` retracts for (docs/nat.md, Rename and remove).
(orphaned-constants kb)Every reified constant the KB maps that is an orphan (orphan?). Reads the whole
map; a teardown reads orphans-named-by.
Every reified constant the KB maps that is an orphan (`orphan?`). Reads the whole map; a teardown reads `orphans-named-by`.
(orphans-named-by kb sentexes)The orphans among the constants the removed sentexes named: the candidate set of one
round of a teardown's sweep.
The orphans among the constants the removed `sentexes` named: the candidate set of one round of a teardown's sweep.
(queue-split-uses! kb sentence)Queue [:reifiable f] on :respell for each function f a ground application in
sentence names whose mark some reader does not believe (split-reifiable?): the
write stores the use reified, and the settle's reconcile stores the spelling each
reader reads (chain/reconcile-reified!). One walk and no index read on a KB whose
reifiable marks every reader believes.
Queue `[:reifiable f]` on `:respell` for each function `f` a ground application in `sentence` names whose mark some reader does not believe (`split-reifiable?`): the write stores the use reified, and the settle's reconcile stores the spelling each reader reads (`chain/reconcile-reified!`). One walk and no index read on a KB whose reifiable marks every reader believes.
(readable-context-application? kb form)True iff form is a context-application? whose head CxUniverse believes denotes
contexts (context-function-believed?): what a read admits as a context slot.
True iff `form` is a `context-application?` whose head CxUniverse believes denotes contexts (`context-function-believed?`): what a read admits as a context slot.
(reconcile-nats! kb sentence context)The reified-constant maintenance a just-asserted sentence owes, in this order: the
collision repair (merge-colliding-nats!), the correspondence, then a result declaration
reaching the constants minted before it. nat-maintenance/reconcile-assert calls it
behind any-reified-constants?. context is where sentence is stored.
The reified-constant maintenance a just-asserted `sentence` owes, in this order: the collision repair (`merge-colliding-nats!`), the correspondence, then a result declaration reaching the constants minted before it. `nat-maintenance/reconcile-assert` calls it behind `any-reified-constants?`. `context` is where `sentence` is stored.
(reified-nats-in form)Every reified constant form names, at any nesting, in a list or a vector.
Every reified constant `form` names, at any nesting, in a list or a vector.
(reify-or-mint-nat kb form)(reify-or-mint-nat kb form ns chain? context)Reify a ground NAT form to its term in reify namespace ns (default nat/) for a
write stored in context (CxUniverse when nil): nested NAT arguments first, then the
existing term (existing-term), else a fresh mint (mint-nat!). A quoting function's
argument is a mention and is not reified (docs/nat.md, Typing an application that is
never minted).
Reify a ground NAT `form` to its term in reify namespace `ns` (default `nat/`) for a write stored in `context` (CxUniverse when nil): nested NAT arguments first, then the existing term (`existing-term`), else a fresh mint (`mint-nat!`). A quoting function's argument is a mention and is not reified (docs/nat.md, Typing an application that is never minted).
(respell-region kb f)The stored sentexes a reifiable_function mark on f moving can re-spell: each one
holding an application of f, and each use of an object constant whose expression
holds one, at any nesting (region-from).
The stored sentexes a `reifiable_function` mark on `f` moving can re-spell: each one holding an application of `f`, and each use of an object constant whose expression holds one, at any nesting (`region-from`).
(respelled kb sentence context)sentence as the write path spells it under the marks believed now: every object
constant expanded to the expression it maps to, then every ground reifiable application
reified again (maybe-reify-nats), minting what has no term yet. Equal to sentence
when no mark it depends on has moved. context is where the row is stored.
`sentence` as the write path spells it under the marks believed now: every object constant expanded to the expression it maps to, then every ground reifiable application reified again (`maybe-reify-nats`), minting what has no term yet. Equal to `sentence` when no mark it depends on has moved. `context` is where the row is stored.
(result-types kb head)(result-types kb head context)Types T with (result head T): what an application of head is an instance of.
Globally, or with context through the declarations visible from it. Given an
application (head a…) in place of head, adds the argument at each position a
(resultArg head n) declares.
Types `T` with `(result head T)`: what an application of `head` is an instance of. Globally, or with `context` through the declarations visible from it. Given an application `(head a…)` in place of `head`, adds the argument at each position a `(resultArg head n)` declares.
(stranded-uses kb k E)The stored uses, believed or not, of object constant k once no stored natFormula
maps it, E being the expression its departed map held: every sentex naming k that
is neither a quoting predicate's row nor k's own (own-sentex-test), and every use
of a constant whose stored map's expression names k, at any nesting (region-from).
Nil while a map of k is stored, since respell-region reaches those uses.
The stored uses, believed or not, of object constant `k` once no stored `natFormula` maps it, `E` being the expression its departed map held: every sentex naming `k` that is neither a quoting predicate's row nor `k`'s own (`own-sentex-test`), and every use of a constant whose stored map's expression names `k`, at any nesting (`region-from`). Nil while a map of `k` is stored, since `respell-region` reaches those uses.
(written-as kb form departed)form with every object constant expanded, recursively, to the expression it maps to,
each key of departed ({k E}, constants whose map left the store) to its value.
`form` with every object constant expanded, recursively, to the expression it maps to,
each key of `departed` (`{k E}`, constants whose map left the store) to its value.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 |