giles
0cb0c1b782
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 46s
(=/= 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.
72 lines
2.2 KiB
Plaintext
72 lines
2.2 KiB
Plaintext
;; 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))))))))))
|