import fol


def test_unify_simple():
    subst = fol.unify(
        fol.p('Hello(x)'),
        fol.p('Hello(ALICE)')
    )

    assert subst is not None
    assert len(subst) == 1
    assert str(subst['x']) == 'CONST[ALICE]'


def test_unify_equals():
    subst = fol.unify(
        fol.p('Hello(ALICE)'),
        fol.p('Hello(ALICE)')
    )

    assert subst is not None
    assert len(subst) == 0


def test_unify_different_predicate_name():
    subst = fol.unify(
        fol.p('Hello(x)'),
        fol.p('World(ALICE)')
    )

    assert subst is None


def test_unify_fun():
    subst = fol.unify(
        fol.p('Hello(x, f(x))'),
        fol.p('Hello(ALICE, f(ALICE))')
    )

    assert subst is not None
    assert len(subst) == 1
    assert str(subst['x']) == 'CONST[ALICE]'


def test_unify_two_vars():
    subst = fol.unify(
        fol.p('Hello(z, f(x), z)'),
        fol.p('Hello(ALICE, f(BOB), ALICE)')
    )

    assert subst is not None
    assert len(subst) == 2
    assert str(subst['x']) == 'CONST[BOB]'
    assert str(subst['z']) == 'CONST[ALICE]'


def test_unify_fun_var():
    subst = fol.unify(
        fol.p('Hello(z, f(x), z)'),
        fol.p('Hello(ALICE, a, ALICE)')
    )

    assert subst is not None
    assert len(subst) == 2
    assert str(subst['a']) == 'FUN[f](VAR[x])'
    assert str(subst['z']) == 'CONST[ALICE]'


def test_unify_formula():
    subst = fol.unify(
        fol.p('Friend(x, y) -> Friend(y, x)'),
        fol.p('Friend(ALICE, y) -> Friend(BOB, x)')
    )

    assert subst is not None
    assert len(subst) == 2
    assert str(subst['x']) == 'CONST[ALICE]'
    assert str(subst['y']) == 'CONST[BOB]'


def test_unify_formula_contradiction():
    subst = fol.unify(
        fol.p('Friend(x, y) -> Friend(y, x)'),
        fol.p('Friend(ALICE, y) -> Friend(BOB, CLARA)')
    )

    assert subst is None