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.
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.
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 the corresponding facts visible from context (CxUniverse when nil) name as
the value of the ground NAT expression E, spelled under context's merges, or nil.
Nil also when they name several values (docs/nat.md, The corresponding predicate).
The term the corresponding facts visible from `context` (CxUniverse when nil) name as the value of the ground NAT expression `E`, spelled under `context`'s merges, or nil. Nil also when they name several values (docs/nat.md, The corresponding predicate).
(corresponding-literal kb E v)The sentence the correspondence makes equivalent to E = v — the predicate applied
to E's arguments with v at the declared position — or nil when E's function has
no single correspondence.
The sentence the correspondence makes equivalent to `E = v` — the predicate applied to `E`'s arguments with `v` at the declared position — or nil when `E`'s function has no single correspondence.
(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.
(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. 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`. 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`).
(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/`.
The two reserved namespaces a reified constant lives in, nat and cx.
The two reserved namespaces a reified constant lives in, `nat` and `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.
(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?`).
(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.
(visible-values kb E context)The terms the corresponding facts visible from context name as the value of the
ground NAT expression E, each spelled under context's merges, as a set. Nil when
E's function has no single correspondence. A variable context reads every context
under the global partition.
The terms the corresponding facts visible from `context` name as the value of the ground NAT expression `E`, each spelled under `context`'s merges, as a set. Nil when `E`'s function has no single correspondence. A variable `context` reads every context under the global partition.
(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 |