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
Five targets are reached the other way, and the static require graph cannot express any
of them. Four are genuine mutual recursion, where the cycle is in the behaviour and
no code motion removes it: the assert path reaches a mint that asserts
(assert-sentence); negation-as-failure runs the prover registry back over its own
argument (solve-goal); the exception read walk asks the claim walk for a second route,
and the claim walk reads facts through the exception read walk (route-reach,
firing-goals, goal-reach); and a KB's open replays its operation log through the
write entry points of vaelii.core (replay-op). The fifth, retract-sentex, is the
teardown entry point a below-core solver reaches while the teardown orchestration is
core-private. lein lint's E8 fails a literal requiring-resolve anywhere else
under src/, E19 any target beyond these five, and E20 a namespace that installs
a function into a lower namespace's slot at load instead of appearing here. Each entry
is a delay over requiring-resolve rather than a dynamic var. See docs/namespaces.md,
"The layering".
*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 Five targets are reached the other way, and the static require graph cannot express any of them. Four are **genuine mutual recursion**, where the cycle is in the *behaviour* and no code motion removes it: the assert path reaches a mint that asserts (`assert-sentence`); negation-as-failure runs the prover registry back over its own argument (`solve-goal`); the exception read walk asks the claim walk for a second route, and the claim walk reads facts through the exception read walk (`route-reach`, `firing-goals`, `goal-reach`); and a KB's open replays its operation log through the write entry points of `vaelii.core` (`replay-op`). The fifth, `retract-sentex`, is the teardown entry point a below-core solver reaches while the teardown orchestration is core-private. `lein lint`'s **E8** fails a literal `requiring-resolve` anywhere else under `src/`, **E19** any target beyond these five, and **E20** a namespace that installs a function into a lower namespace's slot at load instead of appearing here. Each entry is a `delay` over `requiring-resolve` rather than a dynamic var. See docs/namespaces.md, "The layering". `*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
(natFormula 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);vaelii.impl.chain/reify-conclusion), a reduced Quasiquote's (Quote E) among
them, which is the same mint inside the same fixpoint 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 `(natFormula 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 placed conclusion minting the constants of its ground reifiable NATs (`vaelii.impl.chain/reify-conclusion`), a reduced `Quasiquote`'s `(Quote E)` among them, which is the same mint inside the same fixpoint 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.
(firing-goals kb j)[goals stated] for the rule firing j: the goals it matched through a reach and the
antecedent handles that state a literal, or nil when it reads no goal off j.
`[goals stated]` for the rule firing `j`: the goals it matched through a reach and the antecedent handles that state a literal, or nil when it reads no goal off `j`.
(goal-reach kb goal reader)Does reader reach the ground goal from a claim it reads?
Does `reader` reach the ground `goal` from a claim it reads?
(replay-op op)The function a logged frame of operation op runs through, or nil when vaelii.core
records no such operation.
The function a logged frame of operation `op` runs through, or nil when `vaelii.core` records no such operation.
(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.
(route-reach kb rel a b reader)Does reader reach b from a over the fact relation rel a transitiveInArgInverse
preserves a claim along?
Does `reader` reach `b` from `a` over the fact relation `rel` a `transitiveInArgInverse` preserves a claim along?
(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 |