The dropped-conclusion ledger: what the derivation path refused to store, kept as a value a caller can read afterwards instead of thrown at whoever happened to be writing.
A namespace of its own because of who writes it. Two paths file entries and they
sit on opposite sides of the engine: the forward chainer
(vaelii.impl.chain) files a conclusion it dropped, and the prover registry
(vaelii.impl.provers) files an aggregate's numeric error — and the chainer is built
on the registry, so the registry cannot name it. The ledger reads nothing from
either, only (:violations kb) and (:chain-stats kb), so it sits below both and the
edge runs the one direction the layering allows.
Why a ledger rather than a throw: an entry is recorded from inside the semi-naive
fixpoint and from inside a relabel, and neither may abort — a definitional check that
aborted mid-fixpoint would leave belief half-computed, which is the failure the value-
first checks (vaelii.impl.checks) exist to avoid. So a violation is reported, and
the run continues without the conclusion.
The dropped-conclusion ledger: what the derivation path refused to store, kept as a value a caller can read afterwards instead of thrown at whoever happened to be writing. A namespace of its own because of **who writes it**. Two paths file entries and they sit on opposite sides of the engine: the forward chainer (`vaelii.impl.chain`) files a conclusion it dropped, and the prover registry (`vaelii.impl.provers`) files an aggregate's numeric error — and the chainer is built *on* the registry, so the registry cannot name it. The ledger reads nothing from either, only `(:violations kb)` and `(:chain-stats kb)`, so it sits below both and the edge runs the one direction the layering allows. Why a ledger rather than a throw: an entry is recorded from inside the semi-naive fixpoint and from inside a relabel, and neither may abort — a definitional check that aborted mid-fixpoint would leave belief half-computed, which is the failure the value- first checks (`vaelii.impl.checks`) exist to avoid. So a violation is *reported*, and the run continues without the conclusion.
(report kb entries)Append dropped-conclusion entries to the accumulating ledger, stamped with the chaining run that dropped them, and log each at :warn — a drop must be visible even to a caller who never reads the ledger (a bulk load polls nothing).
No !: this accumulates a report and destroys nothing, and the ledger it appends to is
emptied only by vaelii.core/clear-violations!, which does.
Append dropped-conclusion entries to the accumulating ledger, stamped with the chaining run that dropped them, and log each at :warn — a drop must be visible even to a caller who never reads the ledger (a bulk load polls nothing). No `!`: this accumulates a report and destroys nothing, and the ledger it appends to is emptied only by `vaelii.core/clear-violations!`, which does.
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 |