###
# 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 (is_logical, is_clause, is_cache,
    resolve_link, snapshot_peek, pred_link,
    MASK_PRED_ARITH, MASK_PRED_TEST, Structure, Item,
    MASK_PRED_SPECIAL, is_goal, stack_peek,
    stack_pop, stack_push, deref, is_compound, is_place,
    VAR_MASK_ODD, VAR_MASK_STATE, VAR_MASK_SERNO,
    snapshot_rope, defined_pred, is_stick, is_element,
    set_engine, Engine, Variable, is_variable,
    array_last_index, Compound, is_structure, is_skeleton)
import time
import asyncio
import platform
import struct
import math
import numbers

VOID_ARGS = []

trail = None
redo = None
call = "[]"


###
# Create an error term from a message.
#
# @param beta The message.
# @return The error term.
##
def make_error(beta):
    return Exception(Compound("error", [beta, fetch_stack(ctx)]))


###
# Retrieve the current stack.
#
# @param buf The context.
# @return The current stack.
##
def fetch_stack(buf):
    temp = pred_link("sys_including", 3)
    if (temp is NotImplemented or (not is_logical(temp.func) and
           not is_stick(temp.func))):
        return "[]"
    data = snapshot_peek(temp.func)
    back = None
    res = None
    i = 0
    while i < len(data):
        clause = data[i]
        if clause.size != 0:
            display = [NotImplemented] * clause.size
        else:
            display = None
        elem = exec_frame(clause.functor, clause.head, display)
        if not object_equals(elem.args[1], buf):
            i += 1
            continue
        elem = Compound("sys_including", [elem.args[0], elem.args[2]])
        elem = Compound(".", [elem, NotImplemented])
        if back is None:
            res = elem
        else:
            back.args[1] = elem
        back = elem
        i += 1
    if back is None:
        res = "[]"
    else:
        back.args[1] = "[]"
    return res


def exec_frame(functor, head, display):
    global temp_display
    if len(head) > 0:
        temp_display = display
        args = [NotImplemented] * len(head)
        i = 0
        while i < len(args):
            args[i] = exec_build(head[i])
            i += 1
        temp_display = None
        return Compound(functor, args)
    else:
        return functor


###
# Create a Prolog compound indicator.
#
# @param functor The functor.
# @param arity The arity.
# @return Compound The Prolog compound indicator.
##
def make_indicator(functor, arity):
    if is_cache(functor):
        functor = functor.name
    return Compound("/", [functor, arity])


################################################################
# Frozen Terms                                                 #
################################################################

##
# Create a Prolog frozen.
#
# @param functor The functor.
# @param args The arguments.
# @constructor The new frozen.
##
class Frozen(Structure):
    def __init__(self, functor, args):
        super().__init__(functor, args)
        self.hash = object_hash_code(functor)
        i = 0
        while i < len(args):
            obj = args[i]
            if is_frozen(obj):
                self.hash = int32(self.hash*31 + obj.hash)
            else:
                self.hash = int32(self.hash*31 + object_hash_code(obj))
            i += 1


###
# Check whether an object is a Prolog frozen.
#
# @param obj The object.
# @return True if the object is a frozen, otherwise false.
##
def is_frozen(obj):
    return isinstance(obj, Frozen)


def object_hash_code(alpha):
    if 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 if sign > 0 else -res
        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


################################################################
# Garbage Collection                                           #
################################################################

if platform.python_implementation() == "PyPy":
    gc_maxinfs = 144000
else:
    gc_maxinfs = 88000

gc_mask = VAR_MASK_ODD

gc_last = 0.0
gc_time = 0.0
gc_enter = 0
gc_tick = gc_maxinfs
gc_tack = 60*gc_maxinfs
gc_tock = 3600*gc_maxinfs


###
# Retrieve the real time.
#
# @return The real time.
##
def real_time():
    return time.monotonic_ns() / 1000000.0


################################################################
# Major Marking                                                #
################################################################

###
# Perform major garbage collection.
##
def gc_major():
    global gc_time
    global gc_mask
    gc_time -= real_time()
    gc_mask ^= VAR_MASK_STATE
    store.engine.low = 0
    store.engine.high = store.engine.serno
    store.engine.serno = 0
    mark_redo()
    adjust_redo()
    sweep_trail(None)
    gc_time += real_time()


###
# Major mark a term.
#
# @param term The term.
##
def mark_term(first):
    stack = None
    while True:
        if is_variable(first):
            if (first.flags & VAR_MASK_STATE) != gc_mask:
                first.flags = (first.flags & ~VAR_MASK_STATE) | gc_mask
                val = first.flags & VAR_MASK_SERNO
                if val != VAR_MASK_SERNO:
                    if val > store.engine.serno:
                        store.engine.serno = val + 1
                    if store.engine.low <= val and val < store.engine.high:
                        if val - store.engine.low > store.engine.high - val:
                            store.engine.high = val
                        else:
                            store.engine.low = val + 1
                if first.instantiated is not NotImplemented:
                    peek = first.instantiated
                    first.instantiated = stack
                    stack = first
                    first = peek
                    continue
        elif is_compound(first):
            if (first.walk & VAR_MASK_STATE) != gc_mask:
                first.walk = (first.walk & ~VAR_MASK_STATE) | gc_mask
                peek = first.args[0]
                first.args[0] = stack
                first.walk &= ~VAR_MASK_SERNO
                stack = first
                first = peek
                continue
        while (stack is not None and (is_variable(stack) or
                (stack.walk & VAR_MASK_SERNO) == len(stack.args) - 1)):
            if is_variable(stack):
                peek = stack.instantiated
                stack.instantiated = first
                first = stack
                stack = peek
            else:
                peek = stack.args[stack.walk & VAR_MASK_SERNO]
                stack.args[stack.walk & VAR_MASK_SERNO] = first
                first = stack
                stack = peek
        if stack is None:
            return
        else:
            peek = stack.args[stack.walk & VAR_MASK_SERNO]
            stack.args[stack.walk & VAR_MASK_SERNO] = first
            stack.walk += 1
            first = stack.args[stack.walk & VAR_MASK_SERNO]
            stack.args[stack.walk & VAR_MASK_SERNO] = peek


###
# Major mark the continuations.
##
def mark_redo():
    term = call
    last = redo
    while True:
        mark_term(term)
        if last is None:
            break
        term = last.cont
        last = last.tail


################################################################
# Minor Marking                                                #
################################################################

###
# Perform minor garbage collection.
##
def gc_minor():
    global gc_time
    global gc_maxinfs
    global gc_last
    gc_time -= real_time()
    mark2_redo()
    mark2_trail(store.engine.backtrail)
    adjust_redo()
    sweep_trail(store.engine.backtrail)
    gc_now = real_time()
    gc_time += gc_now
    val = gc_now - gc_last
    gc_last = gc_now
    val = (gc_maxinfs * 1000) / val
    gc_maxinfs = round((3 * gc_maxinfs + val) / 4)


###
# Minor mark a term.
#
# @param first The term.
##
def mark2_term(first):
    stack = None
    while True:
        if is_variable(first):
            if (first.flags & VAR_MASK_STATE) != gc_mask:
                first.flags = (first.flags & ~VAR_MASK_STATE) | gc_mask
                if first.instantiated is not NotImplemented:
                    peek = first.instantiated
                    first.instantiated = stack
                    stack = first
                    first = peek
                    continue
        elif is_compound(first):
            if (first.walk & VAR_MASK_STATE) != gc_mask:
                first.walk = (first.walk & ~VAR_MASK_STATE) | gc_mask
                peek = first.args[0]
                first.args[0] = stack
                first.walk &= ~VAR_MASK_SERNO
                stack = first
                first = peek
                continue
        while (stack is not None and (is_variable(stack) or
                (stack.walk & VAR_MASK_SERNO) == len(stack.args) - 1)):
            if is_variable(stack):
                peek = stack.instantiated
                stack.instantiated = first
                first = stack
                stack = peek
            else:
                peek = stack.args[stack.walk & VAR_MASK_SERNO]
                stack.args[stack.walk & VAR_MASK_SERNO] = first
                first = stack
                stack = peek
        if stack is None:
            return
        else:
            peek = stack.args[stack.walk & VAR_MASK_SERNO]
            stack.args[stack.walk & VAR_MASK_SERNO] = first
            stack.walk += 1
            first = stack.args[stack.walk & VAR_MASK_SERNO]
            stack.args[stack.walk & VAR_MASK_SERNO] = peek


###
# Minor mark the continuations.
##
def mark2_redo():
    term = call
    last = redo
    while True:
        mark2_term(term)
        if last is None:
            break
        term = last.cont
        last = last.tail


################################################################
# Variable Sweep                                               #
################################################################

###
# Adjust the markers into the trail.
##
def adjust_redo():
    last = redo
    while last is not None:
        temp = last.mark
        while temp is not None:
            if (temp.flags & VAR_MASK_STATE) == gc_mask:
                break
            else:
                temp = temp.tail
        last.mark = temp
        last = last.tail


###
# Minor mark the trail
#
# @param stop The stop.
##
def mark2_trail(stop):
    temp = trail
    while temp is not stop:
        if (temp.flags & VAR_MASK_STATE) == VAR_MASK_STATE:
            mark2_term(temp)
        temp = temp.tail


###
# Sweep the trail.
#
# @param stop The stop.
##
def sweep_trail(stop):
    global trail
    temp = trail
    back = None
    while temp is not stop:
        term = temp
        temp = term.tail
        if (term.flags & VAR_MASK_STATE) == gc_mask:
            if back is not None:
                back.tail = term
            else:
                trail = term
            back = term
        else:
            term.instantiated = NotImplemented
            term.tail = None
    if back is not None:
        back.tail = stop
    else:
        trail = stop
    store.engine.backtrail = trail


################################################################
# Signal Handling                                              #
################################################################

###
# Check the signal message.
##
def solve_signal(rope, at, choice):
    if store.engine.signal is not NotImplemented:
        message = store.engine.signal
        store.engine.signal = NotImplemented
        raise make_error(message)
    return True


################################################################
# Clause Loops                                                 #
################################################################

SYS_MASK_ASYNC_MODE = 0x00000001
SYS_MASK_ALLOW_YIELD = 0x00000008
SYS_MASK_FULL_ASYNC = SYS_MASK_ASYNC_MODE | SYS_MASK_ALLOW_YIELD


###
# Set the continuation.
#
# @param term The continuation.
##
def cont(term):
    global call
    call = term


###
# Solve Prolog goals.
#
# @param snap The choice point boundary.
# @param found True for call, and false for redo.
# @return True if execution succeeds, otherwise false.
##
def solve(snap, found):
    global call
    global redo
    global gc_enter
    global gc_tick
    global gc_tack
    global gc_tock
    while True:
        if found is True:
            if gc_enter >= gc_tick:
                if gc_enter >= gc_tock:
                    gc_major()
                    gc_tock += 3600*gc_maxinfs
                elif gc_enter >= gc_tack:
                    gc_minor()
                    gc_tack += 60*gc_maxinfs
                gc_tick += gc_maxinfs
                if (store.engine.flags & SYS_MASK_ASYNC_MODE) != 0:
                    more(Choice(solve_signal, None, 0, trail))
                    return lambda: immediate_promise()
            goal = call
            if is_structure(goal):
                gc_enter += 1
                goal = goal.args[0]
                peek = lookup_pred(goal)
                if peek is NotImplemented or (peek.flags & MASK_PRED_ARITH) != 0:
                    raise make_error(Compound("existence_error",
                        ["procedure", make_indicator_term(goal)]))
                if is_structure(goal):
                    goal = goal.args
                else:
                    goal = VOID_ARGS
                if (peek.flags & MASK_PRED_TEST) != 0:
                    if not peek.func(goal):
                        found = False
                    else:
                        cont(call.args[1])
                        found = True
                elif (peek.flags & MASK_PRED_SPECIAL) != 0:
                    found = peek.func(goal)
                else:
                    peek = defined_pred(peek, goal)
                    found = solve2_rope(goal, snapshot_rope(peek), 0, None)
            else:
                break
        elif found is False:
            if redo is not snap:
                choice = redo
                redo = choice.tail
                unbind(choice.mark)
                call = choice.cont
                found = choice.func(choice.data, choice.at, choice)
            else:
                break
        else:
            break
    return found


async def immediate_promise():
    try:
        await asyncio.sleep(0)
    except asyncio.CancelledError:
        pass


################################################################
# Linked Provables                                             #
################################################################

###
# Lookup a predicate.
#
# @param goal The goal.
# @return The predicate or NotImplemented
##
def lookup_pred(goal):
    if is_element(goal):
        functor = goal.functor
        arity = len(goal.args)
    else:
        functor = goal
        arity = 0
    return resolve_link(functor, arity)


###
# Lookup an evaluable function.
#
# @param expr The arithmetic expression.
# @return The evaluable function or NotImplemented
##
def lookup_eval(expr):
    if is_element(expr):
        functor = expr.functor
        arity = len(expr.args)
    else:
        functor = expr
        arity = 0
    return resolve_link(functor, arity + 1)


def make_indicator_term(goal):
    if is_structure(goal):
        functor = goal.functor
        arity = len(goal.args)
    else:
        functor = goal
        arity = 0
    return make_indicator(functor, arity)


def solve_rope(rope, at, choice):
    goal = deref(call.args[0])
    if is_structure(goal):
        goal = goal.args
    else:
        goal = VOID_ARGS
    return solve2_rope(goal, rope, at, choice)


###
# Search a Prolog clause and add it to the continuation.
#
# @param paras The called goal.
# @param rope The clausse list.
# @param at The clause index.
# @param choice The choice point for reuse or None.
# @return True if search succeeds, otherwise false.
##
def solve2_rope(paras, rope, at, choice):
    mark = trail
    while at < len(rope):
        clause = rope[at]
        at += 1
        if clause.size != 0:
            display = [NotImplemented] * clause.size
        else:
            display = None
        if exec_head(clause.head, display, paras):
            peek = clause.cutvar
            if peek != -1:
                display[peek] = redo
            if at < len(rope):
                if choice is None:
                    choice = Choice(solve_rope, rope, at, mark)
                else:
                    choice.at = at
                more(choice)
                if exec_check(clause.body, display):
                    return True
                if redo is not choice:
                    return False
                more(choice.tail)
            else:
                return exec_check(clause.body, display)
        unbind(mark)
    return False


###
# Remove choice points.
#
# @param last The last choice point.
##
def cut(last):
    global redo
    redo = last


###
# Sets the choice point.
#
# @param choice The new choice point.
##
def more(choice):
    global redo
    redo = choice


###
# Create a choice point.
#
# @param func The choice point handler.
# @param data The choice point data.
# @param at The choice point index.
# @param mark The trail mark.
# @constructor The choice point.
##
class Choice:
    def __init__(self, func, data, at, mark):
        self.func = func
        self.data = data
        self.at = at
        self.mark = mark
        self.cont = call
        self.tail = redo


################################################################
# Directives                                                   #
################################################################

CTX_MAIN = "main"


###
# Run a compiled goal once. The goal is run with auto-yield
# disabled and promises are not accepted.
#
# @param goal The compiled goal.
# @throw If false.
##
def run(goal):
    if not launch(goal, CTX_MAIN, VOID_ARGS):
        raise make_error(Compound("syntax_error", ["directive_failed"]))


def snap_setup():
    global redo
    redo = Choice(solve_setup, None, 0, trail)
    return redo


def solve_setup(rope, at, choice):
    return False


def snap_cleanup(snap):
    global call
    more(snap.tail)
    unbind(snap.mark)
    call = snap.cont


################################################################
# Terms                                                        #
################################################################

###
# Check whether an object is an atom.
#
# @param obj The object.
# @return True if the object is an atom, otherwise false.
##
def is_atom(obj):
    return isinstance(obj, str)


###
# Check whether an object is a number.
#
# @param obj The object.
# @return True if the object is a number, otherwise false.
##
def is_number(obj):
    return isinstance(obj, numbers.Number) and not isinstance(obj, bool)


###
# Check whether an object is an integer.
#
# @param obj The object.
# @return True if the object is an integer, otherwise false.
##
def is_integer(obj):
    return isinstance(obj, int) and not isinstance(obj, bool)


###
# Check whether an object is a float.
#
# @param obj The object.
# @return True if the object is a float, otherwise false.
##
def is_float(obj):
    return isinstance(obj, float)


###
# Check whether an object is a special value.
#
# @param alpha The object.
# @return boolean True if the object is a special value, otherwise false.
##
def is_special(alpha):
    return (isinstance(alpha, float) and
            not math.isfinite(alpha))


################################################################
# Albufeira Lazy                                               #
################################################################

temp_display: (list | None) = None

def is_pending(template):
    if template is NotImplemented:
        return True
    elif is_place(template):
        return True
    else:
        return False


def exec_deref(template):
    if template is NotImplemented:
        return template
    elif is_place(template):
        index = template.index
        peek = temp_display[index]
        if peek is NotImplemented:
            return template
        else:
            return deref(peek)
    else:
        return deref(template)


################################################################
# Albufeira Modes                                              #
################################################################

def exec_build(template):
    back = None
    while True:
        if template is NotImplemented:
            template = Variable()
            break
        elif is_place(template):
            index = template.index
            template = temp_display[index]
            if template is NotImplemented:
                template = Variable()
                temp_display[index] = template
            else:
                template = deref(template)
            break
        elif is_skeleton(template):
            args = [NotImplemented] * len(template.args)
            args[len(args)-1] = back
            back = Compound(template.functor, args)
            template = template.args
            i = 0
            while i < len(args) - 1:
                args[i] = exec_build(template[i])
                i += 1
            template = template[i]
        else:
            template = deref(template)
            break
    while back is not None:
        peek = back.args[len(back.args) - 1]
        back.args[len(back.args) - 1] = template
        template = back
        back = peek
    return template


def exec_unify(template, alpha):
    while True:
        if template is NotImplemented:
            return True
        elif is_place(template):
            index = template.index
            template = temp_display[index]
            if template is NotImplemented:
                temp_display[index] = deref(alpha)
                return True
            else:
                return unify(alpha, template)
        elif is_skeleton(template):
            alpha = deref(alpha)
            if is_variable(alpha):
                args = [NotImplemented] * len(template.args)
                bind(Compound(template.functor, args), alpha)
                template = template.args
                i = 0
                while i < len(args):
                    args[i] = exec_build(template[i])
                    i += 1
                return True
            elif is_structure(alpha):
                if len(template.args) != len(alpha.args):
                    return False
                if template.functor != alpha.functor:
                    return False
                template = template.args
                alpha = alpha.args
                i = 0
                while i < len(template) - 1:
                    if not exec_unify(template[i], alpha[i]):
                        return False
                    i += 1
                template = template[i]
                alpha = alpha[i]
            else:
                return False
        else:
            return unify(template, alpha)


################################################################
# Albufeira Clauses                                            #
################################################################

def exec_body(code, display):
    global temp_display
    temp_display = display
    back = None
    res = None
    i = 0
    while i < len(code):
        goal = exec_build(code[i])
        temp = Compound(".", [goal, NotImplemented])
        if back is None:
            res = temp
        else:
            back.args[1] = temp
        back = temp
        i += 1
    if back is None:
        res = "[]"
    else:
        back.args[1] = "[]"
    temp_display = None
    return res


def exec_head(code, display, aux):
    global temp_display
    if len(aux) != len(code):
        return False
    temp_display = display
    i = 0
    while i < len(code):
        if not exec_unify(code[i], aux[i]):
            temp_display = None
            return False
        i += 1
    temp_display = None
    return True


################################################################
# Head Check                                                   #
################################################################

def exec_eval(template):
    if template is NotImplemented:
        raise make_error("instantiation_error")
    elif is_place(template):
        index = template.index
        template = temp_display[index]
        if template is NotImplemented:
            raise make_error("instantiation_error")
    template = deref(template)
    if is_number(template):
        return template
    peek = lookup_eval(template)
    if peek is NotImplemented or (peek.flags & MASK_PRED_ARITH) == 0:
        raise make_error(Compound("type_error",
              ["evaluable", make_indicator_term(template)]))
    if is_element(template):
        template = template.args
    else:
        template = VOID_ARGS
    return peek.func(template)


def exec_test(template):
    global gc_enter
    peek = lookup_pred(template)
    if peek is NotImplemented or (peek.flags & MASK_PRED_TEST) == 0:
        return exec_build(template)
    else:
        if is_element(template):
            template = template.args
        else:
            template = VOID_ARGS
        gc_enter += 1
        return peek.func(template)


def exec_check(code, display):
    global temp_display
    temp_display = display
    check = True
    back = None
    res = None
    i = 0
    while i < len(code):
        goal = exec_test(code[i]) if check else exec_build(code[i])
        if True is goal:
            i += 1
            continue
        if False is goal:
            temp_display = None
            return False
        goal = Compound(".", [goal, NotImplemented])
        if back is None:
            res = goal
        else:
            back.args[1] = goal
        back = goal
        check = False
        i += 1
    if back is None:
        res = call.args[1]
    else:
        back.args[1] = call.args[1]
    temp_display = None
    cont(res)
    return True


################################################################
# Object Equals                                                #
################################################################

###
# Determine whether two objects are equal.
#
# @param alpha The first object.
# @param beta The second object.
##
def object_equals(alpha, beta):
    if is_atom(alpha) or is_number(alpha):
        if is_float(alpha):
            return (is_float(beta) and
                    (math.isnan(beta) if math.isnan(alpha) else alpha == beta))
        elif is_float(beta):
            return False
        else:
            return alpha == beta
    elif is_atom(beta) or is_number(beta):
        return False
    else:
        return alpha is beta


################################################################
# Unification                                                  #
################################################################

###
# Determine whether two terms unify.
# 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(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:
                    bind(second, first)
            elif is_variable(second):
                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:
                        item2 = Item(first, second, 0)
                        stack = stack_push(stack, item2)
                    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)


###
# The function returns the representative of a structure.
#
# @param obj The structure.
# @return The representative.
##
def union_find(obj):
    while is_structure(obj.functor):
        obj = obj.functor
    return obj


###
# The function merges respresentatives and returns a new log.
#
# @param log The log.
# @param from The first representative.
# @param to The second representative.
# @return The new log.
##
def union_add(log, vfrom, to):
    vfrom.functor = to
    if log is None:
        log = []
    log.append(vfrom)
    return log


###
# The routine uses the log L to undo modifications.
#
# @param log The log.
##
def union_undo(log):
    if log is None:
        return
    i = len(log) - 1
    while i >= 0:
        elem = log[i]
        elem.functor = elem.functor.functor
        i -= 1


###
# Bind a variable to a term.
#
# @param source The Prolog term.
# @param term The variable.
##
def bind(source, term):
    global trail
    term.instantiated = source
    term.tail = trail
    if (term.flags & VAR_MASK_STATE) == gc_mask:
        term.flags |= VAR_MASK_STATE
    trail = term


###
# Unbind variable binds.
#
# @param mark The trail mark.
##
def unbind(mark):
    global trail
    while mark is not trail:
        term = trail
        if store.engine.backtrail is term:
            store.engine.backtrail = term.tail
        trail = term.tail
        term.instantiated = NotImplemented
        term.tail = None


################################################################
# Context                                                      #
################################################################

tasks = []


###
# Create a task context.
#
# @param goal The list of goals.
# @constructor The task context.
##
class Context:
    def __init__(self):
        self.trail = None
        self.redo = None
        self.call = "[]"
        self.gc_mask = VAR_MASK_ODD
        self.engine = Engine()
        self.engine.text_output = store.engine.text_output
        self.engine.text_error = store.engine.text_error
        self.engine.text_input = store.engine.text_input
        tasks.append(self)


def ctx_ended(buf):
    k = array_last_index(tasks, buf)
    if k != -1:
        del tasks[k]


################################################################
# Switching                                                    #
################################################################


def group_teardown():
    i = 0
    while i < len(tasks):
        buf = tasks[i]
        msg = Compound("system_error", ["user_exit"])
        register_signal(buf, msg)
        invoke_interrupt(buf)
        i += 1


################################################################
# Switching                                                    #
################################################################

ctx = CTX_MAIN


###
# Set the task context.
#
# @param buf The task context.
##
def ctx_set(buf):
    global ctx
    ctx = buf


###
# Switch the task context.
#
# @param buf The context.
##
def ctx_switch(buf):
    global trail
    global redo
    global call
    global gc_mask
    temp = trail
    trail = buf.trail
    buf.trail = temp
    temp = redo
    redo = buf.redo
    buf.redo = temp
    temp = call
    call = buf.call
    buf.call = temp
    temp = gc_mask
    gc_mask = buf.gc_mask
    buf.gc_mask = temp
    temp = store.engine
    set_engine(buf.engine)
    buf.engine = temp


################################################################
# Callback                                                     #
################################################################

###
# Run a callback once, i.e. no choice point or trailing left
# behind. Callbacks are run with auto-yield disabled and
# promises are not accepted, i.e. run "stackless" on top of the
# given main stack or side stack. "stackless" because completion,
# i.e. return or exception by the callback, is the only context switch.
#
# @param form The goal or closure.
# @param buf The context or "main"
# @param paras The actual parameters.
# @return True or false.
##
def launch(form, buf, paras):
    global call
    if buf != CTX_MAIN:
        ctx_set(buf)
        ctx_switch(buf)
    back = store.engine.flags & SYS_MASK_FULL_ASYNC
    store.engine.flags &= ~SYS_MASK_FULL_ASYNC
    snap = snap_setup()
    if is_clause(form):
        call = melt_clause(form, paras)
    elif is_goal(form):
        call = melt_directive(form)
    else:
        call = form
    try:
        found = solve(snap, True)
    finally:
        snap_cleanup(snap)
        store.engine.flags &= ~SYS_MASK_FULL_ASYNC
        store.engine.flags |= back
        if buf != CTX_MAIN:
            ctx_switch(buf)
            ctx_set(CTX_MAIN)
    return found


def callback(form, buf, paras):
    try:
        return launch(form, buf, paras)
    except BaseException:
        return False


def melt_directive(goal):
    if goal.size != 0:
        display = [NotImplemented] * goal.size
    else:
        display = None
    peek = goal.cutvar
    if peek != -1:
        display[peek] = redo
    return exec_body(goal.body, display)


def melt_clause(clause, paras):
    if clause.size != 0:
        display = [NotImplemented] * clause.size
    else:
        display = None
    if exec_head(clause.head, display, paras):
        peek = clause.cutvar
        if peek != -1:
            display[peek] = redo
        return exec_body(clause.body, display)
    else:
        return "[]"


################################################################
# Task                                                         #
################################################################

###
# Run a task once, i.e. no choice point or trailing left
# behind. Tasks are run with auto-yield enabled and promises are
# accepted, i.e. run "stackfull" on top of the given main stack
# or side stack. "stackfull" because not only completion, i.e.
# return or exception by the task, cause a context switch, but
# also await of an auto-yield or promise.
#
# @param form The goal or closure.
# @param buf  The context or "main".
# @param paras   The actual parameters.
# @return True or false.
##
async def launch_async(form, buf, paras):
    global gc_last
    global call
    gc_last += real_time()
    if buf != CTX_MAIN:
        ctx_set(buf)
        ctx_switch(buf)
    back = store.engine.flags & SYS_MASK_FULL_ASYNC
    store.engine.flags |= SYS_MASK_FULL_ASYNC
    found = True
    snap = snap_setup()
    if is_clause(form):
        call = melt_clause(form, paras)
    elif is_goal(form):
        call = melt_directive(form)
    else:
        call = form
    try:
        while True:
            found = solve(snap, found)
            if found is False:
                break
            elif found is not True:
                if buf != CTX_MAIN:
                    ctx_switch(buf)
                    ctx_set(CTX_MAIN)
                gc_last -= real_time()
                await found()
                gc_last += real_time()
                if buf != CTX_MAIN:
                    ctx_set(buf)
                    ctx_switch(buf)
                found = False
            else:
                break
    finally:
        snap_cleanup(snap)
        store.engine.flags &= ~SYS_MASK_FULL_ASYNC
        store.engine.flags |= back
        if buf != CTX_MAIN:
            ctx_switch(buf)
            ctx_set(CTX_MAIN)
            ctx_ended(buf)
    gc_last -= real_time()
    return found


async def task_async(form, buf, paras):
    try:
        await launch_async(form, buf, paras)
    except BaseException:
        pass


###
# Register an abort function in a context.
#
# @param buf The context.
# @param func The function.
##
def register_interrupt(buf, func):
    en = determine_engine(buf)
    en.abort = func


###
# Register a signal in a context.
#
# @param buf The context.
# @param msg The signal.
##
def register_signal(buf, msg):
    en = determine_engine(buf)
    en.signal = msg


###
# Invoke the abort handler of a context.
#
# @param buf The context.
##
def invoke_interrupt(buf):
    en = determine_engine(buf)
    en.abort()


def determine_engine(buf):
    if buf != CTX_MAIN:
        if buf is not ctx:
            return buf.engine
        else:
            return store.engine
    else:
        if ctx != CTX_MAIN:
            return ctx.engine
        else:
            return store.engine