The structural genlCx producer for reified-NAT contexts — docs/context-nat.md.
(contextArgSubrelation F pos R) orders two F-contexts by the product of the declared
sub-relations at the positions where they differ, and (contextArgGenlCx F pos) places
every F-context under its argument at pos. This namespace materializes each such
genlCx edge as a justified sentex in CxUniverse, never a premise. R is resolved
by a bounded oracle: a registered pure comparator, else the genlCx closure for a
sub-relation in closure-orders and each believed stored (R a b) fact.
The structural genlCx producer for reified-NAT contexts — docs/context-nat.md. `(contextArgSubrelation F pos R)` orders two `F`-contexts by the product of the declared sub-relations at the positions where they differ, and `(contextArgGenlCx F pos)` places every `F`-context under its argument at `pos`. This namespace **materializes** each such `genlCx` edge as a **justified** sentex in CxUniverse, never a premise. `R` is resolved by a bounded oracle: a registered pure comparator, else the `genlCx` closure for a sub-relation in `closure-orders` and each believed stored `(R a b)` fact.
(any-context-declarations? kb)Presence check: does the KB declare any contextArgSubrelation or contextArgGenlCx?
The producer is a no-op otherwise — two O(1) functor counts per assert, the shape
res/any-corresponding-predicates? has.
Presence check: does the KB declare any `contextArgSubrelation` or `contextArgGenlCx`? The producer is a no-op otherwise — two O(1) functor counts per assert, the shape `res/any-corresponding-predicates?` has.
(arg-supers kb k e)The contexts the structural producer places k under for (natFormula k e) in
CxUniverse: the arg-context at each of the arg-genlcx-declarations of e's
function, in position order.
The contexts the structural producer places `k` under for `(natFormula k e)` in CxUniverse: the `arg-context` at each of the `arg-genlcx-declarations` of `e`'s function, in position order.
(reconcile-genlCx kb sentence moves)The structural-genlCx maintenance a just-asserted sentence and the belief moves of its
write (moves, reconcile-moves) call for: the arrival of sentence
(reconcile-arrival), a genlCx edge read with the moved edges once. A no-op, two
functor counts, on a KB that declares no contextArgSubrelation and no
contextArgGenlCx. Returns true when an
edge gained a justification, which the caller settles.
The structural-genlCx maintenance a just-asserted `sentence` and the belief moves of its write (`moves`, `reconcile-moves`) call for: the arrival of `sentence` (`reconcile-arrival`), a `genlCx` edge read with the moved edges once. A no-op, two functor counts, on a KB that declares no `contextArgSubrelation` and no `contextArgGenlCx`. Returns true when an edge gained a justification, which the caller settles.
(reconcile-moves kb {:keys [edges arrived derived] :as moves})The structural genlCx maintenance the belief moves moves call for, once the write that
moved them has settled. moves is what special/take-producer-moves! answers:
:edges, the genlCx edges the write's settles moved, each reconciled by
reconcile-edge-move; :arrived, handles revived, and :derived, handles derived by
functor, each read as an arrival when believed and of a functor declared-heads names.
Edges and sentences are read in content order. Local: the cost follows the moves and
the contexts they name, never the context-NAT population. Returns true when an edge
gained a justification, which the caller settles.
The structural genlCx maintenance the belief moves `moves` call for, once the write that moved them has settled. `moves` is what `special/take-producer-moves!` answers: `:edges`, the `genlCx` edges the write's settles moved, each reconciled by `reconcile-edge-move`; `:arrived`, handles revived, and `:derived`, handles derived by functor, each read as an arrival when believed and of a functor `declared-heads` names. Edges and sentences are read in content order. Local: the cost follows the moves and the contexts they name, never the context-NAT population. Returns true when an edge gained a justification, which the caller settles.
(reconcile-revivals kb moves removed)The structural genlCx maintenance a teardown owes once its belief has settled: the
belief moves of the teardown (moves, reconcile-moves), and the target of every
except or defeat among the removed sentences, whose belief or visibility the removal
gave back with no relabel. Behind nat/any-reified-constants?. Returns true when an edge
gained a justification, which the caller settles.
The structural genlCx maintenance a teardown owes once its belief has settled: the belief moves of the teardown (`moves`, `reconcile-moves`), and the target of every `except` or `defeat` among the `removed` sentences, whose belief or visibility the removal gave back with no relabel. Behind `nat/any-reified-constants?`. Returns true when an edge gained a justification, which the caller settles.
(unwritten-read kb expr)[k read-kb] for a read of the context of expr nobody has written into: k the
cx/ constant its content names, read-kb kb with a genlCx edge from k to each
of unminted-supers (kb/with-context-edges); nil when there are none. Held among the
resident values under the change clock (observe/cached), so the reads between two
writes share one read copy and its caches.
`[k read-kb]` for a read of the context of `expr` nobody has written into: `k` the `cx/` constant its content names, `read-kb` `kb` with a `genlCx` edge from `k` to each of `unminted-supers` (`kb/with-context-edges`); nil when there are none. Held among the resident values under the change clock (`observe/cached`), so the reads between two writes share one read copy and its caches.
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 |