Narrowing the exceptWhen re-check to the firings a trigger can reach: a memory-only
filter over a queued rule's firings and recorded refusals, run before any level-6
query, in which every "cannot tell" answers keep. A settle pass reads it through
exception-blocked-set and released-refusals. See docs/exceptions.md, "Narrowing
the re-check to the firings a trigger can reach".
Narrowing the `exceptWhen` re-check to the firings a trigger can reach: a memory-only filter over a queued rule's firings and recorded refusals, run before any level-6 query, in which every "cannot tell" answers keep. A settle pass reads it through `exception-blocked-set` and `released-refusals`. See docs/exceptions.md, "Narrowing the re-check to the firings a trigger can reach".
(exception-blocked-set kb queued)(exception-blocked-set kb _queued cands)The blocked set after re-deciding, for each of exception-candidates' firings,
whether an except hides an antecedent or something the rule carries blocks the firing
(chain/justification-excepted?): a block outside the candidates is carried forward.
The whole set, since jtms/set-blocked replaces rather than adds; the caller adds the
rule-carried withdrawals. cands is exception-candidates' answer for queued, when
the caller holds it.
The blocked set after re-deciding, for each of `exception-candidates`' firings, whether an `except` hides an antecedent or something the rule carries blocks the firing (`chain/justification-excepted?`): a block outside the candidates is carried forward. The whole set, since `jtms/set-blocked` replaces rather than adds; the caller adds the rule-carried withdrawals. `cands` is `exception-candidates`' answer for `queued`, when the caller holds it.
(exception-candidates kb queued)The justifications of the queued rules whose block condition the queued triggers could
have flipped. One record fetch per rule, and none for a rule queued :all, which
keeps every firing. The block literals are the exception conjuncts read through
their query frames (rules/watched-literals), the NAF inner queries and the aggregate
bodies (docs/naf.md). A withdrawal marker adds the firings its own test keeps
(entailment-candidates, preserving-candidates, except-candidates, and
firings-naming for a separation's types and a merge's class), and ::computed
keeps every firing. A different-only rule's triggers narrow to the firings naming
the terms they moved (special/different-rechecked-terms).
One question memo (inherit/with-memo) holds every marker's moved-goal-test reads:
the markers one settle pass queues share their terms, and a genl edge into a broad
type reads that type's whole reach, which a memo per marker read again for each edge.
The re-check moves no belief, so the memo needs no invalidation.
The justifications of the queued rules whose block condition the queued triggers could have flipped. One record fetch per rule, and none for a rule queued `:all`, which keeps every firing. The block literals are the exception conjuncts read through their query frames (`rules/watched-literals`), the NAF inner queries and the aggregate bodies (docs/naf.md). A withdrawal marker adds the firings its own test keeps (`entailment-candidates`, `preserving-candidates`, `except-candidates`, and `firings-naming` for a separation's types and a merge's class), and `::computed` keeps every firing. A `different`-only rule's triggers narrow to the firings naming the terms they moved (`special/different-rechecked-terms`). One question memo (`inherit/with-memo`) holds every marker's `moved-goal-test` reads: the markers one settle pass queues share their terms, and a `genl` edge into a broad type reads that type's whole reach, which a memo per marker read again for each edge. The re-check moves no belief, so the memo needs no invalidation.
(released-refusals kb queued)The recorded refusals the queued triggers may have released: {:free [[rule-handle entry] …] :overflow [rule-handle …]}. Narrowed as exception-candidates narrows
justifications. A dead entry is dropped as it is read, and an overflowed rule is named
for the caller to re-join (docs/exceptions.md, "A refused firing is remembered as
bindings").
The recorded refusals the queued triggers may have released: `{:free [[rule-handle
entry] …] :overflow [rule-handle …]}`. Narrowed as `exception-candidates` narrows
justifications. A dead entry is dropped as it is read, and an overflowed rule is named
for the caller to re-join (docs/exceptions.md, "A refused firing is remembered as
bindings").(withdrawal-marker? t)Is queued trigger t one of special's withdrawal markers rather than a sentence?
Is queued trigger `t` one of `special`'s withdrawal markers rather than a sentence?
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 |