datalog: aggregate arg validators (259/259)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 28s

Bug: dl-eval-aggregate accepted non-variable agg-vars and non-
literal goals silently, producing weird/incorrect counts:
- `count(N, 5, p(X))` would compute count over the single
  constant 5 (always 1), ignoring p entirely.
- `count(N, X, 42)` would crash with "unknown body-literal
  shape" at saturation time rather than at rule-add time.

Fix: dl-eval-aggregate now validates up front that the second
arg is a variable (the value to aggregate) and the third arg is
a positive literal (the goal). Errors are descriptive and
include the offending argument.

2 new aggregate tests.
This commit is contained in:
2026-05-11 07:26:48 +00:00
parent 9a16f27075
commit dcae125955
4 changed files with 44 additions and 24 deletions

View File

@@ -104,24 +104,32 @@
(result-var (nth lit 1))
(agg-var (nth lit 2))
(goal (nth lit 3)))
(let
((substs (dl-find-bindings (list goal) db subst))
(vals (list)))
(do
(for-each
(fn
(s)
(let ((v (dl-apply-subst agg-var s)))
(when
(not (dl-val-member? v vals))
(append! vals v))))
substs)
(let ((agg-val (dl-do-aggregate op vals)))
(cond
((= agg-val :empty) (list))
(else
(let ((s2 (dl-unify result-var agg-val subst)))
(if (nil? s2) (list) (list s2)))))))))))
(cond
((not (dl-var? agg-var))
(error (str "datalog aggregate (" op
"): second arg must be a variable, got " agg-var)))
((not (and (list? goal) (> (len goal) 0)
(symbol? (first goal))))
(error (str "datalog aggregate (" op
"): third arg must be a positive literal, got "
goal)))
(else
(let ((vals (list)))
(do
(for-each
(fn
(s)
(let ((v (dl-apply-subst agg-var s)))
(when (not (dl-val-member? v vals))
(append! vals v))))
(dl-find-bindings (list goal) db subst))
(let ((agg-val (dl-do-aggregate op vals)))
(cond
((= agg-val :empty) (list))
(else
(let ((s2 (dl-unify result-var agg-val subst)))
(if (nil? s2) (list) (list s2)))))))))))))
;; Stratification edges from aggregates: like negation, the goal's
;; relation must be in a strictly lower stratum so that the aggregate