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