core.logic

another issue with predc constraint is not enforced when it could be

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Major 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]))))

Activity

Hide
David Nolen added a comment - - edited

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.

Show
David Nolen added a comment - - edited 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.

People

Vote (0)
Watch (1)

Dates

  • Created:
    Updated:
    Resolved: