###
# 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.
##

import nova.store as store
from nova.store import (add, is_variable, Compound, deref,
     stack_push, stack_pop, stack_peek, is_structure)
import nova.machine as machine
from nova.machine import (cont, exec_build, Item,
     is_number, exec_eval, exec_unify, Choice, more,
     union_find, union_add, is_atom, is_integer,
     make_error, unbind, union_undo, exec_deref,
     is_pending, unify, object_equals, VAR_MASK_SERNO)
from nova.special import (check_integer, MAX_ARITY, make_check,
     check_nil, check_atom, narrow_float, make_special,
     make_arithmetic)
import math
import sys
import struct


################################################################
# is/2                                                         #
################################################################

###
# X is Y: [ISO 8.6.1]
# The predicate succeeds in X with the evaluation of Y.
##
def test_eval(args):
    res = exec_eval(args[1])
    return exec_unify(args[0], res)


################################################################
# (-)/2, (+)/3, (-)/3, (*)/3, (/)/3, (//)/3 and (rem)/3.       #
################################################################

###
# -(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the negation of A.
##
def arit_neg(args):
    alpha = exec_eval(args[0])
    return -alpha


###
# +(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with the sum of A and B.
##
def arit_add(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        return alpha + beta
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# -(A, B, C):
# The predicate succeeds in C with A subtracted by B.
##
def arit_sub(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        return alpha - beta
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# *(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with the product of A and B.
##
def arit_mul(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        return alpha * beta
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# /(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with A float divided by B.
##
def arit_quot(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    if beta == 0:
        raise make_error(Compound("evaluation_error", ["zero_divisor"]))
    try:
        if is_integer(alpha) and is_integer(beta):
            return float(alpha) / float(beta)
        else:
            return alpha / beta
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# //(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with A truncate divided by B.
##
def arit_intquot(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta == 0:
        raise make_error(Compound("evaluation_error", ["zero_divisor"]))
    res = abs(alpha) // abs(beta)
    if (alpha < 0) != (beta < 0):
        return -res
    else:
        return res


###
# rem(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with A remainder B.
##
def arit_rem(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta == 0:
        raise make_error(Compound("evaluation_error", ["zero_divisor"]))
    res = abs(alpha) % abs(beta)
    if alpha < 0:
        return -res
    else:
        return res


################################################################
# float/2, ^/3, div/3 and mod/3                                #
################################################################

###
# float(A, B): [ISO 9.17]
# The predicate succeeds in B with the approximated A.
##
def arit_float(args):
    alpha = exec_eval(args[0])
    return narrow_float(alpha)


###
# ^(A, B, C): [TC2 9.3.10]
# The predicate succeeds in C with A int power by B.
##
def arit_intpow(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        if is_integer(alpha) and is_integer(beta):
            if beta < 0:
                raise make_error(Compound("domain_error",
                     ["not_less_than_zero", beta]))
            return alpha ** beta
        else:
            return math.pow(alpha, beta)
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# div(A, B, C): [TC2 9.1.3]
# The predicate succeeds in C with A floor divided by B.
##
def arit_div(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta == 0:
        raise make_error(Compound("evaluation_error", ["zero_divisor"]))
    return alpha // beta


###
# mod(A, B, C): [ISO 9.1.7]
# The predicate succeeds in C with A modulus B.
##
def arit_mod(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta == 0:
        raise make_error(Compound("evaluation_error", ["zero_divisor"]))
    return alpha % beta


################################################################
# abs/2, sign/2, min/3 and max/3                               #
################################################################

###
# abs(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the absolute value of A.
##
def arit_abs(args):
    alpha = exec_eval(args[0])
    return abs(alpha)


###
# sign(A, B): [ISO 9.1.4]
# The predicate succeeds in B with the sign of A.
##
def arit_sign(args):
    alpha = exec_eval(args[0])
    if is_integer(alpha):
        if alpha < 0:
            return -1
        elif alpha == 0:
            return 0
        else:
            return 1
    else:
        if alpha < 0.0:
            return -1.0
        elif alpha == 0.0:
            return 0.0
        else:
            return 1.0


###
# min(A, B, C): [TC2 9.3.9]
# The predicate succeeds in C with the minimum of A and B.
##
def arit_min(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    if is_integer(alpha) and is_integer(beta):
        return min(alpha, beta)
    else:
        return min(narrow_float(alpha), narrow_float(beta))


###
# max(A, B, C): [TC2 9.3.8]
# The predicate succeeds in C with the maximum of A and B.
##
def arit_max(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    if is_integer(alpha) and is_integer(beta):
        return max(alpha, beta)
    else:
        return max(narrow_float(alpha), narrow_float(beta))


################################################################
# truncate/2, floor/2, ceiling/2 and round/2.                  #
################################################################

###
# truncate(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the truncate of A.
##
def arit_truncate(args):
    alpha = exec_eval(args[0])
    if is_integer(alpha):
        return alpha
    else:
        return math.trunc(alpha)


###
# floor(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the floor of A.
##
def arit_floor(args):
    alpha = exec_eval(args[0])
    if is_integer(alpha):
        return alpha
    else:
        return math.floor(alpha)


###
# ceiling(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the ceiling of A.
##
def arit_ceiling(args):
    alpha = exec_eval(args[0])
    if is_integer(alpha):
        return alpha
    else:
        return math.ceil(alpha)


###
# round(A, B): [ISO 9.1.7]
# The predicate succeeds in B with the round of A.
##
def arit_round(args):
    alpha = exec_eval(args[0])
    if is_integer(alpha):
        return alpha
    else:
        return (math.floor(2*alpha)+1) >> 1


################################################################
# =:=/2, =\=/2, </2, >=/2, >/2 and =</2                        #
################################################################

###
# X =:= Y: [ISO 8.7.1]
# The predicate succeeds when X number equals Y, otherwise fails.
##
def test_numberequal(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return number_equal(alpha, beta)


###
# X =\= Y: [ISO 8.7.1]
# The predicate succeeds when X does not number equal Y, otherwise fails.
##
def test_numbernotequal(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return not number_equal(alpha, beta)


###
# Determine whether two Prolog numbers are equal.
#
# @param alpha The first Prolog number.
# @param beta The second Prolog number.
# @return True if the two Prolog numbers are equal.
##
def number_equal(alpha, beta):
    if is_integer(alpha) and is_integer(beta):
        return alpha == beta
    else:
        return narrow_float(alpha) == narrow_float(beta)


###
# X < Y: [ISO 8.7.1]
# The predicate succeeds when X is number less than Y, otherwise fails.
##
def test_numberless(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return number_less(alpha, beta)


###
# X >= Y: [ISO 8.7.1]
# The predicate succeeds when X is number greater or equal to Y, otherwise fails.
##
def test_numbergreaterequal(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return not number_less(alpha, beta)


###
# X > Y: [ISO 8.7.1]
# The predicate succeeds when X is number greater than Y, otherwise fails.
##
def test_numbergreater(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return number_less(beta, alpha)


###
# X =< Y: [ISO 8.7.1]
# The predicate succeeds when X is number less or equal to Y, otherwise fails.
##
def test_numberlessequal(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    return not number_less(beta, alpha)


###
# Determine whether a Prolog numbers is less than a Prolog number.
#
# @param alpha The first Prolog number.
# @param beta The second Prolog number.
# @return True if the two Prolog numbers are equal.
##
def number_less(alpha, beta):
    if is_integer(alpha) and is_integer(beta):
        return alpha < beta
    else:
        return narrow_float(alpha) < narrow_float(beta)


################################################################
# sin/3, cos/2, tan/2, asin/2, acos/2, atan/2 and pi/1.        #
################################################################

###
# sin(A, B): [ISO 9.3.2]
# The predicate succeeds in B with the sine of A.
##
def arit_sin(args):
    alpha = exec_eval(args[0])
    return math.sin(alpha)


###
# cos(A, B): [ISO 9.3.3]
# The predicate succeeds in B with the cosine of A.
##
def arit_cos(args):
    alpha = exec_eval(args[0])
    return math.cos(alpha)


###
# tan(A, B): [TC2 9.3.14]
# The predicate succeeds in B with the tangent of A.
##
def arit_tan(args):
    alpha = exec_eval(args[0])
    try:
        return math.tan(alpha)
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# asin(A, B): [TC2 9.3.11]
# The predicate succeeds in B with the arcus sine of A.
##
def arit_asin(args):
    alpha = exec_eval(args[0])
    try:
        return math.asin(alpha)
    except ValueError:
        raise make_error(Compound("evaluation_error", ["undefined"]))


###
# acos(A, B): [TC2 9.3.12]
# The predicate succeeds in B with the arcus cosine of A.
##
def arit_acos(args):
    alpha = exec_eval(args[0])
    try:
        return math.acos(alpha)
    except ValueError:
        raise make_error(Compound("evaluation_error", ["undefined"]))


###
# atan(A, B): [ISO 9.3.4]
# The predicate succeeds in B with the arcus tangent of A.
##
def arit_atan(args):
    alpha = exec_eval(args[0])
    return math.atan(alpha)


###
# pi(A): [TC2 9.3.15]
# The predicate succeeds in A with π.
##
def arit_pi(args):
    return math.pi


################################################################
# (**)/3, exp/2, log/2, sqrt/2, e/1, epsilon/1 and atan2/3     #
################################################################

###
# **(A, B, C): [ISO 9.3.1]
# The predicate succeeds in C with A float power by B.
##
def arit_pow(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        return math.pow(alpha, beta)
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# exp(A, B): [ISO 9.3.5]
# The predicate succeeds in B with e power by A.
##
def arit_exp(args):
    alpha = exec_eval(args[0])
    try:
        return math.exp(alpha)
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


###
# log(A, B): [ISO 9.3.6]
# The predicate succeeds in B with the natural logarithm of A.
##
def arit_log(args):
    alpha = exec_eval(args[0])
    try:
        return math.log(alpha)
    except ValueError:
        raise make_error(Compound("evaluation_error", ["undefined"]))


###
# sqrt(A, B): [ISO 9.3.7]
# The predicate succeeds in B with the square root of A.
##
def arit_sqrt(args):
    alpha = exec_eval(args[0])
    try:
        return math.sqrt(alpha)
    except ValueError:
        raise make_error(Compound("evaluation_error", ["undefined"]))


###
# e(A): [N208 9.7.2]
# The predicate succeeds in A with the Euler number.
##
def arit_e(args):
    return math.e


###
# epsilon(A): [N208 9.7.3]
# The predicate succeeds in A with the machine epsilon.
##
def arit_epsilon(args):
    return sys.float_info.epsilon


###
# atan2(A, B, C): [TC2 9.3.13]
# The predicate succeeds in C with the arc tangent of A and B.
##
def arit_atan2(args):
    alpha = exec_eval(args[0])
    beta = exec_eval(args[1])
    try:
        if alpha == 0 and beta == 0:
            raise make_error(Compound("evaluation_error", ["undefined"]))
        else:
            return math.atan2(alpha, beta)
    except OverflowError:
        raise make_error(Compound("evaluation_error", ["float_overflow"]))


################################################################
# (\)/2, (/\)/3, (\/)/3, (xor)/3, (>>)/3 and (<</3)            #
################################################################

###
# \(A, B): [ISO 9.4.5]
# The predicate succeeds in B with the bitwise not of A.
##
def arit_not(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    return ~alpha


###
# /\(A, B, C): [ISO 9.4.3]
# The predicate succeeds in C with the bitwise and of A and B.
##
def arit_and(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    return alpha & beta


###
# \/(A, B, C): [ISO 9.4.4]
# The predicate succeeds in C with the bitwise or of A and B.
##
def arit_or(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    return alpha | beta


###
# xor(A, B, C): [TC2 9.4.6]
# The predicate succeeds in C with the bitwise xor of A and B.
##
def arit_xor(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    return alpha ^ beta


###
# >>(A, B, C): [ISO 9.4.1]
# The predicate succeeds in C with A shift right by B.
##
def arit_shiftright(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta >= 0:
        return alpha >> beta
    else:
        return alpha << (- beta)


###
# <<(A, B, C): [ISO 9.4.2]
# The predicate succeeds in C with A shift left by B.
##
def arit_shiftleft(args):
    alpha = exec_eval(args[0])
    check_integer(alpha)
    beta = exec_eval(args[1])
    check_integer(beta)
    if beta >= 0:
        return alpha << beta
    else:
        return alpha >> (- beta)


################################################################
# ==/2, \==/2                                                  #
################################################################

###
# S == T: [ISO 8.4.1]
# The built-in succeeds when S and T are syntactically equivalent
# Prolog terms, otherwise the built-in fails.
##
def test_equal(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return equal_term(alpha, beta)


###
# S \== T: [ISO 8.4.1]
# The built-in succeeds when S and T are not syntactically equivalent
# Prolog terms, otherwise the built-in fails.
##
def test_notequal(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return not equal_term(alpha, beta)


###
# Determine whether two Prolog terms are syntactically equivalent.
# Can handle cyclic terms and deep recursion.
#
# @param first The first Prolog term.
# @param second The second Prolog term.
# @return True if they are syntactically equivalent, otherwise false.
##
def equal_term(first, second):
    stack = None
    log = None
    try:
        while True:
            first = deref(first)
            second = deref(second)
            if 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)


################################################################
# same_term/2 and hash_code/2                                  #
################################################################

###
# same_term(A, B):
# The built-in succeeds when A and B are equal objects.
# Otherwise the built-in fails.
##
def test_same_term(args):
    alpha = exec_build(args[0])
    beta = exec_build(args[1])
    return object_equals(alpha, beta)


###
# hash_code(X, H):
# The predicate succeeds in H with the hash code of the object X.
##
def test_hash_code(args):
    alpha = exec_build(args[0])
    alpha = object_hash_code(alpha)
    return exec_unify(args[1], alpha)


###
# Compute the hash code of an object
#
# @param alpha The object.
# @return The hash code, a signed 32-bit integer
##
def object_hash_code(alpha):
    if is_variable(alpha):
        return variable_serno(alpha)
    elif is_atom(alpha):
        res = 0
        i = 0
        while i < len(alpha):
            res = int32(res * 31 + ord(alpha[i]))
            i += 1
        return res
    elif is_number(alpha):
        if is_integer(alpha):
            if -0x8000000 < alpha <= 0x7FFFFFFF:
                return alpha
            else:
                if alpha < 0:
                    sign = -1
                    alpha = -alpha
                else:
                    sign = 1
                alpha = "%x" % alpha
                res = 0
                i = len(alpha) % 8
                if i > 0:
                    res = int32(int(alpha[0:i], 16))
                while i < len(alpha):
                    res = int32(res * 31 + int(alpha[i:i+8], 16))
                    i += 8
                return res*sign
        else:
            beta = struct.pack(">d", alpha)
            gamma = struct.unpack(">l", beta[0:4]) + struct.unpack(">l", beta[4:8])
            return gamma[0] ^ gamma[1]
    elif alpha is None:
        return 0
    elif alpha is True:
        return 1231
    elif alpha is False:
        return 1237
    else:
        return 2467


def int32(alpha):
    alpha &= 0xFFFFFFFF
    if alpha >= 0x80000000:
        return alpha - 0x100000000
    else:
        return alpha


def variable_serno(alpha):
    val = alpha.flags & VAR_MASK_SERNO
    if val == VAR_MASK_SERNO:
        if store.engine.low < store.engine.high:
            val = store.engine.low
            store.engine.low = val + 1
        else:
            val = store.engine.serno
            store.engine.serno = val + 1
        alpha.flags &= ~VAR_MASK_SERNO
        alpha.flags |= val
    return val


################################################################
# atom_codes/2 and char_code/2                                 #
################################################################

###
# atom_codes(A, L): [ISO 8.16.5]
# If A is a variable, the built-in succeeds in A with the atom
# for the Prolog list L. Otherwise the built-in succeeds in L
# with the Prolog list from the atom A.
##
def test_atom_codes(args):
    text = exec_deref(args[0])
    if is_variable(text) or is_pending(text):
        res = exec_build(args[1])
        res = atom_codes_pack(res)
        return exec_unify(text, res)
    else:
        text = exec_build(text)
        check_atom(text)
        text = atom_codes_unpack(text)
        return exec_unify(args[1], text)


def atom_codes_pack(peek):
    temp = peek
    i = 0
    while (is_structure(temp) and
           temp.functor == "." and
           len(temp.args) == 2 and
           i < MAX_ARITY):
        ch = deref(temp.args[0])
        check_integer(ch)
        if ch < 0 or ch > 0x10FFFF:
            raise make_error(Compound("type_error", ["character_code", ch]))
        i += 1
        temp = deref(temp.args[1])
    check_nil(temp)
    res = [NotImplemented] * i
    temp = peek
    i = 0
    while (is_structure(temp) and
           temp.functor == "." and
           len(temp.args) == 2):
        ch = deref(temp.args[0])
        res[i] = chr(ch)
        i += 1
        temp = deref(temp.args[1])
    return ''.join(res)


def atom_codes_unpack(text):
    back = None
    res = None
    i = 0
    while i < len(text):
        ch = ord(text[i])
        ch = Compound(".", [ch, NotImplemented])
        if back is not None:
            back.args[1] = ch
        else:
            res = ch
        back = ch
        i += 1
    if back is not None:
        back.args[1] = "[]"
    else:
        res = "[]"
    return res


###
# char_code(C, N): [ISO 8.16.6]
# If C is a variable, the built-in succeeds in C with the
# character for the code N. Otherwise the built-in succeeds
# in N with the code from character C.
##
def test_char_code(args):
    text = exec_deref(args[0])
    if is_variable(text) or is_pending(text):
        ch = exec_build(args[1])
        check_integer(ch)
        if ch < 0 or ch > 0x10FFFF:
            raise make_error(Compound("type_error", ["character_code", ch]))
        ch = chr(ch)
        return exec_unify(text, ch)
    else:
        text = exec_build(text)
        check_atom(text)
        if len(text) != 1:
            raise make_error(Compound("type_error", ["character", text]))
        text = ord(text)
        return exec_unify(args[1], text)


#######################################################################
# atom_length/2 and atom_concat/3                                     #
#######################################################################

###
# atom_length(X, Y): [ISO 8.16.1]
# The predicate succeeds in Y with the length of the atom X.
##
def test_atom_length(args):
    text = exec_build(args[0])
    check_atom(text)
    return exec_unify(args[1], len(text))


###
# atom_concat(X, Y, Z): [ISO 8.16.2]
# The built-in succeeds when Z is the concatenation of X and Y.
##
def special_atom_concat(args):
    first = deref(args[0])
    second = deref(args[1])
    third = deref(args[2])
    if is_variable(second):
        if is_variable(first):
            check_atom(third)
            return solve2_concat(args, None, 0, None)
        else:
            check_atom(first)
            check_atom(third)
            if not third.startswith(first):
                return False
            if not unify(second, third[len(first):]):
                return False
    elif is_variable(first):
        check_atom(second)
        check_atom(third)
        if not third.endswith(second):
            return False
        if not unify(first, third[:len(third)-len(second)]):
            return False
    else:
        check_atom(first)
        check_atom(second)
        if not unify(third, first+second):
            return False
        cont(machine.call.args[1])
    return True


def solve_concat(rope, at, choice):
    goal = deref(machine.call.args[0])
    return solve2_concat(goal.args, rope, at, choice)


def solve2_concat(args, rope, at, choice):
    text = deref(args[2])
    mark = machine.trail
    while at <= len(text):
        if unify(args[0], text[0:at]) and \
                unify(args[1], text[at:]):
            at += 1
            if at <= len(text):
                if choice is None:
                    choice = Choice(solve_concat, None, at, mark)
                else:
                    choice.at = at
                more(choice)
            cont(machine.call.args[1])
            return True
        unbind(mark)
        at += 1
    return False


###################################################################
# atom_join/2                                                     #
###################################################################

###
# atom_join(L, A):
# The built-in succeeds in A with the join of the atoms L.
##
def test_atom_join(args):
    alpha = exec_build(args[0])
    res = atom_join(alpha)
    return exec_unify(args[1], res)


def atom_join(res):
    peek = res
    i = 0
    while is_structure(peek) and \
            peek.functor == "." and \
            len(peek.args) == 2 and \
            i < MAX_ARITY:
        i += 1
        peek = deref(peek.args[1])
    check_nil(peek)
    elems = [NotImplemented] * i
    peek = res
    i = 0
    while is_structure(peek) and \
            peek.functor == "." and \
            len(peek.args) == 2:
        val = deref(peek.args[0])
        check_atom(val)
        elems[i] = val
        i += 1
        peek = deref(peek.args[1])
    return "".join(elems)


#######################################################################
# sys_atom_match/3 and sys_atom_part/4                                #
#######################################################################

###
# sys_atom_match(X, Y, Z):
# The built-in succeeds if X has substring Y at Z.
##
def special_sys_atom_match(args):
    text = deref(args[0])
    check_atom(text)
    part = deref(args[1])
    check_atom(part)
    alpha = deref(args[2])
    if is_variable(alpha):
        return solve2_match(args, None, 0, None)
    else:
        check_integer(alpha)
        if alpha < 0 or alpha > len(text):
            return False
        if not text.startswith(part, alpha):
            return False
    cont(machine.call.args[1])
    return True


def solve_match(rope, at, choice):
    goal = deref(machine.call.args[0])
    return solve2_match(goal.args, rope, at, choice)


def solve2_match(args, rope, at, choice):
    text = deref(args[0])
    part = deref(args[1])
    mark = machine.trail
    while at + len(part) <= len(text):
        at = text.find(part, at)
        if at < 0:
            return False
        if unify(args[2], at):
            at += 1
            if at + len(part) <= len(text):
                if choice is None:
                    choice = Choice(solve_match, None, at, mark)
                else:
                    choice.at = at
                more(choice)
            cont(machine.call.args[1])
            return True
        unbind(mark)
        at += 1
    return False


###
# sys_atom_part(X, Y, Z, T):
# The built-in succeeds in T with the substring at
# offset Y and with length Z from X.
##
def special_sys_atom_part(args):
    text = deref(args[0])
    check_atom(text)
    alpha = deref(args[1])
    if is_variable(alpha):
        beta = deref(args[2])
        check_integer(beta)
        if beta < 0 or beta > len(text):
            return False
        return solve2_part(args, 0, beta, None)
    else:
        check_integer(alpha)
        beta = deref(args[2])
        check_integer(beta)
        if alpha < 0 or alpha > len(text):
            return False
        if beta < 0 or alpha+beta > len(text):
            return False
        if not unify(args[3], text[alpha:alpha+beta]):
            return False
    cont(machine.call.args[1])
    return True


def solve_part(rope, at, choice):
    goal = deref(machine.call.args[0])
    return solve2_part(goal.args, rope, at, choice)


def solve2_part(args, alpha, beta, choice):
    text = deref(args[0])
    mark = machine.trail
    while beta <= len(text):
        if unify(args[1], alpha) and \
                unify(args[3], text[alpha:beta]):
            alpha += 1
            beta += 1
            if beta <= len(text):
                if choice is None:
                    choice = Choice(solve_part, alpha, beta, mark)
                else:
                    choice.data = alpha
                    choice.at = beta
                more(choice)
            cont(machine.call.args[1])
            return True
        unbind(mark)
        alpha += 1
        beta += 1
    return False


#######################################################################
# sys_last_atom_match/3 and sys_last_atom_part/4                      #
#######################################################################

###
# sys_last_atom_match(X, Y, Z):
# The built-in succeeds if X has substring Y at Z.
##
def special_sys_last_atom_match(args):
    text = deref(args[0])
    check_atom(text)
    part = deref(args[1])
    check_atom(part)
    alpha = deref(args[2])
    if is_variable(alpha):
        return solve2_last_match(args, None, len(text)-len(part), None)
    else:
        check_integer(alpha)
        if alpha < 0 or alpha > len(text):
            return False
        if not text.startswith(part, alpha):
            return False
    cont(machine.call.args[1])
    return True


def solve_last_match(rope, at, choice):
    goal = deref(machine.call.args[0])
    return solve2_last_match(goal.args, rope, at, choice)


def solve2_last_match(args, rope, at, choice):
    text = deref(args[0])
    part = deref(args[1])
    mark = machine.trail
    while at >= 0:
        at = text.rfind(part, 0, at+len(part))
        if at < 0:
            return False
        if unify(args[2], at):
            at -= 1
            if at >= 0:
                if choice is None:
                    choice = Choice(solve_last_match, None, at, mark)
                else:
                    choice.at = at
                more(choice)
            cont(machine.call.args[1])
            return True
        unbind(mark)
        at -= 1
    return False


###
# sys_last_atom_part(X, Y, Z, T):
# The built-in succeeds in T with the substring at
# offset Y and with length Z from X.
##
def special_sys_last_atom_part(args):
    text = deref(args[0])
    check_atom(text)
    alpha = deref(args[1])
    if is_variable(alpha):
        beta = deref(args[2])
        check_integer(beta)
        if beta < 0 or beta > len(text):
            return False
        return solve2_last_part(args, len(text)-beta, len(text), None)
    else:
        check_integer(alpha)
        beta = deref(args[2])
        check_integer(beta)
        if alpha < 0 or alpha > len(text):
            return False
        if beta < 0 or alpha+beta > len(text):
            return False
        if not unify(args[3], text[alpha:alpha+beta]):
            return False
    cont(machine.call.args[1])
    return True


def solve_last_part(rope, at, choice):
    goal = deref(machine.call.args[0])
    return solve2_last_part(goal.args, rope, at, choice)


def solve2_last_part(args, alpha, beta, choice):
    text = deref(args[0])
    mark = machine.trail
    while alpha >= 0:
        if unify(args[1], alpha) and \
                unify(args[3], text[alpha:beta]):
            alpha -= 1
            beta -= 1
            if alpha >= 0:
                if choice is None:
                    choice = Choice(solve_last_part, alpha, beta, mark)
                else:
                    choice.data = alpha
                    choice.at = beta
                more(choice)
            cont(machine.call.args[1])
            return True
        unbind(mark)
        alpha -= 1
        beta -= 1
    return False


#######################################################################
# Special Init                                                        #
#######################################################################

# number specials, basic predicates
add("is", 2, make_check(test_eval))

# number specials, basic operations
add("-", 2, make_arithmetic(arit_neg))
add("+", 3, make_arithmetic(arit_add))
add("-", 3, make_arithmetic(arit_sub))
add("*", 3, make_arithmetic(arit_mul))
add("/", 3, make_arithmetic(arit_quot))
add("//", 3, make_arithmetic(arit_intquot))
add("rem", 3, make_arithmetic(arit_rem))

# number specials, more operations
add("float", 2, make_arithmetic(arit_float))
add("^", 3, make_arithmetic(arit_intpow))
add("div", 3, make_arithmetic(arit_div))
add("mod", 3, make_arithmetic(arit_mod))

# number specials, magnitude operations
add("abs", 2, make_arithmetic(arit_abs))
add("sign", 2, make_arithmetic(arit_sign))
add("min", 3, make_arithmetic(arit_min))
add("max", 3, make_arithmetic(arit_max))

# number specials, rounding operations
add("truncate", 2, make_arithmetic(arit_truncate))
add("floor", 2, make_arithmetic(arit_floor))
add("ceiling", 2, make_arithmetic(arit_ceiling))
add("round", 2, make_arithmetic(arit_round))

# number specials, magnitude predicates
add("=:=", 2, make_check(test_numberequal))
add("=\\=", 2, make_check(test_numbernotequal))
add("<", 2, make_check(test_numberless))
add(">=", 2, make_check(test_numbergreaterequal))
add(">", 2, make_check(test_numbergreater))
add("=<", 2, make_check(test_numberlessequal))

# number specials, trigonometric operations
add("sin", 2, make_arithmetic(arit_sin))
add("cos", 2, make_arithmetic(arit_cos))
add("tan", 2, make_arithmetic(arit_tan))
add("asin", 2, make_arithmetic(arit_asin))
add("acos", 2, make_arithmetic(arit_acos))
add("atan", 2, make_arithmetic(arit_atan))
add("pi", 1, make_arithmetic(arit_pi))

# number specials, exponential operations
add("**", 3, make_arithmetic(arit_pow))
add("exp", 2, make_arithmetic(arit_exp))
add("log", 2, make_arithmetic(arit_log))
add("sqrt", 2, make_arithmetic(arit_sqrt))
add("e", 1, make_arithmetic(arit_e))
add("epsilon", 1, make_arithmetic(arit_epsilon))
add("atan2", 3, make_arithmetic(arit_atan2))

# number specials, bitwise operations
add("\\", 2, make_arithmetic(arit_not))
add("/\\", 3, make_arithmetic(arit_and))
add("\\/", 3, make_arithmetic(arit_or))
add("xor", 3, make_arithmetic(arit_xor))
add(">>", 3, make_arithmetic(arit_shiftright))
add("<<", 3, make_arithmetic(arit_shiftleft))

# term specials, miscellaneous equality
add("==", 2, make_check(test_equal))
add("\\==", 2, make_check(test_notequal))
add("same_term", 2, make_check(test_same_term))
add("hash_code", 2, make_check(test_hash_code))

# atom specials, standard
add("atom_codes", 2, make_check(test_atom_codes))
add("char_code", 2, make_check(test_char_code))
add("atom_length", 2, make_check(test_atom_length))
add("atom_concat", 3, make_special(special_atom_concat))

# atom specials, non-standard
add("atom_join", 2, make_check(test_atom_join))
add("sys_atom_match", 3, make_special(special_sys_atom_match))
add("sys_atom_part", 4, make_special(special_sys_atom_part))
add("sys_last_atom_match", 3, make_special(special_sys_last_atom_match))
add("sys_last_atom_part", 4, make_special(special_sys_last_atom_part))
