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.
nat-read/any-result-declarations?.
`nat-read/any-result-declarations?`.
(applies? f sentence)Does sentence hold an application of f, at any nesting?
Does `sentence` hold an application of `f`, at any nesting?
(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, and the modal_predicate mark KB-wide
(tax/mention-marks): 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, and the `modal_predicate` mark KB-wide (`tax/mention-marks`): 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 :held forced set is one record every reader shares).
The stored rules `held-application?` holds, read off the rule extent of every context (the `:held` forced set is one record every reader shares).
(held-application? kb sx)Does stored rule sx hold an open application in an antecedent that
res/respell-applications left as written, so the rule is held in the :held forced
set: one of a reifiable_function (the mark read unscoped), or a variable-functor
application outside a sentence position (res/holds-variable-application?)? The
consequent is not read: a firing mints its applications (docs/nat.md, Derivation
path).
Does stored rule `sx` hold an open application in an antecedent that `res/respell-applications` left as written, so the rule is held in the `:held` forced set: one of a `reifiable_function` (the mark read unscoped), or a variable-functor application outside a sentence position (`res/holds-variable-application?`)? The consequent is not read: a firing mints its applications (docs/nat.md, Derivation path).
(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, all
:monotonic, then queues K for the correspondence derivations (nat-read/note-values,
the projection among them). The result types 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, all `:monotonic`, then queues `K` for the correspondence derivations (`nat-read/note-values`, the projection among them). The result types 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).
(minted-applications kb f)The [expression constant] pairs minted for function f in argument position, read
off the inverted term index for f.
The `[expression constant]` pairs minted for function `f` in argument position, read off the inverted term index for `f`.
(names-open-application? kb form)Does form hold an open application of a reifiable_function (the mark read
unscoped), outside a mention: a quoting position or a modal_predicate's proposition
(res/open-applications)? 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: a quoting position or a `modal_predicate`'s proposition (`res/open-applications`)? 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.
(own-sentex-test kb k E sentexes)A test of whether a stored sentex naming constant k is k's own rather than a use:
its bookkeeping (nat-bookkeeping-of?), a projection of its map (projected-from?),
for a context a genlCx edge the structural producer computed
(nat-read/computed-genlCx-edge?), or a record the argument-type entailment derives
from k's own sentexes alone (entailed-from?), read transitively over sentexes.
E is the expression k maps to, and sentexes the term-index answer for k.
A test of whether a stored sentex naming constant `k` is `k`'s own rather than a use: its bookkeeping (`nat-bookkeeping-of?`), a projection of its map (`projected-from?`), for a context a `genlCx` edge the structural producer computed (`nat-read/computed-genlCx-edge?`), or a record the argument-type entailment derives from `k`'s own sentexes alone (`entailed-from?`), read transitively over `sentexes`. `E` is the expression `k` maps to, and `sentexes` the term-index answer for `k`.
(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)The reified-constant maintenance a just-asserted sentence owes, in this order: the
collision repair (merge-colliding-nats!), then a result declaration reaching the
constants minted before it. nat-maintenance/reconcile-assert calls it behind
any-reified-constants?, and queues the correspondence derivations itself.
The reified-constant maintenance a just-asserted `sentence` owes, in this order: the collision repair (`merge-colliding-nats!`), then a result declaration reaching the constants minted before it. `nat-maintenance/reconcile-assert` calls it behind `any-reified-constants?`, and queues the correspondence derivations itself.
(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
(nat-read/visible-result-types). 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 (`nat-read/visible-result-types`). 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 |