Prol: a minimal, inefficient Prolog interpreter in a few LOCs of Python

.gitignore

pytype_output/
.pytype/
__pycache__/
*.swp
*.swo

parser.py

from prol import is_compound, to_list, solve, set_trace_on, set_trace_off

def parser_clauses():
    """Return clauses for parsing a limited subset of Prolog.
    """
    clauses = []
    def add_fact(term):
        add_clause(term)
    def add_clause(head, *body):
        assert is_compound(head), head
        for term in body:
            assert is_compound(term), term
        clauses.append((head, list(body)))
    
    add_fact(("=", "X", "X"))
    
    for i in range(ord('a'), ord('z')+1):
        add_fact(("lower", chr(i)))
    
    # '_' is added as an 'uppercase' character because it's a valid var
    # starting character.
    add_fact(("upper", "'_'"))
    for i in range(ord('A'), ord('Z')+1):
        add_fact(("upper", f"'{chr(i)}'"))
    
    for i in range(ord('0'), ord('9')+1):
        add_fact(("digit", chr(i)))
    
    for symbol in "\"#$&'*+-./:;<=>?@\\^`{|}~":
        add_fact(("symbol", symbol))
    
    for escaped in "(,)":
        add_fact(("symbol", f"'{escaped}'"))
    
    add_fact(("white", " "))
    add_fact(("white", "\n"))
    
    # Identifier chars, accepted after the first char of an atom or var.
    # ident(Ch) :- lower(Ch) ; upper(Ch) ; digit(Ch) ; symbol(Ch).
    add_clause(("ident", "Ch"),
    	   ("lower", "Ch"))
    add_clause(("ident", "Ch"),
    	   ("upper", "Ch"))
    add_clause(("ident", "Ch"),
    	   ("digit", "Ch"))
    add_clause(("ident", "Ch"),
    	   ("symbol", "Ch"))
    
    # Sequence of zero or more ident characters.
    # idents([]) --> [].
    # idents([Ch|T]) --> [Ch], { ident(Ch) }, idents(Ch).
    add_fact(("idents", "[]", "L", "L"))  
    add_clause(("idents", (".", "Ch", "T"), (".", "Ch", "L0"), "L1"),
    	   ("ident", "Ch"),
    	   ("idents", "T", "L0", "L1"))
    
    # Sequence of zero or more digit characters.
    # digits([]) --> [].
    # digits([Ch|T]) --> [Ch], { digit(Ch) }, digits(Ch).
    add_fact(("digits", "[]", "L", "L"))  
    add_clause(("digits", (".", "Ch", "T"), (".", "Ch", "L0"), "L1"),
    	   ("digit", "Ch"),
    	   ("digits", "T", "L0", "L1"))
    
    # Sequence of zero or more whitespace characters.
    # ws --> [].
    # ws --> [Ch], { white(Ch) }, ws.
    add_fact(("ws", "L", "L"))  
    add_clause(("ws", (".", "Ch", "L0"), "L1"),
    	   ("white", "Ch"),
    	   ("ws", "L0", "L1")) 
    
    # atom_start: valid characters for starting an atom.
    # atom_start(Ch) :- lower(Ch) ; symbol(Ch).
    add_clause(("atom_start", "Ch"),
    	   ("lower", "Ch"))
    add_clause(("atom_start", "Ch"),
    	   ("symbol", "Ch"))
    
    # atom: captures a sequence of characters that form an atom.
    # atom(atom([Ch|T])) --> [Ch], { atom_start(Ch) }, idents(T).
    add_clause(("atom", ("atom", (".", "Ch", "T")), (".", "Ch", "L0"), "L1"),
    	   ("atom_start", "Ch"),
    	   ("idents", "T", "L0", "L1"))
    
    # var: captures a sequence of characters that form a var.
    # var(var([Ch|T])) --> [Ch], { upper(Ch) }, idents(T).
    add_clause(("var", ("var", (".", "Ch", "T")), (".", "Ch", "L0"), "L1"),
    	   ("upper", "Ch"),
    	   ("idents", "T", "L0", "L1"))
    
    # number: captures a sequence of characters that form a (decimal) number.
    # number(number([Ch|T])) --> [Ch], { digit(Ch) }, digits(T).
    add_clause(("number", ("number", (".", "Ch", "T")), (".", "Ch", "L0"), "L1"),
    	   ("digit", "Ch"),
    	   ("digits", "T", "L0", "L1"))
    
    # compound: captures a Prolog compound term.
    # compound(compound(Functor, [])) -->
    #     atom(Functor), ws, ['('], ws, [')'].
    # compound(compound(Functor, Args)) -->
    #     atom(Functor), ws,
    #     ['('], ws,
    #     args(Args), ws,
    #     [')'].
    add_clause(("compound", ("compound", "Functor", "[]"), "L0", "L5"),
    	   ("atom", "Functor", "L0", "L1"),
    	   ("ws", "L1", "L2"),
    	   ("=", "L2", (".", "(", "L3")),
    	   	("ws", "L3", "L4"),
    	   	("=", "L4", (".", ")", "L5")))
    add_clause(("compound", ("compound", "Functor", "Args"), "L0", "L7"),
    	   ("atom", "Functor", "L0", "L1"),
    	   ("ws", "L1", "L2"),
    	   ("=", "L2", (".", "(", "L3")),
    	   	("ws", "L3", "L4"),
    	   	("args", "Args", "L4", "L5"),
    	   	("ws", "L5", "L6"),
    	   	("=", "L6", (".", ")", "L7")))
    
    # args: captures a list of one or more arguments of a compound term or list.
    # Since this is *my* parser, I augment the syntax to accept a trailing
    # comma, like Python :)
    #
    # args([Arg]) --> term(Arg).
    # args([Arg]) --> term(Arg), ws, ','. 
    # args([Arg|Args]) -->
    #     term(Arg), ws,
    #     [','], ws,
    #     args(Args).
    add_clause(("args", (".", "Arg", "[]"), "L0", "L1"),
    	   ("term", "Arg", "L0", "L1"))
    add_clause(("args", (".", "Arg", "[]"), "L0", "L3"),
    	   ("term", "Arg", "L0", "L1"),
    	   ("ws", "L1", "L2"),
    	   ("=", "L2", (".", ",", "L3")))
    add_clause(("args", (".", "Arg", "Args"), "L0", "L5"),
    	   ("term", "Arg", "L0", "L1"),
    	   ("ws", "L1", "L2"),
    	   ("=", "L2", (".", ",", "L3")),
    	   ("ws", "L3", "L4"),
    	   ("args", "Args", "L4", "L5"))
    	   
    # list: syntax sugar for cons-cell representation of a list.
    # This also accepts a trailing comma after the last term.
    #
    # empty_list(atom(['[', ']'])). 
    # list(EmptyList) --> ['['], ws, [']'], { empty_list(EmptyList) }.
    # list(Args) -->
    #     ['['], ws,
    #     list_args_1p(Args), ws,
    #     [']'].
    add_fact(("empty_list", ("atom", to_list("[]"))))
    add_clause(("list", "Empty", "L0", "L3"),
    	   ("=", "L0", (".", "[", "L1")),
    	   ("ws", "L1", "L2"),
    	   ("=", "L2", (".", "]", "L3")),
           ("empty_list", "Empty"))
    add_clause(("list", "Args", "L0", "L5"),
    	   ("=", "L0", (".", "[", "L1")),
    	   ("ws", "L1", "L2"),
    	   ("list_args", "Args", "L2", "L3"),
    	   ("ws", "L3", "L4"),
    	   ("=", "L4", (".", "]", "L5")))
    
    # list_args: one or more argument list.
    #
    # list_args(compound(atom(['.']), [Arg]) -->
    #     term(Arg),
    #     { empty_list(Empty) }.
    # list_args(compound(atom(['.']), [Arg]) -->
    #     term(Arg), ws, [','],
    #     { empty_list(Empty) }.
    # list_args(compound(atom(['.']), [Arg|Args])) -->
    #    term(Arg), ws,
    #    [','], ws,
    #    list_args(Args).
    add_fact(("dot", ("atom", to_list("."))))
    add_clause(("list_args", ("compound", "Dot", (".", "Arg", "[]")), "L0", "L1"),
        ("term", "Arg", "L0", "L1"),
        ("dot", "Dot"),
        ("empty_list", "Empty"))
    add_clause(("list_args", ("compound", "Dot", (".", "Arg", "[]")), "L0", "L3"),
        ("term", "Arg", "L0", "L1"),
        ("ws", "L1", "L2"),
        ("=", "L2", (".", ",", "L3")),
        ("dot", "Dot"),
        ("empty_list", "Empty"))
    add_clause(("list_args", ("compound", "Dot", (".", "Arg", "Args")), "L0", "L5"),
        ("term", "Arg", "L0", "L1"),
        ("ws", "L1", "L2"),
        ("=", "L2", (".", ",", "L3")),
        ("ws", "L3", "L4"),
        ("dot", "Dot"),
        ("list_args", "Args", "L4", "L5"))

    # term: captures a Prolog term.
    # term(Term) -->
    #     atom(Term)
    #     | var(Term)
    #     | number(Term)
    #     | compound(Term)
    #     | list(Term).
    add_clause(("term", "Term", "L0", "L1"),
    	   ("atom", "Term", "L0", "L1"))
    add_clause(("term", "Term", "L0", "L1"),
    	   ("var", "Term", "L0", "L1"))
    add_clause(("term", "Term", "L0", "L1"),
    	   ("number", "Term", "L0", "L1"))
    add_clause(("term", "Term", "L0", "L1"),
    	   ("compound", "Term", "L0", "L1"))
    add_clause(("term", "Term", "L0", "L1"),
    	   ("list", "Term", "L0", "L1"))
    
    # program: captures the AST of a Prolog program.
    # Currently it only accepts a single term, and no operators.
    #
    # program(Tree) --> ws, term(Tree), ws.
    add_clause(("program", "Tree", "L0", "L3"),
    	   ("ws", "L0", "L1"),
    	   ("term", "Tree", "L1", "L2"),
    	   ("ws", "L2", "L3"))
    
    return clauses
  
  
class ParseError(Exception):
    """Generic exception for parsing errors.
    """
    pass


def parse(text):
    """Parse a Prolog program and return its tree representation.
    """
    
    solutions = solve(parser_clauses(), [
    	   ("program", "Tree", to_list(text), "[]")])
    parsings = [s for i, s in enumerate(solutions) if i < 2]
    if not parsings:
        raise ParseError(f"Couldn't parse {text!r}")
    if len(parsings) > 1:
        raise ParseError(f"Ambiguous parse tree for {text!r}: {tree} and {bindings}")
    bindings = parsings[0]
    
    tree = bindings.get("Tree")
    if not tree:
        raise ParseError(f"No binding for Tree in {bindings}!")
    
    return tree


def main():  
    parse_tests = [
    	   ("ab_X1", ("atom", to_list("ab_X1"))),
    	   ("X1", ("var", to_list("X1"))),
    	   ("120", ("number", to_list("120"))),
    	   ("a()", ("compound", ("atom", to_list("a")), "[]")),
    	   ("a(b)", ("compound", ("atom", to_list("a")), to_list([
    	   	    ("atom", to_list("b"))]))),
       	   ("a(b,)", ("compound", ("atom", to_list("a")), to_list([
    	   	    ("atom", to_list("b"))]))),
           ("a(b,1)", ("compound", ("atom", to_list("a")), to_list([
    	   	    ("atom", to_list("b")),
    	   	    ("number", to_list("1"))]))),
           ("a(b,X1,)", ("compound", ("atom", to_list("a")), to_list([
    	   	    ("atom", to_list("b")),
    	   	    ("var", to_list("X1"))]))),
           ("a (  b , )", ("compound", ("atom", to_list("a")), to_list([
    	   	    ("atom", to_list("b"))]))),
    	   (" a ( b , X1, .(10, []) ) ", ('compound', ('atom', to_list('a')), to_list([
    	   	    ('atom', to_list('b')),
    	   	    ('var', to_list('X1')),
    	   	    ('compound', ('atom', to_list('.')), to_list([
    	   	    	   ('number', to_list('10')),
    	   	    	   ('atom', to_list('[]'))]))]))),
    	   ("f([], [a,], [1, 2, 3])", ("compound", ("atom", to_list("f")), to_list([
    	   	    ("atom", to_list("[]")),
                    ("compound", ("atom", to_list(".")), to_list([
                        ("atom", to_list("a"))])),
    	   	    ("compound", ("atom", to_list(".")), to_list([
    	   	    	   ("number", to_list("1")),
                           ("compound", ("atom", to_list(".")), to_list([
                               ("number", to_list("2")),
                               ("compound", ("atom", to_list(".")), to_list([
                                   ("number", to_list("3"))]))]))]))]))),
    ]
    
    for text, expected in parse_tests:
        try:
            result = parse(text)
            if result != expected:
                print(f"Expected \n\t{expected}\n\t for \n\t{text!r}\n\t, got \n\t{result}\n\t!")
        except ParseError:
            set_trace_on()
            try:
                parse(text)
            except ParseError:
                pass
            set_trace_off()

if __name__ == '__main__':
    main()

prol.py

"""A minimal logic programming solver.

Logic terms are represented with plain Python objects:
    number -> int or float
    var -> str, starting with an uppercase letter (or '_')
    atom -> str, that is not a var
    compound -> tuple, where the first element is the functor and the remaining are its args.

For example, the following Prolog term

    foo(a, 10, X, bar(_List, []))

is represented by

    ("foo", "a", 10, "X", ("bar", "_List", "[]"))

Lists are represented by nested cons cells, that is,

    [1, 2, 3]
    
is represented as

    (".", 1, (".", 2, (".", 3, "[]")))

The utility function 'to_list' may be used to convert
Python lists to this representation.
   
Conjunctions are represented by a list of terms, and
clauses are given as a pair of (head, body) elements.
Facts are simply clauses with an empty body.
The following Prolog program, then

    reverse([], []).
    reverse([X|T], R) :-
    	   reverse(T, R0),
    	   append(R0, [X], R).

is written as the following clauses:

    (("reverse", "[]", "[]"), [])
    (("reverse", (".", "X", "T"), "R"), [
    	   ("reverse", "T", "R0"),
    	   ("append", "R0", (".", "X", "[]"), "R")])

Generated vars are identified by a trailing '_', so do not
name your vars like this, or they will cause an error if
clashing with the introduced var.
"""

import itertools as it
from numbers import Number
from operator import itemgetter

def is_number(x):
    return isinstance(x, Number)

def is_atom(x):
    return isinstance(x, str) and not is_var(x)

def is_atomic(x):
    return is_number(x) or is_atom(x)

def is_var(x):
    return isinstance(x, str) and (x[0].isupper() or x[0] == '_')

def is_compound(x):
    return isinstance(x, tuple) and len(x) > 0 and is_atom(x[0])

def is_term(x):
    return is_atomic(x) or is_var(x) or is_compound(x)


class UnifyError(Exception):
    """Generic error in unification.
    """
    pass


_trace = False
def set_trace_on():
    global _trace
    _trace = True
def set_trace_off():
    global _trace
    _trace = False


def to_list(xs):
    """Converts a Python list or str to a cons-cell representation.
    
    Care is taken to escape var characters in a string:
    
    >>> to_list("aX_1")
    ('.', 'a', ('.', "'X'", ('.', "'_'", ('.', '1', '[]'))))
    """
    if not xs:
        return "[]"
    head, tail = xs[0], xs[1:]
    if isinstance(xs, str) and is_var(head):
        head = f"'{head}'"
    return (".", head, to_list(tail))


def by_type(x):
    """Sorting keyfunc for terms.
    
    The order of terms by type is
        var < number < atom < compound.
    """ 
    if is_var(x):
        return (1, x)
    if is_number(x):
        return (2, str(x))
    if is_atom(x):
        return (3, x)
    if is_compound(x):
        return (4, str(x))
    return (99, str(x))


def bind(bindings, x, term):
    """Binds x to term in bindings.
    
    If x is already bound, unify term with its value,
    raising UnifyError if they don't match. If they do,
    pick the minimum between the two to be bound, in the
    order of 'by_type'.
    
    >>> bindings = {}
    >>> bind(bindings, "X", 10)
    >>> bind(bindings, "X", "Y")
    >>> bindings
    {'X': 'Y', 'Y': 10}
    """
    assert is_var(x), x
    if x == '_':
        return
    if x in bindings:   
        unify(term, bindings[x], bindings)
        term = min(term, bindings[x], key=by_type)
    bindings[x] = term


def unify(t1, t2, bindings=None):
    """Unify terms and returns a set of variable bindings that satisfy the equality.
    
    If the terms don't unify, raise a UnifyError.
    
    This implementation doesn't perform an occurs check, so it's possible to work
    with infinite recursive structures.
    
    >>> unify("X", ("f", "X"))
    {'X': ('f', 'X')}
    >>> unify(
    ...     ("g", "X", "Y", "X"),
    ...     ("g", ("f", "Y"), ("f", "X"), ("f", "X")))
    {'X': ('f', 'X'), 'Y': 'X'}
    """
    if bindings is None:
        bindings = {}
    if not is_term(t1):
        raise UnifyError(f"Unknown type for {t1}")
    if not is_term(t2):
        raise UnifyError(f"Unknown type for {t2}")

    if is_var(t1) and is_var(t2):
        if t1 != t2:
            # Var-to-var bindings are made in a specific order to
            # avoid reference cycles.
            x, y = sorted([t1, t2])
            bind(bindings, y, x)
    elif is_var(t1):
        bind(bindings, t1, t2)
    elif is_var(t2):
        bind(bindings, t2, t1)
    elif is_compound(t1) and is_compound(t2):
       functor1, *args1 = t1
       functor2, *args2 = t2
       if functor1 != functor2 or len(args1) != len(args2):
           raise UnifyError(f"{functor1}/{len(args1)} != {functor2}/{len(args2)}")
       for arg1, arg2 in zip(args1, args2):
           unify(arg1, arg2, bindings)
    else:
        if t1 != t2:
            raise UnifyError(f"{t1} != {t2}")
    
    return bindings


def solve(clauses, terms):
    """Yields all solutions of the conjunction of terms, subject to clauses.
    
    >>> clauses = [
    ...     (("append", "[]", "L", "L"), []),
    ...     (("append", (".", "X", "T"), "L", (".", "X", "T0")), [
    ...         ("append", "T", "L", "T0")])]
    >>> solutions = solve(clauses, [("append", "X", "Y", to_list([1, 2]))])
    >>> next(solutions)
    {'X': '[]', 'Y': ('.', 1, ('.', 2, '[]'))}
    >>> next(solutions)
    {'X': ('.', 1, '[]'), 'Y': ('.', 2, '[]')}
    >>> next(solutions)
    {'X': ('.', 1, ('.', 2, '[]')), 'Y': '[]'}
    
    
    Variables starting with an '_' will not be included, unless they are unbound.
    
    >>> clauses = [
    ...     (("eq", "X", "X"), [])]
    >>> list(solve(clauses, [("eq", "X", "Y"), ("eq", "Y", "a")]))
    [{'Y': 'X', 'X': 'a'}]
    >>> list(solve(clauses, [("eq", "X", "_Y"), ("eq", "_Y", "a")]))
    [{'X': 'a'}]
    >>> list(solve(clauses, [("eq", "X", "_Y"), ("eq", "_Y", "_Z")]))
    [{'X': '_Z'}]
    """

    queue = []
    index = index_clauses(clauses)

    # Enqueue all clauses matching the given query for later processing.
    def push(bindings, query, level):
        term, terms = query[0], query[1:]
        clauses = index.get(term[0], [])
        for clause in clauses:
            if _trace: print("  "*level, term, clause)
            queue.insert(0, (bindings, term, terms, clause, level+1))

    push({}, terms, 0)
    while queue:
        bindings, term, terms, (head, body), level = queue.pop()
        if _trace:
            print("  "*level, head, term, end=" ")
        head, *body = rename_vars([head] + body, level)

        try:
            # Unify term with clause head. If it matches, solve the conjunction of the body terms
            # and the remainging query recursively.
            local_bindings = unify(term, head, dict(bindings))
            if _trace: print(_diff_dicts(local_bindings, bindings))

            query = body + terms
            if query:
                push(local_bindings, query, level)
                continue
            yield ignore_vars(local_bindings)
        except UnifyError:
            if _trace: print("Fail")


def _diff_dicts(d1, d2):
    d = dict(d1)
    for k in d2:
        d.pop(k, None)
    return d


def index_clauses(clauses):
    """Return a map indexing clauses by their functor.
    
    Clauses should appear contiguously, otherwise the latest addition will override
    the previous ones.
    """
    index = {}
    for functor, clauses0 in it.groupby(clauses, key=lambda clause: clause[0][0]):
        index[functor] = list(clauses0)
    return index


def vars(terms, xs=None):
    """Return all vars within term.
    """
    if xs is None:
        xs = set()

    for term in terms:
        if is_var(term):
            xs.add(term)
        elif is_compound(term):
            vars(term[1:], xs)

    return xs


def replace_var(x, replacement, term):
    """Replace x with replacement within term.
    """
    if term == x:
        return replacement
    if is_compound(term):
        functor, *args = term
        return tuple([functor] + [replace_var(x, replacement, arg) for arg in args])
    return term


def rename_vars(terms, uid):
    """Rename all vars within terms to a unique, auto-generated name.
    """
    xs = sorted(vars(terms))  # Sort to remove non-determinism

    def gen_var(term):
        x = f"{term}{uid}_"
        if x in xs:
            raise ValueError(f"Generated var clash: {x}")
        return x

    replacements = {x: gen_var(x) for x in xs}

    for term in terms:
        for x in xs:
            term = replace_var(x, replacements[x], term)
        yield term


def ignore_vars(bindings):
    """Remove all bound variables starting or ending with '_'.
    """
    to_delete = set()
    for x, term in bindings.items():
        if x[0] != '_' and x[-1] != '_':
            continue
        for y, y_term in bindings.items():
            if x == y:
                continue
            bindings[y] = replace_var(x, term, y_term)
        to_delete.add(x)
    for x in to_delete:
        del bindings[x]

    return bindings


def main():
    unify_tests = [
        (1, 1, {}),
        (1.0, 1.0, {}),
        ("a", "a", {}),
        ("a", "b", "a != b"),
        ("aTom1", "aTom1", {}),
        (1, "a", "1 != a"),
        ("X", "X", {}),
        ("X", "Y", {"Y": "X"}),
        ("Y", "X", {"Y": "X"}),
        ("X", "a", {"X": "a"}),
        (("f",), ("f",), {}),
        (("f",), ("g",), "f/0 != g/0"),
        (("f", "a"), ("g", "a"), "f/1 != g/1"),
        (("f", "a"), ("g", "a", "b"), "f/1 != g/2"),
        (("f", "a"), ("f", "a", "b"), "f/1 != f/2"),
        (("f", 1), ("f", 1), {}),
        (("f", 1), ("f", 2), "1 != 2"),
        (("f", "X"), ("f", 1), {"X": 1}),
        (("f", "X"), "X", {"X": ("f", "X")}),
        (("f", "X", "Y"), ("f", "Y", 1), {"X": 1, "Y": "X"}),
        (("f", "X", "Y", "a"), ("f", "Y", "X", "X"), {"X": "a", "Y": "X"}),
        (
            ("g", "X",        "Y",        "X"),
            ("g", ("f", "Y"), ("f", "X"), ("f", ("f", ("f", ("f", "X"))))), {
                "X": ("f", "Y"), "Y": ("f", "X")}),
    ]

    for t1, t2, expected in unify_tests:
        if isinstance(expected, str):
            try:
                result = unify(t1, t2)
                raise Exception(f"Expected ({t1} = {t2}) to fail, got {result}!")
            except UnifyError as ex:
                message, = ex.args
                result = message
        else:
            result = unify(t1, t2)

        if result != expected:
            print(f"{t1} = {t2} => {result!r}, not {expected!r}")

    clauses = [
        (("bit", 0), []),
        (("bit", 1), []),
        (("color", "red"), []),
        (("color", "green"), []),
        (("color", "blue"), []),
        (("color_value", "Color", "Bit"), [
            ("color", "Color"),
            ("bit", "Bit"),
        ]),
        (("eq", "X", "X"), []),
        (("nat", "zero"), []),
        (("nat", ("succ", "X")), [("nat", "X")]),
        (("peano", 0, "zero"), []),
        (("peano", 1, ("succ", "X")), [("peano", 0, "X")]),
        (("peano", 2, ("succ", "X")), [("peano", 1, "X")]),
        (("peano", 3, ("succ", "X")), [("peano", 2, "X")]),
        (("add", "zero", "S", "S"), []),
        (("add", ("succ", "X"), "Y", ("succ", "S")), [
            ("add", "X", "Y", "S")]),
        (("length", "[]", "zero"), []),
        (("length", (".", "X", "T"), ("succ", "Len")), [
            ("length", "T", "Len")]),
    ]
    solve_tests = [
        ([("bit", 0)], [{}]), 
        ([("bit", 1)], [{}]), 
        ([("bit", 2)], []),
        ([("bit", "X")], [{"X": 0}, {"X": 1}]),
        ([("color", "Y")], [{"Y": "red"}, {"Y": "green"}, {"Y": "blue"}]),
        ([("color_value", "red", "Y")], [{"Y": 0}, {"Y": 1}]),
        ([("color_value", "X", "Y")], [
            {"X": "red", "Y": 0}, {"X": "red", "Y": 1},
            {"X": "green", "Y": 0}, {"X": "green", "Y": 1},
            {"X": "blue", "Y": 0}, {"X": "blue", "Y": 1},
        ]),
        ([("color_value", "red", "Bit")], [{"Bit": 0}, {"Bit": 1}]),
        ([("color_value", "Color", "Bit")], [
            {"Color": "red", "Bit": 0}, {"Color": "red", "Bit": 1},
            {"Color": "green", "Bit": 0}, {"Color": "green", "Bit": 1},
            {"Color": "blue", "Bit": 0}, {"Color": "blue", "Bit": 1},
        ]),
        ([("color", "red"), ("bit", 1)], [{}]),
        ([("color", "red"), ("bit", "X")], [{"X": 0}, {"X": 1}]),
        ([("bit", "X"), ("color", "red")], [{"X": 0}, {"X": 1}]),
        ([("eq", "_", 1)], [{}]),
        ([("eq", "_", "_")], [{}]),
        ([("nat", "zero")], [{}]),
        ([("nat", ("succ", "zero"))], [{}]),
        ([("nat", ("succ", ("succ", "zero")))], [{}]),
        ([("peano", "Num", "_")], [
            {"Num": 0}, {"Num": 1}, {"Num": 2}, {"Num": 3}]),
        ([
            ("peano", 2, "_Two"),
            ("peano", 3, "_Three"),
            ("add", "_Two", "_Three", "Result"),
        ], [
            {"Result": ("succ", ("succ", ("succ", ("succ", ("succ", "zero")))))},
        ]),
         ([
             ("peano", 3, "_Three"),
             ("add", "_X", "_Y", "_Three"),
             ("peano", "X", "_X"),
             ("peano", "Y", "_Y"),
         ], [
             {"X": 0, "Y": 3},
             {"X": 1, "Y": 2},
             {"X": 2, "Y": 1},
             {"X": 3, "Y": 0},
         ]),
         ([("length", "[]", "Len")], [{"Len": "zero"}]),
         ([("length", (".", "a", "[]"), "Len")], [{"Len": ("succ", "zero")}]),
         ([
            ("eq", "_List", to_list(["a", 1, "X"])),
            ("length", "_List", "_Len"),
            ("peano", "Len", "_Len"),
        ], [
            {"Len": 3},
        ]),
        ([("peano", 3, "_Three"), ("length", "List", "_Three")], [
            {"List": to_list(["X5_", "X6_", "X7_"])}]),
    ]

    for terms, expected in solve_tests:
        results = list(solve(clauses, terms))
        if results != expected:
            def fmt_(solutions):
                result = [""] + [str(s) for s in solutions] + [""]
                return "\n\t".join(result)
            term = ", ".join(str(t) for t in terms)
            print(f"{term} => {fmt_(results)}\n, not {fmt_(expected)}\n!")


if __name__ == '__main__':
    main()