From 0cb0c1b7827890b754d621cd4ecfa520618110e4 Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 9 May 2026 14:08:44 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=205=20polish=20=E2=80=94=20=3D/=3D?= =?UTF-8?q?=20disequality=20with=20constraint=20store?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (=/= 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 | 71 ++++++++++++++++++++++++++++++ lib/minikanren/tests/diseq.sx | 83 +++++++++++++++++++++++++++++++++++ 2 files changed, 154 insertions(+) create mode 100644 lib/minikanren/diseq.sx create mode 100644 lib/minikanren/tests/diseq.sx diff --git a/lib/minikanren/diseq.sx b/lib/minikanren/diseq.sx new file mode 100644 index 00000000..1567287e --- /dev/null +++ b/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)))))))))) diff --git a/lib/minikanren/tests/diseq.sx b/lib/minikanren/tests/diseq.sx new file mode 100644 index 00000000..e88fc5bc --- /dev/null +++ b/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!)