datalog: unification + substitution + 28 tests (Phase 2, 72/72)

dl-unify returns immutable extended subst dict (or nil). dl-walk
chases bindings, dl-apply-subst recursively resolves vars. Lists
unify element-wise so arithmetic compounds work too. dl-ground? and
dl-vars-of for safety analysis (Phase 3).

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))))))