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