A rule is a sentex — same structure (sentence + context), different indexing. Its sentence is an implication:
(implies (and <antecedent> ...) <consequent>) ; single antecedent needs no and
Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free.
Rules must be range-restricted: every consequent variable appears in some
antecedent, so a fired consequent is ground. The one exemption is a head
existential — a consequent variable explicitly marked (exists ?y C), which
forward firing skolemizes to a deterministic constant (docs/skolem.md); range
restriction permits only the marked variable and still rejects any accidentally
unbound one. The same closure is required of an exceptWhen exception, which is a
query rather than a conclusion but must be ground for the same reason (checked at the
assert layer via sentex/check-exception-closed).
A rule *is* a sentex — same structure (sentence + context), different indexing. Its sentence is an implication: (implies (and <antecedent> ...) <consequent>) ; single antecedent needs no `and` Antecedents and consequent are sentence patterns that may contain variables. Rules are indexed by their antecedent/consequent predicates (see the index store) so forward chaining finds candidate rules without scanning, and — being ordinary sentexes — they get handles, TMS support, and retraction for free. Rules must be range-restricted: every consequent variable appears in some antecedent, so a fired consequent is ground. The one exemption is a **head existential** — a consequent variable explicitly marked `(exists ?y C)`, which forward firing skolemizes to a deterministic constant (docs/skolem.md); range restriction permits only the marked variable and still rejects any *accidentally* unbound one. The same closure is required of an `exceptWhen` exception, which is a query rather than a conclusion but must be ground for the same reason (checked at the assert layer via `sentex/check-exception-closed`).
(aggregate-antecedents sentex)The aggregate antecedent literals of a stored rule.
The aggregate antecedent literals of a stored rule.
(aggregate-antecedents-of rule-sentence)The aggregate antecedent literals of a raw rule sentence — for the checks that run before a rule is stored as a sentex (stratification).
The aggregate antecedent literals of a raw rule *sentence* — for the checks that run before a rule is stored as a sentex (stratification).
(aggregate-predicates sentex)The predicates a stored rule's aggregate bodies mention.
The predicates a stored rule's aggregate bodies mention.
(aggregate-predicates-of rule-sentence)The predicates a raw rule sentence's aggregate bodies mention — the negative-edge keys the stratification graph reads, and the re-check keys the index posts under.
The predicates a raw rule *sentence*'s aggregate bodies mention — the negative-edge keys the stratification graph reads, and the re-check keys the index posts under.
(aggregate-queries sentex)The body queries of a rule's aggregate antecedents, so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts. Each mentions the reduction variable by construction, so none of them is ground and every one falls through to 'keep' — an aggregate's firings are never narrowed away, which is the safe direction.
The body queries of a rule's aggregate antecedents, so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts. Each mentions the reduction variable by construction, so none of them is ground and every one falls through to 'keep' — an aggregate's firings are never narrowed away, which is the safe direction.
(antecedents sentence)The antecedent patterns of a rule sentence (unwrapping a leading and).
The antecedent patterns of a rule sentence (unwrapping a leading `and`).
(assumption? sentex)Is this stored rule sentex a set/assumptionRule — a choice rule whose head a solve
decides rather than the chainer deriving? Read straight off the record's
:assumption field, like :defeasible (docs/solving.md).
Is this stored rule sentex a `set/assumptionRule` — a choice rule whose head a solve decides rather than the chainer deriving? Read straight off the record's `:assumption` field, like `:defeasible` (docs/solving.md).
(backward-sentex? sentex)Does this stored rule sentex backward-chain? An assumptionRule / constraint rule
does not (see forward-sentex?).
Does this stored rule sentex backward-chain? An `assumptionRule` / constraint rule does not (see `forward-sentex?`).
(check-indexable-functors sentence)Throw :type :not-indexable when a literal of the rule sentence puts a variable in
functor position.
The rule index is keyed by predicate, and a variable names none. Canonicalization
numbers the functor to ?var0 before the rule is indexed, so the postings land under a
key no arriving fact and no goal can ever spell: chain/fire-rules-for reads the
arriving fact's functor and its genls, resolution/concluding-rule-handles reads the
goal's predicate and its specs, and neither can produce a canonical variable. The rule
answers no backward goal at all, and fires forward only when a concrete-predicate
antecedent beside it arrives — so (transitive foo) before the facts derives nothing,
and after them joins over whatever happens to be stored at that instant. Two arrival
orders, two answers, from a rule the engine reported as accepted.
The workaround the message names is the instantiated rule: one rule per predicate the metarule was meant to range over, each with a functor the index can read.
An :inert rule is exempt at the caller (core/check-rule-sentence): it runs in
neither engine by construction, so it claims nothing the index has to honour.
Throw `:type :not-indexable` when a literal of the rule `sentence` puts a variable in functor position. **The rule index is keyed by predicate**, and a variable names none. Canonicalization numbers the functor to `?var0` before the rule is indexed, so the postings land under a key no arriving fact and no goal can ever spell: `chain/fire-rules-for` reads the arriving fact's functor and its `genls`, `resolution/concluding-rule-handles` reads the goal's predicate and its specs, and neither can produce a canonical variable. The rule answers no backward goal at all, and fires forward only when a *concrete*-predicate antecedent beside it arrives — so `(transitive foo)` before the facts derives nothing, and after them joins over whatever happens to be stored at that instant. Two arrival orders, two answers, from a rule the engine reported as accepted. The workaround the message names is the instantiated rule: one rule per predicate the metarule was meant to range over, each with a functor the index can read. An `:inert` rule is exempt at the caller (`core/check-rule-sentence`): it runs in neither engine by construction, so it claims nothing the index has to honour.
(check-range-restricted antecedents consequent)Throw :type :not-range-restricted unless every consequent variable is bound by
some antecedent (and the consequent is a well-formed conclusion).
Uses ex-info, not clojure.core/assert: an elidable check under *assert* false
would store the junk rule silently — the exact failure check-ground exists to
prevent — and an AssertionError carries no :type for callers to discriminate
on.
Throw `:type :not-range-restricted` unless every consequent variable is bound by some antecedent (and the consequent is a well-formed conclusion). Uses `ex-info`, not `clojure.core/assert`: an elidable check under `*assert*` false would store the junk rule *silently* — the exact failure `check-ground` exists to prevent — and an `AssertionError` carries no `:type` for callers to discriminate on.
(consequent-predicate sentence)The predicate a rule concludes. A consequent of the form (ist Ctx S) (place S
into context Ctx) is indexed by S's predicate, not by ist.
A generator concludes a rule, so its key is implies — reached by peeling the
set/*Rule wrapper first, because that wrapper belongs to the rule being stamped
rather than to the generator (docs/generators.md). Without the peel one generator
files under set/defaultRule and the next under implies, by nothing more than how
its stamped rule happened to be written, and the single cell that answers which rules
are generators would answer for some of them.
The predicate a rule concludes. A consequent of the form `(ist Ctx S)` (place S into context Ctx) is indexed by S's predicate, not by ist. A **generator** concludes a rule, so its key is `implies` — reached by peeling the `set/*Rule` wrapper first, because that wrapper belongs to the rule being stamped rather than to the generator (docs/generators.md). Without the peel one generator files under `set/defaultRule` and the next under `implies`, by nothing more than how its stamped rule happened to be written, and the single cell that answers *which rules are generators* would answer for some of them.
(constraint-of sentex)The constraint class of this stored rule sentex — :hard / :soft from its
set/hardConstraint / set/softConstraint wrapper, or nil for an ordinary rule.
Read straight off the record's :constraint field (docs/solving.md).
The constraint class of this stored rule sentex — `:hard` / `:soft` from its `set/hardConstraint` / `set/softConstraint` wrapper, or nil for an ordinary rule. Read straight off the record's `:constraint` field (docs/solving.md).
(constraint? sentex)Is this stored rule sentex a set/hardConstraint / set/softConstraint — a
contradiction rule whose conjunctive body a solve grounds into a nogood?
Is this stored rule sentex a `set/hardConstraint` / `set/softConstraint` — a contradiction rule whose conjunctive body a solve grounds into a nogood?
(expand-consequent sentence)Polycanonicalize a rule that concludes a conjunction into one rule per conjunct,
preserving any virtual wrapper (default / forward / backward / inert / assumptionRule).
A rule (implies A (and C1 C2)) becomes [(implies A C1) (implies A C2)]; anything
else (a non-rule, or a rule with a single consequent) returns [sentence] unchanged.
Runs on a rule whose exceptWhen has already been split off (split-exceptWhen), so
the exception is re-attached once per conjunct by the caller, against each conjunct's
own handle.
Polycanonicalize a rule that concludes a conjunction into one rule per conjunct, preserving any virtual wrapper (default / forward / backward / inert / assumptionRule). A rule `(implies A (and C1 C2))` becomes `[(implies A C1) (implies A C2)]`; anything else (a non-rule, or a rule with a single consequent) returns `[sentence]` unchanged. Runs on a rule whose exceptWhen has already been split off (`split-exceptWhen`), so the exception is re-attached once per conjunct by the caller, against each conjunct's own handle.
(forward-sentex? sentex)Does this stored rule sentex forward-chain? Read off the record, which carries
the direction its set/*Rule wrapper set. An assumptionRule (a choice head) and a
hard/softConstraint (a contradiction marker) never chain — their heads are decided
or forbidden by a solve, not derived — so they are inference-inert in both directions
regardless of the direction they were written with.
Does this stored rule sentex forward-chain? Read off the record, which carries the direction its `set/*Rule` wrapper set. An `assumptionRule` (a choice head) and a `hard`/`softConstraint` (a contradiction marker) never chain — their heads are decided or forbidden by a solve, not derived — so they are inference-inert in both directions regardless of the direction they were written with.
(generated-rule consequent)The bare rule form a generator's consequent stamps out — the (implies …) inside
whatever set/*Rule wrapper the author put on it — or nil when the consequent
concludes a fact, which is every ordinary rule.
The wrapper is peeled here and kept by the caller that mints: it sets the stamped rule's direction, which is the only place a direction can be written for a rule nobody types out.
The bare rule form a generator's `consequent` stamps out — the `(implies …)` inside whatever `set/*Rule` wrapper the author put on it — or nil when the consequent concludes a fact, which is every ordinary rule. The wrapper is peeled here and *kept* by the caller that mints: it sets the **stamped** rule's direction, which is the only place a direction can be written for a rule nobody types out.
(generator-sentex? sentex)Is this stored rule sentex a generator? Read off the record's :consequent, which
is where the canonicalized rule kept it.
Is this stored rule sentex a generator? Read off the record's `:consequent`, which is where the canonicalized rule kept it.
(generator? sentence)Is this rule sentence a generator — does it conclude a rule?
Is this rule *sentence* a generator — does it conclude a rule?
(has-aggregate? sentex)Does this rule carry any aggregate antecedent?
Does this rule carry any aggregate antecedent?
(has-naf? sentex)Does this rule carry any unknown antecedent?
Does this rule carry any `unknown` antecedent?
(holes antecedents generated)The variables a generator's stamped rule takes from the firing — those its
enclosing antecedents also mention, as a set.
Computed rather than declared, which is the whole reason a generator needs no vocabulary of its own: sharing a variable name with the antecedents is how an author says "fill this in", and the remaining variables are the stamped rule's own by the same token. Two spellings cannot disagree, because there is only one.
The variables a generator's stamped rule takes from the firing — those its enclosing `antecedents` also mention, as a set. Computed rather than declared, which is the whole reason a generator needs no vocabulary of its own: sharing a variable name with the antecedents *is* how an author says "fill this in", and the remaining variables are the stamped rule's own by the same token. Two spellings cannot disagree, because there is only one.
(inner-rule sentence)The bare (implies …) inside any virtual rule wrappers (set/*Rule and
exceptWhen, which may nest in any order — a defeasible forward rule with an
exception). The direction / default / assumption wrappers become record fields and
the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work
on this.
The bare `(implies …)` inside any virtual rule wrappers (`set/*Rule` and `exceptWhen`, which may nest in any order — a defeasible forward rule with an exception). The direction / default / assumption wrappers become record fields and the exceptWhen becomes a meta-sentex, so the checks and the stored sentence both work on this.
(naf-antecedents sentex)The (unknown S) antecedent literals of a stored rule — its negation-as-failure
conditions.
The `(unknown S)` antecedent literals of a stored rule — its negation-as-failure conditions.
(naf-antecedents-of rule-sentence)The (unknown S) antecedent literals of a raw rule sentence — for the checks
that run before a rule is stored as a sentex (stratification).
The `(unknown S)` antecedent literals of a raw rule *sentence* — for the checks that run before a rule is stored as a sentex (stratification).
(naf-predicates sentex)The predicates a rule's unknown antecedents mention — the keys the re-check index
posts the rule under, so a fact arriving or leaving on one re-evaluates the NAF
condition. The exception analogue is exception-predicates; both feed the same
[:exception-index …] index.
The predicates a rule's `unknown` antecedents mention — the keys the re-check index posts the rule under, so a fact arriving or leaving on one re-evaluates the NAF condition. The exception analogue is `exception-predicates`; both feed the same `[:exception-index …]` index.
(naf-predicates-of rule-sentence)The predicates a raw rule sentence's unknown antecedents mention — for the
stratification check on a rule not yet stored (the mirror of the exception's
negative dependence).
The predicates a raw rule *sentence*'s `unknown` antecedents mention — for the stratification check on a rule not yet stored (the mirror of the exception's negative dependence).
(naf-queries sentex)The inner query literals of a rule's unknown antecedents (each conjunct, unwrapped
past a thereExists), so the settle-time firing filter can shape them against a
trigger exactly as it shapes an exception's conjuncts — the ground ones narrow, the
existential ones fall through to 'keep' like any non-flat conjunct.
The inner query literals of a rule's `unknown` antecedents (each conjunct, unwrapped past a `thereExists`), so the settle-time firing filter can shape them against a trigger exactly as it shapes an exception's conjuncts — the ground ones narrow, the existential ones fall through to 'keep' like any non-flat conjunct.
(post-join-antecedents sentex)post-join-literals over a stored rule's antecedents.
`post-join-literals` over a stored rule's antecedents.
(post-join-literals antes)The antecedent literals evaluated after the join: every aggregate, plus every
deferred literal reading a variable an aggregate produces — or that one of those
produces in turn, so an (evaluate ?d (+ ?n 1)) carries a later (lessThan ?d 9)
along with it.
In written order, which is the order they run in, because a computed literal
reads what is written before it. That is not a rule aggregates introduce: an
evaluate chain has always had to be written downhill, since canonical order holds a
deferred literal in the author's position and every chainer runs it there. Making an
aggregate an exception — reordering the phase so a comparison could be written above
its own count — is what a forward chainer could do and a backward one could not, so
it would buy convenience at the price of the two disagreeing about one rule.
sentex/check-naf-closed refuses the uphill writing instead.
unknown is deliberately not here: it binds nothing, so it never needs the ordering,
and it is already evaluated per placement as :naf.
Asked on every join, so the gate is a short-circuiting some that allocates
nothing: no aggregate, no post-join phase, and the overwhelming majority of rules
have none.
The antecedent literals evaluated **after** the join: every aggregate, plus every deferred literal reading a variable an aggregate produces — or that one of *those* produces in turn, so an `(evaluate ?d (+ ?n 1))` carries a later `(lessThan ?d 9)` along with it. **In written order**, which is the order they run in, because a computed literal reads what is written before it. That is not a rule aggregates introduce: an `evaluate` chain has always had to be written downhill, since canonical order holds a deferred literal in the author's position and every chainer runs it there. Making an aggregate an exception — reordering the phase so a comparison could be written above its own count — is what a *forward* chainer could do and a backward one could not, so it would buy convenience at the price of the two disagreeing about one rule. `sentex/check-naf-closed` refuses the uphill writing instead. `unknown` is deliberately not here: it binds nothing, so it never needs the ordering, and it is already evaluated per placement as `:naf`. Asked on **every** join, so the gate is a short-circuiting `some` that allocates nothing: no aggregate, no post-join phase, and the overwhelming majority of rules have none.
(range-problems antecedents consequent)Why antecedents => consequent is not range-restricted, as a seq of problem
strings — empty when the rule is fine. The value form, like the wff arms:
a caller that refuses wraps it in a throw, and a fixpoint that must not abort
can record it instead.
A head existential (exists ?y C) exempts only its marked variable(s): the
check runs over the inner C, and every consequent variable that is neither
antecedent-bound nor existentially marked is still a problem — so an accidental
typo is caught while a deliberate ∃ is allowed (docs/skolem.md).
A generator is checked one level in, and the two claims are about different rules. The generator's own range restriction is vacuous — its consequent is a rule rather than a conclusion, and the stamped rule's free variables are unbound on purpose — so what is checked is the stamped rule's, with the holes counted as bound because substitution makes them ground before anything is stored. Checking it here rather than at firing is what makes the refusal reach the author: a generator that can only ever stamp junk is refused where it is written, not once per binding at the far end of a fixpoint.
Why `antecedents => consequent` is not range-restricted, as a seq of problem strings — empty when the rule is fine. The value form, like the wff arms: a caller that refuses wraps it in a throw, and a fixpoint that must not abort can record it instead. A head existential `(exists ?y C)` exempts **only** its marked variable(s): the check runs over the inner `C`, and every consequent variable that is neither antecedent-bound nor existentially marked is still a problem — so an accidental typo is caught while a deliberate `∃` is allowed (docs/skolem.md). A **generator** is checked one level in, and the two claims are about *different* rules. The generator's own range restriction is vacuous — its consequent is a rule rather than a conclusion, and the stamped rule's free variables are unbound on purpose — so what is checked is the **stamped** rule's, with the holes counted as bound because substitution makes them ground before anything is stored. Checking it here rather than at firing is what makes the refusal reach the author: a generator that can only ever stamp junk is refused where it is written, not once per binding at the far end of a fixpoint.
(recheck-predicates sentex)The predicates whose change must re-check this rule for its own re-check
conditions — the predicates its unknown antecedents and its aggregate bodies
mention. (An exceptWhen exception is a separate meta-sentex, registered under its
rule by the meta-sentex's own indexing; it is not read off the rule.) The key set
the [:exception-index …] index posts a rule under when it is indexed.
The two kinds are one key set because they are one problem: both read what the KB believes at firing time rather than a fact the justification names, so both need a fact arriving on those predicates to bring the firing back for re-decision.
The predicates whose change must re-check this rule for its **own** re-check conditions — the predicates its `unknown` antecedents and its **aggregate** bodies mention. (An exceptWhen exception is a separate meta-sentex, registered under its rule by the meta-sentex's own indexing; it is not read off the rule.) The key set the `[:exception-index …]` index posts a rule under when it is indexed. The two kinds are one key set because they are one problem: both read what the KB believes at firing time rather than a fact the justification names, so both need a fact arriving on those predicates to bring the firing back for re-decision.
(rechecked? sentex)Does this rule carry a re-check condition of its own — an unknown antecedent
or an aggregate? The gate on registering it in the re-check index; an exceptWhen
exception is registered by its own meta-sentex and is not read off the rule.
Does this rule carry a re-check condition of its **own** — an `unknown` antecedent or an aggregate? The gate on registering it in the re-check index; an exceptWhen exception is registered by its own meta-sentex and is not read off the rule.
(rewrap sentence direction defeasible assumption constraint)Put the direction / default / assumption / constraint wrappers a rule was written
with back around sentence — the inverse of sx/peel-rule-wrapper, since the
wrappers ride the record, not the stored sentence. Two callers: a polycanonicalized
conjunct keeps the mode of the rule it came from, and an equality merge's migrated
rule twin keeps the mode of the rule it restates (special/migrate-sentex). An
exceptWhen is not among them — it is split off before this runs and stored as a
meta-sentex against each conjunct's handle (split-exceptWhen).
Put the direction / default / assumption / constraint wrappers a rule was written with back around `sentence` — the inverse of `sx/peel-rule-wrapper`, since the wrappers ride the record, not the stored sentence. Two callers: a polycanonicalized conjunct keeps the mode of the rule it came from, and an equality merge's migrated rule twin keeps the mode of the rule it restates (`special/migrate-sentex`). An exceptWhen is not among them — it is split off before this runs and stored as a meta-sentex against each conjunct's handle (`split-exceptWhen`).
(rule-sentence antecedents consequent)Build a rule sentence from antecedent patterns and a consequent pattern.
One spelling for the whole codebase — see sentex/rule-sentence.
Build a rule sentence from antecedent patterns and a consequent pattern. One spelling for the whole codebase — see `sentex/rule-sentence`.
(rule-sentence? sentence)Is sentence a rule form (implies <ante> <conseq>)?
Is `sentence` a rule form `(implies <ante> <conseq>)`?
(split-exceptWhen sentence)Split an (exceptWhen <query> <rule>) assertion into [exception inner].
exception is the flattened conjunction of every exceptWhen wrapper (a vector of
literals in the author's variable names, block-if-all-hold), and inner is what the
exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its
direction / default / assumption wrappers intact, or the (sentexHandle H) a
bare-handle exceptWhen named. [nil sentence] when there is no exceptWhen.
This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert
layer stores inner as the rule (or resolves the handle) and the exception as
(exceptWhen <aligned-query> (sentexHandle H)) against it.
Split an `(exceptWhen <query> <rule>)` assertion into `[exception inner]`. `exception` is the flattened conjunction of every exceptWhen wrapper (a vector of literals in the author's variable names, block-if-all-hold), and `inner` is what the exceptWhen qualifies: the wrapped rule with its exceptWhen(s) stripped but its direction / default / assumption wrappers intact, or the `(sentexHandle H)` a bare-handle exceptWhen named. `[nil sentence]` when there is no exceptWhen. This is the layer at which an exceptWhen becomes a separate meta-sentex: the assert layer stores `inner` as the rule (or resolves the handle) and the exception as `(exceptWhen <aligned-query> (sentexHandle H))` against it.
(variable-functor-literals sentence)The [role literal] pairs of a rule whose functor is a variable — (?p ?x ?y),
or the dotted rest (?pred . ?args). Read through naming/applied-literals, so the
frames descended into are the ones the naming check descends: a negated antecedent, an
ist consequent, a head existential, an aggregate's body.
Inside a generator's stamped rule the question is asked of non-holes only, and that is the carve the whole feature rests on. The index's claim is on what gets stored as a rule; a stamped rule is a pattern, and what gets stored is the mint — checked in its own right, by this function, when it is minted. A hole in functor position is therefore fine, because substitution makes it concrete before anything is keyed on it, and that is what lets one generator range over a family of predicates while every rule the index ever sees has a concrete functor.
A stamped variable functor that is not a hole is refused as loudly as any other, and it has to be: nothing will ever bind it, so every mint it produces is the accepted-and-inert rule this check exists to keep out — and refusing it here names the generator, where refusing it at the mint would name a rule the author never wrote.
The `[role literal]` pairs of a rule whose functor is a **variable** — `(?p ?x ?y)`, or the dotted rest `(?pred . ?args)`. Read through `naming/applied-literals`, so the frames descended into are the ones the naming check descends: a negated antecedent, an `ist` consequent, a head existential, an aggregate's body. Inside a generator's stamped rule the question is asked of **non-holes only**, and that is the carve the whole feature rests on. The index's claim is on what gets stored as a rule; a stamped rule is a pattern, and what gets stored is the mint — checked in its own right, by this function, when it is minted. A **hole** in functor position is therefore fine, because substitution makes it concrete before anything is keyed on it, and that is what lets one generator range over a family of predicates while every rule the index ever sees has a concrete functor. A stamped variable functor that is *not* a hole is refused as loudly as any other, and it has to be: nothing will ever bind it, so every mint it produces is the accepted-and-inert rule this check exists to keep out — and refusing it here names the generator, where refusing it at the mint would name a rule the author never wrote.
(watched-literals q)The literals a re-check must actually watch for the query literal q — the frames
peeled off until what is left is something a fact can carry.
A query operator's own functor is not one: no sentex is stored under unknown,
thereExists or agg/count, so a rule registered in the re-check index under one is
registered under a predicate nothing ever arrives on, and no fact can ever queue it.
The condition would then be evaluated correctly and re-evaluated never, which reads as
a guard that holds whatever happens.
So each frame yields what it reads: an unknown its conjuncts (recursively — a
conjunction is watched conjunct by conjunct, since it starts holding when the last
of them does), a thereExists its body, an aggregate its census body. Anything else
is a literal a fact can carry, and is watched as itself.
A not frame is deliberately not peeled: the trigger side keys an arriving
(not S) under not too (special/recheck-on-sentence reads the sentence's own
functor), so the two agree — coarsely, one bucket for every negated condition, but
they agree, and peeling one side alone is what would break it.
One function for both readers: an unknown antecedent's query, and an exceptWhen
conjunct — which may itself be any of these, exceptWhen's query being any closed
level-6 goal.
The literals a re-check must actually watch for the query literal `q` — the frames peeled off until what is left is something a *fact* can carry. A query operator's own functor is not one: no sentex is stored under `unknown`, `thereExists` or `agg/count`, so a rule registered in the re-check index under one is registered under a predicate nothing ever arrives on, and no fact can ever queue it. The condition would then be evaluated correctly and re-evaluated never, which reads as a guard that holds whatever happens. So each frame yields what it reads: an `unknown` its conjuncts (recursively — a conjunction is watched conjunct by conjunct, since it starts holding when the *last* of them does), a `thereExists` its body, an aggregate its census body. Anything else is a literal a fact can carry, and is watched as itself. A `not` frame is deliberately **not** peeled: the trigger side keys an arriving `(not S)` under `not` too (`special/recheck-on-sentence` reads the sentence's own functor), so the two agree — coarsely, one bucket for every negated condition, but they agree, and peeling one side alone is what would break it. One function for both readers: an `unknown` antecedent's query, and an `exceptWhen` conjunct — which may itself be any of these, `exceptWhen`'s query being any closed level-6 goal.
(watched-predicates queries)The predicates a re-check keys queries under — watched-literals of each, then its
functor. What exceptWhen's three registration sites and the stratification graph
read of an exception's conjuncts, and what naf-predicates reads of an unknown
antecedent's.
The predicates a re-check keys `queries` under — `watched-literals` of each, then its functor. What `exceptWhen`'s three registration sites and the stratification graph read of an exception's conjuncts, and what `naf-predicates` reads of an `unknown` antecedent's.
(wrap-direction sentence direction)Express direction as the corresponding set/*Rule wrapper around sentence.
:both needs no wrapper — a bare (implies …) already works both ways.
Express `direction` as the corresponding `set/*Rule` wrapper around `sentence`. `:both` needs no wrapper — a bare `(implies …)` already works both ways.
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 |