The read-mode reify of a ground NAT: the reserved namespaces, the reifiable_function
mark, the natFormula and correspondence lookups a reader or writer in a context
resolves an application through, and the walk both reify modes share. Below provers,
so the belief projection reifies a proposition in the agent's context. See docs/nat.md.
The read-mode reify of a ground NAT: the reserved namespaces, the `reifiable_function` mark, the `natFormula` and correspondence lookups a reader or writer in a context resolves an application through, and the walk both reify modes share. Below `provers`, so the belief projection reifies a proposition in the agent's context. See docs/nat.md.
True while nat/mint-nat! stores a constant's bookkeeping: its asserts queue nothing,
and the mint queues the constant once its bookkeeping is stored.
True while `nat/mint-nat!` stores a constant's bookkeeping: its asserts queue nothing, and the mint queues the constant once its bookkeeping is stored.
The reifiable_function functions whose ground applications stay as written while
bound: the ones a reader does not believe the mark of (withheld-at), so the reconcile
stores, and a read looks up, the spelling that reader reads (chain/reconcile-reified!).
The `reifiable_function` functions whose ground applications stay as written while bound: the ones a reader does not believe the mark of (`withheld-at`), so the reconcile stores, and a read looks up, the spelling that reader reads (`chain/reconcile-reified!`).
(any-reifiable-functions? kb)Does the KB declare a reifiable_function? One in-memory taxonomy prop read. False
means no sentence holds a reifiable NAT, and every reify pass returns its input.
Does the KB declare a `reifiable_function`? One in-memory taxonomy prop read. False means no sentence holds a reifiable NAT, and every reify pass returns its input.
(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.
(computed-genlCx-edge? kb sx)Is sx a genlCx edge the structural producer computed: not a premise, and every
support under the contextArgSubrelation informant (docs/context-nat.md, Orphan
collection)? Belief is not read. The orphan sweep reads such an edge as the engine's
own wiring, and a declaration's sweep over stored facts draws nothing from it
(special/entail-existing).
Is `sx` a `genlCx` edge the structural producer computed: not a premise, and every support under the `contextArgSubrelation` informant (docs/context-nat.md, Orphan collection)? Belief is not read. The orphan sweep reads such an edge as the engine's own wiring, and a declaration's sweep over stored facts draws nothing from it (`special/entail-existing`).
Reserved namespace of a context reified constant, which a ground application in a sentex's context slot mints, whatever is declared about its head (docs/context-nat.md).
Reserved namespace of a context reified constant, which a ground application in a sentex's context slot mints, whatever is declared about its head (docs/context-nat.md).
(correspondence-value kb E context)The term a :monotonic corresponding fact visible from context (CxUniverse when nil)
names as the value of the ground NAT expression E, spelled under context's merges,
when the visible facts name that one value and no other, or nil. A value only
:default facts name resolves no write (docs/nat.md, The corresponding predicate).
The term a `:monotonic` corresponding fact visible from `context` (CxUniverse when nil) names as the value of the ground NAT expression `E`, spelled under `context`'s merges, when the visible facts name that one value and no other, or nil. A value only `:default` facts name resolves no write (docs/nat.md, The corresponding predicate).
(dedup-constant kb E)(dedup-constant kb E ns context)The existing reified constant for the ground NAT expression E in reify namespace ns
(default nat/) for a reader in context (CxUniverse when nil), or nil: the
natFormula rows map-rows reads. Where several constants map E in one namespace
(an import restores what the dump held, or a merge the reader sees joins two
expressions), the lexicographically smallest, the survivor group-collisions elects.
The existing reified constant for the ground NAT expression `E` in reify namespace `ns` (default `nat/`) for a reader in `context` (CxUniverse when nil), or nil: the `natFormula` rows `map-rows` reads. Where several constants map `E` in one namespace (an import restores what the dump held, or a merge the reader sees joins two expressions), the lexicographically smallest, the survivor `group-collisions` elects.
(existing-term kb E ns context)The term ground NAT expression E already resolves to in reify namespace ns for a
reader or writer in context, or nil: a rewriteOf target, the value its
corresponding predicate names where context reads it (correspondence-value), else
the constant dedup-constant finds. A context slot (cx/) takes no correspondence
value, which names an object.
The term ground NAT expression `E` already resolves to in reify namespace `ns` for a reader or writer in `context`, or nil: a `rewriteOf` target, the value its corresponding predicate names where `context` reads it (`correspondence-value`), else the constant `dedup-constant` finds. A context slot (`cx/`) takes no correspondence value, which names an object.
(fact-constants kb sentence)The constants minted for the applications the positive literal sentence names a value
of under each stored correspondence declaration of its functor, read off the map
(dedup-constant).
The constants minted for the applications the positive literal `sentence` names a value of under each stored correspondence declaration of its functor, read off the map (`dedup-constant`).
(in-namespace? ns k)Does the term k a natFormula map names belong to reify namespace ns? A context
slot's constant is a context (nm/context?), and an argument's is any other term.
Does the term `k` a `natFormula` map names belong to reify namespace `ns`? A context slot's constant is a context (`nm/context?`), and an argument's is any other term.
(maybe-reify-for-read kb sentence context)Reify every reifiable ground NAT subterm of a query sentence to its existing term for
a reader in context (CxUniverse when nil), never minting; a never-minted NAT resolves
to no-match, except a quoting application, which stays as written. An application
of a function context does not believe reifiable stays as written (withheld-at).
Reify every reifiable ground NAT subterm of a query `sentence` to its existing term for a reader in `context` (CxUniverse when nil), never minting; a never-minted NAT resolves to `no-match`, except a quoting application, which stays as written. An application of a function `context` does not believe reifiable stays as written (`withheld-at`).
Reserved namespace of an object reified constant, which a ground application of a
(reifiable_function F) in argument position mints.
Reserved namespace of an object reified constant, which a ground application of a `(reifiable_function F)` in argument position mints.
The reserved constant a read-mode reify resolves a never-minted NAT to (sx/no-match).
The reserved constant a read-mode reify resolves a never-minted NAT to (`sx/no-match`).
(note-values kb sentences uses?)Queue on :respell what the stored, removed or relabelled sentences move the
values of: [:valued-fn f] for a correspondence declaration of f, [:valued k] for
each constant a corresponding fact names a value of (fact-constants) and for each
constant minted for the expression of a compound rewriteOf, and with uses? for each
constant a sentence names whose function is declared or whose expression a compound
rewriteOf names (valued-constants). Answers whether it queued anything. The
correspondence arms are behind values-reachable?, a use's rewriteOf arm behind
rewrites-reachable?, read once and only for a use naming a reified constant; nothing
while *minting?*.
Queue on `:respell` what the stored, removed or relabelled `sentences` move the values of: `[:valued-fn f]` for a correspondence declaration of `f`, `[:valued k]` for each constant a corresponding fact names a value of (`fact-constants`) and for each constant minted for the expression of a compound `rewriteOf`, and with `uses?` for each constant a sentence names whose function is declared or whose expression a compound `rewriteOf` names (`valued-constants`). Answers whether it queued anything. The correspondence arms are behind `values-reachable?`, a use's `rewriteOf` arm behind `rewrites-reachable?`, read once and only for a use naming a reified constant; nothing while `*minting?*`.
(reifiable-entries kb f){[:prop :reifiable f] {handle context}}, the reifiable_function mark of f and its
supporters, in res/mark-entries' shape.
`{[:prop :reifiable f] {handle context}}`, the `reifiable_function` mark of `f` and its
supporters, in `res/mark-entries`' shape.(reifiable-function? kb head)True iff head reifies its ground applications in argument position: a believed
(reifiable_function head), and head not in *withheld*. The mark is read
unscoped; a reader that does not believe it binds *withheld*.
True iff `head` reifies its ground applications in argument position: a believed `(reifiable_function head)`, and `head` not in `*withheld*`. The mark is read unscoped; a reader that does not believe it binds `*withheld*`.
(reifiable-ground-nat? kb form)True iff form is a ground (F …) whose head is a reifiable function: a NAT the
argument-position reify mints to a nat/ constant.
True iff `form` is a ground `(F …)` whose head is a reifiable function: a NAT the argument-position reify mints to a `nat/` constant.
(reified-context-symbol? term)True iff term is a reified context constant, a symbol in cx/.
True iff `term` is a reified context constant, a symbol in `cx/`.
(reified-nat-symbol? term)True iff term is a reified constant: a symbol in nat/ or cx/.
True iff `term` is a reified constant: a symbol in `nat/` or `cx/`.
(reified-object-symbol? term)True iff term is a reified object constant, a symbol in nat/.
True iff `term` is a reified object constant, a symbol in `nat/`.
(reify-existing kb sentence context)Reify every reifiable ground NAT subterm of sentence that has an existing term for a
reader in context (CxUniverse when nil) to that term, and leave every other one as
written. Never mints. vaelii.core/check reads a sentence through this (docs/nat.md,
Typing an application that is never minted).
Reify every reifiable ground NAT subterm of `sentence` that has an existing term for a reader in `context` (CxUniverse when nil) to that term, and leave every other one as written. Never mints. `vaelii.core/check` reads a sentence through this (docs/nat.md, Typing an application that is never minted).
(reify-in kb s nat-fn)Reify every reifiable ground NAT subterm of literal/sentence s, calling nat-fn (a
(fn [kb form])) at each one; nat-fn returns the NAT's term, having reified its
nested NAT arguments itself. A head predicate, a quoting-predicate argument and a
modal_predicate's proposition (res/attitude-application?) stay opaque. The modal
mark is read KB-wide, once per walk: whether an argument is a mention is a fact about
the sentence (tax/mention-marks). A vector is descended element by element
(docs/nat.md, Write path).
Reify every reifiable ground NAT subterm of literal/sentence `s`, calling `nat-fn` (a `(fn [kb form])`) at each one; `nat-fn` returns the NAT's term, having reified its nested NAT arguments itself. A head predicate, a quoting-predicate argument and a `modal_predicate`'s proposition (`res/attitude-application?`) stay opaque. The modal mark is read KB-wide, once per walk: whether an argument is a mention is a fact about the sentence (`tax/mention-marks`). A vector is descended element by element (docs/nat.md, Write path).
(reify-nat-for-read kb form ns context)Read-mode leaf: reify nested NAT arguments, then resolve the expression to its
existing term in reify namespace ns for a reader in context (existing-term), or
to no-match. Never mints. A quoting function's argument stays opaque, as
reify-or-mint-nat holds it.
Read-mode leaf: reify nested NAT arguments, then resolve the expression to its existing term in reify namespace `ns` for a reader in `context` (`existing-term`), or to `no-match`. Never mints. A quoting function's argument stays opaque, as `reify-or-mint-nat` holds it.
(resolve-for-read kb sentence context)The read-mode reify of sentence for a reader in context (maybe-reify-for-read)
when every reifiable NAT in it has a stored term, else nil.
The read-mode reify of `sentence` for a reader in `context` (`maybe-reify-for-read`) when every reifiable NAT in it has a stored term, else nil.
(result-arg-types E ns)The symbols application E holds at the positions ns its function's (resultArg F n) declarations name. A position E lacks, or a non-symbol there, names no type.
The symbols application `E` holds at the positions `ns` its function's `(resultArg F n)` declarations name. A position `E` lacks, or a non-symbol there, names no type.
(rewrite-target kb E ns context)The real term T a (rewriteOf T E) a reader in context (CxUniverse when nil)
reads (map-rows) reifies NAT expression E to, spelled under context's merges, or
nil. Nil when the declarations name more than one target (docs/nat.md, The
corresponding predicate), and when the one T lies outside reify namespace ns
(in-namespace?).
The real term `T` a `(rewriteOf T E)` a reader in `context` (CxUniverse when nil) reads (`map-rows`) reifies NAT expression `E` to, spelled under `context`'s merges, or nil. Nil when the declarations name more than one target (docs/nat.md, The corresponding predicate), and when the one `T` lies outside reify namespace `ns` (`in-namespace?`).
(rewrites-reachable? kb)Can a compound rewriteOf reach a minted constant: does the KB declare a reifiable
function and store a rewriteOf and a natFormula map? One set read, then two O(1)
functor counts.
Can a compound `rewriteOf` reach a minted constant: does the KB declare a reifiable function and store a `rewriteOf` and a `natFormula` map? One set read, then two O(1) functor counts.
(split-reifiable? kb f)Does some reader not believe f's stored reifiable_function mark
(res/uniform-marks?)?
Does some reader not believe `f`'s stored `reifiable_function` mark (`res/uniform-marks?`)?
The context every NAT bookkeeping fact is stored in.
The context every NAT bookkeeping fact is stored in.
(values-reachable? kb)Can a corresponding fact reach a minted constant: does the KB declare a reifiable
function (any-reifiable-functions?) and store a correspondence declaration and a
natFormula map? One set read, then two O(1) functor counts.
Can a corresponding fact reach a minted constant: does the KB declare a reifiable function (`any-reifiable-functions?`) and store a correspondence declaration and a `natFormula` map? One set read, then two O(1) functor counts.
(visible-result-targets kb pred head context)The distinct arg2s of the believed (<pred> head ?t) facts visible from context
(res/matches-visible), as a check and a goal read a declaration (docs/nat.md, Typing
an application that is never minted).
The distinct arg2s of the believed `(<pred> head ?t)` facts visible from `context` (`res/matches-visible`), as a check and a goal read a declaration (docs/nat.md, Typing an application that is never minted).
(visible-result-types kb head context)Types T with a (result head T) visible from context: what an application of
head is an instance of. Given an application (head a…) in place of head, adds the
argument at each position a visible (resultArg head n) declares, behind one O(1)
functor count.
Types `T` with a `(result head T)` visible from `context`: what an application of `head` is an instance of. Given an application `(head a…)` in place of `head`, adds the argument at each position a visible `(resultArg head n)` declares, behind one O(1) functor count.
(withheld-at kb reader)The reifiable functions reader does not believe the mark of while another reader
does, as a set: what *withheld* holds to spell a sentence as reader reads it.
Empty for a variable or nil reader.
The reifiable functions `reader` does not believe the mark of while another reader does, as a set: what `*withheld*` holds to spell a sentence as `reader` reads it. Empty for a variable or nil `reader`.
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 |