giles
66aa003461
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
The canonical Datalog idiom for "no X has any Y": orphan(X) :- person(X), not(parent(X, _)). was rejected by the safety check with "negation refers to unbound variable(s) (\"_anon1\")". The parser renames each anonymous `_` to a fresh `_anon*` symbol so multiple `_` occurrences don't unify with each other, and the negation safety walk then demanded all free vars in the negated lit be bound by an earlier positive body lit — including the renamed anonymous vars. Anonymous vars in a negation are existentially quantified within the negation, not requirements from outside. Added dl-non-anon-vars to strip `_anon*` names from the `needed` set before the binding check in dl-process-neg!. Real vars (like `X` in the orphan idiom) still must be bound by an earlier positive body lit, just as before. 2 new regression tests (orphan idiom + multi-anon "solo" pattern); conformance 273/273. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
407 lines
14 KiB
Plaintext
407 lines
14 KiB
Plaintext
;; lib/datalog/builtins.sx — comparison + arithmetic body literals.
|
|
;;
|
|
;; Built-in predicates filter / extend candidate substitutions during
|
|
;; rule evaluation. They are not stored facts and do not participate in
|
|
;; the Herbrand base.
|
|
;;
|
|
;; (< a b) (<= a b) (> a b) (>= a b) ; numeric (or string) compare
|
|
;; (= a b) ; unify (binds vars)
|
|
;; (!= a b) ; ground-only inequality
|
|
;; (is X expr) ; bind X to expr's value
|
|
;;
|
|
;; Arithmetic expressions are SX-list compounds:
|
|
;; (+ a b) (- a b) (* a b) (/ a b)
|
|
;; or numbers / variables (must be bound at evaluation time).
|
|
|
|
(define
|
|
dl-comparison?
|
|
(fn
|
|
(lit)
|
|
(and
|
|
(list? lit)
|
|
(> (len lit) 0)
|
|
(let
|
|
((rel (dl-rel-name lit)))
|
|
(cond
|
|
((nil? rel) false)
|
|
(else (dl-member-string? rel (list "<" "<=" ">" ">=" "!="))))))))
|
|
|
|
(define
|
|
dl-eq?
|
|
(fn
|
|
(lit)
|
|
(and
|
|
(list? lit)
|
|
(> (len lit) 0)
|
|
(let ((rel (dl-rel-name lit))) (and (not (nil? rel)) (= rel "="))))))
|
|
|
|
(define
|
|
dl-is?
|
|
(fn
|
|
(lit)
|
|
(and
|
|
(list? lit)
|
|
(> (len lit) 0)
|
|
(let
|
|
((rel (dl-rel-name lit)))
|
|
(and (not (nil? rel)) (= rel "is"))))))
|
|
|
|
;; Evaluate an arithmetic expression under subst. Returns the numeric
|
|
;; result, or raises if any operand is unbound or non-numeric.
|
|
(define
|
|
dl-eval-arith
|
|
(fn
|
|
(expr subst)
|
|
(let
|
|
((w (dl-walk expr subst)))
|
|
(cond
|
|
((number? w) w)
|
|
((dl-var? w)
|
|
(error (str "datalog arith: unbound variable " (symbol->string w))))
|
|
((list? w)
|
|
(let
|
|
((rel (dl-rel-name w)) (args (rest w)))
|
|
(cond
|
|
((not (= (len args) 2))
|
|
(error (str "datalog arith: need 2 args, got " w)))
|
|
(else
|
|
(let
|
|
((a (dl-eval-arith (first args) subst))
|
|
(b (dl-eval-arith (nth args 1) subst)))
|
|
(cond
|
|
((= rel "+") (+ a b))
|
|
((= rel "-") (- a b))
|
|
((= rel "*") (* a b))
|
|
((= rel "/")
|
|
(cond
|
|
((= b 0)
|
|
(error
|
|
(str "datalog arith: division by zero in "
|
|
w)))
|
|
(else (/ a b))))
|
|
(else (error (str "datalog arith: unknown op " rel)))))))))
|
|
(else (error (str "datalog arith: not a number — " w)))))))
|
|
|
|
;; Comparable types — both operands must be the same primitive type
|
|
;; (both numbers, both strings). `!=` is the exception: it's defined
|
|
;; for any pair (returns true iff not equal) since dl-tuple-equal?
|
|
;; handles type-mixed comparisons.
|
|
(define
|
|
dl-compare-typeok?
|
|
(fn
|
|
(rel a b)
|
|
(cond
|
|
((= rel "!=") true)
|
|
((and (number? a) (number? b)) true)
|
|
((and (string? a) (string? b)) true)
|
|
(else false))))
|
|
|
|
(define
|
|
dl-eval-compare
|
|
(fn
|
|
(lit subst)
|
|
(let
|
|
((rel (dl-rel-name lit))
|
|
(a (dl-walk (nth lit 1) subst))
|
|
(b (dl-walk (nth lit 2) subst)))
|
|
(cond
|
|
((or (dl-var? a) (dl-var? b))
|
|
(error
|
|
(str
|
|
"datalog: comparison "
|
|
rel
|
|
" has unbound argument; "
|
|
"ensure prior body literal binds the variable")))
|
|
((not (dl-compare-typeok? rel a b))
|
|
(error
|
|
(str "datalog: comparison " rel " requires same-type "
|
|
"operands (both numbers or both strings), got "
|
|
a " and " b)))
|
|
(else
|
|
(let
|
|
((ok (cond ((= rel "<") (< a b)) ((= rel "<=") (<= a b)) ((= rel ">") (> a b)) ((= rel ">=") (>= a b)) ((= rel "!=") (not (dl-tuple-equal? a b))) (else (error (str "datalog: unknown compare " rel))))))
|
|
(if ok subst nil)))))))
|
|
|
|
(define
|
|
dl-eval-eq
|
|
(fn
|
|
(lit subst)
|
|
(dl-unify (nth lit 1) (nth lit 2) subst)))
|
|
|
|
(define
|
|
dl-eval-is
|
|
(fn
|
|
(lit subst)
|
|
(let
|
|
((target (nth lit 1)) (expr (nth lit 2)))
|
|
(let
|
|
((value (dl-eval-arith expr subst)))
|
|
(dl-unify target value subst)))))
|
|
|
|
(define
|
|
dl-eval-builtin
|
|
(fn
|
|
(lit subst)
|
|
(cond
|
|
((dl-comparison? lit) (dl-eval-compare lit subst))
|
|
((dl-eq? lit) (dl-eval-eq lit subst))
|
|
((dl-is? lit) (dl-eval-is lit subst))
|
|
(else (error (str "dl-eval-builtin: not a built-in: " lit))))))
|
|
|
|
;; ── Safety analysis ──────────────────────────────────────────────
|
|
;;
|
|
;; Walks body literals left-to-right tracking a "bound" set. The check
|
|
;; understands these literal kinds:
|
|
;;
|
|
;; positive non-built-in → adds its vars to bound
|
|
;; (is X expr) → vars(expr) ⊆ bound, then add X (if var)
|
|
;; <,<=,>,>=,!= → all vars ⊆ bound (no binding)
|
|
;; (= a b) where:
|
|
;; both non-vars → constraint check, no binding
|
|
;; a var, b not → bind a
|
|
;; b var, a not → bind b
|
|
;; both vars → at least one in bound; bind the other
|
|
;; {:neg lit} → all vars ⊆ bound (Phase 7 enforces fully)
|
|
;;
|
|
;; At end, head vars (minus `_`) must be ⊆ bound.
|
|
|
|
(define
|
|
dl-vars-not-in
|
|
(fn
|
|
(vs bound)
|
|
(let
|
|
((out (list)))
|
|
(do
|
|
(for-each
|
|
(fn
|
|
(v)
|
|
(when (not (dl-member-string? v bound)) (append! out v)))
|
|
vs)
|
|
out))))
|
|
|
|
;; Filter a list of variable-name strings to exclude anonymous-renamed
|
|
;; vars (`_` in source → `_anon*` by dl-rename-anon-term). Used by
|
|
;; the negation safety check, where anonymous vars are existential
|
|
;; within the negated literal.
|
|
(define
|
|
dl-non-anon-vars
|
|
(fn
|
|
(vs)
|
|
(let
|
|
((out (list)))
|
|
(do
|
|
(for-each
|
|
(fn
|
|
(v)
|
|
(when
|
|
(not (and (>= (len v) 5)
|
|
(= (slice v 0 5) "_anon")))
|
|
(append! out v)))
|
|
vs)
|
|
out))))
|
|
|
|
(define
|
|
dl-rule-check-safety
|
|
(fn
|
|
(rule)
|
|
(let
|
|
((head (get rule :head))
|
|
(body (get rule :body))
|
|
(bound (list))
|
|
(err nil))
|
|
(do
|
|
(define
|
|
dl-add-bound!
|
|
(fn
|
|
(vs)
|
|
(for-each
|
|
(fn
|
|
(v)
|
|
(when (not (dl-member-string? v bound)) (append! bound v)))
|
|
vs)))
|
|
(define
|
|
dl-process-eq!
|
|
(fn
|
|
(lit)
|
|
(let
|
|
((a (nth lit 1)) (b (nth lit 2)))
|
|
(let
|
|
((va (dl-var? a)) (vb (dl-var? b)))
|
|
(cond
|
|
((and (not va) (not vb)) nil)
|
|
((and va (not vb))
|
|
(dl-add-bound! (list (symbol->string a))))
|
|
((and (not va) vb)
|
|
(dl-add-bound! (list (symbol->string b))))
|
|
(else
|
|
(let
|
|
((sa (symbol->string a)) (sb (symbol->string b)))
|
|
(cond
|
|
((dl-member-string? sa bound)
|
|
(dl-add-bound! (list sb)))
|
|
((dl-member-string? sb bound)
|
|
(dl-add-bound! (list sa)))
|
|
(else
|
|
(set!
|
|
err
|
|
(str
|
|
"= between two unbound variables "
|
|
(list sa sb)
|
|
" — at least one must be bound by an "
|
|
"earlier positive body literal")))))))))))
|
|
(define
|
|
dl-process-cmp!
|
|
(fn
|
|
(lit)
|
|
(let
|
|
((needed (dl-vars-of (list (nth lit 1) (nth lit 2)))))
|
|
(let
|
|
((missing (dl-vars-not-in needed bound)))
|
|
(when
|
|
(> (len missing) 0)
|
|
(set!
|
|
err
|
|
(str
|
|
"comparison "
|
|
(dl-rel-name lit)
|
|
" requires bound variable(s) "
|
|
missing
|
|
" (must be bound by an earlier positive "
|
|
"body literal)")))))))
|
|
(define
|
|
dl-process-is!
|
|
(fn
|
|
(lit)
|
|
(let
|
|
((tgt (nth lit 1)) (expr (nth lit 2)))
|
|
(let
|
|
((needed (dl-vars-of expr)))
|
|
(let
|
|
((missing (dl-vars-not-in needed bound)))
|
|
(cond
|
|
((> (len missing) 0)
|
|
(set!
|
|
err
|
|
(str
|
|
"is RHS uses unbound variable(s) "
|
|
missing
|
|
" — bind them via a prior positive body "
|
|
"literal")))
|
|
(else
|
|
(when
|
|
(dl-var? tgt)
|
|
(dl-add-bound! (list (symbol->string tgt)))))))))))
|
|
(define
|
|
dl-process-neg!
|
|
(fn
|
|
(lit)
|
|
(let
|
|
((inner (get lit :neg)))
|
|
(let
|
|
((inner-rn
|
|
(cond
|
|
((and (list? inner) (> (len inner) 0))
|
|
(dl-rel-name inner))
|
|
(else nil)))
|
|
;; Anonymous variables (`_` in source → `_anon*` after
|
|
;; renaming) are existentially quantified within the
|
|
;; negated literal — they don't need to be bound by
|
|
;; an earlier body lit, since `not p(X, _)` is a
|
|
;; valid idiom for "no Y exists s.t. p(X, Y)". Filter
|
|
;; them out of the safety check.
|
|
(needed (dl-non-anon-vars (dl-vars-of inner)))
|
|
(missing (dl-vars-not-in needed bound)))
|
|
(cond
|
|
((and (not (nil? inner-rn)) (dl-reserved-rel? inner-rn))
|
|
(set! err
|
|
(str "negated literal uses reserved name '"
|
|
inner-rn
|
|
"' — nested `not(...)` / negated built-ins are "
|
|
"not supported; introduce an intermediate "
|
|
"relation and negate that")))
|
|
((> (len missing) 0)
|
|
(set! err
|
|
(str "negation refers to unbound variable(s) "
|
|
missing
|
|
" — they must be bound by an earlier "
|
|
"positive body literal"))))))))
|
|
(define
|
|
dl-process-agg!
|
|
(fn
|
|
(lit)
|
|
(let
|
|
((result-var (nth lit 1)))
|
|
;; Aggregate goal vars are existentially quantified within
|
|
;; the aggregate; nothing required from outer context. The
|
|
;; result var becomes bound after the aggregate fires.
|
|
(when
|
|
(dl-var? result-var)
|
|
(dl-add-bound! (list (symbol->string result-var)))))))
|
|
|
|
(define
|
|
dl-process-lit!
|
|
(fn
|
|
(lit)
|
|
(when
|
|
(nil? err)
|
|
(cond
|
|
((and (dict? lit) (has-key? lit :neg))
|
|
(dl-process-neg! lit))
|
|
;; A bare dict that is not a recognised negation is
|
|
;; almost certainly a typo (e.g. `{:negs ...}` instead
|
|
;; of `{:neg ...}`). Without this guard the dict would
|
|
;; silently fall through every clause; the head safety
|
|
;; check would then flag the head variables as unbound
|
|
;; even though the real bug is the malformed body lit.
|
|
((dict? lit)
|
|
(set! err
|
|
(str "body literal is a dict but lacks :neg — "
|
|
"the only dict-shaped body lit recognised is "
|
|
"{:neg <positive-lit>} for stratified "
|
|
"negation, got " lit)))
|
|
((dl-aggregate? lit) (dl-process-agg! lit))
|
|
((dl-eq? lit) (dl-process-eq! lit))
|
|
((dl-is? lit) (dl-process-is! lit))
|
|
((dl-comparison? lit) (dl-process-cmp! lit))
|
|
((and (list? lit) (> (len lit) 0))
|
|
(let ((rn (dl-rel-name lit)))
|
|
(cond
|
|
((and (not (nil? rn)) (dl-reserved-rel? rn))
|
|
(set! err
|
|
(str "body literal uses reserved name '" rn
|
|
"' — built-ins / aggregates have their own "
|
|
"syntax; nested `not(...)` is not supported "
|
|
"(use stratified negation via an "
|
|
"intermediate relation)")))
|
|
(else (dl-add-bound! (dl-vars-of lit))))))
|
|
(else
|
|
;; Anything that's not a dict, not a list, or an
|
|
;; empty list. Numbers / strings / symbols as body
|
|
;; lits don't make sense — surface the type.
|
|
(set! err
|
|
(str "body literal must be a positive lit, "
|
|
"built-in, aggregate, or {:neg ...} dict, "
|
|
"got " lit)))))))
|
|
(for-each dl-process-lit! body)
|
|
(when
|
|
(nil? err)
|
|
(let
|
|
((head-vars (dl-vars-of head)) (missing (list)))
|
|
(do
|
|
(for-each
|
|
(fn
|
|
(v)
|
|
(when
|
|
(and (not (dl-member-string? v bound)) (not (= v "_")))
|
|
(append! missing v)))
|
|
head-vars)
|
|
(when
|
|
(> (len missing) 0)
|
|
(set!
|
|
err
|
|
(str
|
|
"head variable(s) "
|
|
missing
|
|
" do not appear in any positive body literal"))))))
|
|
err))))
|