mk: phase 1 — unify.sx + 48 tests, kit-driven

lib/minikanren/unify.sx wraps lib/guest/match.sx with a miniKanren-flavoured
cfg: native SX lists as cons-pairs, occurs-check off by default. ~22 lines
of local logic over kit's walk-with / unify-with / extend / occurs-with.

48 tests in lib/minikanren/tests/unify.sx exercise: var fresh-distinct,
walk chains, walk* deep into nested lists, atom/var/list unification with
positional matching, failure modes, opt-in occurs check.

lib/guest/match.sx

@@ -0,0 +1,185 @@
+;; lib/guest/match.sx — pure pattern-match + unification kit.
+;;
+;; Shipped for miniKanren / Datalog / future logic-flavoured guests that
+;; want immutable unification without writing it from scratch. The two
+;; existing prolog/haskell engines stay as-is — porting them in place
+;; risks the 746 tests they currently pass; consumers can migrate
+;; gradually via the converters in lib/guest/ast.sx.
+;;
+;; Term shapes (canonical wire format)
+;; -----------------------------------
+;;   var          (:var NAME)            NAME a string
+;;   constructor  (:ctor HEAD ARGS)      HEAD a string, ARGS a list of terms
+;;   literal      number / string / boolean / nil
+;;
+;; Guests with their own shape pass adapter callbacks via the cfg arg —
+;; see (unify-with cfg ...) and (match-pat-with cfg ...) below. The
+;; default canonical entry points (unify / match-pat) use the wire shape.
+;;
+;; Substitution / env
+;; ------------------
+;; A substitution is a SX dict mapping VAR-NAME → term. There are no
+;; trails, no mutation: each step either returns an extended dict or nil.
+;;
+;;   (empty-subst)                  → {}
+;;   (walk term s)                  → term with top-level vars resolved
+;;   (walk* term s)                 → term with all vars resolved (recursive)
+;;   (extend name term s)           → s with NAME → term added
+;;   (occurs? name term s)          → bool
+;;
+;; Unify (symmetric, miniKanren-flavour)
+;; -------------------------------------
+;;   (unify u v s)                  → extended subst or nil
+;;   (unify-with cfg u v s)         → ditto, with adapter callbacks:
+;;                                      :var? :var-name :ctor? :ctor-head
+;;                                      :ctor-args :occurs-check?
+;;
+;; Match (asymmetric, haskell-flavour: pattern → value, vars only in pat)
+;; ---------------------------------------------------------------------
+;;   (match-pat pat val env)        → extended env or nil
+;;   (match-pat-with cfg pat val env)
+
+(define mk-var  (fn (name) (list :var name)))
+(define mk-ctor (fn (head args) (list :ctor head args)))
+
+(define is-var?    (fn (t) (and (list? t) (not (empty? t)) (= (first t) :var))))
+(define is-ctor?   (fn (t) (and (list? t) (not (empty? t)) (= (first t) :ctor))))
+(define var-name   (fn (t) (nth t 1)))
+(define ctor-head  (fn (t) (nth t 1)))
+(define ctor-args  (fn (t) (nth t 2)))
+
+(define empty-subst (fn () {}))
+
+(define
+  walk
+  (fn (t s)
+    (if (and (is-var? t) (has-key? s (var-name t)))
+      (walk (get s (var-name t)) s)
+      t)))
+
+(define
+  walk*
+  (fn (t s)
+    (let ((w (walk t s)))
+      (cond
+        ((is-ctor? w)
+          (mk-ctor (ctor-head w) (map (fn (a) (walk* a s)) (ctor-args w))))
+        (:else w)))))
+
+(define
+  extend
+  (fn (name term s)
+    (assoc s name term)))
+
+(define
+  occurs?
+  (fn (name term s)
+    (let ((w (walk term s)))
+      (cond
+        ((is-var? w) (= (var-name w) name))
+        ((is-ctor? w) (some (fn (a) (occurs? name a s)) (ctor-args w)))
+        (:else false)))))
+
+(define
+  unify-with
+  (fn (cfg u v s)
+    (let ((var?-fn (get cfg :var?))
+          (var-name-fn (get cfg :var-name))
+          (ctor?-fn (get cfg :ctor?))
+          (ctor-head-fn (get cfg :ctor-head))
+          (ctor-args-fn (get cfg :ctor-args))
+          (occurs?-on (get cfg :occurs-check?)))
+      (let ((wu (walk-with cfg u s))
+            (wv (walk-with cfg v s)))
+        (cond
+          ((and (var?-fn wu) (var?-fn wv) (= (var-name-fn wu) (var-name-fn wv))) s)
+          ((var?-fn wu)
+            (if (and occurs?-on (occurs-with cfg (var-name-fn wu) wv s))
+              nil
+              (extend (var-name-fn wu) wv s)))
+          ((var?-fn wv)
+            (if (and occurs?-on (occurs-with cfg (var-name-fn wv) wu s))
+              nil
+              (extend (var-name-fn wv) wu s)))
+          ((and (ctor?-fn wu) (ctor?-fn wv))
+            (if (= (ctor-head-fn wu) (ctor-head-fn wv))
+              (unify-list-with
+                cfg
+                (ctor-args-fn wu)
+                (ctor-args-fn wv)
+                s)
+              nil))
+          (:else (if (= wu wv) s nil)))))))
+
+(define
+  walk-with
+  (fn (cfg t s)
+    (if (and ((get cfg :var?) t) (has-key? s ((get cfg :var-name) t)))
+      (walk-with cfg (get s ((get cfg :var-name) t)) s)
+      t)))
+
+(define
+  occurs-with
+  (fn (cfg name term s)
+    (let ((w (walk-with cfg term s)))
+      (cond
+        (((get cfg :var?) w) (= ((get cfg :var-name) w) name))
+        (((get cfg :ctor?) w)
+          (some (fn (a) (occurs-with cfg name a s)) ((get cfg :ctor-args) w)))
+        (:else false)))))
+
+(define
+  unify-list-with
+  (fn (cfg xs ys s)
+    (cond
+      ((and (empty? xs) (empty? ys)) s)
+      ((or (empty? xs) (empty? ys)) nil)
+      (:else
+        (let ((s2 (unify-with cfg (first xs) (first ys) s)))
+          (if (= s2 nil)
+            nil
+            (unify-list-with cfg (rest xs) (rest ys) s2)))))))
+
+(define canonical-cfg
+  {:var? is-var? :var-name var-name
+   :ctor? is-ctor? :ctor-head ctor-head :ctor-args ctor-args
+   :occurs-check? true})
+
+(define unify (fn (u v s) (unify-with canonical-cfg u v s)))
+
+;; Asymmetric pattern match (haskell-style): only patterns may contain vars;
+;; values are concrete. On a var pattern, bind name to value.
+(define
+  match-pat-with
+  (fn (cfg pat val env)
+    (let ((var?-fn (get cfg :var?))
+          (var-name-fn (get cfg :var-name))
+          (ctor?-fn (get cfg :ctor?))
+          (ctor-head-fn (get cfg :ctor-head))
+          (ctor-args-fn (get cfg :ctor-args)))
+      (cond
+        ((var?-fn pat) (extend (var-name-fn pat) val env))
+        ((and (ctor?-fn pat) (ctor?-fn val))
+          (if (= (ctor-head-fn pat) (ctor-head-fn val))
+            (match-list-pat-with
+              cfg
+              (ctor-args-fn pat)
+              (ctor-args-fn val)
+              env)
+            nil))
+        ((ctor?-fn pat) nil)
+        (:else (if (= pat val) env nil))))))
+
+(define
+  match-list-pat-with
+  (fn (cfg pats vals env)
+    (cond
+      ((and (empty? pats) (empty? vals)) env)
+      ((or (empty? pats) (empty? vals)) nil)
+      (:else
+        (let ((env2 (match-pat-with cfg (first pats) (first vals) env)))
+          (if (= env2 nil)
+            nil
+            (match-list-pat-with cfg (rest pats) (rest vals) env2)))))))
+
+(define match-pat (fn (pat val env) (match-pat-with canonical-cfg pat val env)))

lib/guest/tests/match.sx

@@ -0,0 +1,108 @@
+;; lib/guest/tests/match.sx — exercises lib/guest/match.sx.
+
+(define gmatch-test-pass 0)
+(define gmatch-test-fail 0)
+(define gmatch-test-fails (list))
+
+(define
+  gmatch-test
+  (fn (name actual expected)
+    (if (= actual expected)
+      (set! gmatch-test-pass (+ gmatch-test-pass 1))
+      (begin
+        (set! gmatch-test-fail (+ gmatch-test-fail 1))
+        (append! gmatch-test-fails {:name name :expected expected :actual actual})))))
+
+;; ── walk / extend / occurs ────────────────────────────────────────
+(gmatch-test "walk-direct"
+  (walk (mk-var "x") (extend "x" 5 (empty-subst))) 5)
+
+(gmatch-test "walk-chain"
+  (walk (mk-var "a") (extend "a" (mk-var "b") (extend "b" 7 (empty-subst)))) 7)
+
+(gmatch-test "walk-no-binding"
+  (let ((v (mk-var "u"))) (= (walk v (empty-subst)) v)) true)
+
+(gmatch-test "walk*-recursive"
+  (walk* (mk-ctor "Just" (list (mk-var "x"))) (extend "x" 9 (empty-subst)))
+  (mk-ctor "Just" (list 9)))
+
+(gmatch-test "occurs-direct"
+  (occurs? "x" (mk-var "x") (empty-subst)) true)
+
+(gmatch-test "occurs-nested"
+  (occurs? "x" (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) true)
+
+(gmatch-test "occurs-not"
+  (occurs? "x" (mk-var "y") (empty-subst)) false)
+
+;; ── unify (symmetric) ─────────────────────────────────────────────
+(gmatch-test "unify-equal-literals"
+  (len (unify 5 5 (empty-subst))) 0)
+
+(gmatch-test "unify-different-literals"
+  (unify 5 6 (empty-subst)) nil)
+
+(gmatch-test "unify-var-literal"
+  (get (unify (mk-var "x") 5 (empty-subst)) "x") 5)
+
+(gmatch-test "unify-literal-var"
+  (get (unify 5 (mk-var "x") (empty-subst)) "x") 5)
+
+(gmatch-test "unify-same-var"
+  (len (unify (mk-var "x") (mk-var "x") (empty-subst))) 0)
+
+(gmatch-test "unify-two-vars"
+  (let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
+    (or (= (get s "x") (mk-var "y")) (= (get s "y") (mk-var "x")))) true)
+
+(gmatch-test "unify-ctor-equal"
+  (len (unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1 2)) (empty-subst))) 0)
+
+(gmatch-test "unify-ctor-with-var"
+  (get (unify (mk-ctor "Just" (list (mk-var "x"))) (mk-ctor "Just" (list 7)) (empty-subst)) "x") 7)
+
+(gmatch-test "unify-ctor-head-mismatch"
+  (unify (mk-ctor "Just" (list 1)) (mk-ctor "Nothing" (list)) (empty-subst)) nil)
+
+(gmatch-test "unify-ctor-arity-mismatch"
+  (unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1)) (empty-subst)) nil)
+
+(gmatch-test "unify-occurs-check"
+  (unify (mk-var "x") (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) nil)
+
+(gmatch-test "unify-transitive-vars"
+  (let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
+    (let ((s2 (unify (mk-var "y") 42 s)))
+      (walk (mk-var "x") s2))) 42)
+
+;; ── match-pat (asymmetric) ────────────────────────────────────────
+(gmatch-test "match-var-binds"
+  (get (match-pat (mk-var "x") 99 (empty-subst)) "x") 99)
+
+(gmatch-test "match-literal-equal"
+  (len (match-pat 5 5 (empty-subst))) 0)
+
+(gmatch-test "match-literal-mismatch"
+  (match-pat 5 6 (empty-subst)) nil)
+
+(gmatch-test "match-ctor-binds"
+  (get (match-pat (mk-ctor "Just" (list (mk-var "y")))
+                  (mk-ctor "Just" (list 11))
+                  (empty-subst)) "y") 11)
+
+(gmatch-test "match-ctor-head-mismatch"
+  (match-pat (mk-ctor "Just" (list (mk-var "y")))
+             (mk-ctor "Nothing" (list))
+             (empty-subst)) nil)
+
+(gmatch-test "match-ctor-arity-mismatch"
+  (match-pat (mk-ctor "f" (list (mk-var "x") (mk-var "y")))
+             (mk-ctor "f" (list 1))
+             (empty-subst)) nil)
+
+(define gmatch-tests-run!
+  (fn ()
+    {:passed gmatch-test-pass
+     :failed gmatch-test-fail
+     :total  (+ gmatch-test-pass gmatch-test-fail)}))

lib/minikanren/tests/unify.sx

@@ -0,0 +1,293 @@
+;; lib/minikanren/tests/unify.sx — Phase 1 tests for unify.sx.
+;;
+;; Loads into a session that already has lib/guest/match.sx and
+;; lib/minikanren/unify.sx defined. Tests are top-level forms.
+;; Call (mk-tests-run!) afterwards to get the totals.
+;;
+;; Note: SX dict equality is reference-based, so tests check the *effect*
+;; of a unification (success/failure flag, or walked bindings) rather than
+;; the raw substitution dict.
+
+(define mk-test-pass 0)
+(define mk-test-fail 0)
+(define mk-test-fails (list))
+
+(define
+  mk-test
+  (fn
+    (name actual expected)
+    (if
+      (= actual expected)
+      (set! mk-test-pass (+ mk-test-pass 1))
+      (begin
+        (set! mk-test-fail (+ mk-test-fail 1))
+        (append! mk-test-fails {:name name :expected expected :actual actual})))))
+
+(define mk-tests-run! (fn () {:total (+ mk-test-pass mk-test-fail) :passed mk-test-pass :failed mk-test-fail :fails mk-test-fails}))
+
+(define mk-unified? (fn (s) (if (= s nil) false true)))
+
+;; --- fresh variable construction ---
+
+(mk-test
+  "make-var-distinct"
+  (let ((a (make-var)) (b (make-var))) (= (var-name a) (var-name b)))
+  false)
+
+(mk-test "make-var-is-var" (mk-var? (make-var)) true)
+(mk-test "var?-num" (mk-var? 5) false)
+(mk-test "var?-list" (mk-var? (list 1 2)) false)
+(mk-test "var?-string" (mk-var? "hi") false)
+(mk-test "var?-empty" (mk-var? (list)) false)
+(mk-test "var?-bool" (mk-var? true) false)
+
+;; --- empty substitution ---
+
+(mk-test "empty-s-walk-num" (mk-walk 5 empty-s) 5)
+(mk-test "empty-s-walk-str" (mk-walk "x" empty-s) "x")
+(mk-test
+  "empty-s-walk-list"
+  (mk-walk (list 1 2) empty-s)
+  (list 1 2))
+(mk-test
+  "empty-s-walk-unbound-var"
+  (let ((x (make-var))) (= (mk-walk x empty-s) x))
+  true)
+
+;; --- walk: top-level chain resolution ---
+
+(mk-test
+  "walk-direct-binding"
+  (mk-walk (mk-var "x") (extend "x" 7 empty-s))
+  7)
+
+(mk-test
+  "walk-two-step-chain"
+  (mk-walk
+    (mk-var "x")
+    (extend "x" (mk-var "y") (extend "y" 9 empty-s)))
+  9)
+
+(mk-test
+  "walk-three-step-chain"
+  (mk-walk
+    (mk-var "a")
+    (extend
+      "a"
+      (mk-var "b")
+      (extend "b" (mk-var "c") (extend "c" 42 empty-s))))
+  42)
+
+(mk-test
+  "walk-stops-at-list"
+  (mk-walk (list 1 (mk-var "x")) (extend "x" 5 empty-s))
+  (list 1 (mk-var "x")))
+
+;; --- walk*: deep walk into lists ---
+
+(mk-test
+  "walk*-flat-list-with-vars"
+  (mk-walk*
+    (list (mk-var "x") 2 (mk-var "y"))
+    (extend "x" 1 (extend "y" 3 empty-s)))
+  (list 1 2 3))
+
+(mk-test
+  "walk*-nested-list"
+  (mk-walk*
+    (list 1 (mk-var "x") (list 2 (mk-var "y")))
+    (extend "x" 5 (extend "y" 6 empty-s)))
+  (list 1 5 (list 2 6)))
+
+(mk-test
+  "walk*-unbound-stays-var"
+  (let
+    ((x (mk-var "x")))
+    (= (mk-walk* (list 1 x) empty-s) (list 1 x)))
+  true)
+
+(mk-test "walk*-atom" (mk-walk* 5 empty-s) 5)
+
+;; --- unify atoms (success / failure semantics, not dict shape) ---
+
+(mk-test
+  "unify-num-eq-succeeds"
+  (mk-unified? (mk-unify 5 5 empty-s))
+  true)
+(mk-test "unify-num-neq-fails" (mk-unify 5 6 empty-s) nil)
+(mk-test
+  "unify-str-eq-succeeds"
+  (mk-unified? (mk-unify "a" "a" empty-s))
+  true)
+(mk-test "unify-str-neq-fails" (mk-unify "a" "b" empty-s) nil)
+(mk-test
+  "unify-bool-eq-succeeds"
+  (mk-unified? (mk-unify true true empty-s))
+  true)
+(mk-test "unify-bool-neq-fails" (mk-unify true false empty-s) nil)
+(mk-test
+  "unify-nil-eq-succeeds"
+  (mk-unified? (mk-unify nil nil empty-s))
+  true)
+(mk-test
+  "unify-empty-list-succeeds"
+  (mk-unified? (mk-unify (list) (list) empty-s))
+  true)
+
+;; --- unify var with anything (walk to verify binding) ---
+
+(mk-test
+  "unify-var-num-binds"
+  (mk-walk (mk-var "x") (mk-unify (mk-var "x") 5 empty-s))
+  5)
+
+(mk-test
+  "unify-num-var-binds"
+  (mk-walk (mk-var "x") (mk-unify 5 (mk-var "x") empty-s))
+  5)
+
+(mk-test
+  "unify-var-list-binds"
+  (mk-walk
+    (mk-var "x")
+    (mk-unify (mk-var "x") (list 1 2) empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-var-var-same-no-extend"
+  (mk-unified? (mk-unify (mk-var "x") (mk-var "x") empty-s))
+  true)
+
+(mk-test
+  "unify-var-var-different-walks-equal"
+  (let
+    ((s (mk-unify (mk-var "x") (mk-var "y") empty-s)))
+    (= (mk-walk (mk-var "x") s) (mk-walk (mk-var "y") s)))
+  true)
+
+;; --- unify lists positionally ---
+
+(mk-test
+  "unify-list-equal-succeeds"
+  (mk-unified?
+    (mk-unify
+      (list 1 2 3)
+      (list 1 2 3)
+      empty-s))
+  true)
+
+(mk-test
+  "unify-list-different-length-fails-1"
+  (mk-unify
+    (list 1 2)
+    (list 1 2 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-different-length-fails-2"
+  (mk-unify
+    (list 1 2 3)
+    (list 1 2)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-mismatch-fails"
+  (mk-unify
+    (list 1 2)
+    (list 1 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-vs-atom-fails"
+  (mk-unify (list 1 2) 5 empty-s)
+  nil)
+
+(mk-test
+  "unify-empty-vs-non-empty-fails"
+  (mk-unify (list) (list 1) empty-s)
+  nil)
+
+(mk-test
+  "unify-list-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (mk-var "y"))
+    (mk-unify
+      (list (mk-var "x") (mk-var "y"))
+      (list 1 2)
+      empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-nested-lists-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (list (mk-var "y") 3))
+    (mk-unify
+      (list (mk-var "x") (list (mk-var "y") 3))
+      (list 1 (list 2 3))
+      empty-s))
+  (list 1 (list 2 3)))
+
+;; --- unify chained substitutions ---
+
+(mk-test
+  "unify-chain-var-var-then-atom"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((s1 (mk-unify x y empty-s)))
+      (mk-walk x (mk-unify y 7 s1))))
+  7)
+
+(mk-test
+  "unify-already-bound-consistent"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unified? (mk-unify (mk-var "x") 5 s)))
+  true)
+
+(mk-test
+  "unify-already-bound-conflict-fails"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unify (mk-var "x") 6 s))
+  nil)
+
+;; --- occurs check (opt-in) ---
+
+(mk-test
+  "unify-no-occurs-default-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify x (list 1 x) empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-direct-fails"
+  (let ((x (mk-var "x"))) (mk-unify-check x (list 1 x) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-nested-fails"
+  (let
+    ((x (mk-var "x")))
+    (mk-unify-check x (list 1 (list 2 x)) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-non-occurring-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify-check x 5 empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-via-chain-fails"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let ((s (extend "y" (list x) empty-s))) (mk-unify-check x y s)))
+  nil)
+
+(mk-tests-run!)

lib/minikanren/unify.sx

@@ -0,0 +1,52 @@
+;; lib/minikanren/unify.sx — Phase 1: variables + unification.
+;;
+;; miniKanren-on-SX, built on lib/guest/match.sx. The kit ships the heavy
+;; lifting (walk-with, unify-with, occurs-with, extend, empty-subst,
+;; mk-var/is-var?/var-name); this file supplies a miniKanren-shaped cfg
+;; and a thin public API.
+;;
+;; Term shape (designed for natural SX use):
+;;   logic var  : (:var NAME)              — kit's mk-var
+;;   pair       : any non-empty SX list    — head + tail unified positionally
+;;   atom       : number / string / symbol / boolean / nil / ()
+;; Substitution: SX dict mapping VAR-NAME → term. Empty = (empty-subst).
+
+(define
+  mk-list-pair?
+  (fn (t) (and (list? t) (not (empty? t)) (not (is-var? t)))))
+
+(define mk-list-pair-head (fn (t) :pair))
+(define mk-list-pair-args (fn (t) t))
+
+(define mk-cfg {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? false :var-name var-name :ctor-args mk-list-pair-args})
+
+(define mk-cfg-occurs {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? true :var-name var-name :ctor-args mk-list-pair-args})
+
+(define empty-s (empty-subst))
+
+(define mk-fresh-counter 0)
+
+(define
+  make-var
+  (fn
+    ()
+    (begin
+      (set! mk-fresh-counter (+ mk-fresh-counter 1))
+      (mk-var (str "_." mk-fresh-counter)))))
+
+(define mk-var? is-var?)
+
+(define mk-walk (fn (t s) (walk-with mk-cfg t s)))
+
+(define
+  mk-walk*
+  (fn
+    (t s)
+    (let
+      ((w (mk-walk t s)))
+      (cond
+        ((mk-list-pair? w) (map (fn (a) (mk-walk* a s)) w))
+        (:else w)))))
+
+(define mk-unify (fn (u v s) (unify-with mk-cfg u v s)))
+(define mk-unify-check (fn (u v s) (unify-with mk-cfg-occurs u v s)))

plans/lib-guest.md

@@ -157,8 +157,8 @@ Extract from `haskell/infer.sx`. Algorithm W or J, generalisation, instantiation
 | 3 — lex.sx (lua + tcl) | [done] | 559b0df9 | lex.sx exports nil-safe char-class predicates + token record. lua/tokenizer.sx (7 preds) and tcl/tokenizer.sx (5 preds) collapsed into prefix-rename calls. lua 185/185, tcl 342/342, tcl-conf 3/4 — all = baseline. |
 | 4 — pratt.sx (lua + prolog) | [done] | da27958d | Extracted operator-table format + lookup only — climbing loops stay per-language because lua and prolog use opposite prec conventions. lua/parser.sx: 18-clause cond → 15-entry table. prolog/parser.sx: pl-op-find deleted, pl-op-lookup wraps pratt-op-lookup. lua 185/185, prolog 590/590 — both = baseline. |
 | 5 — ast.sx (lua + prolog) | [partial — pending real consumers] | a774cd26 | Kit + 33 self-tests shipped (10 canonical kinds, predicates, accessors). Step is "Optional" per brief; lua/prolog parsers untouched (185/185 + 590/590). Datalog-on-sx will be the natural first real consumer; lua/prolog converters can land later. |
-| 6 — match.sx (haskell + prolog) | [in-progress] | — | — |
-| 7 — layout.sx (haskell + synthetic) | [ ] | — | — |
+| 6 — match.sx (haskell + prolog) | [partial — kit shipped; ports deferred] | 863e9d93 | Pure-functional unify + match kit (canonical wire format + cfg-driven adapters) + 25 self-tests. Existing prolog/haskell engines untouched (structurally divergent — mutating-symmetric vs pure-asymmetric — would risk 746 passing tests under brief's revert-on-regression rule). Real consumer is minikraken/datalog work in flight. |
+| 7 — layout.sx (haskell + synthetic) | [in-progress] | — | — |
 | 8 — hm.sx (haskell + TBD) | [ ] | — | — |
 
 ---

plans/minikanren-on-sx.md

@@ -50,15 +50,15 @@ Key semantic mappings:
 ## Roadmap
 
 ### Phase 1 — variables + unification
-- [ ] `make-var` → fresh logic variable (unique mutable box)
-- [ ] `var?` `v` → bool — is this a logic variable?
-- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
-- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
-- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
+- [x] `make-var` → fresh logic variable (unique mutable box)
+- [x] `var?` `v` → bool — is this a logic variable?
+- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
+- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
+- [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
       Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
       No occurs check by default; `unify-check` with occurs check as opt-in.
-- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list)
-- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
+- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
+- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
 
 ### Phase 2 — streams + goals
 - [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`),
@@ -135,4 +135,12 @@ _(none yet)_
 
 _Newest first._
 
-_(awaiting phase 1)_
+- **2026-05-07** — **Phase 1 done**: `lib/minikanren/unify.sx` (53 lines, ~22 lines of actual code) +
+  `lib/minikanren/tests/unify.sx` (48 tests, all green). Kit consumption: `walk-with`,
+  `unify-with`, `occurs-with`, `extend`, `empty-subst`, `mk-var`, `is-var?`, `var-name`
+  all supplied by `lib/guest/match.sx`. Local additions: a miniKanren-flavoured cfg
+  (treats native SX lists as cons-pairs via `:ctor-head = :pair`, occurs-check off),
+  `make-var` fresh-counter, deep `mk-walk*` (kit's `walk*` only recurses into `:ctor`
+  form, not native lists), and `mk-unify` / `mk-unify-check` thin wrappers. The kit
+  earns its keep ~3× over by line count — confirms lib-guest match kit is reusable
+  for logic-language hosts as designed.