diff --git a/lib/datalog/aggregates.sx b/lib/datalog/aggregates.sx index af0ef0f1..4911a330 100644 --- a/lib/datalog/aggregates.sx +++ b/lib/datalog/aggregates.sx @@ -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 diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json index 4115dc2e..f2224ebf 100644 --- a/lib/datalog/scoreboard.json +++ b/lib/datalog/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "datalog", - "total_passed": 257, + "total_passed": 259, "total_failed": 0, - "total": 257, + "total": 259, "suites": [ {"name":"tokenize","passed":30,"failed":0,"total":30}, {"name":"parse","passed":22,"failed":0,"total":22}, @@ -11,10 +11,10 @@ {"name":"builtins","passed":23,"failed":0,"total":23}, {"name":"semi_naive","passed":8,"failed":0,"total":8}, {"name":"negation","passed":10,"failed":0,"total":10}, - {"name":"aggregates","passed":20,"failed":0,"total":20}, + {"name":"aggregates","passed":22,"failed":0,"total":22}, {"name":"api","passed":20,"failed":0,"total":20}, {"name":"magic","passed":36,"failed":0,"total":36}, {"name":"demo","passed":21,"failed":0,"total":21} ], - "generated": "2026-05-11T07:20:07+00:00" + "generated": "2026-05-11T07:26:33+00:00" } diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md index 3e5c0e4e..0d02305b 100644 --- a/lib/datalog/scoreboard.md +++ b/lib/datalog/scoreboard.md @@ -1,6 +1,6 @@ # datalog scoreboard -**257 / 257 passing** (0 failure(s)). +**259 / 259 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -11,7 +11,7 @@ | builtins | 23 | 23 | ok | | semi_naive | 8 | 8 | ok | | negation | 10 | 10 | ok | -| aggregates | 20 | 20 | ok | +| aggregates | 22 | 22 | ok | | api | 20 | 20 | ok | | magic | 36 | 36 | ok | | demo | 21 | 21 | ok | diff --git a/lib/datalog/tests/aggregates.sx b/lib/datalog/tests/aggregates.sx index 63af21dc..45b3ab88 100644 --- a/lib/datalog/tests/aggregates.sx +++ b/lib/datalog/tests/aggregates.sx @@ -244,6 +244,18 @@ {:U (quote carol) :N 0})) ;; Stratification: recursion through aggregation is rejected. + ;; Aggregate validates that second arg is a variable. + (dl-at-test! "agg second arg must be var" + (dl-at-throws? + (fn () (dl-eval "p(1). q(N) :- count(N, 5, p(X))." "?- q(N)."))) + true) + + ;; Aggregate validates that third arg is a positive literal. + (dl-at-test! "agg third arg must be a literal" + (dl-at-throws? + (fn () (dl-eval "p(1). q(N) :- count(N, X, 42)." "?- q(N)."))) + true) + ;; Indirect recursion through aggregation also rejected. ;; q -> r (via positive lit), r -> q (via aggregate body). ;; The aggregate edge counts as negation for stratification.