Merge pull request #17 from brandonwillard/fix-isinstanceo-bug

Perform a constraint-specific grounded check in PredicateStore

kanren/constraints.py

@@ -6,6 +6,8 @@
 
 from toolz import groupby
 
+from cons.core import ConsPair
+
 from unification import unify, reify, Var, var
 from unification.core import _reify, isground
 
@@ -274,6 +276,10 @@ def neq_goal(S):
 class PredicateStore(ConstraintStore, ABC):
     """An abstract store for testing simple predicates."""
 
+    # Require that all constraints be satisfied for a term; otherwise, succeed
+    # if only one is satisfied.
+    require_all_constraints = True
+
     # @abstractmethod
     # def cterm_type_check(self, lvt):
     #     """Check the type of the constrained term when it's ground."""
@@ -292,49 +298,61 @@ def constraint_check(self, lv, lvt):
         """
         raise NotImplementedError()
 
+    @abstractmethod
+    def constraint_isground(self, lv, lvar_map):
+        """Check whether or not the constrained term is "ground enough" to be checked."""
+        raise NotImplementedError()
+
     def post_unify_check(self, lvar_map, lvar=None, value=None, old_state=None):
 
         for lv_key, constraints in list(self.lvar_constraints.items()):
 
             lv = reify(lv_key, lvar_map)
 
-            is_lv_ground = isground(lv, lvar_map)
+            is_lv_ground = self.constraint_isground(lv, lvar_map) or isground(
+                lv, lvar_map
+            )
+
+            if not is_lv_ground:
+                # This constraint isn't ready to be checked
+                continue
+
             # if is_lv_ground and not self.cterm_type_check(lv):
             #     self.lvar_constraints[lv_key]
             #     return False
 
-            constraints = reify(tuple(constraints), lvar_map)
-
-            constraint_grps = groupby(lambda x: isground(x, lvar_map), constraints)
+            constraint_grps = groupby(
+                lambda x: isground(x, lvar_map), reify(iter(constraints), lvar_map)
+            )
 
             constraints_unground = constraint_grps.get(False, ())
-            constraints_ground = tuple(
-                lvt
-                for lvt in constraint_grps.get(True, ())
-                if self.cparam_type_check(lvt)
-            )
+            constraints_ground = constraint_grps.get(True, ())
 
-            # There are no unground types and no valid ground types;
-            # this means that we had some invalid type values.
-            # Fail and remove constraint
-            if len(constraints_unground) == 0 and len(constraints_ground) == 0:
-                del self.lvar_constraints[lv_key]
+            if len(constraints_ground) > 0 and not all(
+                self.cparam_type_check(c) for c in constraints_ground
+            ):
+                # Some constraint parameters aren't the correct type, so fail.
+                # del self.lvar_constraints[lv_key]
                 return False
 
-            # FIXME TODO: This should be "is ground"
+            assert constraints_unground or constraints_ground
+
             if is_lv_ground and len(constraints_unground) == 0:
-                any_satisfied = any(
+
+                if self.require_all_constraints and any(
+                    not self.constraint_check(lv, t) for t in constraints_ground
+                ):
+                    return False
+                elif not self.require_all_constraints and not any(
                     self.constraint_check(lv, t) for t in constraints_ground
-                )
+                ):
+                    return False
 
-                del self.lvar_constraints[lv_key]
+                # The instance and constraint parameters are all ground and the
+                # constraint is satisfied, so, since nothing should change from
+                # here on, we can remove the constraint.
 
-                # When the instance and all types are ground and none of them
-                # are satisfactory, we're done checking.
-                if not any_satisfied:
-                    return False
-                else:
-                    return True
+                del self.lvar_constraints[lv_key]
 
         # Some types are unground, so we continue checking until they are
         return True
@@ -346,11 +364,19 @@ def pre_unify_check(self, lvar_map, lvar=None, value=None):
 class TypeStore(PredicateStore):
     """A constraint store for asserting object types."""
 
+    require_all_constraints = True
+
     op_str = "typeo"
 
     def __init__(self, lvar_constraints=None):
         super().__init__(lvar_constraints)
 
+    def add(self, lvt, cparams):
+        if lvt in self.lvar_constraints:
+            raise ValueError("Only one type constraint can be applied to a term")
+
+        return super().add(lvt, cparams)
+
     # def cterm_type_check(self, lvt):
     #     return True
 
@@ -360,6 +386,9 @@ def cparam_type_check(self, x):
     def constraint_check(self, x, cx):
         return type(x) == cx
 
+    def constraint_isground(self, lv, lvar_map):
+        return not (isinstance(lv, Var) or issubclass(type(lv), ConsPair))
+
 
 def typeo(u, u_type):
     """Construct a goal specifying the type of a term."""
@@ -385,7 +414,9 @@ def typeo_goal(S):
                 S[u_lv] = u_rf
                 cs.add(u_lv, u_type_rf)
 
-            yield S
+            if cs.post_unify_check(S.data, u_rf, u_type_rf):
+                yield S
+
         elif isinstance(u_type_rf, type) and type(u_rf) == u_type_rf:
             yield S
 
@@ -397,6 +428,9 @@ class IsinstanceStore(PredicateStore):
 
     op_str = "isinstanceo"
 
+    # Satisfying any one constraint is good enough
+    require_all_constraints = False
+
     def __init__(self, lvar_constraints=None):
         super().__init__(lvar_constraints)
 
@@ -409,6 +443,9 @@ def cparam_type_check(self, lvt):
     def constraint_check(self, lv, lvt):
         return isinstance(lv, lvt)
 
+    def constraint_isground(self, lv, lvar_map):
+        return not (isinstance(lv, Var) or issubclass(type(lv), ConsPair))
+
 
 def isinstanceo(u, u_type):
     """Construct a goal specifying that a term is an instance of a type.
@@ -445,7 +482,8 @@ def isinstanceo_goal(S):
                 S[u_lv] = u_rf
                 cs.add(u_lv, u_type_rf)
 
-            yield S
+            if cs.post_unify_check(S.data, u_rf, u_type_rf):
+                yield S
 
         # elif isground(u_type, S):
         #     yield from lany(eq(u_type, u_t) for u_t in type(u).mro())(S)

tests/test_constraints.py

@@ -1,3 +1,5 @@
+from pytest import raises
+
 from itertools import permutations
 
 from unification import var, unify
@@ -220,6 +222,9 @@ def test_typeo():
     # Invalid second arg type (i.e. not a type)
     assert run(0, q_lv, typeo(1, 1)) == ()
 
+    with raises(ValueError):
+        run(0, q_lv, typeo(a_lv, str), typeo(a_lv, int))
+
     goal_sets = [
         # Logic variable instance type that's immediately ground in another
         # goal
@@ -256,12 +261,14 @@ def test_typeo():
         # arguments are ground to the value `1`, which violates the second
         # argument type expectations)
         ([typeo(q_lv, b_lv), eq(b_lv, 1), eq(b_lv, q_lv)], ()),
+        # Check a term that's unground by ground enough for this constraint
+        ([typeo(a_lv, tuple), eq([(b_lv,)], a_lv)], ()),
     ]
 
-    for goal, results in goal_sets:
+    for goal, expected in goal_sets:
         for goal_ord in permutations(goal):
             res = run(0, q_lv, *goal_ord)
-            assert res == results
+            assert res == expected
 
 
 def test_instanceo():
@@ -296,7 +303,6 @@ def test_instanceo():
         # ),
         # A non-ground, non-logic variable instance argument that changes type
         # when ground
-        # TODO FIXME: We need to do a proper "is grounded" check for this to work!
         ([isinstanceo(cons(1, q_lv), list), eq(q_lv, [])], ([],)),
         # Logic variable instance argument that's eventually grounded through
         # another logic variable
@@ -323,9 +329,11 @@ def test_instanceo():
         # arguments are ground to the value `1`, which violates the second
         # argument type expectations)
         ([isinstanceo(q_lv, b_lv), eq(b_lv, 1), eq(b_lv, q_lv)], ()),
+        # Check a term that's unground by ground enough for this constraint
+        ([isinstanceo(q_lv, tuple), eq([(b_lv,)], q_lv)], ()),
     ]
 
-    for goal, results in goal_sets:
+    for i, (goal, expected) in enumerate(goal_sets):
         for goal_ord in permutations(goal):
             res = run(0, q_lv, *goal_ord)
-            assert res == results
+            assert res == expected