A dict in a rule body that isn't `{:neg <positive-lit>}` (the only
recognised dict shape) used to silently fall through every dispatch
clause in dl-rule-check-safety, contributing zero bound variables.
The user would then see a confusing "head variable(s) X do not
appear in any positive body literal" pointing at the head — not at
the actual bug in the body. Typos like `{:negs ...}` are the typical
trigger.
dl-process-lit! now flags both:
- a dict that lacks :neg
- a bare number / string / symbol used as a body lit
with a clear error naming the offending literal.
1 new regression test; conformance 265/265.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`is(R, /(X, 0))` was silently producing IEEE infinity:
(dl-eval "p(10). q(R) :- p(X), is(R, /(X, 0))." "?- q(R).")
=> ({:R inf})
That value then flowed through comparisons (anything < inf, anything
> inf) and aggregations (sum of inf, max of inf) producing nonsense
results downstream. `dl-eval-arith` now checks the divisor before
the host `/` and raises "division by zero in <expr>" — surfacing
the bug at its source rather than letting infinity propagate.
1 new test; conformance 264/264.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Nested `not(not(P))` silently misparsed: outer `not(...)` is
recognised as negation, but the inner `not(banned(X))` was parsed
as a positive call to a relation called `not`. With no `not`
relation present, the inner match was empty, the outer negation
succeeded vacuously, and `vip(X) :- u(X), not(not(banned(X))).`
collapsed to `vip(X) :- u(X).` — a silent double-negation = identity
fallacy.
Fix in `dl-rule-check-safety`: the positive-literal branch and
`dl-process-neg!` both reject any body literal whose relation
name is in `dl-reserved-rel-names`. Error message names the
relation and points the user at stratified negation through an
intermediate relation.
1 regression test; conformance 260/260.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
New lib/datalog/aggregates.sx: (count R V Goal), (sum R V Goal),
(min R V Goal), (max R V Goal). dl-eval-aggregate runs
dl-find-bindings on the goal under the outer subst, collects
distinct values of V, applies the operator, binds R. Empty input:
count/sum return 0; min/max produce no binding (rule fails).
Group-by emerges naturally from outer-subst substitution into the
goal — `popular(P) :- post(P), count(N, U, liked(U, P)), >=(N, 3).`
counts per-post.
Stratifier extended: dl-aggregate-dep-edge contributes a
negation-like edge so the aggregate's goal relation is fully
derived before the aggregate fires (non-monotonicity respected).
Safety relaxed for aggregates: goal-internal vars are existentials,
only the result var becomes bound.
New lib/datalog/builtins.sx: (< <= > >= = !=) and (is X expr) with
+ - * /. dl-eval-arith recursively evaluates nested compounds.
Safety analysis now walks body left-to-right tracking the bound
set: comparisons require all args bound, is RHS vars must be bound
(LHS becomes bound), = special-cases the var/non-var combos.
db.sx keeps the simple safety check as a forward-reference
fallback; builtins.sx redefines dl-rule-check-safety to the
comprehensive version. eval.sx dispatches built-ins through
dl-eval-builtin instead of erroring. 19 new tests.
