Skip to content

Commit

Permalink
Merge pull request #24 from brandonwillard/updates-for-stream-unifica…
Browse files Browse the repository at this point in the history
…tion

Updates for stream/trampoline-based unification
  • Loading branch information
brandonwillard committed Feb 22, 2020
2 parents cd96923 + 0228b95 commit 96bea27
Show file tree
Hide file tree
Showing 5 changed files with 53 additions and 47 deletions.
15 changes: 10 additions & 5 deletions kanren/constraints.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

from unification import unify, reify, Var, var
from unification.core import _reify, isground
from unification.utils import transitive_get as walk

from .util import FlexibleSet

Expand Down Expand Up @@ -185,12 +186,16 @@ def __hash__(self):
return hash((Var, self.token))


def reify_ConstrainedState(u, S):
u_res = reify(u, S.data)
return ConstrainedVar(u_res, S)
def _reify_ConstrainedState(u, S):
u_res = walk(u, S.data)

if u_res is u:
yield ConstrainedVar(u_res, S)
else:
yield _reify(u_res, S)

_reify.add((Var, ConstrainedState), reify_ConstrainedState)

_reify.add((Var, ConstrainedState), _reify_ConstrainedState)


class DisequalityStore(ConstraintStore):
Expand Down Expand Up @@ -398,7 +403,7 @@ def typeo_goal(S):

u_rf, u_type_rf = reify((u, u_type), S)

if not isground(u_rf, S) or not isground(u_type, S):
if not isground(u_rf, S) or not isground(u_type_rf, S):

if not isinstance(S, ConstrainedState):
S = ConstrainedState(S)
Expand Down
23 changes: 11 additions & 12 deletions kanren/term.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
from collections.abc import Sequence
from collections.abc import Sequence, Mapping

from unification import unify, reify
from unification.core import _unify, _reify
from unification.core import _unify, _reify, construction_sentinel

from cons.core import cons

Expand All @@ -17,23 +16,23 @@ def term_Sequence(rator, rands):


def unifiable_with_term(cls):
_reify.add((cls, dict), reify_term)
_unify.add((cls, cls, dict), unify_term)
_reify.add((cls, Mapping), reify_term)
_unify.add((cls, cls, Mapping), unify_term)
return cls


def reify_term(obj, s):
op, args = operator(obj), arguments(obj)
op = reify(op, s)
args = reify(args, s)
new = term(op, args)
return new
op = yield _reify(op, s)
args = yield _reify(args, s)
yield construction_sentinel
yield term(op, args)


def unify_term(u, v, s):
u_op, u_args = operator(u), arguments(u)
v_op, v_args = operator(v), arguments(v)
s = unify(u_op, v_op, s)
s = yield _unify(u_op, v_op, s)
if s is not False:
s = unify(u_args, v_args, s)
return s
s = yield _unify(u_args, v_args, s)
yield s
6 changes: 3 additions & 3 deletions setup.py
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@
packages=["kanren"],
install_requires=[
"toolz",
"cons",
"cons >= 0.4.0",
"multipledispatch",
"etuples >= 0.1.1",
"logical-unification >= 0.3.2",
"etuples >= 0.3.1",
"logical-unification >= 0.4.1",
],
tests_require=["pytest", "sympy"],
long_description=open("README.md").read() if exists("README.md") else "",
Expand Down
9 changes: 1 addition & 8 deletions tests/test_assoccomm.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

from cons import cons

from unification import reify, var, variables, isvar, unify
from unification import reify, var, isvar, unify

from kanren.core import goaleval, run_all as run
from kanren.facts import fact
Expand Down Expand Up @@ -569,10 +569,3 @@ def test_assoccomm_objects():
assert run(0, True, eq_assoccomm(add(1, 2, 3), add(3, 1, 2))) == (True,)
assert run(0, x, eq_assoccomm(add(1, 2, 3), add(1, 2, x))) == (3,)
assert run(0, x, eq_assoccomm(add(1, 2, 3), add(x, 2, 1))) == (3,)

v = add(1, 2, 3)
with variables(v):
x = add(5, 6)
# TODO: There are two more cases here, but they're in tuple form.
# See `test_eq_comm_object`.
assert x in run(0, v, eq_assoccomm(v, x))
47 changes: 28 additions & 19 deletions tests/test_constraints.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@

from itertools import permutations

from unification import var, unify
from unification.core import _reify
from unification import var, unify, reify
from unification.core import _reify, stream_eval

from cons import cons

Expand Down Expand Up @@ -90,8 +90,8 @@ def test_reify():
assert repr(ConstrainedVar(var_a, ks)) == "~a: {neq {1, 2}}"

# TODO: Make this work with `reify` when `var('a')` isn't in `ks`.
assert isinstance(_reify(var_a, ks), ConstrainedVar)
assert repr(_reify(var_a, ks)) == "~a: {neq {1, 2}}"
assert isinstance(reify(var_a, ks), ConstrainedVar)
assert repr(stream_eval(_reify(var_a, ks))) == "~a: {neq {1, 2}}"


def test_ConstraintStore():
Expand All @@ -116,7 +116,7 @@ def test_ConstrainedVar():
assert a_clv in {a_lv}


def test_disequality():
def test_disequality_basic():

a_lv, b_lv = var(), var()

Expand Down Expand Up @@ -164,6 +164,10 @@ def test_disequality():
res = list(lconj(eq(a_lv, 1), neq(a_lv, 1))({}))
assert res == []


def test_disequality():

a_lv, b_lv = var(), var()
q_lv, c_lv = var(), var()

goal_sets = [
Expand Down Expand Up @@ -203,17 +207,16 @@ def test_disequality():
for goal_ord in permutations(goal):

res = list(lconj(*goal_ord)({}))
assert len(res) == num_results
assert len(res) == num_results, (i, goal_ord)

res = list(lconj(*goal_ord)(ConstrainedState()))
assert len(res) == num_results
assert len(res) == num_results, (i, goal_ord)

assert len(run(0, q_lv, *goal_ord)) == num_results
assert len(run(0, q_lv, *goal_ord)) == num_results, (i, goal_ord)


def test_typeo():

a_lv, b_lv, q_lv = var(), var(), var()
def test_typeo_basic():
a_lv, q_lv = var(), var()

assert run(0, q_lv, typeo(q_lv, int)) == (q_lv,)
assert run(0, q_lv, typeo(1, int)) == (q_lv,)
Expand All @@ -230,17 +233,20 @@ def test_typeo():
with raises(ValueError):
run(0, q_lv, typeo(a_lv, str), typeo(a_lv, int))


def test_typeo():
a_lv, b_lv, q_lv = var(), var(), var()

goal_sets = [
# Logic variable instance type that's immediately ground in another
# goal
([typeo(q_lv, int), eq(q_lv, 1)], (1,)),
# Use an unhashable constrained term
([typeo(q_lv, list), eq(q_lv, [])], ([],)),
# A constraint parameter that is never ground
# TODO: A constraint parameter that is never ground
# ([typeo(a_lv, q_lv), eq(a_lv, 1)], (int,)),
# A non-ground, non-logic variable instance argument that changes type
# when ground
# NOTE: We can't do that until we have/use a proper "is ground" check
([typeo(cons(1, a_lv), list), eq(a_lv, [])], (q_lv,)),
# Logic variable instance and type arguments
([typeo(q_lv, int), eq(b_lv, 1), eq(b_lv, q_lv)], (1,)),
Expand Down Expand Up @@ -270,15 +276,14 @@ def test_typeo():
([typeo(a_lv, tuple), eq([(b_lv,)], a_lv)], ()),
]

for goal, expected 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 == expected
assert res == expected, (i, goal_ord)


def test_instanceo():

b_lv, q_lv = var(), var()
def test_instanceo_basic():
q_lv = var()

assert run(0, q_lv, isinstanceo(q_lv, int)) == (q_lv,)
assert run(0, q_lv, isinstanceo(1, int)) == (q_lv,)
Expand All @@ -292,6 +297,10 @@ def test_instanceo():
# Invalid second arg type (i.e. not a type)
assert run(0, q_lv, isinstanceo(1, 1)) == ()


def test_instanceo():
b_lv, q_lv = var(), var()

goal_sets = [
# Logic variable instance type that's immediately ground in another
# goal
Expand Down Expand Up @@ -341,4 +350,4 @@ def test_instanceo():
for i, (goal, expected) in enumerate(goal_sets):
for goal_ord in permutations(goal):
res = run(0, q_lv, *goal_ord)
assert res == expected
assert res == expected, (i, goal_ord)

0 comments on commit 96bea27

Please sign in to comment.