giles
7ce723f732
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 50s
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.
301 lines
9.3 KiB
Plaintext
301 lines
9.3 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 "/") (/ a b))
|
|
(else (error (str "datalog arith: unknown op " rel)))))))))
|
|
(else (error (str "datalog arith: not a number — " w)))))))
|
|
|
|
(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")))
|
|
(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))))
|
|
|
|
(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
|
|
((needed (dl-vars-of (get lit :neg))))
|
|
(let
|
|
((missing (dl-vars-not-in needed bound)))
|
|
(when
|
|
(> (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-lit!
|
|
(fn
|
|
(lit)
|
|
(when
|
|
(nil? err)
|
|
(cond
|
|
((and (dict? lit) (has-key? lit :neg))
|
|
(dl-process-neg! 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))
|
|
(dl-add-bound! (dl-vars-of 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))))
|