datalog: reject compound terms in fact / rule-head args
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Datalog has no function symbols in argument positions, but the
existing dl-add-fact! / dl-add-rule! validators only checked that
literals were ground (no free variables). A compound like `+(1, 2)`
contains no variables, so:
p(+(1, 2)).
=> stored as the unreduced tuple `(p (+ 1 2))`
double(*(X, 2)) :- n(X). n(3).
=> saturates `double((* 3 2))` instead of `double(6)`
Added dl-simple-term? (number / string / symbol) and an
args-simple? walker, used by:
- dl-add-fact!: all args must be simple terms
- dl-add-rule!: rule head args must be simple terms (variables
are symbols, so they pass)
Compounds remain legal in body literals where they encode `is` /
arithmetic / aggregate sub-goals. Error messages name the offending
literal and point the user at the body-only mechanism.
2 new regression tests; conformance 271/271.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -234,6 +234,24 @@
|
||||
:body (list {:weird "stuff"})}))))
|
||||
true)
|
||||
|
||||
;; Facts may only have simple-term args (number / string / symbol).
|
||||
;; A compound arg like `+(1, 2)` would otherwise be silently
|
||||
;; stored as the unreduced expression `(+ 1 2)` because dl-ground?
|
||||
;; sees no free variables.
|
||||
(dl-et-test!
|
||||
"compound arg in fact rejected"
|
||||
(dl-et-throws? (fn () (dl-program "p(+(1, 2)).")))
|
||||
true)
|
||||
|
||||
;; Rule heads may only have variable or constant args — no
|
||||
;; compounds. Compound heads would be saturated as unreduced
|
||||
;; tuples rather than the arithmetic result the user expected.
|
||||
(dl-et-test!
|
||||
"compound arg in rule head rejected"
|
||||
(dl-et-throws?
|
||||
(fn () (dl-program "n(3). double(*(X, 2)) :- n(X).")))
|
||||
true)
|
||||
|
||||
(dl-et-test!
|
||||
"unsafe head var"
|
||||
(dl-et-throws? (fn () (dl-program "p(X, Y) :- q(X).")))
|
||||
|
||||
Reference in New Issue
Block a user