mk: phase 5 polish — =/= disequality with constraint store

(=/= u v) posts a closure to the same _fd constraint store the
CLP(FD) goals use; the closure is fd-fire-store-driven, so it
re-checks after every binding.

Semantics:
  - mk-unify u v s; nil result -> distinct, drop the constraint.
  - unify succeeded with no new bindings (key-count unchanged) -> equal,
    fail.
  - otherwise -> partially unifiable, keep the constraint.

==-cs is the constraint-aware drop-in for == that fires fd-fire-store
after the binding; plain == doesn't reactivate the store, so a binding
that should violate a pending =/= would go undetected. Use ==-cs
whenever a program mixes =/= (or fd-* goals re-checked after non-FD
bindings) with regular unification.

12 new tests covering ground/structural/late-binding cases; 60/60
clpfd-and-diseq tests pass.

lib/minikanren/diseq.sx

@@ -0,0 +1,71 @@
+;; lib/minikanren/diseq.sx — Phase 5 polish: =/= disequality with a
+;; constraint store, generalising nafc / fd-neq to logic terms.
+;;
+;; The constraint store lives under the same `_fd` reserved key as the
+;; CLP(FD) propagators (a disequality is just another constraint
+;; closure that the existing fd-fire-store machinery re-runs).
+;;
+;; =/= semantics:
+;;   - If u and v walk to ground non-unifiable terms, succeed (drop).
+;;   - If they walk to terms that COULD become equal under a future
+;;     binding, store the constraint; re-check after each binding.
+;;   - If they're already equal (unify with no new bindings), fail.
+;;
+;; Implementation: each =/= test attempts (mk-unify wu wv s).
+;;   nil      — distinct, keep s, drop the constraint (return s).
+;;   subst eq — equal, fail (return nil).
+;;   subst >  — partially unifiable; keep the constraint, return s.
+;;
+;; "Substitution equal to s" is detected via key-count: mk-unify only
+;; ever extends a substitution, never removes from it, so equal
+;; key-count means no new bindings were needed.
+
+(define
+  =/=-prop
+  (fn
+    (u v s)
+    (let
+      ((s-after (mk-unify u v s)))
+      (cond
+        ((= s-after nil) s)
+        ((= (len (keys s)) (len (keys s-after))) nil)
+        (:else s)))))
+
+(define
+  =/=
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (=/=-prop u v sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- constraint-aware == ---
+;;
+;; Plain `==` doesn't fire the constraint store, so a binding that
+;; should violate a pending =/= goes undetected. `==-cs` is the
+;; drop-in replacement that fires fd-fire-store after each binding.
+;; Use ==-cs in any program that mixes =/= (or fd-* goals that should
+;; re-check after non-FD bindings) with regular unification.
+
+(define
+  ==-cs
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((s2 (mk-unify u v s)))
+        (cond
+          ((= s2 nil) mzero)
+          (:else
+            (let
+              ((s3 (fd-fire-store s2)))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))

lib/minikanren/tests/diseq.sx

@@ -0,0 +1,83 @@
+;; 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!)