Details
-
Type:
Defect
-
Status:
Closed
-
Priority:
Major
-
Resolution: Completed
-
Affects Version/s: None
-
Fix Version/s: None
-
Component/s: None
-
Labels:None
Description
This returns ([1 1]) instead of ().
(run* [q]
(fresh [x y]
(predc y even? `even?)
(predc x odd? `odd)
(== x y)
(== x 1)
(== q [x y]))))
This is actually related to the deeper problem also demonstrated by
LOGIC-77. The problem is that cKanren checks constraints via "update-prefix" which calls "update" which calls "run-constraints*". "update" is called on the Substitution prior to unification. This creates all kinds of issues as it's during unification that we "migrate" constraints from one logic var to another.I'm pondering eliminating "update" and moving "run-constraints*" lower into the system - perhaps at the level of "ext-no-check". A related change would be putting SubstValue smarts into "ext-no-check". For example a "ext-no-check" on a unbound constrained logic var would simply update its SubstValue. This is critical as SubstValue might contain constraint information that must be preserved.
LOGIC-77. The problem is that cKanren checks constraints via "update-prefix" which calls "update" which calls "run-constraints*". "update" is called on the Substitution prior to unification. This creates all kinds of issues as it's during unification that we "migrate" constraints from one logic var to another. I'm pondering eliminating "update" and moving "run-constraints*" lower into the system - perhaps at the level of "ext-no-check". A related change would be putting SubstValue smarts into "ext-no-check". For example a "ext-no-check" on a unbound constrained logic var would simply update its SubstValue. This is critical as SubstValue might contain constraint information that must be preserved.