;; lib/minikanren/tests/diseq.sx — Phase 5 polish: =/= disequality.

;; --- ground cases ---

(mk-test
  "=/=-ground-distinct"
  (run* q (=/= 1 2))
  (list (make-symbol "_.0")))
(mk-test "=/=-ground-equal" (run* q (=/= 1 1)) (list))
(mk-test
  "=/=-ground-strings"
  (run* q (=/= "a" "b"))
  (list (make-symbol "_.0")))
(mk-test "=/=-ground-strings-eq" (run* q (=/= "a" "a")) (list))

;; --- structural ---

(mk-test
  "=/=-pair-distinct"
  (run* q (=/= (list 1 2) (list 1 3)))
  (list (make-symbol "_.0")))
(mk-test
  "=/=-pair-equal"
  (run* q (=/= (list 1 2) (list 1 2)))
  (list))
(mk-test
  "=/=-pair-vs-atom"
  (run* q (=/= (list 1) 1))
  (list (make-symbol "_.0")))

;; --- partial / late binding ---
;;
;; ==-cs is required to wake up the constraint store after a binding;
;; plain == doesn't fire constraints.

(mk-test
  "=/=-late-bind-violates"
  (run* q (fresh (x) (=/= x 5) (==-cs x 5) (== q x)))
  (list))

(mk-test
  "=/=-late-bind-ok"
  (run* q (fresh (x) (=/= x 5) (==-cs x 7) (== q x)))
  (list 7))

(mk-test
  "=/=-two-vars-equal-late-fails"
  (run*
    q
    (fresh
      (x y)
      (=/= x y)
      (==-cs x 1)
      (==-cs y 1)
      (== q (list x y))))
  (list))

(mk-test
  "=/=-two-vars-distinct-late"
  (run*
    q
    (fresh
      (x y)
      (=/= x y)
      (==-cs x 1)
      (==-cs y 2)
      (== q (list x y))))
  (list (list 1 2)))

;; --- compose with conde / fresh ---

(mk-test
  "=/=-with-membero-filter"
  (run*
    q
    (fresh
      (x)
      (membero x (list 1 2 3))
      (=/= x 2)
      (== q x)))
  (list 1 3))

(mk-tests-run!)