mk: phase 1 — unify.sx + 48 tests, kit-driven
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
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.
This commit is contained in:
293
lib/minikanren/tests/unify.sx
Normal file
293
lib/minikanren/tests/unify.sx
Normal file
@@ -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!)
|
||||
52
lib/minikanren/unify.sx
Normal file
52
lib/minikanren/unify.sx
Normal file
@@ -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)))
|
||||
Reference in New Issue
Block a user