datalog: built-ins + body arithmetic + order-aware safety (Phase 4, 106/106)

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.

lib/datalog/builtins.sx

@@ -0,0 +1,300 @@
+;; 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))))

lib/datalog/conformance.conf

@@ -0,0 +1,21 @@
+# Datalog conformance config — sourced by lib/guest/conformance.sh.
+
+LANG_NAME=datalog
+MODE=dict
+
+PRELOADS=(
+  lib/datalog/tokenizer.sx
+  lib/datalog/parser.sx
+  lib/datalog/unify.sx
+  lib/datalog/db.sx
+  lib/datalog/builtins.sx
+  lib/datalog/eval.sx
+)
+
+SUITES=(
+  "tokenize:lib/datalog/tests/tokenize.sx:(dl-tokenize-tests-run!)"
+  "parse:lib/datalog/tests/parse.sx:(dl-parse-tests-run!)"
+  "unify:lib/datalog/tests/unify.sx:(dl-unify-tests-run!)"
+  "eval:lib/datalog/tests/eval.sx:(dl-eval-tests-run!)"
+  "builtins:lib/datalog/tests/builtins.sx:(dl-builtins-tests-run!)"
+)

lib/datalog/conformance.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+# Thin wrapper — see lib/guest/conformance.sh and lib/datalog/conformance.conf.
+exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@"

lib/datalog/db.sx

@@ -0,0 +1,227 @@
+;; lib/datalog/db.sx — Datalog database (EDB + IDB + rules) + safety hook.
+;;
+;; A db is a mutable dict:
+;;   {:facts {<rel-name-string> -> (literal ...)}
+;;    :rules ({:head literal :body (literal ...)} ...)}
+;;
+;; Facts are stored as full literals `(rel arg ... arg)` so they unify
+;; directly against rule body literals. Each relation's tuple list is
+;; deduplicated on insert.
+;;
+;; Phase 3 introduced safety analysis for head variables; Phase 4 (in
+;; lib/datalog/builtins.sx) swaps in the real `dl-rule-check-safety`,
+;; which is order-aware and understands built-in predicates.
+
+(define dl-make-db (fn () {:facts {} :rules (list)}))
+
+(define
+  dl-rel-name
+  (fn
+    (lit)
+    (cond
+      ((and (dict? lit) (has-key? lit :neg)) (dl-rel-name (get lit :neg)))
+      ((and (list? lit) (> (len lit) 0) (symbol? (first lit)))
+        (symbol->string (first lit)))
+      (else nil))))
+
+(define dl-builtin-rels (list "<" "<=" ">" ">=" "=" "!=" "is"))
+
+(define
+  dl-member-string?
+  (fn
+    (s xs)
+    (cond
+      ((= (len xs) 0) false)
+      ((= (first xs) s) true)
+      (else (dl-member-string? s (rest xs))))))
+
+(define
+  dl-builtin?
+  (fn
+    (lit)
+    (and
+      (list? lit)
+      (> (len lit) 0)
+      (let
+        ((rel (dl-rel-name lit)))
+        (cond
+          ((nil? rel) false)
+          (else (dl-member-string? rel dl-builtin-rels)))))))
+
+(define
+  dl-positive-lit?
+  (fn
+    (lit)
+    (cond
+      ((and (dict? lit) (has-key? lit :neg)) false)
+      ((dl-builtin? lit) false)
+      ((and (list? lit) (> (len lit) 0)) true)
+      (else false))))
+
+(define
+  dl-tuple-equal?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-tuple-equal-list? a b 0)))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-tuple-equal-list?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-tuple-equal? (nth a i) (nth b i))) false)
+      (else (dl-tuple-equal-list? a b (+ i 1))))))
+
+(define
+  dl-tuple-member?
+  (fn
+    (lit lits)
+    (cond
+      ((= (len lits) 0) false)
+      ((dl-tuple-equal? lit (first lits)) true)
+      (else (dl-tuple-member? lit (rest lits))))))
+
+(define
+  dl-ensure-rel!
+  (fn
+    (db rel-key)
+    (let
+      ((facts (get db :facts)))
+      (do
+        (when
+          (not (has-key? facts rel-key))
+          (dict-set! facts rel-key (list)))
+        (get facts rel-key)))))
+
+(define
+  dl-rel-tuples
+  (fn
+    (db rel-key)
+    (let
+      ((facts (get db :facts)))
+      (if (has-key? facts rel-key) (get facts rel-key) (list)))))
+
+(define
+  dl-add-fact!
+  (fn
+    (db lit)
+    (cond
+      ((not (and (list? lit) (> (len lit) 0)))
+        (error (str "dl-add-fact!: expected literal list, got " lit)))
+      ((not (dl-ground? lit (dl-empty-subst)))
+        (error (str "dl-add-fact!: expected ground literal, got " lit)))
+      (else
+        (let
+          ((rel-key (dl-rel-name lit)))
+          (let
+            ((tuples (dl-ensure-rel! db rel-key)))
+            (cond
+              ((dl-tuple-member? lit tuples) false)
+              (else (do (append! tuples lit) true)))))))))
+
+;; The full safety check lives in builtins.sx (it has to know which
+;; predicates are built-ins). dl-add-rule! calls it via forward
+;; reference; load builtins.sx alongside db.sx in any setup that
+;; adds rules. The fallback below is used if builtins.sx isn't loaded.
+(define
+  dl-rule-check-safety
+  (fn
+    (rule)
+    (let
+      ((head-vars (dl-vars-of (get rule :head))) (body-vars (list)))
+      (do
+        (for-each
+          (fn
+            (lit)
+            (when
+              (and
+                (list? lit)
+                (> (len lit) 0)
+                (not (and (dict? lit) (has-key? lit :neg))))
+              (for-each
+                (fn
+                  (v)
+                  (when
+                    (not (dl-member-string? v body-vars))
+                    (append! body-vars v)))
+                (dl-vars-of lit))))
+          (get rule :body))
+        (let
+          ((missing (list)))
+          (do
+            (for-each
+              (fn
+                (v)
+                (when
+                  (and
+                    (not (dl-member-string? v body-vars))
+                    (not (= v "_")))
+                  (append! missing v)))
+              head-vars)
+            (cond
+              ((> (len missing) 0)
+                (str
+                  "head variable(s) "
+                  missing
+                  " do not appear in any body literal"))
+              (else nil))))))))
+
+(define
+  dl-add-rule!
+  (fn
+    (db rule)
+    (cond
+      ((not (dict? rule))
+        (error (str "dl-add-rule!: expected rule dict, got " rule)))
+      ((not (has-key? rule :head))
+        (error (str "dl-add-rule!: rule missing :head, got " rule)))
+      (else
+        (let
+          ((err (dl-rule-check-safety rule)))
+          (cond
+            ((not (nil? err)) (error (str "dl-add-rule!: " err)))
+            (else
+              (let
+                ((rules (get db :rules)))
+                (do (append! rules rule) true)))))))))
+
+(define
+  dl-add-clause!
+  (fn
+    (db clause)
+    (cond
+      ((has-key? clause :query) false)
+      ((and (has-key? clause :body) (= (len (get clause :body)) 0))
+        (dl-add-fact! db (get clause :head)))
+      (else (dl-add-rule! db clause)))))
+
+(define
+  dl-load-program!
+  (fn
+    (db source)
+    (let
+      ((clauses (dl-parse source)))
+      (do (for-each (fn (c) (dl-add-clause! db c)) clauses) db))))
+
+(define
+  dl-program
+  (fn (source) (let ((db (dl-make-db))) (dl-load-program! db source))))
+
+(define dl-rules (fn (db) (get db :rules)))
+
+(define
+  dl-fact-count
+  (fn
+    (db)
+    (let
+      ((facts (get db :facts)) (total 0))
+      (do
+        (for-each
+          (fn (k) (set! total (+ total (len (get facts k)))))
+          (keys facts))
+        total))))

lib/datalog/eval.sx

@@ -0,0 +1,147 @@
+;; lib/datalog/eval.sx — naive bottom-up fixpoint evaluator.
+;;
+;; (dl-saturate! db) iterates rules until no new tuples are derived.
+;; The Herbrand base is finite (no function symbols) so termination is
+;; guaranteed by the language.
+;;
+;; Body literal kinds handled here:
+;;   positive (rel arg ... arg)  → match against EDB+IDB tuples (dl-match-positive)
+;;   built-in (< X Y), (is X e)  → constraint via dl-eval-builtin (Phase 4)
+;;   negation {:neg lit}         → Phase 7
+
+(define
+  dl-match-positive
+  (fn
+    (lit db subst)
+    (let
+      ((rel (dl-rel-name lit)) (results (list)))
+      (cond
+        ((nil? rel) (error (str "dl-match-positive: bad literal " lit)))
+        (else
+          (let
+            ((tuples (dl-rel-tuples db rel)))
+            (do
+              (for-each
+                (fn
+                  (tuple)
+                  (let
+                    ((s (dl-unify lit tuple subst)))
+                    (when (not (nil? s)) (append! results s))))
+                tuples)
+              results)))))))
+
+(define
+  dl-match-lit
+  (fn
+    (lit db subst)
+    (cond
+      ((and (dict? lit) (has-key? lit :neg))
+        (error "datalog: negation not yet supported (Phase 7)"))
+      ((dl-builtin? lit)
+        (let
+          ((s (dl-eval-builtin lit subst)))
+          (if (nil? s) (list) (list s))))
+      ((and (list? lit) (> (len lit) 0))
+        (dl-match-positive lit db subst))
+      (else (error (str "datalog: unknown body-literal shape: " lit))))))
+
+(define
+  dl-find-bindings
+  (fn
+    (lits db subst)
+    (cond
+      ((nil? subst) (list))
+      ((= (len lits) 0) (list subst))
+      (else
+        (let
+          ((options (dl-match-lit (first lits) db subst))
+            (results (list)))
+          (do
+            (for-each
+              (fn
+                (s)
+                (for-each
+                  (fn (s2) (append! results s2))
+                  (dl-find-bindings (rest lits) db s)))
+              options)
+            results))))))
+
+(define
+  dl-apply-rule!
+  (fn
+    (db rule)
+    (let
+      ((head (get rule :head)) (body (get rule :body)) (new? false))
+      (do
+        (for-each
+          (fn
+            (s)
+            (let
+              ((derived (dl-apply-subst head s)))
+              (when (dl-add-fact! db derived) (set! new? true))))
+          (dl-find-bindings body db (dl-empty-subst)))
+        new?))))
+
+(define
+  dl-saturate!
+  (fn
+    (db)
+    (let
+      ((changed true))
+      (do
+        (define
+          dl-sat-loop
+          (fn
+            ()
+            (when
+              changed
+              (do
+                (set! changed false)
+                (for-each
+                  (fn (r) (when (dl-apply-rule! db r) (set! changed true)))
+                  (dl-rules db))
+                (dl-sat-loop)))))
+        (dl-sat-loop)
+        db))))
+
+(define
+  dl-query
+  (fn
+    (db goal)
+    (do
+      (dl-saturate! db)
+      (let
+        ((substs (dl-find-bindings (list goal) db (dl-empty-subst)))
+          (vars (dl-vars-of goal))
+          (results (list)))
+        (do
+          (for-each
+            (fn
+              (s)
+              (let
+                ((proj (dl-project-subst s vars)))
+                (when
+                  (not (dl-tuple-member? proj results))
+                  (append! results proj))))
+            substs)
+          results)))))
+
+(define
+  dl-project-subst
+  (fn
+    (subst names)
+    (let
+      ((out {}))
+      (do
+        (for-each
+          (fn
+            (n)
+            (let
+              ((sym (string->symbol n)))
+              (let
+                ((v (dl-walk sym subst)))
+                (dict-set! out n (dl-apply-subst v subst)))))
+          names)
+        out))))
+
+(define dl-relation (fn (db name) (dl-rel-tuples db name)))

lib/datalog/parser.sx

@@ -0,0 +1,242 @@
+;; lib/datalog/parser.sx — Datalog tokens → AST
+;;
+;; Output shapes:
+;;   Literal (positive)  := (relname arg ... arg)        — SX list
+;;   Literal (negative)  := {:neg (relname arg ... arg)} — dict
+;;   Argument            := var-symbol | atom-symbol | number | string
+;;                        | (op-name arg ... arg)        — arithmetic compound
+;;   Fact                := {:head literal :body ()}
+;;   Rule                := {:head literal :body (lit ... lit)}
+;;   Query               := {:query (lit ... lit)}
+;;   Program             := list of facts / rules / queries
+;;
+;; Variables and constants are both SX symbols; the evaluator dispatches
+;; on first-char case ('A'..'Z' or '_' = variable, otherwise constant).
+;;
+;; The parser permits nested compounds in arg position to support
+;; arithmetic (e.g. (is Z (+ X Y))). Safety analysis at rule-load time
+;; rejects compounds whose head is not an arithmetic operator.
+
+(define
+  dl-pp-peek
+  (fn
+    (st)
+    (let
+      ((i (get st :idx)) (tokens (get st :tokens)))
+      (if (< i (len tokens)) (nth tokens i) {:type "eof" :value nil :pos 0}))))
+
+(define
+  dl-pp-peek2
+  (fn
+    (st)
+    (let
+      ((i (+ (get st :idx) 1)) (tokens (get st :tokens)))
+      (if (< i (len tokens)) (nth tokens i) {:type "eof" :value nil :pos 0}))))
+
+(define
+  dl-pp-advance!
+  (fn (st) (dict-set! st :idx (+ (get st :idx) 1))))
+
+(define
+  dl-pp-at?
+  (fn
+    (st type value)
+    (let
+      ((t (dl-pp-peek st)))
+      (and
+        (= (get t :type) type)
+        (or (= value nil) (= (get t :value) value))))))
+
+(define
+  dl-pp-error
+  (fn
+    (st msg)
+    (let
+      ((t (dl-pp-peek st)))
+      (error
+        (str
+          "Parse error at pos "
+          (get t :pos)
+          ": "
+          msg
+          " (got "
+          (get t :type)
+          " '"
+          (if (= (get t :value) nil) "" (get t :value))
+          "')")))))
+
+(define
+  dl-pp-expect!
+  (fn
+    (st type value)
+    (let
+      ((t (dl-pp-peek st)))
+      (if
+        (dl-pp-at? st type value)
+        (do (dl-pp-advance! st) t)
+        (dl-pp-error
+          st
+          (str "expected " type (if (= value nil) "" (str " '" value "'"))))))))
+
+;; Argument: variable, atom, number, string, or compound (relname/op + parens).
+(define
+  dl-pp-parse-arg
+  (fn
+    (st)
+    (let
+      ((t (dl-pp-peek st)))
+      (let
+        ((ty (get t :type)) (vv (get t :value)))
+        (cond
+          ((= ty "number") (do (dl-pp-advance! st) vv))
+          ((= ty "string") (do (dl-pp-advance! st) vv))
+          ((= ty "var") (do (dl-pp-advance! st) (string->symbol vv)))
+          ((or (= ty "atom") (= ty "op"))
+            (do
+              (dl-pp-advance! st)
+              (if
+                (dl-pp-at? st "punct" "(")
+                (do
+                  (dl-pp-advance! st)
+                  (let
+                    ((args (dl-pp-parse-arg-list st)))
+                    (do
+                      (dl-pp-expect! st "punct" ")")
+                      (cons (string->symbol vv) args))))
+                (string->symbol vv))))
+          (else (dl-pp-error st "expected term")))))))
+
+;; Comma-separated args inside parens.
+(define
+  dl-pp-parse-arg-list
+  (fn
+    (st)
+    (let
+      ((args (list)))
+      (do
+        (append! args (dl-pp-parse-arg st))
+        (define
+          dl-pp-arg-loop
+          (fn
+            ()
+            (when
+              (dl-pp-at? st "punct" ",")
+              (do
+                (dl-pp-advance! st)
+                (append! args (dl-pp-parse-arg st))
+                (dl-pp-arg-loop)))))
+        (dl-pp-arg-loop)
+        args))))
+
+;; A positive literal: relname (atom or op) followed by optional (args).
+(define
+  dl-pp-parse-positive
+  (fn
+    (st)
+    (let
+      ((t (dl-pp-peek st)))
+      (let
+        ((ty (get t :type)) (vv (get t :value)))
+        (if
+          (or (= ty "atom") (= ty "op"))
+          (do
+            (dl-pp-advance! st)
+            (if
+              (dl-pp-at? st "punct" "(")
+              (do
+                (dl-pp-advance! st)
+                (let
+                  ((args (dl-pp-parse-arg-list st)))
+                  (do
+                    (dl-pp-expect! st "punct" ")")
+                    (cons (string->symbol vv) args))))
+              (list (string->symbol vv))))
+          (dl-pp-error st "expected literal head"))))))
+
+;; A body literal: positive, or not(positive).
+(define
+  dl-pp-parse-body-lit
+  (fn
+    (st)
+    (let
+      ((t1 (dl-pp-peek st)) (t2 (dl-pp-peek2 st)))
+      (if
+        (and
+          (= (get t1 :type) "atom")
+          (= (get t1 :value) "not")
+          (= (get t2 :type) "punct")
+          (= (get t2 :value) "("))
+        (do
+          (dl-pp-advance! st)
+          (dl-pp-advance! st)
+          (let
+            ((inner (dl-pp-parse-positive st)))
+            (do (dl-pp-expect! st "punct" ")") {:neg inner})))
+        (dl-pp-parse-positive st)))))
+
+;; Comma-separated body literals.
+(define
+  dl-pp-parse-body
+  (fn
+    (st)
+    (let
+      ((lits (list)))
+      (do
+        (append! lits (dl-pp-parse-body-lit st))
+        (define
+          dl-pp-body-loop
+          (fn
+            ()
+            (when
+              (dl-pp-at? st "punct" ",")
+              (do
+                (dl-pp-advance! st)
+                (append! lits (dl-pp-parse-body-lit st))
+                (dl-pp-body-loop)))))
+        (dl-pp-body-loop)
+        lits))))
+
+;; Single clause: fact, rule, or query. Consumes trailing dot.
+(define
+  dl-pp-parse-clause
+  (fn
+    (st)
+    (cond
+      ((dl-pp-at? st "op" "?-")
+        (do
+          (dl-pp-advance! st)
+          (let
+            ((body (dl-pp-parse-body st)))
+            (do (dl-pp-expect! st "punct" ".") {:query body}))))
+      (else
+        (let
+          ((head (dl-pp-parse-positive st)))
+          (cond
+            ((dl-pp-at? st "op" ":-")
+              (do
+                (dl-pp-advance! st)
+                (let
+                  ((body (dl-pp-parse-body st)))
+                  (do (dl-pp-expect! st "punct" ".") {:body body :head head}))))
+            (else (do (dl-pp-expect! st "punct" ".") {:body (list) :head head}))))))))
+
+(define
+  dl-parse-program
+  (fn
+    (tokens)
+    (let
+      ((st {:tokens tokens :idx 0}) (clauses (list)))
+      (do
+        (define
+          dl-pp-prog-loop
+          (fn
+            ()
+            (when
+              (not (dl-pp-at? st "eof" nil))
+              (do
+                (append! clauses (dl-pp-parse-clause st))
+                (dl-pp-prog-loop)))))
+        (dl-pp-prog-loop)
+        clauses))))
+
+(define dl-parse (fn (src) (dl-parse-program (dl-tokenize src))))

lib/datalog/scoreboard.json

@@ -0,0 +1,14 @@
+{
+  "lang": "datalog",
+  "total_passed": 106,
+  "total_failed": 0,
+  "total": 106,
+  "suites": [
+    {"name":"tokenize","passed":26,"failed":0,"total":26},
+    {"name":"parse","passed":18,"failed":0,"total":18},
+    {"name":"unify","passed":28,"failed":0,"total":28},
+    {"name":"eval","passed":15,"failed":0,"total":15},
+    {"name":"builtins","passed":19,"failed":0,"total":19}
+  ],
+  "generated": "2026-05-07T23:50:44+00:00"
+}

lib/datalog/scoreboard.md

@@ -0,0 +1,11 @@
+# datalog scoreboard
+
+**106 / 106 passing** (0 failure(s)).
+
+| Suite | Passed | Total | Status |
+|-------|--------|-------|--------|
+| tokenize | 26 | 26 | ok |
+| parse | 18 | 18 | ok |
+| unify | 28 | 28 | ok |
+| eval | 15 | 15 | ok |
+| builtins | 19 | 19 | ok |

lib/datalog/tests/builtins.sx

@@ -0,0 +1,228 @@
+;; lib/datalog/tests/builtins.sx — comparison + arithmetic body literals.
+
+(define dl-bt-pass 0)
+(define dl-bt-fail 0)
+(define dl-bt-failures (list))
+
+(define
+  dl-bt-deep=?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-bt-deq-l? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let
+          ((ka (keys a)) (kb (keys b)))
+          (and (= (len ka) (len kb)) (dl-bt-deq-d? a b ka 0))))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-bt-deq-l?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-bt-deep=? (nth a i) (nth b i))) false)
+      (else (dl-bt-deq-l? a b (+ i 1))))))
+
+(define
+  dl-bt-deq-d?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i))) (not (dl-bt-deep=? (get a k) (get b k))))
+        false)
+      (else (dl-bt-deq-d? a b ka (+ i 1))))))
+
+(define
+  dl-bt-set=?
+  (fn
+    (a b)
+    (and (= (len a) (len b)) (dl-bt-subset? a b) (dl-bt-subset? b a))))
+
+(define
+  dl-bt-subset?
+  (fn
+    (xs ys)
+    (cond
+      ((= (len xs) 0) true)
+      ((not (dl-bt-contains? ys (first xs))) false)
+      (else (dl-bt-subset? (rest xs) ys)))))
+
+(define
+  dl-bt-contains?
+  (fn
+    (xs target)
+    (cond
+      ((= (len xs) 0) false)
+      ((dl-bt-deep=? (first xs) target) true)
+      (else (dl-bt-contains? (rest xs) target)))))
+
+(define
+  dl-bt-test-set!
+  (fn
+    (name got expected)
+    (if
+      (dl-bt-set=? got expected)
+      (set! dl-bt-pass (+ dl-bt-pass 1))
+      (do
+        (set! dl-bt-fail (+ dl-bt-fail 1))
+        (append!
+          dl-bt-failures
+          (str
+            name
+            "\n    expected (set): "
+            expected
+            "\n    got:            "
+            got))))))
+
+(define
+  dl-bt-test!
+  (fn
+    (name got expected)
+    (if
+      (dl-bt-deep=? got expected)
+      (set! dl-bt-pass (+ dl-bt-pass 1))
+      (do
+        (set! dl-bt-fail (+ dl-bt-fail 1))
+        (append!
+          dl-bt-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+(define
+  dl-bt-throws?
+  (fn
+    (thunk)
+    (let
+      ((threw false))
+      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
+
+(define
+  dl-bt-run-all!
+  (fn
+    ()
+    (do
+      (dl-bt-test-set!
+        "less than filter"
+        (dl-query
+          (dl-program
+            "age(alice, 30). age(bob, 17). age(carol, 22).\n             adult(X) :- age(X, A), >=(A, 18).")
+          (list (quote adult) (quote X)))
+        (list {:X (quote alice)} {:X (quote carol)}))
+      (dl-bt-test-set!
+        "less-equal filter"
+        (dl-query
+          (dl-program
+            "n(1). n(2). n(3). n(4). n(5).\n             small(X) :- n(X), <=(X, 3).")
+          (list (quote small) (quote X)))
+        (list {:X 1} {:X 2} {:X 3}))
+      (dl-bt-test-set!
+        "not-equal filter"
+        (dl-query
+          (dl-program
+            "p(1, 2). p(2, 2). p(3, 4).\n             diff(X, Y) :- p(X, Y), !=(X, Y).")
+          (list (quote diff) (quote X) (quote Y)))
+        (list {:X 1 :Y 2} {:X 3 :Y 4}))
+      (dl-bt-test-set!
+        "is plus"
+        (dl-query
+          (dl-program
+            "n(1). n(2). n(3).\n             succ(X, Y) :- n(X), is(Y, +(X, 1)).")
+          (list (quote succ) (quote X) (quote Y)))
+        (list {:X 1 :Y 2} {:X 2 :Y 3} {:X 3 :Y 4}))
+      (dl-bt-test-set!
+        "is multiply"
+        (dl-query
+          (dl-program
+            "n(2). n(3). n(4).\n             square(X, Y) :- n(X), is(Y, *(X, X)).")
+          (list (quote square) (quote X) (quote Y)))
+        (list {:X 2 :Y 4} {:X 3 :Y 9} {:X 4 :Y 16}))
+      (dl-bt-test-set!
+        "is nested expr"
+        (dl-query
+          (dl-program
+            "n(1). n(2). n(3).\n             f(X, Y) :- n(X), is(Y, *(+(X, 1), 2)).")
+          (list (quote f) (quote X) (quote Y)))
+        (list {:X 1 :Y 4} {:X 2 :Y 6} {:X 3 :Y 8}))
+      (dl-bt-test-set!
+        "is bound LHS — equality"
+        (dl-query
+          (dl-program
+            "n(1, 2). n(2, 5). n(3, 4).\n             succ(X, Y) :- n(X, Y), is(Y, +(X, 1)).")
+          (list (quote succ) (quote X) (quote Y)))
+        (list {:X 1 :Y 2} {:X 3 :Y 4}))
+      (dl-bt-test-set!
+        "triple via is"
+        (dl-query
+          (dl-program
+            "n(1). n(2). n(3).\n             triple(X, Y) :- n(X), is(Y, *(X, 3)).")
+          (list (quote triple) (quote X) (quote Y)))
+        (list {:X 1 :Y 3} {:X 2 :Y 6} {:X 3 :Y 9}))
+      (dl-bt-test-set!
+        "= unifies var with constant"
+        (dl-query
+          (dl-program "p(a). p(b).\n             qual(X) :- p(X), =(X, a).")
+          (list (quote qual) (quote X)))
+        (list {:X (quote a)}))
+      (dl-bt-test-set!
+        "= unifies two vars (one bound)"
+        (dl-query
+          (dl-program "p(a). p(b).\n             twin(X, Y) :- p(X), =(Y, X).")
+          (list (quote twin) (quote X) (quote Y)))
+        (list {:X (quote a) :Y (quote a)} {:X (quote b) :Y (quote b)}))
+      (dl-bt-test!
+        "big count"
+        (let
+          ((db (dl-program "n(0). n(1). n(2). n(3). n(4). n(5). n(6). n(7). n(8). n(9).\n                  big(X) :- n(X), >=(X, 5).")))
+          (do (dl-saturate! db) (len (dl-relation db "big"))))
+        5)
+      (dl-bt-test!
+        "unsafe — comparison without binder"
+        (dl-bt-throws? (fn () (dl-program "p(X) :- <(X, 5).")))
+        true)
+      (dl-bt-test!
+        "unsafe — comparison both unbound"
+        (dl-bt-throws? (fn () (dl-program "p(X, Y) :- <(X, Y), q(X).")))
+        true)
+      (dl-bt-test!
+        "unsafe — is uses unbound RHS var"
+        (dl-bt-throws?
+          (fn () (dl-program "p(X, Y) :- q(X), is(Y, +(X, Z)).")))
+        true)
+      (dl-bt-test!
+        "unsafe — is on its own"
+        (dl-bt-throws? (fn () (dl-program "p(Y) :- is(Y, +(X, 1)).")))
+        true)
+      (dl-bt-test!
+        "unsafe — = between two unbound"
+        (dl-bt-throws? (fn () (dl-program "p(X, Y) :- =(X, Y).")))
+        true)
+      (dl-bt-test!
+        "safe — is binds head var"
+        (dl-bt-throws?
+          (fn () (dl-program "n(1). p(Y) :- n(X), is(Y, +(X, 1)).")))
+        false)
+      (dl-bt-test!
+        "safe — comparison after binder"
+        (dl-bt-throws?
+          (fn () (dl-program "n(1). big(X) :- n(X), >=(X, 0).")))
+        false)
+      (dl-bt-test!
+        "safe — = binds head var"
+        (dl-bt-throws?
+          (fn () (dl-program "p(a). p(b). x(Y) :- p(X), =(Y, X).")))
+        false))))
+
+(define
+  dl-builtins-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-bt-pass 0)
+      (set! dl-bt-fail 0)
+      (set! dl-bt-failures (list))
+      (dl-bt-run-all!)
+      {:failures dl-bt-failures :total (+ dl-bt-pass dl-bt-fail) :passed dl-bt-pass :failed dl-bt-fail})))

lib/datalog/tests/eval.sx

@@ -0,0 +1,206 @@
+;; lib/datalog/tests/eval.sx — naive evaluation + safety analysis tests.
+
+(define dl-et-pass 0)
+(define dl-et-fail 0)
+(define dl-et-failures (list))
+
+;; Same deep-equal helper used in other suites.
+(define
+  dl-et-deep=?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-et-deq-l? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let
+          ((ka (keys a)) (kb (keys b)))
+          (and (= (len ka) (len kb)) (dl-et-deq-d? a b ka 0))))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-et-deq-l?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-et-deep=? (nth a i) (nth b i))) false)
+      (else (dl-et-deq-l? a b (+ i 1))))))
+
+(define
+  dl-et-deq-d?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i))) (not (dl-et-deep=? (get a k) (get b k))))
+        false)
+      (else (dl-et-deq-d? a b ka (+ i 1))))))
+
+;; Set-equality on lists (order-independent, uses dl-et-deep=?).
+(define
+  dl-et-set=?
+  (fn
+    (a b)
+    (and (= (len a) (len b)) (dl-et-subset? a b) (dl-et-subset? b a))))
+
+(define
+  dl-et-subset?
+  (fn
+    (xs ys)
+    (cond
+      ((= (len xs) 0) true)
+      ((not (dl-et-contains? ys (first xs))) false)
+      (else (dl-et-subset? (rest xs) ys)))))
+
+(define
+  dl-et-contains?
+  (fn
+    (xs target)
+    (cond
+      ((= (len xs) 0) false)
+      ((dl-et-deep=? (first xs) target) true)
+      (else (dl-et-contains? (rest xs) target)))))
+
+(define
+  dl-et-test!
+  (fn
+    (name got expected)
+    (if
+      (dl-et-deep=? got expected)
+      (set! dl-et-pass (+ dl-et-pass 1))
+      (do
+        (set! dl-et-fail (+ dl-et-fail 1))
+        (append!
+          dl-et-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+(define
+  dl-et-test-set!
+  (fn
+    (name got expected)
+    (if
+      (dl-et-set=? got expected)
+      (set! dl-et-pass (+ dl-et-pass 1))
+      (do
+        (set! dl-et-fail (+ dl-et-fail 1))
+        (append!
+          dl-et-failures
+          (str
+            name
+            "\n    expected (set): "
+            expected
+            "\n    got:            "
+            got))))))
+
+(define
+  dl-et-throws?
+  (fn
+    (thunk)
+    (let
+      ((threw false))
+      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
+
+(define
+  dl-et-run-all!
+  (fn
+    ()
+    (do
+      (dl-et-test-set!
+        "fact lookup any"
+        (dl-query
+          (dl-program "parent(tom, bob). parent(bob, ann).")
+          (list (quote parent) (quote X) (quote Y)))
+        (list {:X (quote tom) :Y (quote bob)} {:X (quote bob) :Y (quote ann)}))
+      (dl-et-test-set!
+        "fact lookup constant arg"
+        (dl-query
+          (dl-program "parent(tom, bob). parent(tom, liz). parent(bob, ann).")
+          (list (quote parent) (quote tom) (quote Y)))
+        (list {:Y (quote bob)} {:Y (quote liz)}))
+      (dl-et-test-set!
+        "no match"
+        (dl-query
+          (dl-program "parent(tom, bob).")
+          (list (quote parent) (quote nobody) (quote X)))
+        (list))
+      (dl-et-test-set!
+        "ancestor closure"
+        (dl-query
+          (dl-program
+            "parent(tom, bob). parent(bob, ann). parent(ann, pat).\n             ancestor(X, Y) :- parent(X, Y).\n             ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")
+          (list (quote ancestor) (quote tom) (quote X)))
+        (list {:X (quote bob)} {:X (quote ann)} {:X (quote pat)}))
+      (dl-et-test-set!
+        "sibling"
+        (dl-query
+          (dl-program
+            "parent(tom, bob). parent(tom, liz). parent(jane, bob). parent(jane, liz).\n             sibling(X, Y) :- parent(P, X), parent(P, Y).")
+          (list (quote sibling) (quote bob) (quote Y)))
+        (list {:Y (quote bob)} {:Y (quote liz)}))
+      (dl-et-test-set!
+        "same-generation"
+        (dl-query
+          (dl-program
+            "parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(liz, joe).\n             person(tom). person(bob). person(liz). person(ann). person(joe).\n             sg(X, X) :- person(X).\n             sg(X, Y) :- parent(P1, X), sg(P1, P2), parent(P2, Y).")
+          (list (quote sg) (quote ann) (quote X)))
+        (list {:X (quote ann)} {:X (quote joe)}))
+      (dl-et-test!
+        "ancestor count"
+        (let
+          ((db (dl-program "parent(a, b). parent(b, c). parent(c, d).\n                  ancestor(X, Y) :- parent(X, Y).\n                  ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")))
+          (do (dl-saturate! db) (len (dl-relation db "ancestor"))))
+        6)
+      (dl-et-test-set!
+        "grandparent"
+        (dl-query
+          (dl-program
+            "parent(a, b). parent(b, c). parent(c, d).\n             grandparent(X, Z) :- parent(X, Y), parent(Y, Z).")
+          (list (quote grandparent) (quote X) (quote Y)))
+        (list {:X (quote a) :Y (quote c)} {:X (quote b) :Y (quote d)}))
+      (dl-et-test!
+        "no recursion infinite loop"
+        (let
+          ((db (dl-program "edge(1, 2). edge(2, 3). edge(3, 1).\n                  reach(X, Y) :- edge(X, Y).\n                  reach(X, Z) :- edge(X, Y), reach(Y, Z).")))
+          (do (dl-saturate! db) (len (dl-relation db "reach"))))
+        9)
+      (dl-et-test!
+        "unsafe head var"
+        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(X).")))
+        true)
+      (dl-et-test!
+        "unsafe — empty body"
+        (dl-et-throws? (fn () (dl-program "p(X) :- .")))
+        true)
+      (dl-et-test!
+        "underscore var ok"
+        (dl-et-throws? (fn () (dl-program "p(X, _) :- q(X).")))
+        false)
+      (dl-et-test!
+        "var only in head — unsafe"
+        (dl-et-throws? (fn () (dl-program "p(X, Y) :- q(Z).")))
+        true)
+      (dl-et-test!
+        "head var bound by body"
+        (dl-et-throws? (fn () (dl-program "p(X) :- q(X).")))
+        false)
+      (dl-et-test!
+        "head subset of body"
+        (dl-et-throws?
+          (fn
+            ()
+            (dl-program
+              "edge(a,b). edge(b,c). reach(X, Z) :- edge(X, Y), edge(Y, Z).")))
+        false))))
+
+(define
+  dl-eval-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-et-pass 0)
+      (set! dl-et-fail 0)
+      (set! dl-et-failures (list))
+      (dl-et-run-all!)
+      {:failures dl-et-failures :total (+ dl-et-pass dl-et-fail) :passed dl-et-pass :failed dl-et-fail})))

lib/datalog/tests/parse.sx

@@ -0,0 +1,147 @@
+;; lib/datalog/tests/parse.sx — parser unit tests
+;;
+;; Run via: bash lib/datalog/conformance.sh
+;; Or:      (load "lib/datalog/tokenizer.sx") (load "lib/datalog/parser.sx")
+;;          (load "lib/datalog/tests/parse.sx") (dl-parse-tests-run!)
+
+(define dl-pt-pass 0)
+(define dl-pt-fail 0)
+(define dl-pt-failures (list))
+
+;; Order-independent structural equality. Lists compared positionally,
+;; dicts as sets of (key, value) pairs. Numbers via = (so 30.0 = 30).
+(define
+  dl-deep-equal?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-deep-equal-list? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let
+          ((ka (keys a)) (kb (keys b)))
+          (and
+            (= (len ka) (len kb))
+            (dl-deep-equal-dict? a b ka 0))))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-deep-equal-list?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-deep-equal? (nth a i) (nth b i))) false)
+      (else (dl-deep-equal-list? a b (+ i 1))))))
+
+(define
+  dl-deep-equal-dict?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i))) (not (dl-deep-equal? (get a k) (get b k))))
+        false)
+      (else (dl-deep-equal-dict? a b ka (+ i 1))))))
+
+(define
+  dl-pt-test!
+  (fn
+    (name got expected)
+    (if
+      (dl-deep-equal? got expected)
+      (set! dl-pt-pass (+ dl-pt-pass 1))
+      (do
+        (set! dl-pt-fail (+ dl-pt-fail 1))
+        (append!
+          dl-pt-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+(define
+  dl-pt-throws?
+  (fn
+    (thunk)
+    (let
+      ((threw false))
+      (do (guard (e (#t (set! threw true))) (thunk)) threw))))
+
+(define
+  dl-pt-run-all!
+  (fn
+    ()
+    (do
+      (dl-pt-test! "empty program" (dl-parse "") (list))
+      (dl-pt-test! "fact" (dl-parse "parent(tom, bob).") (list {:body (list) :head (list (quote parent) (quote tom) (quote bob))}))
+      (dl-pt-test!
+        "two facts"
+        (dl-parse "parent(tom, bob). parent(bob, ann).")
+        (list {:body (list) :head (list (quote parent) (quote tom) (quote bob))} {:body (list) :head (list (quote parent) (quote bob) (quote ann))}))
+      (dl-pt-test! "zero-ary fact" (dl-parse "ready.") (list {:body (list) :head (list (quote ready))}))
+      (dl-pt-test!
+        "rule one body lit"
+        (dl-parse "ancestor(X, Y) :- parent(X, Y).")
+        (list {:body (list (list (quote parent) (quote X) (quote Y))) :head (list (quote ancestor) (quote X) (quote Y))}))
+      (dl-pt-test!
+        "recursive rule"
+        (dl-parse "ancestor(X, Z) :- parent(X, Y), ancestor(Y, Z).")
+        (list {:body (list (list (quote parent) (quote X) (quote Y)) (list (quote ancestor) (quote Y) (quote Z))) :head (list (quote ancestor) (quote X) (quote Z))}))
+      (dl-pt-test!
+        "query single"
+        (dl-parse "?- ancestor(tom, X).")
+        (list {:query (list (list (quote ancestor) (quote tom) (quote X)))}))
+      (dl-pt-test!
+        "query multi"
+        (dl-parse "?- p(X), q(X).")
+        (list {:query (list (list (quote p) (quote X)) (list (quote q) (quote X)))}))
+      (dl-pt-test!
+        "negation"
+        (dl-parse "safe(X) :- person(X), not(parent(X, _)).")
+        (list {:body (list (list (quote person) (quote X)) {:neg (list (quote parent) (quote X) (quote _))}) :head (list (quote safe) (quote X))}))
+      (dl-pt-test!
+        "number arg"
+        (dl-parse "age(alice, 30).")
+        (list {:body (list) :head (list (quote age) (quote alice) 30)}))
+      (dl-pt-test!
+        "string arg"
+        (dl-parse "label(x, \"hi\").")
+        (list {:body (list) :head (list (quote label) (quote x) "hi")}))
+      (dl-pt-test!
+        "comparison literal"
+        (dl-parse "p(X) :- <(X, 5).")
+        (list {:body (list (list (string->symbol "<") (quote X) 5)) :head (list (quote p) (quote X))}))
+      (dl-pt-test!
+        "is with arith"
+        (dl-parse "succ(X, Y) :- nat(X), is(Y, +(X, 1)).")
+        (list {:body (list (list (quote nat) (quote X)) (list (quote is) (quote Y) (list (string->symbol "+") (quote X) 1))) :head (list (quote succ) (quote X) (quote Y))}))
+      (dl-pt-test!
+        "mixed program"
+        (dl-parse "p(a). p(b). q(X) :- p(X). ?- q(Y).")
+        (list {:body (list) :head (list (quote p) (quote a))} {:body (list) :head (list (quote p) (quote b))} {:body (list (list (quote p) (quote X))) :head (list (quote q) (quote X))} {:query (list (list (quote q) (quote Y)))}))
+      (dl-pt-test!
+        "comments skipped"
+        (dl-parse "% comment\nfoo(a).\n/* block */ bar(b).")
+        (list {:body (list) :head (list (quote foo) (quote a))} {:body (list) :head (list (quote bar) (quote b))}))
+      (dl-pt-test!
+        "underscore var"
+        (dl-parse "p(X) :- q(X, _).")
+        (list {:body (list (list (quote q) (quote X) (quote _))) :head (list (quote p) (quote X))}))
+      (dl-pt-test!
+        "missing dot raises"
+        (dl-pt-throws? (fn () (dl-parse "p(a)")))
+        true)
+      (dl-pt-test!
+        "trailing comma raises"
+        (dl-pt-throws? (fn () (dl-parse "p(a,).")))
+        true))))
+
+(define
+  dl-parse-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-pt-pass 0)
+      (set! dl-pt-fail 0)
+      (set! dl-pt-failures (list))
+      (dl-pt-run-all!)
+      {:failures dl-pt-failures :total (+ dl-pt-pass dl-pt-fail) :passed dl-pt-pass :failed dl-pt-fail})))

lib/datalog/tests/tokenize.sx

@@ -0,0 +1,139 @@
+;; lib/datalog/tests/tokenize.sx — tokenizer unit tests
+;;
+;; Run via: bash lib/datalog/conformance.sh
+;; Or:      (load "lib/datalog/tokenizer.sx") (load "lib/datalog/tests/tokenize.sx")
+;;          (dl-tokenize-tests-run!)
+
+(define dl-tk-pass 0)
+(define dl-tk-fail 0)
+(define dl-tk-failures (list))
+
+(define
+  dl-tk-test!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! dl-tk-pass (+ dl-tk-pass 1))
+      (do
+        (set! dl-tk-fail (+ dl-tk-fail 1))
+        (append!
+          dl-tk-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+(define dl-tk-types (fn (toks) (map (fn (t) (get t :type)) toks)))
+(define dl-tk-values (fn (toks) (map (fn (t) (get t :value)) toks)))
+
+(define
+  dl-tk-run-all!
+  (fn
+    ()
+    (do
+      (dl-tk-test! "empty" (dl-tk-types (dl-tokenize "")) (list "eof"))
+      (dl-tk-test!
+        "atom dot"
+        (dl-tk-types (dl-tokenize "foo."))
+        (list "atom" "punct" "eof"))
+      (dl-tk-test!
+        "atom dot value"
+        (dl-tk-values (dl-tokenize "foo."))
+        (list "foo" "." nil))
+      (dl-tk-test!
+        "var"
+        (dl-tk-types (dl-tokenize "X."))
+        (list "var" "punct" "eof"))
+      (dl-tk-test!
+        "underscore var"
+        (dl-tk-types (dl-tokenize "_x."))
+        (list "var" "punct" "eof"))
+      (dl-tk-test!
+        "integer"
+        (dl-tk-values (dl-tokenize "42"))
+        (list 42 nil))
+      (dl-tk-test!
+        "decimal"
+        (dl-tk-values (dl-tokenize "3.14"))
+        (list 3.14 nil))
+      (dl-tk-test!
+        "string"
+        (dl-tk-values (dl-tokenize "\"hello\""))
+        (list "hello" nil))
+      (dl-tk-test!
+        "quoted atom"
+        (dl-tk-types (dl-tokenize "'two words'"))
+        (list "atom" "eof"))
+      (dl-tk-test!
+        "quoted atom value"
+        (dl-tk-values (dl-tokenize "'two words'"))
+        (list "two words" nil))
+      (dl-tk-test! ":-" (dl-tk-values (dl-tokenize ":-")) (list ":-" nil))
+      (dl-tk-test! "?-" (dl-tk-values (dl-tokenize "?-")) (list "?-" nil))
+      (dl-tk-test! "<=" (dl-tk-values (dl-tokenize "<=")) (list "<=" nil))
+      (dl-tk-test! ">=" (dl-tk-values (dl-tokenize ">=")) (list ">=" nil))
+      (dl-tk-test! "!=" (dl-tk-values (dl-tokenize "!=")) (list "!=" nil))
+      (dl-tk-test!
+        "single op values"
+        (dl-tk-values (dl-tokenize "< > = + - * /"))
+        (list "<" ">" "=" "+" "-" "*" "/" nil))
+      (dl-tk-test!
+        "single op types"
+        (dl-tk-types (dl-tokenize "< > = + - * /"))
+        (list "op" "op" "op" "op" "op" "op" "op" "eof"))
+      (dl-tk-test!
+        "punct"
+        (dl-tk-values (dl-tokenize "( ) , ."))
+        (list "(" ")" "," "." nil))
+      (dl-tk-test!
+        "fact tokens"
+        (dl-tk-types (dl-tokenize "parent(tom, bob)."))
+        (list "atom" "punct" "atom" "punct" "atom" "punct" "punct" "eof"))
+      (dl-tk-test!
+        "rule shape"
+        (dl-tk-types (dl-tokenize "p(X) :- q(X)."))
+        (list
+          "atom"
+          "punct"
+          "var"
+          "punct"
+          "op"
+          "atom"
+          "punct"
+          "var"
+          "punct"
+          "punct"
+          "eof"))
+      (dl-tk-test!
+        "comparison literal"
+        (dl-tk-values (dl-tokenize "<(X, 5)"))
+        (list "<" "(" "X" "," 5 ")" nil))
+      (dl-tk-test!
+        "is form"
+        (dl-tk-values (dl-tokenize "is(Y, +(X, 1))"))
+        (list "is" "(" "Y" "," "+" "(" "X" "," 1 ")" ")" nil))
+      (dl-tk-test!
+        "line comment"
+        (dl-tk-types (dl-tokenize "% comment line\nfoo."))
+        (list "atom" "punct" "eof"))
+      (dl-tk-test!
+        "block comment"
+        (dl-tk-types (dl-tokenize "/* a\nb */ x."))
+        (list "atom" "punct" "eof"))
+      (dl-tk-test!
+        "whitespace"
+        (dl-tk-types (dl-tokenize "  foo  ,\t bar  ."))
+        (list "atom" "punct" "atom" "punct" "eof"))
+      (dl-tk-test!
+        "positions"
+        (map (fn (t) (get t :pos)) (dl-tokenize "foo bar"))
+        (list 0 4 7)))))
+
+(define
+  dl-tokenize-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-tk-pass 0)
+      (set! dl-tk-fail 0)
+      (set! dl-tk-failures (list))
+      (dl-tk-run-all!)
+      {:failures dl-tk-failures :total (+ dl-tk-pass dl-tk-fail) :passed dl-tk-pass :failed dl-tk-fail})))

lib/datalog/tests/unify.sx

@@ -0,0 +1,185 @@
+;; lib/datalog/tests/unify.sx — unification + substitution tests.
+
+(define dl-ut-pass 0)
+(define dl-ut-fail 0)
+(define dl-ut-failures (list))
+
+(define
+  dl-ut-deep-equal?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-ut-deq-list? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let
+          ((ka (keys a)) (kb (keys b)))
+          (and (= (len ka) (len kb)) (dl-ut-deq-dict? a b ka 0))))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-ut-deq-list?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-ut-deep-equal? (nth a i) (nth b i))) false)
+      (else (dl-ut-deq-list? a b (+ i 1))))))
+
+(define
+  dl-ut-deq-dict?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i))) (not (dl-ut-deep-equal? (get a k) (get b k))))
+        false)
+      (else (dl-ut-deq-dict? a b ka (+ i 1))))))
+
+(define
+  dl-ut-test!
+  (fn
+    (name got expected)
+    (if
+      (dl-ut-deep-equal? got expected)
+      (set! dl-ut-pass (+ dl-ut-pass 1))
+      (do
+        (set! dl-ut-fail (+ dl-ut-fail 1))
+        (append!
+          dl-ut-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+(define
+  dl-ut-run-all!
+  (fn
+    ()
+    (do
+      (dl-ut-test! "var? uppercase" (dl-var? (quote X)) true)
+      (dl-ut-test! "var? underscore" (dl-var? (quote _foo)) true)
+      (dl-ut-test! "var? lowercase" (dl-var? (quote tom)) false)
+      (dl-ut-test! "var? number" (dl-var? 5) false)
+      (dl-ut-test! "var? string" (dl-var? "hi") false)
+      (dl-ut-test! "var? list" (dl-var? (list 1)) false)
+      (dl-ut-test!
+        "atom-atom match"
+        (dl-unify (quote tom) (quote tom) (dl-empty-subst))
+        {})
+      (dl-ut-test!
+        "atom-atom fail"
+        (dl-unify (quote tom) (quote bob) (dl-empty-subst))
+        nil)
+      (dl-ut-test!
+        "num-num match"
+        (dl-unify 5 5 (dl-empty-subst))
+        {})
+      (dl-ut-test!
+        "num-num fail"
+        (dl-unify 5 6 (dl-empty-subst))
+        nil)
+      (dl-ut-test!
+        "string match"
+        (dl-unify "hi" "hi" (dl-empty-subst))
+        {})
+      (dl-ut-test! "string fail" (dl-unify "hi" "bye" (dl-empty-subst)) nil)
+      (dl-ut-test!
+        "var-atom binds"
+        (dl-unify (quote X) (quote tom) (dl-empty-subst))
+        {:X (quote tom)})
+      (dl-ut-test!
+        "atom-var binds"
+        (dl-unify (quote tom) (quote X) (dl-empty-subst))
+        {:X (quote tom)})
+      (dl-ut-test!
+        "var-var same"
+        (dl-unify (quote X) (quote X) (dl-empty-subst))
+        {})
+      (dl-ut-test!
+        "var-var bind"
+        (let
+          ((s (dl-unify (quote X) (quote Y) (dl-empty-subst))))
+          (dl-walk (quote X) s))
+        (quote Y))
+      (dl-ut-test!
+        "tuple match"
+        (dl-unify
+          (list (quote parent) (quote X) (quote bob))
+          (list (quote parent) (quote tom) (quote Y))
+          (dl-empty-subst))
+        {:X (quote tom) :Y (quote bob)})
+      (dl-ut-test!
+        "tuple arity mismatch"
+        (dl-unify
+          (list (quote p) (quote X))
+          (list (quote p) (quote a) (quote b))
+          (dl-empty-subst))
+        nil)
+      (dl-ut-test!
+        "tuple head mismatch"
+        (dl-unify
+          (list (quote p) (quote X))
+          (list (quote q) (quote X))
+          (dl-empty-subst))
+        nil)
+      (dl-ut-test!
+        "walk chain"
+        (let
+          ((s1 (dl-unify (quote X) (quote Y) (dl-empty-subst))))
+          (let
+            ((s2 (dl-unify (quote Y) (quote tom) s1)))
+            (dl-walk (quote X) s2)))
+        (quote tom))
+      (dl-ut-test!
+        "apply subst on tuple"
+        (let
+          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
+          (dl-apply-subst (list (quote parent) (quote X) (quote Y)) s))
+        (list (quote parent) (quote tom) (quote Y)))
+      (dl-ut-test!
+        "ground? all const"
+        (dl-ground?
+          (list (quote p) (quote tom) 5)
+          (dl-empty-subst))
+        true)
+      (dl-ut-test!
+        "ground? unbound var"
+        (dl-ground? (list (quote p) (quote X)) (dl-empty-subst))
+        false)
+      (dl-ut-test!
+        "ground? bound var"
+        (let
+          ((s (dl-bind (quote X) (quote tom) (dl-empty-subst))))
+          (dl-ground? (list (quote p) (quote X)) s))
+        true)
+      (dl-ut-test!
+        "ground? bare var"
+        (dl-ground? (quote X) (dl-empty-subst))
+        false)
+      (dl-ut-test!
+        "vars-of basic"
+        (dl-vars-of
+          (list (quote p) (quote X) (quote tom) (quote Y) (quote X)))
+        (list "X" "Y"))
+      (dl-ut-test!
+        "vars-of ground"
+        (dl-vars-of (list (quote p) (quote tom) (quote bob)))
+        (list))
+      (dl-ut-test!
+        "vars-of nested compound"
+        (dl-vars-of
+          (list
+            (quote is)
+            (quote Z)
+            (list (string->symbol "+") (quote X) 1)))
+        (list "Z" "X")))))
+
+(define
+  dl-unify-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-ut-pass 0)
+      (set! dl-ut-fail 0)
+      (set! dl-ut-failures (list))
+      (dl-ut-run-all!)
+      {:failures dl-ut-failures :total (+ dl-ut-pass dl-ut-fail) :passed dl-ut-pass :failed dl-ut-fail})))

lib/datalog/tokenizer.sx

@@ -0,0 +1,254 @@
+;; lib/datalog/tokenizer.sx — Datalog source → token stream
+;;
+;; Tokens: {:type T :value V :pos P}
+;; Types:
+;;   "atom"    — lowercase-start ident or quoted 'atom'
+;;   "var"     — uppercase-start or _-start ident (value is the name)
+;;   "number"  — numeric literal (decoded to number)
+;;   "string"  — "..." string literal
+;;   "punct"   — ( ) , .
+;;   "op"      — :- ?- <= >= != < > = + - * /
+;;   "eof"
+;;
+;; Datalog has no function symbols in arg position; the parser still
+;; accepts nested compounds for arithmetic ((is X (+ A B))) but safety
+;; analysis rejects non-arithmetic nesting at rule-load time.
+
+(define dl-make-token (fn (type value pos) {:type type :value value :pos pos}))
+
+(define dl-digit? (fn (c) (and (>= c "0") (<= c "9"))))
+(define dl-lower? (fn (c) (and (>= c "a") (<= c "z"))))
+(define dl-upper? (fn (c) (and (>= c "A") (<= c "Z"))))
+
+(define
+  dl-ident-char?
+  (fn (c) (or (dl-lower? c) (dl-upper? c) (dl-digit? c) (= c "_"))))
+
+(define dl-ws? (fn (c) (or (= c " ") (= c "\t") (= c "\n") (= c "\r"))))
+
+(define
+  dl-tokenize
+  (fn
+    (src)
+    (let
+      ((tokens (list)) (pos 0) (src-len (len src)))
+      (define
+        dl-peek
+        (fn
+          (offset)
+          (if (< (+ pos offset) src-len) (nth src (+ pos offset)) nil)))
+      (define cur (fn () (dl-peek 0)))
+      (define advance! (fn (n) (set! pos (+ pos n))))
+      (define
+        at?
+        (fn
+          (s)
+          (let
+            ((sl (len s)))
+            (and (<= (+ pos sl) src-len) (= (slice src pos (+ pos sl)) s)))))
+      (define
+        dl-emit!
+        (fn
+          (type value start)
+          (append! tokens (dl-make-token type value start))))
+      (define
+        skip-line-comment!
+        (fn
+          ()
+          (when
+            (and (< pos src-len) (not (= (cur) "\n")))
+            (do (advance! 1) (skip-line-comment!)))))
+      (define
+        skip-block-comment!
+        (fn
+          ()
+          (cond
+            ((>= pos src-len) nil)
+            ((and (= (cur) "*") (< (+ pos 1) src-len) (= (dl-peek 1) "/"))
+              (advance! 2))
+            (else (do (advance! 1) (skip-block-comment!))))))
+      (define
+        skip-ws!
+        (fn
+          ()
+          (cond
+            ((>= pos src-len) nil)
+            ((dl-ws? (cur)) (do (advance! 1) (skip-ws!)))
+            ((= (cur) "%")
+              (do (advance! 1) (skip-line-comment!) (skip-ws!)))
+            ((and (= (cur) "/") (< (+ pos 1) src-len) (= (dl-peek 1) "*"))
+              (do (advance! 2) (skip-block-comment!) (skip-ws!)))
+            (else nil))))
+      (define
+        read-ident
+        (fn
+          (start)
+          (do
+            (when
+              (and (< pos src-len) (dl-ident-char? (cur)))
+              (do (advance! 1) (read-ident start)))
+            (slice src start pos))))
+      (define
+        read-decimal-digits!
+        (fn
+          ()
+          (when
+            (and (< pos src-len) (dl-digit? (cur)))
+            (do (advance! 1) (read-decimal-digits!)))))
+      (define
+        read-number
+        (fn
+          (start)
+          (do
+            (read-decimal-digits!)
+            (when
+              (and
+                (< pos src-len)
+                (= (cur) ".")
+                (< (+ pos 1) src-len)
+                (dl-digit? (dl-peek 1)))
+              (do (advance! 1) (read-decimal-digits!)))
+            (parse-number (slice src start pos)))))
+      (define
+        read-quoted
+        (fn
+          (quote-char)
+          (let
+            ((chars (list)))
+            (advance! 1)
+            (define
+              loop
+              (fn
+                ()
+                (cond
+                  ((>= pos src-len) nil)
+                  ((= (cur) "\\")
+                    (do
+                      (advance! 1)
+                      (when
+                        (< pos src-len)
+                        (let
+                          ((ch (cur)))
+                          (do
+                            (cond
+                              ((= ch "n") (append! chars "\n"))
+                              ((= ch "t") (append! chars "\t"))
+                              ((= ch "r") (append! chars "\r"))
+                              ((= ch "\\") (append! chars "\\"))
+                              ((= ch "'") (append! chars "'"))
+                              ((= ch "\"") (append! chars "\""))
+                              (else (append! chars ch)))
+                            (advance! 1))))
+                      (loop)))
+                  ((= (cur) quote-char) (advance! 1))
+                  (else
+                    (do (append! chars (cur)) (advance! 1) (loop))))))
+            (loop)
+            (join "" chars))))
+      (define
+        scan!
+        (fn
+          ()
+          (do
+            (skip-ws!)
+            (when
+              (< pos src-len)
+              (let
+                ((ch (cur)) (start pos))
+                (cond
+                  ((at? ":-")
+                    (do
+                      (dl-emit! "op" ":-" start)
+                      (advance! 2)
+                      (scan!)))
+                  ((at? "?-")
+                    (do
+                      (dl-emit! "op" "?-" start)
+                      (advance! 2)
+                      (scan!)))
+                  ((at? "<=")
+                    (do
+                      (dl-emit! "op" "<=" start)
+                      (advance! 2)
+                      (scan!)))
+                  ((at? ">=")
+                    (do
+                      (dl-emit! "op" ">=" start)
+                      (advance! 2)
+                      (scan!)))
+                  ((at? "!=")
+                    (do
+                      (dl-emit! "op" "!=" start)
+                      (advance! 2)
+                      (scan!)))
+                  ((dl-digit? ch)
+                    (do
+                      (dl-emit! "number" (read-number start) start)
+                      (scan!)))
+                  ((= ch "'")
+                    (do (dl-emit! "atom" (read-quoted "'") start) (scan!)))
+                  ((= ch "\"")
+                    (do (dl-emit! "string" (read-quoted "\"") start) (scan!)))
+                  ((dl-lower? ch)
+                    (do (dl-emit! "atom" (read-ident start) start) (scan!)))
+                  ((or (dl-upper? ch) (= ch "_"))
+                    (do (dl-emit! "var" (read-ident start) start) (scan!)))
+                  ((= ch "(")
+                    (do
+                      (dl-emit! "punct" "(" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch ")")
+                    (do
+                      (dl-emit! "punct" ")" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch ",")
+                    (do
+                      (dl-emit! "punct" "," start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch ".")
+                    (do
+                      (dl-emit! "punct" "." start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "<")
+                    (do
+                      (dl-emit! "op" "<" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch ">")
+                    (do
+                      (dl-emit! "op" ">" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "=")
+                    (do
+                      (dl-emit! "op" "=" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "+")
+                    (do
+                      (dl-emit! "op" "+" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "-")
+                    (do
+                      (dl-emit! "op" "-" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "*")
+                    (do
+                      (dl-emit! "op" "*" start)
+                      (advance! 1)
+                      (scan!)))
+                  ((= ch "/")
+                    (do
+                      (dl-emit! "op" "/" start)
+                      (advance! 1)
+                      (scan!)))
+                  (else (do (advance! 1) (scan!)))))))))
+      (scan!)
+      (dl-emit! "eof" nil pos)
+      tokens)))

lib/datalog/unify.sx

@@ -0,0 +1,159 @@
+;; lib/datalog/unify.sx — unification + substitution for Datalog terms.
+;;
+;; Term taxonomy (after parsing):
+;;   variable  — SX symbol whose first char is uppercase A–Z or '_'.
+;;   constant  — SX symbol whose first char is lowercase a–z (atom name).
+;;   number    — numeric literal.
+;;   string    — string literal.
+;;   compound  — SX list (functor arg ... arg). In core Datalog these
+;;               only appear as arithmetic expressions (see Phase 4
+;;               safety analysis); compound-against-compound unification
+;;               is supported anyway for completeness.
+;;
+;; Substitutions are immutable dicts keyed by variable name (string).
+;; A failed unification returns nil; success returns the extended subst.
+
+(define dl-empty-subst (fn () {}))
+
+(define
+  dl-var?
+  (fn
+    (term)
+    (and
+      (symbol? term)
+      (let
+        ((name (symbol->string term)))
+        (and
+          (> (len name) 0)
+          (let
+            ((c (slice name 0 1)))
+            (or (and (>= c "A") (<= c "Z")) (= c "_"))))))))
+
+;; Walk: chase variable bindings until we hit a non-variable or an unbound
+;; variable. The result is either a non-variable term or an unbound var.
+(define
+  dl-walk
+  (fn
+    (term subst)
+    (if
+      (dl-var? term)
+      (let
+        ((name (symbol->string term)))
+        (if
+          (and (dict? subst) (has-key? subst name))
+          (dl-walk (get subst name) subst)
+          term))
+      term)))
+
+;; Bind a variable symbol to a value in subst, returning a new subst.
+(define
+  dl-bind
+  (fn (var-sym value subst) (assoc subst (symbol->string var-sym) value)))
+
+(define
+  dl-unify
+  (fn
+    (t1 t2 subst)
+    (if
+      (nil? subst)
+      nil
+      (let
+        ((u1 (dl-walk t1 subst)) (u2 (dl-walk t2 subst)))
+        (cond
+          ((dl-var? u1)
+            (cond
+              ((and (dl-var? u2) (= (symbol->string u1) (symbol->string u2)))
+                subst)
+              (else (dl-bind u1 u2 subst))))
+          ((dl-var? u2) (dl-bind u2 u1 subst))
+          ((and (list? u1) (list? u2))
+            (if
+              (= (len u1) (len u2))
+              (dl-unify-list u1 u2 subst 0)
+              nil))
+          ((and (number? u1) (number? u2)) (if (= u1 u2) subst nil))
+          ((and (string? u1) (string? u2)) (if (= u1 u2) subst nil))
+          ((and (symbol? u1) (symbol? u2))
+            (if (= (symbol->string u1) (symbol->string u2)) subst nil))
+          (else nil))))))
+
+(define
+  dl-unify-list
+  (fn
+    (a b subst i)
+    (cond
+      ((nil? subst) nil)
+      ((>= i (len a)) subst)
+      (else
+        (dl-unify-list
+          a
+          b
+          (dl-unify (nth a i) (nth b i) subst)
+          (+ i 1))))))
+
+;; Apply substitution: walk the term and recurse into lists.
+(define
+  dl-apply-subst
+  (fn
+    (term subst)
+    (let
+      ((w (dl-walk term subst)))
+      (if (list? w) (map (fn (x) (dl-apply-subst x subst)) w) w))))
+
+;; Ground? — true iff no free variables remain after walking.
+(define
+  dl-ground?
+  (fn
+    (term subst)
+    (let
+      ((w (dl-walk term subst)))
+      (cond
+        ((dl-var? w) false)
+        ((list? w) (dl-ground-list? w subst 0))
+        (else true)))))
+
+(define
+  dl-ground-list?
+  (fn
+    (xs subst i)
+    (cond
+      ((>= i (len xs)) true)
+      ((not (dl-ground? (nth xs i) subst)) false)
+      (else (dl-ground-list? xs subst (+ i 1))))))
+
+;; Return the list of variable names appearing in a term (deduped, in
+;; left-to-right order). Useful for safety analysis later.
+(define
+  dl-vars-of
+  (fn (term) (let ((seen (list))) (do (dl-vars-of-aux term seen) seen))))
+
+(define
+  dl-vars-of-aux
+  (fn
+    (term acc)
+    (cond
+      ((dl-var? term)
+        (let
+          ((name (symbol->string term)))
+          (when (not (dl-member? name acc)) (append! acc name))))
+      ((list? term) (dl-vars-of-list term acc 0))
+      (else nil))))
+
+(define
+  dl-vars-of-list
+  (fn
+    (xs acc i)
+    (when
+      (< i (len xs))
+      (do
+        (dl-vars-of-aux (nth xs i) acc)
+        (dl-vars-of-list xs acc (+ i 1))))))
+
+(define
+  dl-member?
+  (fn
+    (x xs)
+    (cond
+      ((= (len xs) 0) false)
+      ((= (first xs) x) true)
+      (else (dl-member? x (rest xs))))))

plans/datalog-on-sx.md

@@ -58,50 +58,108 @@ Key differences from Prolog:
 ## Roadmap
 
 ### Phase 1 — tokenizer + parser
-- [ ] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings,
-      operators (`:- `, `?-`, `,`, `.`), comments (`%`, `/* */`)
-      Note: no function symbol syntax (no nested `f(...)` in arg position).
-- [ ] Parser:
+- [x] Tokenizer: atoms (lowercase/quoted), variables (uppercase/`_`), numbers, strings,
+      punct (`( )`, `,`, `.`), operators (`:-`, `?-`, `<=`, `>=`, `!=`, `<`, `>`, `=`,
+      `+`, `-`, `*`, `/`), comments (`%`, `/* */`)
+      Note: no function symbol syntax (no nested `f(...)` in arg position) — but the
+      parser permits nested compounds for arithmetic; safety analysis (Phase 3) rejects
+      non-arithmetic nesting.
+- [x] Parser:
       - Facts: `parent(tom, bob).` → `{:head (parent tom bob) :body ()}`
       - Rules: `ancestor(X,Z) :- parent(X,Y), ancestor(Y,Z).`
               → `{:head (ancestor X Z) :body ((parent X Y) (ancestor Y Z))}`
-      - Queries: `?- ancestor(tom, X).` → `{:query (ancestor tom X)}`
+      - Queries: `?- ancestor(tom, X).` → `{:query ((ancestor tom X))}`
+        (`:query` value is always a list of literals; `?- p, q.` → `{:query ((p) (q))}`)
       - Negation: `not(parent(X,Y))` in body position → `{:neg (parent X Y)}`
-- [ ] Tests in `lib/datalog/tests/parse.sx`
+- [x] Tests in `lib/datalog/tests/parse.sx` (18) and `lib/datalog/tests/tokenize.sx` (26).
+      Conformance harness: `bash lib/datalog/conformance.sh` → 44 / 44 passing.
 
 ### Phase 2 — unification + substitution
-- [ ] Share or port unification from `lib/prolog/` — term walk, occurs check off by default
-- [ ] `dl-unify` `t1` `t2` `subst` → extended subst or nil (no function symbols means simpler)
-- [ ] `dl-ground?` `term` → bool — all variables bound in substitution
-- [ ] Tests: atom/atom, var/atom, var/var, list args
+- [x] Ported (not shared) from `lib/prolog/` — term walk, no occurs check.
+- [x] `dl-unify t1 t2 subst` → extended subst dict, or `nil` on failure.
+- [x] `dl-walk`, `dl-bind`, `dl-apply-subst`, `dl-ground?`, `dl-vars-of`.
+- [x] Substitutions are immutable dicts keyed by variable name (string).
+      Lists/tuples unify element-wise (used for arithmetic compounds too).
+- [x] Tests in `lib/datalog/tests/unify.sx` (28). 72 / 72 conformance.
 
-### Phase 3 — extensional DB + naive evaluation
-- [ ] EDB: `{:relation-name → set-of-ground-tuples}` using SX sets (Phase 18 of primitives)
-- [ ] `dl-add-fact!` `db` `relation` `args` → add ground tuple
-- [ ] `dl-add-rule!` `db` `head` `body` → add rule clause
-- [ ] Naive evaluation: iterate rules until fixpoint
-      For each rule, for each combination of body tuples that unify, derive head tuple.
-      Repeat until no new tuples added.
-- [ ] `dl-query` `db` `goal` → list of substitutions satisfying goal against derived DB
-- [ ] Tests: transitive closure (ancestor), sibling, same-generation — classic Datalog programs
+### Phase 3 — extensional DB + naive evaluation + safety analysis
+- [x] EDB+IDB combined: `{:facts {<rel-name-string> -> (literal ...)}}` —
+      relations indexed by name; tuples stored as full literals so they
+      unify directly. Dedup on insert via `dl-tuple-equal?`.
+- [x] `dl-add-fact! db lit` (rejects non-ground) and `dl-add-rule! db rule`
+      (rejects unsafe). `dl-program source` parses + loads in one step.
+- [x] Naive evaluation `dl-saturate! db`: iterate rules until no new tuples.
+      `dl-find-bindings` recursively joins body literals; `dl-match-positive`
+      unifies a literal against every tuple in the relation.
+- [x] `dl-query db goal` → list of substitutions over `goal`'s vars,
+      deduplicated. `dl-relation db name` for derived tuples.
+- [x] Safety analysis at `dl-add-rule!` time: every head variable except
+      `_` must appear in some positive body literal. Built-ins and negated
+      literals do not satisfy safety. Helpers `dl-positive-body-vars`,
+      `dl-rule-unsafe-head-vars` exposed for later phases.
+- [x] Negation and arithmetic built-ins error cleanly at saturate time
+      (Phase 4 / Phase 7 will swap in real semantics).
+- [x] Tests in `lib/datalog/tests/eval.sx` (15): transitive closure,
+      sibling, same-generation, grandparent, cyclic graph reach, six
+      safety cases. 87 / 87 conformance.
 
-### Phase 4 — semi-naive evaluation (performance)
+### Phase 4 — built-in predicates + body arithmetic
+Almost every real query needs `<`, `=`, simple arithmetic, and string
+comparisons in body position. These are not EDB lookups — they're
+constraints that filter bindings.
+- [x] Recognise built-in predicates in body: `(< X Y)`, `(<= X Y)`, `(> X Y)`,
+      `(>= X Y)`, `(= X Y)`, `(!= X Y)` and arithmetic forms `(is Z (+ X Y))`,
+      `(is Z (- X Y))`, `(is Z (* X Y))`, `(is Z (/ X Y))`. Live in
+      `lib/datalog/builtins.sx`.
+- [x] `dl-eval-builtin` dispatches; `dl-eval-arith` recursively evaluates
+      `(+ a b)` etc. with full nesting. `=` unifies; `!=` rejects equal
+      ground terms.
+- [x] Order-aware safety analysis (`dl-rule-check-safety`): walks body
+      left-to-right tracking which vars are bound. `is`'s RHS vars must
+      be already bound; LHS becomes bound. Comparisons require both
+      sides bound. `=` is special-cased — at least one side bound binds
+      the other. Negation vars must be bound (will be enforced fully in
+      Phase 7).
+- [x] Wired through SX numeric primitives — no separate number tower.
+- [x] Tests in `lib/datalog/tests/builtins.sx` (19): range filters,
+      arithmetic derivations, equality binding, eight safety violations
+      and three safe-shape tests. Conformance 106 / 106.
+
+### Phase 5 — semi-naive evaluation (performance)
 - [ ] Delta sets: track newly derived tuples per iteration
 - [ ] Semi-naive rule: only join against delta tuples from last iteration, not full relation
 - [ ] Significant speedup for recursive rules — avoids re-deriving known tuples
-- [ ] `dl-stratify` `db` → dependency graph + SCC analysis → stratum ordering
 - [ ] Tests: verify semi-naive produces same results as naive; benchmark on large ancestor chain
 
-### Phase 5 — stratified negation
+### Phase 6 — magic sets (goal-directed bottom-up, opt-in)
+Naive bottom-up derives **all** consequences before answering. Magic sets
+rewrite the program so the fixpoint only derives tuples relevant to the
+goal — a major perf win for "what's reachable from node X" queries on
+large graphs.
+- [ ] Adornments: annotate rule predicates with bound (`b`) / free (`f`)
+      patterns based on how they're called.
+- [ ] Magic transformation: for each adorned predicate, generate a
+      `magic_<pred>` relation and rewrite rule bodies to filter through it.
+- [ ] Sideways information passing strategy (SIPS): left-to-right by
+      default; pluggable.
+- [ ] Optional pass — `(dl-set-strategy! db :magic)`; default semi-naive.
+- [ ] Tests: equivalence vs naive on small inputs; perf win on a 10k-node
+      reachability query from a single root.
+
+### Phase 7 — stratified negation
 - [ ] Dependency graph analysis: which relations depend on which (positively or negatively)
 - [ ] Stratification check: error if negation is in a cycle (non-stratifiable program)
-- [ ] Evaluation: process strata in order — lower stratum fully computed before using its
-      complement in a higher stratum
-- [ ] `not(P)` in rule body: at evaluation time, check P is NOT in the derived EDB
-- [ ] Tests: non-member (`not(member(X,L))`), colored-graph (`not(same-color(X,Y))`),
-      stratification error detection
+- [ ] `dl-stratify db` → SCC analysis → stratum ordering
+- [ ] Evaluation: process strata in order — lower stratum fully computed
+      before using its complement in a higher stratum
+- [ ] `not(P)` in rule body: at evaluation time, check P is NOT in the
+      derived EDB
+- [ ] Safety extension: head vars in negative literals must also appear in
+      some positive body literal of the same rule
+- [ ] Tests: non-member (`not(member(X,L))`), colored-graph
+      (`not(same-color(X,Y))`), stratification error detection
 
-### Phase 6 — aggregation (Datalog+)
+### Phase 8 — aggregation (Datalog+)
 - [ ] `count(X, Goal)` → number of distinct X satisfying Goal
 - [ ] `sum(X, Goal)` → sum of X values satisfying Goal
 - [ ] `min(X, Goal)` / `max(X, Goal)` → min/max of X satisfying Goal
@@ -109,7 +167,7 @@ Key differences from Prolog:
 - [ ] Aggregation breaks stratification — evaluate in a separate post-fixpoint pass
 - [ ] Tests: social network statistics, grade aggregation, inventory sums
 
-### Phase 7 — SX embedding API
+### Phase 9 — SX embedding API
 - [ ] `(dl-program facts rules)` → database from SX data directly (no parsing required)
       ```
       (dl-program
@@ -123,7 +181,7 @@ Key differences from Prolog:
 - [ ] Integration demo: federation graph query — `(ancestor actor1 actor2)` over
       rose-ash ActivityPub follow relationships
 
-### Phase 8 — Datalog as a query language for rose-ash
+### Phase 10 — Datalog as a query language for rose-ash
 - [ ] Schema: map SQLAlchemy model relationships to Datalog EDB facts
       (e.g. `(follows user1 user2)`, `(authored user post)`, `(tagged post tag)`)
 - [ ] Loader: `dl-load-from-db!` — query PostgreSQL, populate Datalog EDB
@@ -142,4 +200,42 @@ _(none yet)_
 
 _Newest first._
 
-_(awaiting phase 1)_
+- 2026-05-07 — Phase 4 done. `lib/datalog/builtins.sx` (~280 LOC) adds
+  `(< X Y)`, `(<= X Y)`, `(> X Y)`, `(>= X Y)`, `(= X Y)`, `(!= X Y)`,
+  and `(is X expr)` with `+ - * /`. `dl-eval-builtin` dispatches;
+  `dl-eval-arith` recursively evaluates nested compounds. Safety
+  check is now order-aware — it walks body literals left-to-right
+  tracking the bound set, requires comparison/`is` inputs to be
+  already bound, and special-cases `=` (binds the var-side; both
+  sides must include at least one bound to bind the other). Phase 3's
+  simple safety check stays in db.sx as a forward-reference fallback;
+  builtins.sx redefines `dl-rule-check-safety` to the comprehensive
+  version. eval.sx's `dl-match-lit` now dispatches built-ins through
+  `dl-eval-builtin`. 19 builtins tests; conformance 106 / 106.
+
+- 2026-05-07 — Phase 3 done. `lib/datalog/db.sx` (~250 LOC) holds facts
+  indexed by relation name plus the rules list, with `dl-add-fact!` /
+  `dl-add-rule!` (rejects non-ground facts and unsafe rules);
+  `lib/datalog/eval.sx` (~150 LOC) implements the naive bottom-up
+  fixpoint via `dl-find-bindings`/`dl-match-positive`/`dl-saturate!`
+  and `dl-query` (deduped projected substitutions). Safety analysis
+  rejects unsafe head vars at load time. Negation and arithmetic
+  built-ins raise clean errors (lifted in later phases). 15 eval
+  tests cover transitive closure, sibling, same-generation, cyclic
+  graph reach, and six safety violations. Conformance 87 / 87.
+
+- 2026-05-07 — Phase 2 done. `lib/datalog/unify.sx` (~140 LOC):
+  `dl-var?` (case + underscore), `dl-walk`, `dl-bind`, `dl-unify` (returns
+  extended dict subst or `nil`), `dl-apply-subst`, `dl-ground?`, `dl-vars-of`.
+  Substitutions are immutable dicts; `assoc` builds extended copies. 28
+  unify tests; conformance now 72 / 72.
+
+- 2026-05-07 — Phase 1 done. `lib/datalog/tokenizer.sx` (~190 LOC) emits
+  `{:type :value :pos}` tokens; `lib/datalog/parser.sx` (~150 LOC) produces
+  `{:head … :body …}` / `{:query …}` clauses, with nested compounds
+  permitted for arithmetic and `not(...)` desugared to `{:neg …}`. 44 / 44
+  via `bash lib/datalog/conformance.sh` (26 tokenize + 18 parse). Local
+  helpers namespace-prefixed (`dl-emit!`, `dl-peek`) after a host-primitive
+  shadow clash. Test harness uses a custom `dl-deep-equal?` that handles
+  out-of-order dict keys and number repr (`equal?` fails on dict key order
+  and on `30` vs `30.0`).