# Malá knihovna pro logické programování.
#
# Dole jsou ukázky použití.
#
# Inspirováno: https://github.com/jasonhemann/microKanren
#
# Článek: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

from functools import reduce

# Počítadlo dočasných proměnných
VAR_COUNTER = 0

class Var:
    """Proměnná."""
    def __init__(self, name=None):
        global VAR_COUNTER
        if name == None:
            name = VAR_COUNTER
            VAR_COUNTER += 1
            
        self.name = name
        
    def get_name(self):
        return self.name

    def __repr__(self):
        name = self.get_name()
        if type(name) == str:
            return name
        else:
            return f"Var({name})"

    def __eq__(self, arg):
        if isinstance(arg, Var):
            return self.get_name() == arg.get_name()
        else:
            return False

# Proměnná je dána svým jménem.
# Proměnné se tisknou jméno.
# Trvalé proměnné pojmenováváme řetězcem:
"""
>>> x = Var("x")
>>> x
x
"""

# Dočasné proměnné mají za jméno celé nezáporné číslo.
# Jméno dočasných proměnných se volí samo.
# Tisknou se Var(i), kde i je zvolené číslo.
"""
>>> Var()
Var(0)
>>> Var()
Var(1)
"""

# Základní trvalé proměnné proměnné:
x = Var("x")
y = Var("y")
z = Var("z")

def is_var(val):
    """Rozhodne, zda je hodnota proměnná."""
    return isinstance(val, Var)

"""
>>> is_var(x)
True
>>> is_var(1)
False
"""

# Pár proměnná-hodnota je pole [var, val].
# Substituce je pole párů proměnná-hodnota.
def sub_get(sub, var):
    """Vrátí pár se zadanou proměnnou, nebo nic."""
    for pair in sub:
        if pair[0] == var:
            return pair
"""
>>> sub_get([[x, 1], [y, 2]], x)
[x, 1]
>>> sub_get([[x, 1], [y, 2]], z)
>>>
"""

def print_sub(sub):
    """Vytiskne substituci."""
    for pair in sub:
        print(f"{pair[0]}: {pair[1]}")

"""
>>> print_sub([[x, 1], [y, 2]])
x: 1
y: 2
"""
        
def walk(val, sub):
    """Vrátí hodnotu vzhledem k substituci."""
    if is_var(val):
        pair = sub_get(sub, val)
        if pair:
            return walk(pair[1], sub)
    return val

"""
>>> walk(x, [[x, 1], [y, 2]])
1
>>> walk(3, [[x, y], [y, 2]])
3
>>> walk(z, [[x, y], [y, 2]])
z
>>> walk(x, [[x, y], [y, 2]])
2
"""



# Prázdná substituce
EMPTY_SUB = []

def extend_sub(var, val, sub):
    """Rozšíří substituci o nový pár proměnná-hodnota."""
    return [[var, val]] + sub

"""
>>> extend_sub(x, 1, [[y, 2]])
[[x, 1], [y, 2]]
"""

def unit_sub(var, val):
    """Vrátí substituci s jediným párem."""
    return extend_sub(var, val, EMPTY_SUB)

"""
>>> unit_sub(x, 1)
[[x, 1]]
"""

# Složené hodnoty reprezentujeme polem.
def is_array(val):
    """Rozhodne, zda je hodnota pole."""
    return type(val) == list

"""
>>> is_array(1)
False
>>> is_array([])
True
>>> is_array([1])
True
"""

# Zhmotnění hodnoty.
def reify(val, sub):
    """Dosadí do hodnoty za proměnné podle substituce."""
    walked_val = walk(val, sub)
    if is_array(walked_val):
        return [reify(el, sub) for el in walked_val]
    else:
        return walked_val

"""
>>> reify([1, x, [y]], [[x, y], [y, 2]])
[1, 2, [2]]
"""

def unify(val1, val2, sub=EMPTY_SUB):
    """Vrátí substituci vyjadřující, kdy se hodnoty rovnají.
       Pokud se hodnoty nemůžou rovnat, nevrátí nic."""
    val1 = walk(val1, sub)
    val2 = walk(val2, sub)
    if val1 == val2: 
        return sub
    if is_var(val1):
        return extend_sub(val1, val2, sub)
    if is_var(val2):
        return extend_sub(val2, val1, sub)
    if is_array(val1) and is_array(val2) and val1 != [] and val2 != []:
        sub = unify(val1[0], val2[0], sub)
        if sub is not None:
            return unify(val1[1:], val2[1:], sub)

"""
>>> unify(1, 1)
[]
>>> unify(1, 2)
>>> unify(1, x)
[[x, 1]]
>>> unify(y, x)
[[y, x]]
>>> unify([1, 2], [1, 2])
[]
>>> unify([1, 2], [2, 2])
>>> unify([1, y], [x, 2])
[[y, 2], [x, 1]]
>>> unify(x, x)
[]
"""

# Cíl je generátor očekávající substituci a vytvářející posloupnost substitucí.
# Očekávaná substituce se nazývá výchozí substituce.
# Substituce v posloupnosti nazýváme možnosti splnění.
# Cíl tedy pro výchozí substituci vrací posloupnost možných splnění.
#
# U funkcí, které vrací cíl, říkáme, že jej stanovují.


def run_sub_lazy(goal):
    """Vrátí posloupnost možností splnění cíle z prázdné substituce."""
    return goal(EMPTY_SUB)

def run_sub(goal):
    """Vrátí pole možností splnění cíle z prázdné substituce."""
    return list(run_sub_lazy(goal))


# tautologie
def taut(sub):
    """Vždy splněný cíl."""
    yield sub

"""
>>> run_sub(taut)
[[]]
"""

# kontradikce
def contr(sub):
    if False:
        yield None # Nikdy se nevykoná.

"""
>>> run_sub(contr)
[]
"""

def eq(val1, val2):
    """Stanoví cíl, který je spněn, pokud se hodnoty rovnají."""
    def goal(sub):
        sub = unify(val1, val2, sub)
        if sub is not None:
            yield sub
    return goal

"""
>>> run_sub(eq(1, 1))
[[]]
>>> run_sub(eq(1, 2))
[]
"""

def disj2(goal1, goal2):
    """Spojí dva cíle logickou disjunkcí."""
    def goal(sub):
        for sub1 in goal1(sub):
            yield sub1
        for sub2 in goal2(sub):
            yield sub2
    return goal

"""
>>> run_sub(disj2(eq(x, 1), eq(x, 2)))
[[[x, 1]], [[x, 2]]]
"""


def disj(*goals):
    """Spojí cíle logickou disjunkcí."""
    return reduce(disj2, goals,
                  contr)
"""
>>> run_sub(disj(eq(x, 1), eq(x, 2), eq(x, 3)))
[[[x, 1]], [[x, 2]], [[x, 3]]]
"""

def bind(subs, goal):
    """Aplikuje cíl na každou substituci a výsledky spojí do jedné posloupnosti."""
    for sub in subs:
        for sub2 in goal(sub):
            yield sub2
            

"""
>>> list(bind([[[x, 1]], []], eq(y, 2)))
[[[y, 2], [x, 1]], [[y, 2]]]
"""

def conj2(goal1, goal2):
    """Spojí dva cíle logickou konjunkcí."""
    def goal(sub):
        return  bind(goal1(sub), goal2)
    return goal

"""
>>> run_sub(conj(eq(x, 1), eq(y, 2)))
[[[y, 2], [x, 1]]]
"""

def conj(*goals):
    """Spojí cíle logickou konjunkcí."""
    return reduce(conj2, goals, taut)

"""
>>> run_sub(conj(eq(x, 1), eq(y, 2), eq(z, 3)))
[[[z, 3], [y, 2], [x, 1]]]
"""

def lazy(goal_constr, *args):
    """Aplikuje líně funkci stanovující cíl na argumenty.""" 
    return lambda sub: goal_constr(*args)(sub)

"""
def ones(var):
    return disj(eq(1, var), lazy(ones, var))

def ones_wrong(var):
    return disj(eq(1, var), ones_wrong(var))
"""
"""
>>> g = run_sub_lazy(ones(x))
>>> next(g)
[[x, 1]]
>>> next(g)
[[x, 1]]
>>> next(g)
[[x, 1]]
...
"""
def neg(goal):
    def goal2(sub):
        res = goal(sub)
        try:
            next(res)
        except StopIteration:
            yield sub
    return goal2


## Následující tři funkce tvoří tři vstupní body do logické knihovny.

def run_lazy(result, *goals):
    """Vrátí posloupnost výsledků."""
    goal = conj(*goals)
    subs = run_sub_lazy(goal)
    return (reify(result, sub) for sub in subs)

def run_one(result, *goals):
    """Vrátí první výsledek."""
    vals = run_lazy(result, *goals)
    return next(vals)

def run(result, *goals):
    """Vrátí seznam výsledků."""
    vals = run_lazy(result, *goals)
    return list(vals)

## Ukázky použití.


# Je 1 rovno 1?
"""
>>> run(True, eq(1, 1))
[True]
"""

# Je 1 rovno 2?
"""
>>> run(True, eq(1, 2))
[]
"""

# Kdy je x rovno 1?
"""
>>> run(x, eq(x, 1))
[1]
"""

def add(x, y, z):
    def goal(sub):
        rx = reify(x, sub)
        ry = reify(y, sub)
        rz = reify(z, sub)
        if not is_var(rx) and not is_var(ry):
            return eq(rx + ry, rz)(sub)
        elif not is_var(rx) and not is_var(rz):
            return eq(rz - rx, ry)(sub)
        elif not is_var(ry) and not is_var(rz):
            return eq(rz - ry, rx)(sub)
        else:
            raise TypeError(f"Goal add({rx}, {ry}, {rz}) is not possible.")
    return goal

"""
>>> run_one(z, add(1, 1, x), add(y, x, 4), add(x, y, z))
4
"""

def relation(tuples):
    def search(*vals):
        array_vals = list(vals) # převedeme na pole
        goals = [eq(array_vals, tup) for tup in tuples]
        return disj(*goals)
    return search

"""
>>> rel = relation([[1, 2], [1, 3], [2, 4]])
>>> run([x, z], rel(x, y), rel(y, z))
[[1, 4]]
"""

def less(x, y):
    def goal(sub):
        rx = reify(x, sub)
        ry = reify(y, sub)
        if not is_var(rx) and not is_var(ry):
            if rx < ry:
                return taut(sub)
            else:
                return contr(sub)
        else:
            raise TypeError(f"Not possible: less({rx}, {ry})")
    return goal