The calls that run up the engine's layering, gathered in one file.
Every edge in the engine is a static require the compiler checks:
kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core
Three calls run the other way, and the static require graph cannot express any of them.
Two are genuine mutual recursion: the cycle is in the behaviour, and no code motion
removes it — the assert path reaches a mint that asserts (assert-sentence), and
negation-as-failure runs the prover registry back over its own argument (solve-goal).
The third, retract-sentex, is the teardown entry point a below-core solver
(vaelii.impl.asp.solve-context) reaches to retract a labeling artifact: the teardown
orchestration is core-private and has not been extracted below core, so this call runs up
rather than down for now. They are collected here so the set can be counted, and so
lein lint's E8 can fail a literal requiring-resolve anywhere else under src/ and
E19 any target beyond these three. Each is a delay over requiring-resolve rather
than a dynamic var; why is docs/namespaces.md, "The layering".
A namespace that merely sits above vaelii.core and calls back down to its public API is
not written here — a call that can point downward is made to point downward. Reading a
dump (vaelii.impl.io.import) recovers through vaelii.impl.recovery, the
predAllSpecified audit (vaelii.impl.predall) reads through vaelii.impl.provers, and the
functional_at_instant audit (vaelii.impl.fluent) reads through vaelii.impl.provers and
the node engine vaelii.impl.inference; all sit below vaelii.core, which requires them.
*defer-settle?* lives here too, because both sides of the assert recursion read it.
The calls that run *up* the engine's layering, gathered in one file. Every edge in the engine is a static require the compiler checks: kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core Three calls run the other way, and the static require graph cannot express any of them. Two are **genuine mutual recursion**: the cycle is in the *behaviour*, and no code motion removes it — the assert path reaches a mint that asserts (`assert-sentence`), and negation-as-failure runs the prover registry back over its own argument (`solve-goal`). The third, `retract-sentex`, is the teardown entry point a below-core solver (`vaelii.impl.asp.solve-context`) reaches to retract a labeling artifact: the teardown orchestration is core-private and has not been extracted below core, so this call runs up rather than down for now. They are collected here so the set can be counted, and so `lein lint`'s **E8** can fail a literal `requiring-resolve` anywhere else under `src/` and **E19** any target beyond these three. Each is a `delay` over `requiring-resolve` rather than a dynamic var; why is docs/namespaces.md, "The layering". A namespace that merely sits *above* `vaelii.core` and calls back down to its public API is **not** written here — a call that can point downward is made to point downward. Reading a dump (`vaelii.impl.io.import`) recovers through `vaelii.impl.recovery`, the `predAllSpecified` audit (`vaelii.impl.predall`) reads through `vaelii.impl.provers`, and the `functional_at_instant` audit (`vaelii.impl.fluent`) reads through `vaelii.impl.provers` and the node engine `vaelii.impl.inference`; all sit below `vaelii.core`, which requires them. `*defer-settle?*` lives here too, because both sides of the assert recursion read it.
When true, the assert path does not settle after storing — belief is left
un-reconciled for the caller to settle once, later. Three callers bind it:
vaelii.impl.skolem): the nested
(termOfUnit K E) assert is monotonic bookkeeping and the enclosing firing settles
once when it finishes, so settling per mint would be redundant churn — and worse,
would relabel belief inside the running chain (docs/skolem.md);Quasiquote to its constant
(vaelii.impl.quasiquote/reduce-in-conclusion), which is the same mint at the same
moment and defers for the same reason;with-deferred-settle / assert-many, which run a whole batch of asserts under it
and settle once at the end, so a bulk load pays one belief reconciliation instead of
N. Chaining still runs per assert (only the settle is deferred), so the final
settle sees the same stored state a per-assert settle would have, and order
independence guarantees the same beliefs.Retraction settles eagerly regardless — reviving a defeated default is not part of an assert batch.
When true, the assert path does **not** `settle` after storing — belief is left un-reconciled for the caller to settle once, later. Three callers bind it: - a rule firing minting a skolem NAT mid-fixpoint (`vaelii.impl.skolem`): the nested `(termOfUnit K E)` assert is monotonic bookkeeping and the enclosing firing settles once when it finishes, so settling per mint would be redundant churn — and worse, would relabel belief inside the running chain (docs/skolem.md); - a fired conclusion reducing a ground `Quasiquote` to its constant (`vaelii.impl.quasiquote/reduce-in-conclusion`), which is the same mint at the same moment and defers for the same reason; - `with-deferred-settle` / `assert-many`, which run a whole batch of asserts under it and settle once at the end, so a bulk load pays one belief reconciliation instead of N. Chaining still runs per assert (only the `settle` is deferred), so the final settle sees the same stored state a per-assert settle would have, and order independence guarantees the same beliefs. Retraction settles eagerly regardless — reviving a defeated default is not part of an assert batch.
(assert-sentence kb sentence context opts)vaelii.core/assert — store sentence in context under opts, returning its handle.
`vaelii.core/assert` — store `sentence` in `context` under `opts`, returning its handle.
(retract-sentex kb handle)vaelii.core/retract! — retract premise support for handle, tearing down
solely-supported sentexes and justifications and reversing their taxonomy / rule-index
effects; returns counts.
`vaelii.core/retract!` — retract premise support for `handle`, tearing down solely-supported sentexes and justifications and reversing their taxonomy / rule-index effects; returns counts.
(solve-goal kb goal context)vaelii.impl.provers/solve-goal — the registry's raw solution bindings for goal in
context.
`vaelii.impl.provers/solve-goal` — the registry's raw solution bindings for `goal` in `context`.
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 |