###
# 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 collections import OrderedDict
from nova.core import (is_compound, is_variable, set_to_list,
       union_undo, object_equals, union_find, union_add, make_check,
       exec_build, int32, assoc_get, assoc_set, stack_push,
       stack_peek, stack_pop, Item, deref, add, VAR_MASK_SEEN,
       bind, walk_vars, is_structure, object_hash_code, exec_unify)

################################################################
# unify_with_occurs_check/2 and 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.functor != second.functor:
                    break
                elif first is not second:
                    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(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


################################################################
# subsumes/2                                                   #
################################################################

###
# subsumes(X, Y): [N208 8.2.4]
# The built-in succeeds if X subsumes Y.
##
def test_subsumes(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return subsumes(alpha, beta)


###
# Determine whether two terms single side unify.
# As a side effect the trail is extended, even if unification fails.
# Tail recursive solution.
#
# @param first The first term.
# @param second The second term.
# @return True if the two terms single side unify, otherwise false.
##
def subsumes(first, second):

    def subsumes2(first2, second2):
        nonlocal second
        while True:
            first2 = deref(first2)
            second2 = deref(second2)
            if is_variable(first2):
                if is_variable(second2) and first2 is second2:
                    return True
                if has_var(first2, second):
                    return False
                bind(second2, first2)
                return True
            if is_variable(second2):
                return False
            if not is_structure(first2):
                return object_equals(first2, second2)
            if not is_structure(second2):
                return False
            if len(first2.args) != len(second2.args):
                return False
            if first2.functor != second2.functor:
                return False
            first2 = first2.args
            second2 = second2.args
            i = 0
            while i < len(first2) - 1:
                if not subsumes2(first2[i], second2[i]):
                    return False
                i += 1
            first2 = first2[i]
            second2 = second2[i]

    return subsumes2(first, second)


################################################################
# term_singletons/2                                            #
################################################################

###
# term_singletons(T, L):
# The built-in succeeds in L with the singleton variables of T.
##
def test_term_singletons(args):
    alpha = exec_build(args[0])
    alpha = walk_singletons(alpha)
    for key, val in list(alpha.items()):
        if val:
            del alpha[key]
    alpha = set_to_list(alpha.keys())
    return exec_unify(args[1], alpha)


###
# Walk a Prolog term completely.
#
# @param first The Prolog term.
# @return The singletons.
##
def walk_singletons(first):
    stack = None
    vmap = None
    while True:
        first = deref(first)
        if is_variable(first):
            first = dict([[first, False]])
        elif is_compound(first):
            peek = assoc_get(vmap, first)
            if peek is NotImplemented:
                vmap = assoc_set(vmap, first, EMPTY_MAP)
                item = Item(first, EMPTY_MAP, 0)
                stack = stack_push(stack, item)
                first = first.args[0]
                continue
            else:
                first = peek
        else:
            first = EMPTY_MAP
        item = stack_peek(stack)
        while (item is not None and
                item.idx == len(item.first.args) - 1):
            first = union_map(item.second, first)
            vmap = assoc_set(vmap, item.first, first)
            stack_pop(stack)
            item = stack_peek(stack)
        if item is None:
            return first
        else:
            item.second = union_map(item.second, first)
            item.idx += 1
            first = item.first.args[item.idx]


EMPTY_MAP = OrderedDict()


def union_map(first, second):
    if len(first) == 0:
        return second
    if len(second) == 0:
        return first
    first = OrderedDict(first)
    for key, val in second.items():
        value = first.get(key, NotImplemented)
        if value is not NotImplemented:
            value = True
        else:
            value = val
        first[key] = value
    return first


#######################################################################
# ground/1 and nonground/2                                            #
#######################################################################

###
# ground(T): [TC2 8.3.10]
# The built-in succceeds if T is ground.
##
def test_ground(args):
    alpha = exec_build(args[0])
    res = walk_vars(alpha, lambda node: True, VAR_MASK_SEEN)
    walk_vars(alpha, lambda node: True, 0)
    return not res


###
# nonground(T, V):
# The built-in succeeds if T is non-ground and V is the first variable.
##
def test_nonground(args):
    alpha = exec_build(args[0])
    hit = NotImplemented

    def nonground2(node):
        nonlocal hit
        hit = node
        return True

    res = walk_vars(alpha, nonground2, VAR_MASK_SEEN)
    walk_vars(alpha, lambda node: True, 0)
    return res and exec_unify(args[1], hit)


#######################################################################
# term_hash/2                                                         #
#######################################################################

###
# term_hash(X, H):
# The predicate succeeds in H with the term hash of the term X.
##
def test_term_hash(args):
    alpha = exec_build(args[0])
    res = walk_hash(alpha)
    return exec_unify(args[1], res)


###
# Walk a Prolog term completely.
#
# @param first The Prolog term.
# @return The hash.
##
def walk_hash(first):
    stack = None
    vmap = None
    while True:
        first = deref(first)
        if is_structure(first):
            peek = assoc_get(vmap, first)
            if peek is NotImplemented:
                vmap = assoc_set(vmap, first, 0)
                peek = object_hash_code(first.functor)
                item = Item(first, peek, 0)
                stack = stack_push(stack, item)
                first = first.args[0]
                continue
            else:
                first = peek
        else:
            first = object_hash_code(first)
        item = stack_peek(stack)
        while (item is not None and
               item.idx == len(item.first.args) - 1):
            first = int32(item.second * 31 + first)
            vmap = assoc_set(vmap, item.first, first)
            stack_pop(stack)
            item = stack_peek(stack)
        if item is None:
            return first
        else:
            item.second = int32(item.second * 31 + first)
            item.idx += 1
            first = item.first.args[item.idx]


#######################################################################
# Fast Lib Init                                                       #
#######################################################################

def main():
    add("unify_with_occurs_check", 2, make_check(test_unify_checked))
    add("occurs_check", 2, make_check(test_has_var))
    add("subsumes", 2, make_check(test_subsumes))
    add("term_singletons", 2, make_check(test_term_singletons))
    add("ground", 1, make_check(test_ground))
    add("nonground", 2, make_check(test_nonground))
    add("term_hash", 2, make_check(test_term_hash))
