Bounded, read-only KB integrity reporting: the passes kb-integrity runs under a work
meter (vaelii.impl.budget). vaelii.core requires this namespace; it requires
predall and provers, which also sit below vaelii.core. vaelii.impl.quality
requires it too: its taxonomy, declaration and clash readings are taxonomy-coverage,
stranded-declarations and clash-pairs here, read over the whole KB. See
docs/integrity.md.
Bounded, read-only KB integrity reporting: the passes `kb-integrity` runs under a work meter (`vaelii.impl.budget`). `vaelii.core` requires this namespace; it requires `predall` and `provers`, which also sit below `vaelii.core`. `vaelii.impl.quality` requires it too: its taxonomy, declaration and clash readings are `taxonomy-coverage`, `stranded-declarations` and `clash-pairs` here, read over the whole KB. See docs/integrity.md.
(by-consequent rows)[polarity functor] -> rule rows — the pruning index a pairing reads, and the reason
neither pairing is a cross product over the rule set.
`[polarity functor] -> rule rows` — the pruning index a pairing reads, and the reason neither pairing is a cross product over the rule set.
(clash-pairs kb rows progress!)Rule pairs of rows whose consequents would clash if both fired and whose
antecedents could shallowly hold at once, as findings in content order:
{:rules [h1 h2] :kind :unifier :context :sentences :excepted}, one per maximal common
descendant of the two rules' contexts the pair clashes in. progress! is called as
clash-units says.
Static analysis of the rules, which is what makes it a different question from
(contradictions kb): nothing here is derived, nothing believed and nothing asked of the
KB's facts. A pair is a clash the rules admit, and whether it ever forms depends on
content nobody has asserted yet.
Rule pairs of `rows` whose consequents would clash if both fired and whose
antecedents could shallowly hold at once, as findings in content order:
`{:rules [h1 h2] :kind :unifier :context :sentences :excepted}`, one per maximal common
descendant of the two rules' contexts the pair clashes in. `progress!` is called as
`clash-units` says.
**Static analysis of the rules**, which is what makes it a different question from
`(contradictions kb)`: nothing here is derived, nothing believed and nothing asked of the
KB's facts. A pair is a clash the rules *admit*, and whether it ever forms depends on
content nobody has asserted yet.The options kb-integrity reads: three cooperative bounds and the categories to run.
The options `kb-integrity` reads: three cooperative bounds and the categories to run.
(kb-integrity kb candidate-terms context)(kb-integrity kb candidate-terms context options)Run the bounded integrity sweep in context over the finite set of ground
candidate-terms. Answers {:status :audited :candidate-count n :work w :elapsed-ms t}
when no pass finds anything, :status :gap with the non-empty categories otherwise, and
:status :truncated with its :reason, the :pass it stopped in and the findings kept
before a bound in options (integrity-opt-keys) ran out. Every answer carries the
:work spent and the :elapsed-ms. :categories, a set of category
keys, runs those passes alone; without it the sweep runs every pass but the
review-categories. Reads only: a diagnostic raised by
evaluating a condition goes to a sink local to the call, and the exception reader states
are kept for the call (except/with-reader-states). See docs/integrity.md.
Run the bounded integrity sweep in `context` over the finite set of ground
`candidate-terms`. Answers `{:status :audited :candidate-count n :work w :elapsed-ms t}`
when no pass finds anything, `:status :gap` with the non-empty categories otherwise, and
`:status :truncated` with its `:reason`, the `:pass` it stopped in and the findings kept
before a bound in `options` (`integrity-opt-keys`) ran out. Every answer carries the
`:work` spent and the `:elapsed-ms`. `:categories`, a set of category
keys, runs those passes alone; without it the sweep runs every pass but the
`review-categories`. Reads only: a diagnostic raised by
evaluating a condition goes to a sink local to the call, and the exception reader states
are kept for the call (`except/with-reader-states`). See docs/integrity.md.(rule-clash-findings kb contexts remaining review?)The clashing pairs among the stored rules each of contexts sees, in content order: the live
pairs no exceptWhen handles and no acknowledgedFinding names under :rule-clash, and
under :rule-clash-review (when review?) the pairs either rule of which is a
set/inertRule, marked :inert true, the :excepted ones, and the acknowledged ones,
marked with the reason as :acknowledged. An inert rule chains in neither engine, so
its pair is a clash the rules would admit if the rule were switched on, a suggestion
rather than a violation; an excepted pair is one the author already handled, and an
acknowledged one is a pair a reviewer looked at and keeps.
The rules are read off the rule extent in the union of the contexts' ancestor sets
(reads/as-stored-rules-in), as rule-macro-findings reads them, and paired once. A
pair is judged in each of contexts that sees both its rules, in print order, reported
with that context as :context, and an acknowledgment is read from there. The findings
are those of the one-context sweeps together, and the rules they share are paired once.
The clashing pairs among the stored rules each of `contexts` sees, in content order: the live pairs no `exceptWhen` handles and no `acknowledgedFinding` names under `:rule-clash`, and under `:rule-clash-review` (when `review?`) the pairs either rule of which is a `set/inertRule`, marked `:inert true`, the `:excepted` ones, and the acknowledged ones, marked with the reason as `:acknowledged`. An inert rule chains in neither engine, so its pair is a clash the rules would admit if the rule were switched on, a suggestion rather than a violation; an excepted pair is one the author already handled, and an acknowledged one is a pair a reviewer looked at and keeps. The rules are read off the rule extent in the union of the `contexts`' ancestor sets (`reads/as-stored-rules-in`), as `rule-macro-findings` reads them, and paired once. A pair is judged in each of `contexts` that sees both its rules, in print order, reported with that context as `:context`, and an acknowledgment is read from there. The findings are those of the one-context sweeps together, and the rules they share are paired once.
(rule-exception-conjuncts kb handle)The exceptWhen conjunctions in force for a rule, or nil. Read only for a rule the
watched-rule set holds, so an ordinary rule — every rule, on nearly every KB — pays one
O(1) membership read and no term lookup.
The `exceptWhen` conjunctions in force for a rule, or nil. Read only for a rule the watched-rule set holds, so an ordinary rule — every rule, on nearly every KB — pays one O(1) membership read and no term lookup.
(rule-rows kb handles progress!)Every rule of handles as a rule-row: the one record read per rule a pairing pays.
progress! is called with {:done i :total n} before the loop and every
progress-every rules.
A negated implication and a variable-functor consequent are dropped here: the first concludes nothing to cover or clash with, and the second concludes anything.
Every rule of `handles` as a `rule-row`: the one record read per rule a pairing pays.
`progress!` is called with `{:done i :total n}` before the loop and every
`progress-every` rules.
A negated implication and a variable-functor consequent are dropped here: the first
concludes nothing to cover or clash with, and the second concludes anything.(rule-variables forms)Every variable across a rule's patterns, sorted by name — so a renaming is a function of the rule's content rather than of a set's iteration order, and two loads of the same KB report the same substitution.
Every variable across a rule's patterns, **sorted by name** — so a renaming is a function of the rule's content rather than of a set's iteration order, and two loads of the same KB report the same substitution.
(stranded-declarations kb context progress!)Which argument constraints name a position their predicate does not have —
{:total n :stranded [entry …] :typed-thing [entry …]}, :total counting the
declarations walked and the :stranded entries
{:handle :sentence :context :predicate :position :arity :via :message} in content
order. :typed-thing lists, in the same order, the declarations that type a position
thing, each {:handle :sentence :context :facts} with :facts its predicate's stored
extent: a declaration typing thing mints nothing (arity/mintable-type?), so the
remedy is a narrower type in the declaration. With a context, only the declarations
it sees are walked; with nil, every stored one.
Enumerated, not probed per predicate. Declarations are vocabulary and vocabulary is
small, so reading all of them and asking each about its own predicate is cheaper than
asking each predicate what declares it, and it does not grow with the spec subtree
underneath. What it does grow with is the hierarchy above: arity/relation-length is
a binding read for a predicate carrying a length of its own and a walk of the supers for
one that inherits its length, so the walk is O(declarations × super-predicates).
Belief-filtered: a stored, disbelieved declaration constrains nothing for a reason that has nothing to do with its position, and listing it would name the wrong defect.
:message is the one checks wrote when it convicted, carried rather than
re-derived: a caller reading this map and a caller reading check's answer are told
the same thing in the same words, and there is no second wording to drift from it.
One membership reader per context met: a reader memoizes for the life of one caller, so
building one per declaration pays the retrieval every time and throws the memo away
unread. progress! is called with {:done 0 :total n} once the declarations are
known.
Which argument constraints name a position their predicate does not have —
`{:total n :stranded [entry …] :typed-thing [entry …]}`, `:total` counting the
declarations walked and the `:stranded` entries
`{:handle :sentence :context :predicate :position :arity :via :message}` in content
order. `:typed-thing` lists, in the same order, the declarations that type a position
`thing`, each `{:handle :sentence :context :facts}` with `:facts` its predicate's stored
extent: a declaration typing `thing` mints nothing (`arity/mintable-type?`), so the
remedy is a narrower type in the declaration. With a `context`, only the declarations
it sees are walked; with nil, every stored one.
**Enumerated, not probed per predicate.** Declarations are vocabulary and vocabulary is
small, so reading all of them and asking each about its own predicate is cheaper than
asking each predicate what declares it, and it does not grow with the spec subtree
underneath. What it does grow with is the hierarchy *above*: `arity/relation-length` is
a binding read for a predicate carrying a length of its own and a walk of the supers for
one that inherits its length, so the walk is `O(declarations × super-predicates)`.
Belief-filtered: a stored, disbelieved declaration constrains nothing for a reason that
has nothing to do with its position, and listing it would name the wrong defect.
`:message` is the one `checks` wrote when it convicted, **carried rather than
re-derived**: a caller reading this map and a caller reading `check`'s answer are told
the same thing in the same words, and there is no second wording to drift from it.
One membership reader per context met: a reader memoizes for the life of one caller, so
building one per declaration pays the retrieval every time and throws the memo away
unread. `progress!` is called with `{:done 0 :total n}` once the declarations are
known.(taxonomy-coverage kb type-names progress!)Two numbers, not one: how many type names carry a genl edge at all, and how many
reach the root — {:names :edged :root :rooted :islands}, read from every context.
:islands is the edged types that do not reach the root, the :taxonomy-island
findings counted, and the gap between the two numbers is the finding.
type-names is the denominator's vocabulary: every type-shaped name, which by
docs/naming.md includes a bare lowercase word (likes is a legal predicate and a
legal type name), filtered as the nodes are. progress! is taxonomy-reach's.
Two numbers, not one: how many type names carry a `genl` edge at all, and how many
reach the root — `{:names :edged :root :rooted :islands}`, read from every context.
`:islands` is the edged types that do not reach the root, the `:taxonomy-island`
findings counted, and **the gap between the two numbers is the finding**.
`type-names` is the denominator's vocabulary: every type-shaped name, which by
`docs/naming.md` includes a bare lowercase word (`likes` is a legal predicate *and* a
legal type name), filtered as the nodes are. `progress!` is `taxonomy-reach`'s.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 |