###
# Modern Albufeira Prolog Interpreter
#
# Warranty & Liability
# To the extent permitted by applicable law and unless explicitly
# otherwise agreed upon, XLOG Technologies AG makes no warranties
# regarding the provided information. XLOG Technologies AG assumes
# no liability that any problems might be solved with the information
# provided by XLOG Technologies AG.
#
# Rights & License
# All industrial property rights regarding the information - copyright
# and patent rights in particular - are the sole property of XLOG
# Technologies AG. If the company was not the originator of some
# excerpts, XLOG Technologies AG has at least obtained the right to
# reproduce, change and translate the information.
#
# Reproduction is restricted to the whole unaltered document. Reproduction
# of the information is only allowed for non-commercial uses. Selling,
# giving away or letting of the execution of the library is prohibited.
# The library can be distributed as part of your applications and libraries
# for execution provided this comment remains unchanged.
#
# Restrictions
# Only to be distributed with programs that add significant and primary
# functionality to the library. Not to be distributed with additional
# software intended to replace any components of the library.
#
# Trademarks
# Jekejeke is a registered trademark of XLOG Technologies AG.
##

from nova.core import (bind, make_check, exec_build, deref,
       is_structure, set, is_frozen, union_find, union_add,
       VAR_MASK_SEEN, VAR_MASK_SERNO, Item, MAX_ARITY,
       stack_pop, stack_peek, stack_push, check_nil,
       Triple, is_triple, walk_uncompute,
       exec_unify, Compound, Variable, is_compound,
       is_variable, object_equals, walk_vars, union_undo)


################################################################
# unify_with_occurs_check/2                                    #
################################################################

###
# unify_with_occurs_check(S, T): [ISO 8.2.2]
# The built-in succeeds when the Prolog terms S and T unify
# with occurs check, otherwise the built-in fails.
##
def test_unify_checked(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return unify_checked(alpha, beta)


###
# Determine whether two terms unify with occurs check.
# As a side effect the trail is extended, even if unification fails.
# Can handle cyclic terms and deep recursion.
#
# @param first The first term.
# @param second The second term.
# @return True if the two terms unify, otherwise false.
##
def unify_checked(first, second):
    stack = None
    log = None
    try:
        while True:
            first = deref(first)
            second = deref(second)
            if is_variable(first):
                if not is_variable(second) or first is not second:
                    if has_var(first, second):
                        break
                    bind(second, first)
            elif is_variable(second):
                if has_var(second, first):
                    break
                bind(first, second)
            elif not is_structure(first):
                if not object_equals(first, second):
                    break
            elif not is_structure(second):
                break
            elif len(first.args) != len(second.args):
                break
            else:
                first = union_find(first)
                second = union_find(second)
                if first is not second:
                    if (is_frozen(first) and is_frozen(second) and
                            first.hash != second.hash):
                        break
                    if first.functor != second.functor:
                        break
                    log = union_add(log, first, second)
                    if 0 != len(first.args) - 1:
                        item = Item(first, second, 0)
                        stack = stack_push(stack, item)
                    first = first.args[0]
                    second = second.args[0]
                    continue
            item = stack_peek(stack)
            if item is None:
                return True
            else:
                item.idx += 1
                first = item.first.args[item.idx]
                second = item.second.args[item.idx]
                if item.idx == len(item.first.args) - 1:
                    stack_pop(stack)
        return False
    finally:
        union_undo(log)


################################################################
# occurs_check/2                                               #
################################################################

##
# occurs_check(S, T): [ISO 7.3.3]
# The built-in succeeds when the Prolog variable S occurs
# in the Prolog term T, otherwise the built-in fails.
##
def test_has_var(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return is_variable(alpha) and has_var(alpha, beta)


###
# Check whether a variable occurs in a term.
# Can handle cyclic terms and deep recursion.
#
# @param vterm The Prolog variable.
# @param first The Prolog term.
# @return True if vterm occurs in alpha, otherwise false.
##
def has_var(vterm, first):

    def has_var2(node):
        return node is vterm

    res = walk_vars(first, has_var2, VAR_MASK_SEEN)
    walk_vars(first, has_var2, 0)
    return res


################################################################
# acyclic_term/1                                               #
################################################################

###
# acyclic_term(T): [TC2 8.3.11]
# The predicate succeeds when the Prolog term T is an acyclic term,
# otherwise the predicate fails.
##
def test_acyclic_term(args):
    alpha = exec_build(args[0])
    res = walk_cyclic(alpha, VAR_MASK_SEEN)
    walk_cyclic(alpha, 0)
    return not res


def walk_cyclic(first, state):
    stack = None
    while True:
        first = deref(first)
        if is_compound(first):
            if (first.walk & VAR_MASK_SEEN) != state:
                first.walk = (first.walk & ~VAR_MASK_SEEN) | state
                first.walk &= ~VAR_MASK_SERNO
                stack = stack_push(stack, first)
                first = first.args[0]
                continue
            elif ((first.walk & VAR_MASK_SERNO)
                  != len(first.args)):
                return True
        item = stack_peek(stack)
        while (item is not None and
               (item.walk & VAR_MASK_SERNO) == len(item.args) - 1):
            item.walk += 1
            stack_pop(stack)
            item = stack_peek(stack)
        if item is None:
            return False
        else:
            item.walk += 1
            first = item.args[item.walk & VAR_MASK_SERNO]


################################################################
# acyclic_decompose/2                                          #
################################################################

###
# acyclic_decompose(X, T, L):
# The built-in succeeds in R with skeleton and substitution
# list cells so that the substitions applied to the skeletons gives
# identical the elements of the Prolog list L.
##
def test_acyclic_decompose(args):
    alpha = exec_build(args[0])
    res = None
    try:
        back = None
        i = 0
        peek = alpha
        while (is_structure(peek) and
               peek.functor == "." and
               len(peek.args) == 2 and
               i < MAX_ARITY):
            temp = deref(peek.args[0])
            temp = walk_decom(temp)
            temp = Compound(".", [temp, NotImplemented])
            if back is None:
                res = temp
            else:
                back.args[1] = temp
            back = temp
            i += 1
            peek = deref(peek.args[1])
        check_nil(peek)
        if back is None:
            res = "[]"
        else:
            back.args[1] = "[]"
    finally:
        peek = alpha
        while (is_structure(peek) and
               peek.functor == "." and
               len(peek.args) == 2):
            temp = deref(peek.args[0])
            walk_uncompute(temp)
            peek = deref(peek.args[1])
    return exec_unify(args[1], res)


def walk_decom(first):
    stack = None
    subst = "[]"
    while True:
        first = deref(first)
        if is_compound(first):
            if not is_triple(first.functor):
                first.functor = Triple(first.functor, NotImplemented,
                         [NotImplemented] * len(first.args))
                first.walk &= ~VAR_MASK_SERNO
                stack = stack_push(stack, first)
                first = first.args[0]
                continue
            else:
                peek = first.functor.accum
                if peek is NotImplemented:
                    peek = Variable()
                    first.functor.accum = peek
                first = peek
        item = stack_peek(stack)
        while (item is not None and
               (item.walk & VAR_MASK_SERNO) == len(item.args) - 1):
            item.functor.children[item.walk & VAR_MASK_SERNO] = first
            first = Compound(item.functor.backup, item.functor.children)
            peek = item.functor.accum
            if peek is NotImplemented:
                item.functor.accum = first
            else:
                first = Compound("=", [peek, first])
                subst = Compound(".", [first, subst])
                first = peek
            stack_pop(stack)
            item = stack_peek(stack)
        if item is None:
            return Compound(".", [first,subst])
        else:
            item.functor.children[item.walk & VAR_MASK_SERNO] = first
            item.walk += 1
            first = item.args[item.walk & VAR_MASK_SERNO]


#######################################################################
# Cyc Lib Init                                                        #
#######################################################################

def main():
    set("unify_with_occurs_check", 2, make_check(test_unify_checked))
    set("occurs_check", 2, make_check(test_has_var))
    set("acyclic_term", 1, make_check(test_acyclic_term))
    set("acyclic_decompose", 2, make_check(test_acyclic_decompose))

