package nova;

import java.math.*;
import java.util.*;

/**
 * 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.
 */
public final class Machine {
    public static final Object[] VOID_ARGS = new Object[0];

    public static Store.Variable trail = null;
    public static Choice redo = null;
    public static Object call = "[]";

    /**
     * Create an error term from a message.
     *
     * @param beta The message.
     * @return Compound The error term.
     */
    public static Handler.Problem make_error(Object beta) {
        return new Handler.Problem(new Store.Compound("error",
                new Object[]{beta, fetch_stack(ctx)}));
    }

    /**
     * Retrieve the current stack.
     *
     * @param buf The context.
     * @return {string | Compound} The current stack.
     */
    private static Object fetch_stack(Object buf) {
        Store.Provable temp = Store.pred_link("sys_including", 3);
        if (temp == null || (!Store.is_logical(temp.func) &&
                !Store.is_stick(temp.func)))
            return "[]";
        Store.Clause[] data = Store.snapshot_peek(temp.func);
        Store.Structure back = null;
        Object res = null;
        for (int i = 0; i < data.length; i++) {
            Store.Clause clause = data[i];
            Object[] display;
            if (clause.size != 0) {
                display = new Object[clause.size];
            } else {
                display = null;
            }
            Store.Structure elem = (Store.Structure)exec_frame(
                    clause.functor, clause.head, display);
            if (!elem.args[1].equals(buf))
                continue;
            elem = fetch_frame(elem);
            elem = new Store.Compound(".", new Object[]{elem, Store.UNDEF_OBJ});
            if (back == null) {
                res = elem;
            } else {
                back.args[1] = elem;
            }
            back = elem;
        }
        if (back == null) {
            res = "[]";
        } else {
            back.args[1] = "[]";
        }
        return res;
    }

    public static Object exec_frame(Object functor,
                                    Object[] head, Object[] display) {
        if (head.length > 0) {
            temp_display = display;
            Object[] args = new Object[head.length];
            for (int i = 0; i < args.length; i++)
                args[i] = exec_build(head[i]);
            temp_display = null;
            return new Store.Compound(functor, args);
        } else {
            return functor;
        }
    }

    public static Store.Structure fetch_frame(Store.Structure elem) {
        String file = (String)elem.args[0];
        int k1 = file.lastIndexOf('/');
        int k2 = file.lastIndexOf('\\');
        String name = file.substring(Math.max(k1, k2)+1);
        runtime.Source stream = (runtime.Source)elem.args[2];
        return new Store.Compound("frame",
                new Object[]{"including", name,
                        Integer.valueOf(stream.lineno)});
    }

    /**
     * Create a Prolog compound indicator.
     *
     * @param functor The functor.
     * @param arity   The arity.
     * @return Compound The Prolog compound indicator.
     */
    public static Object make_indicator(Object functor, int arity) {
        if (Store.is_cache(functor))
            functor = ((Store.Cache)functor).name;
        return new Store.Compound("/", new Object[]{functor, Integer.valueOf(arity)});
    }

    /**************************************************************/
    /* Frozen Terms                                               */
    /**************************************************************/

    public static final class Frozen extends Store.Structure {
        public int hash;

        /**
         * Create a Prolog frozen.
         *
         * @param functor The functor.
         * @param args    The arguments.
         */
        public Frozen(Object functor, Object[] args) {
            super(functor, args);
            hash = Objects.hashCode(functor);
            for (int i = 0; i < args.length; i++) {
                Object obj = args[i];
                if (is_frozen(obj)) {
                    hash = hash * 31 + ((Frozen) obj).hash;
                } else {
                    hash = hash * 31 + Objects.hashCode(obj);
                }
            }
        }

    }

    /**
     * Check whether an object is a Prolog frozen.
     *
     * @param obj The object.
     * @return True if the object is a frozen, otherwise false.
     */
    public static boolean is_frozen(Object obj) {
        return obj instanceof Frozen;
    }

    /**************************************************************/
    /* Garbage Collection                                         */
    /**************************************************************/

    public static long gc_maxinfs = 352000L;

    public static int gc_mask = Store.VAR_MASK_ODD;

    public static double gc_last = 0.0;
    public static double gc_time = 0.0;
    public static long gc_enter = 0;
    public static long gc_tick = gc_maxinfs;
    public static long gc_tack = 60*gc_maxinfs;
    public static long gc_tock = 3600*gc_maxinfs;

    /**
     * Retrieve the real time.
     *
     * @return The real time.
     */
    public static double real_time() {
        return System.nanoTime() / 1000000.0;
    }

    /**************************************************************/
    /* Major Marking                                              */
    /**************************************************************/

    /**
     * Perform major garbage collection.
     */
    public static void gc_major() {
        gc_time -= real_time();
        gc_mask ^= Store.VAR_MASK_STATE;
        Store.engine.low = 0;
        Store.engine.high = Store.engine.serno;
        Store.engine.serno = 0;
        mark_redo();
        adjust_redo();
        sweep_trail(null);
        gc_time += real_time();
    }

    /**
     * Major mark a term.
     *
     * @param first The term.
     */
    private static void mark_term(Object first) {
        Object stack = null;
        for (;;) {
            if (Store.is_variable(first)) {
                if ((((Store.Variable)first).flags & Store.VAR_MASK_STATE) != gc_mask) {
                    ((Store.Variable)first).flags = (((Store.Variable)first).flags & ~Store.VAR_MASK_STATE) | gc_mask;
                    int val = ((Store.Variable)first).flags & Store.VAR_MASK_SERNO;
                    if (val != Store.VAR_MASK_SERNO) {
                        if (val > Store.engine.serno)
                            Store.engine.serno = val + 1;
                        if (Store.engine.low <= val && val < Store.engine.high) {
                            if (val - Store.engine.low > Store.engine.high - val) {
                                Store.engine.high = val;
                            } else {
                                Store.engine.low = val + 1;
                            }
                        }
                    }
                    if (((Store.Variable)first).instantiated != Store.UNDEF_OBJ) {
                        Object peek = ((Store.Variable)first).instantiated;
                        ((Store.Variable)first).instantiated = stack;
                        stack = first;
                        first = peek;
                        continue;
                    }
                }
            } else if (Store.is_compound(first)) {
                if ((((Store.Compound)first).walk & Store.VAR_MASK_STATE) != gc_mask) {
                    ((Store.Compound)first).walk = (((Store.Compound)first).walk & ~Store.VAR_MASK_STATE) | gc_mask;
                    Object peek = ((Store.Structure)first).args[0];
                    ((Store.Structure)first).args[0] = stack;
                    ((Store.Compound)first).walk &= ~Store.VAR_MASK_SERNO;
                    stack = first;
                    first = peek;
                    continue;
                }
            }
            while (stack != null && (Store.is_variable(stack) ||
                    (((Store.Compound)stack).walk & Store.VAR_MASK_SERNO) ==
                            ((Store.Structure)stack).args.length - 1)) {
                if (Store.is_variable(stack)) {
                    Object peek = ((Store.Variable)stack).instantiated;
                    ((Store.Variable)stack).instantiated = first;
                    first = stack;
                    stack = peek;
                } else {
                    Object peek = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                    ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = first;
                    first = stack;
                    stack = peek;
                }
            }
            if (stack == null) {
                return;
            } else {
                Object peek = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = first;
                ((Store.Compound)stack).walk++;
                first = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = peek;
            }
        }
    }

    /**
     * Major mark the continuations.
     */
    private static void mark_redo() {
        Object term = call;
        Choice last = redo;
        for (;;) {
            mark_term(term);
            if (last == null)
                break;
            term = last.cont;
            last = last.tail;
        }
    }

    /**************************************************************/
    /* Minor Marking                                              */
    /**************************************************************/

    /**
     * Perform minor garbage collection.
     */
    private static void gc_minor() {
        gc_time -= real_time();
        mark2_redo();
        mark2_trail(Store.engine.backtrail);
        adjust_redo();
        sweep_trail(Store.engine.backtrail);
        double gc_now = real_time();
        gc_time += gc_now;
        double val = gc_now - gc_last;
        gc_last = gc_now;
        val = (gc_maxinfs * 1000) / val;
        gc_maxinfs = Math.round((3 * gc_maxinfs + val) / 4);
    }

    /**
     * Minor mark a term.
     *
     * @param first The term.
     */
    public static void mark2_term(Object first) {
        Object stack = null;
        for (;;) {
            if (Store.is_variable(first)) {
                if ((((Store.Variable)first).flags & Store.VAR_MASK_STATE) != gc_mask) {
                    ((Store.Variable)first).flags = (((Store.Variable)first).flags & ~Store.VAR_MASK_STATE) | gc_mask;
                    if (((Store.Variable)first).instantiated != Store.UNDEF_OBJ) {
                        Object peek = ((Store.Variable)first).instantiated;
                        ((Store.Variable)first).instantiated = stack;
                        stack = first;
                        first = peek;
                        continue;
                    }
                }
            } else if (Store.is_compound(first)) {
                if ((((Store.Compound)first).walk & Store.VAR_MASK_STATE) != gc_mask) {
                    ((Store.Compound)first).walk = (((Store.Compound)first).walk & ~Store.VAR_MASK_STATE) | gc_mask;
                    Object peek = ((Store.Structure)first).args[0];
                    ((Store.Structure)first).args[0] = stack;
                    ((Store.Compound)first).walk &= ~Store.VAR_MASK_SERNO;
                    stack = first;
                    first = peek;
                    continue;
                }
            }
            while (stack != null && (Store.is_variable(stack) ||
                    (((Store.Compound)stack).walk & Store.VAR_MASK_SERNO) ==
                            ((Store.Structure)stack).args.length - 1)) {
                if (Store.is_variable(stack)) {
                    Object peek = ((Store.Variable)stack).instantiated;
                    ((Store.Variable)stack).instantiated = first;
                    first = stack;
                    stack = peek;
                } else {
                    Object peek = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                    ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = first;
                    first = stack;
                    stack = peek;
                }
            }
            if (stack == null) {
                return;
            } else {
                Object peek = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = first;
                ((Store.Compound)stack).walk++;
                first = ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO];
                ((Store.Structure)stack).args[((Store.Compound)stack).walk & Store.VAR_MASK_SERNO] = peek;
            }
        }
    }

    /**
     * Minor mark the continuations.
     */
    private static void mark2_redo() {
        Object term = call;
        Choice last = redo;
        for (;;) {
            mark2_term(term);
            if (last == null)
                break;
            term = last.cont;
            last = last.tail;
        }
    }

    /**************************************************************/
    /* Variable Sweep                                             */
    /**************************************************************/

    /**
     * Adjust the markers into the trail.
     */
    private static void adjust_redo() {
        Choice last = redo;
        while (last != null) {
            Store.Variable temp = last.mark;
            while (temp != null) {
                if ((temp.flags & Store.VAR_MASK_STATE) == gc_mask) {
                    break;
                } else {
                    temp = (Store.Variable)temp.tail;
                }
            }
            last.mark = temp;
            last = last.tail;
        }
    }

    /**
     * Minor mark the trail
     *
     * @param stop The stop.
     */
    private static void mark2_trail(Store.Variable stop) {
        Store.Variable temp = trail;
        while (temp != stop) {
            if ((temp.flags & Store.VAR_MASK_STATE) == Store.VAR_MASK_STATE)
                mark2_term(temp);
            temp = (Store.Variable)temp.tail;
        }
    }

    /**
     * Sweep the trail.
     *
     * @param stop The stop.
     */
    private static void sweep_trail(Store.Variable stop) {
        Store.Variable temp = trail;
        Store.Variable back = null;
        while (temp != stop) {
            Store.Variable term = temp;
            temp = (Store.Variable)term.tail;
            if ((term.flags & Store.VAR_MASK_STATE) == gc_mask) {
                if (back != null) {
                    back.tail = term;
                } else {
                    trail = term;
                }
                back = term;
            } else {
                term.instantiated = Store.UNDEF_OBJ;
                term.tail = null;
            }
        }
        if (back != null) {
            back.tail = stop;
        } else {
            trail = stop;
        }
        Store.engine.backtrail = trail;
    }

    /**************************************************************/
    /* Signal Handling                                            */
    /**************************************************************/

    /**
     * Check the signal message.
     */
    public static Object solve_signal(Object rope, int at, Choice choice) {
        if (Store.engine.signal != Store.UNDEF_OBJ) {
            Object message = Store.engine.signal;
            Store.engine.signal = Store.UNDEF_OBJ;
            throw make_error(message);
        }
        return Boolean.TRUE;
    }

    /**************************************************************/
    /* Clause Loops                                               */
    /**************************************************************/

    public static final int SYS_MASK_ASYNC_MODE = 0x00000001;
    public static final int SYS_MASK_ALLOW_YIELD = 0x00000008;
    public static final int SYS_MASK_FULL_ASYNC =
            SYS_MASK_ASYNC_MODE | SYS_MASK_ALLOW_YIELD;

    /**
     * Set the continuation.
     *
     * @param term The continuation.
     */
    public static void cont(Object term) {
        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.
     */
    public static Object solve(Choice snap, Object found) {
        for (; ; ) {
            if (found == Boolean.TRUE) {
                if (gc_enter >= gc_tick) {
                    if (gc_enter >= gc_tock) {
                        gc_major();
                        gc_tock += 3600*gc_maxinfs;
                    } else if (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(new Choice(Machine::solve_signal, null, 0, trail));
                        return immediate_promise();
                    }
                }
                Object goal = call;
                if (Store.is_structure(goal)) {
                    gc_enter++;
                    goal = ((Store.Structure) goal).args[0];
                    Store.Provable peek = lookup_pred(goal);
                    if (peek == null || (peek.flags & Store.MASK_PRED_ARITH) != 0)
                        throw make_error(new Store.Compound("existence_error",
                                new Object[]{"procedure", make_indicator_term(goal)}));
                    Object[] args;
                    if (Store.is_structure(goal)) {
                        args = ((Store.Structure) goal).args;
                    } else {
                        args = VOID_ARGS;
                    }
                    if ((peek.flags & Store.MASK_PRED_TEST) != 0) {
                        if (!((Handler.Check) peek.func).run(args)) {
                            found = Boolean.FALSE;
                        } else {
                            cont(((Store.Structure) call).args[1]);
                            found = Boolean.TRUE;
                        }
                    } else if ((peek.flags & Store.MASK_PRED_SPECIAL) != 0) {
                        found = ((Handler.Builtin) peek.func).run(args);
                    } else {
                        Store.Logical rope = Store.defined_pred(peek, args);
                        found = solve2_rope(args, Store.snapshot_rope(rope), 0, null);
                    }
                } else {
                    break;
                }
            } else if (found == Boolean.FALSE) {
                if (redo != snap) {
                    Choice choice = redo;
                    redo = choice.tail;
                    unbind(choice.mark);
                    call = choice.cont;
                    found = choice.func.run(choice.data, choice.at, choice);
                } else {
                    break;
                }
            } else {
                break;
            }
        }
        return found;
    }

    private static Handler.Promise immediate_promise() {
        return new Handler.Promise(() -> {
            try {
                Thread.sleep(0);
            } catch (InterruptedException x) {
                throw make_error(new Store.Compound("resource_error",
                        new Object[]{"interrupted_exception"}));
            }
        });
    }

    /******************************************************************/
    /* Linked Provables                                               */
    /******************************************************************/

    /**
     * Lookup a predicate.
     *
     * @param goal The goal.
     * @return Provable The predicate or null.
     */
    public static Store.Provable lookup_pred(Object goal) {
        Object functor;
        int arity;
        if (Store.is_element(goal)) {
            functor = ((Store.Element) goal).functor;
            arity = ((Store.Element) goal).args.length;
        } else {
            functor = goal;
            arity = 0;
        }
        return Store.resolve_link(functor, arity);
    }

    /**
     * Lookup an evaluable function.
     *
     * @param expr The arithmetic expression.
     * @return Provable The evaluable function or null.
     */
    private static Store.Provable lookup_eval(Object expr) {
        Object functor;
        int arity;
        if (Store.is_element(expr)) {
            functor = ((Store.Element) expr).functor;
            arity = ((Store.Element) expr).args.length;
        } else {
            functor = expr;
            arity = 0;
        }
        return Store.resolve_link(functor, arity + 1);
    }

    public static Object make_indicator_term(Object goal) {
        Object functor;
        int arity;
        if (Store.is_structure(goal)) {
            Store.Structure cmp = (Store.Structure) goal;
            functor = cmp.functor;
            arity = cmp.args.length;
        } else {
            functor = goal;
            arity = 0;
        }
        return make_indicator(functor, arity);
    }

    private static Object solve_rope(Object rope, int at, Choice choice) {
        Object[] args;
        Object goal = Store.deref(((Store.Structure) call).args[0]);
        if (Store.is_structure(goal)) {
            args = ((Store.Structure) goal).args;
        } else {
            args = VOID_ARGS;
        }
        return solve2_rope(args, rope, at, choice);
    }

    /**
     * Search a Prolog clause and add it to the continuation.
     *
     * @param paras   The called goal.
     * @param data   The clause list.
     * @param at     The clause index.
     * @param choice The choice point for reuse or null.
     * @return boolean True if search succeeds, otherwise false.
     */
    static Object solve2_rope(Object[] paras, Object data, int at, Choice choice) {
        Store.Variable mark = trail;
        Store.Clause[] rope = (Store.Clause[]) data;
        while (at < rope.length) {
            Store.Clause clause = rope[at++];
            Object[] display;
            if (clause.size != 0) {
                display = new Object[clause.size];
            } else {
                display = null;
            }
            if (exec_head(clause.head, display, paras)) {
                int peek = clause.cutvar;
                if (peek != -1)
                    display[peek] = redo;
                if (at < rope.length) {
                    if (choice == null) {
                        choice = new Choice(Machine::solve_rope, rope, at, mark);
                    } else {
                        choice.at = at;
                    }
                    more(choice);
                    if (exec_check(clause.body, display))
                        return Boolean.TRUE;
                    if (redo != choice)
                        return Boolean.FALSE;
                    more(choice.tail);
                } else {
                    return Boolean.valueOf(exec_check(clause.body, display));
                }
            }
            unbind(mark);
        }
        return Boolean.FALSE;
    }

    /**
     * Sets the choice point.
     *
     * @param choice The new choice point.
     */
    public static void more(Choice choice) {
        redo = choice;
    }

    public static final class Choice {
        public Handler.Callback func;
        public Object data;
        public int at;
        public Store.Variable mark;
        public Object cont;
        public Choice tail;

        /**
         * 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.
         */
        public Choice(Handler.Callback func, Object data, int at, Store.Variable mark) {
            this.func = func;
            this.data = data;
            this.at = at;
            this.mark = mark;
            this.cont = call;
            this.tail = redo;
        }

    }

    /**************************************************************/
    /* Directives                                                 */
    /**************************************************************/

    public static final String 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.
     */
    public static void run(Store.Goal goal) {
        if (!launch(goal, CTX_MAIN, VOID_ARGS))
            throw make_error(new Store.Compound("syntax_error",
                    new Object[]{"directive_failed"}));
    }

    public static Choice snap_setup() {
        redo = new Choice(Machine::solve_setup, null, 0, trail);
        return redo;
    }

    static Object solve_setup(Object rope, int at, Choice choice) {
        return Boolean.FALSE;
    }

    public static void snap_cleanup(Choice snap) {
        more(snap.tail);
        unbind(snap.mark);
        call = snap.cont;
    }

    /**************************************************************/
    /* Terms                                                      */
    /**************************************************************/

    /**
     * Check whether an object is an atom.
     *
     * @param obj The object.
     * @return boolean True if the object is an atom, otherwise false.
     */
    public static boolean is_atom(Object obj) {
        return obj instanceof String;
    }

    /**
     * Check whether an object is a number.
     *
     * @param obj The object.
     * @return boolean True if the object is a number, otherwise false.
     */
    public static boolean is_number(Object obj) {
        return obj instanceof Number;
    }

    /**
     * Check whether an object is an integer.
     *
     * @param obj The object.
     * @return boolean True if the object is an integer, otherwise false.
     */
    public static boolean is_integer(Object obj) {
        return (obj instanceof Integer) || (obj instanceof BigInteger);
    }

    /**
     * Check whether an object is a float.
     *
     * @param obj The object.
     * @return boolean True if the object is a float, otherwise false.
     */
    public static boolean is_float(Object obj) {
        return obj instanceof Double;
    }

    /**
     * Check whether an object is a bigint.
     *
     * @param alpha The object.
     * @return boolean True if the object is a bignum, otherwise false.
     */
    public static boolean is_bigint(Object alpha) {
        return alpha instanceof BigInteger;
    }

    /**
     * Check whether an object is a special value.
     *
     * @param alpha The object.
     * @return boolean True if the object is a special value, otherwise false.
     */
    public static boolean is_special(Object alpha) {
        return (alpha instanceof Double &&
                !Double.isFinite(((Double)alpha).doubleValue()));
    }

    /**************************************************************/
    /* Albufeira Lazy                                             */
    /**************************************************************/

    public static Object[] temp_display;

    private static Object flip(Object value) {
        if (value == null) return Store.UNDEF_OBJ;
        if (value == Store.UNDEF_OBJ) return null;
        return value;
    }

    public static boolean is_pending(Object template) {
        if (template == Store.UNDEF_OBJ) {
            return true;
        } else if (Store.is_place(template)) {
            return true;
        } else {
            return false;
        }
    }

    public static Object exec_deref(Object template) {
        if (template == Store.UNDEF_OBJ) {
            return template;
        } else if (Store.is_place(template)) {
            int index = ((Store.Place) template).index;
            Object peek = flip(temp_display[index]);
            if (peek == Store.UNDEF_OBJ) {
                return template;
            } else {
                return Store.deref(peek);
            }
        } else {
            return Store.deref(template);
        }
    }

    /**************************************************************/
    /* Albufeira Modes                                            */
    /**************************************************************/

    public static Object exec_build(Object template) {
        Store.Structure back = null;
        for (; ; ) {
            if (template == Store.UNDEF_OBJ) {
                template = new Store.Variable();
                break;
            } else if (Store.is_place(template)) {
                int index = ((Store.Place) template).index;
                template = flip(temp_display[index]);
                if (template == Store.UNDEF_OBJ) {
                    template = new Store.Variable();
                    temp_display[index] = template;
                } else {
                    template = Store.deref(template);
                }
                break;
            } else if (Store.is_skeleton(template)) {
                Object[] args = new Object[((Store.Skeleton) template).args.length];
                args[args.length - 1] = back;
                back = new Store.Compound(((Store.Skeleton) template).functor, args);
                template = ((Store.Skeleton) template).args;
                int i = 0;
                for (; i < args.length - 1; i++)
                    args[i] = exec_build(((Object[])template)[i]);
                template = ((Object[])template)[i];
            } else {
                template = Store.deref(template);
                break;
            }
        }
        while (back != null) {
            Object peek = back.args[back.args.length - 1];
            back.args[back.args.length - 1] = template;
            template = back;
            back = (Store.Structure) peek;
        }
        return template;
    }

    public static boolean exec_unify(Object template, Object alpha) {
        for (; ; ) {
            if (template == Store.UNDEF_OBJ) {
                return true;
            } else if (Store.is_place(template)) {
                int index = ((Store.Place) template).index;
                template = flip(temp_display[index]);
                if (template == Store.UNDEF_OBJ) {
                    temp_display[index] = flip(Store.deref(alpha));
                    return true;
                } else {
                    return unify(alpha, template);
                }
            } else if (Store.is_skeleton(template)) {
                alpha = Store.deref(alpha);
                if (Store.is_variable(alpha)) {
                    Object[] args = new Object[((Store.Skeleton) template).args.length];
                    bind(new Store.Compound(((Store.Skeleton) template).functor, args), (Store.Variable) alpha);
                    template = ((Store.Skeleton) template).args;
                    for (int i = 0; i < args.length; i++)
                        args[i] = exec_build(((Object[])template)[i]);
                    return true;
                } else if (Store.is_structure(alpha)) {
                    if (((Store.Skeleton) template).args.length !=
                            ((Store.Structure) alpha).args.length)
                        return false;
                    if (!((Store.Skeleton) template).functor.equals(
                            ((Store.Structure) alpha).functor))
                        return false;
                    template = ((Store.Skeleton) template).args;
                    alpha = ((Store.Structure) alpha).args;
                    int i = 0;
                    for (; i < ((Object[])template).length - 1; i++)
                        if (!exec_unify(((Object[])template)[i], ((Object[])alpha)[i]))
                            return false;
                    template = ((Object[])template)[i];
                    alpha = ((Object[])alpha)[i];
                } else {
                    return false;
                }
            } else {
                return unify(template, alpha);
            }
        }
    }

    /**************************************************************/
    /* Albufeira Clauses                                          */
    /**************************************************************/

    public static Object exec_body(Object[] code, Object[] display) {
        temp_display = display;
        Store.Structure back = null;
        Object res = null;
        for (int i = 0; i < code.length; i++) {
            Object goal = exec_build(code[i]);
            Store.Structure temp = new Store.Compound(".", new Object[]{goal, Store.UNDEF_OBJ});
            if (back == null) {
                res = temp;
            } else {
                back.args[1] = temp;
            }
            back = temp;
        }
        if (back == null) {
            res = "[]";
        } else {
            back.args[1] = "[]";
        }
        temp_display = null;
        return res;
    }

    public static boolean exec_head(Object[] code, Object[] display,
                             Object[] aux) {
        if (aux.length != code.length)
            return false;
        temp_display = display;
        for (int i = 0; i < code.length; i++) {
            if (!exec_unify(code[i], aux[i])) {
                temp_display = null;
                return false;
            }
        }
        temp_display = null;
        return true;
    }

    /**************************************************************/
    /* Head Check                                                 */
    /**************************************************************/

    public static Number exec_eval(Object template) {
        if (template == Store.UNDEF_OBJ) {
            throw make_error("instantiation_error");
        } else if (Store.is_place(template)) {
            int index = ((Store.Place) template).index;
            template = flip(temp_display[index]);
            if (template == Store.UNDEF_OBJ)
                throw make_error("instantiation_error");
        }
        template = Store.deref(template);
        if (is_number(template))
            return (Number) template;
        Store.Provable peek = lookup_eval(template);
        if (peek == null || (peek.flags & Store.MASK_PRED_ARITH) == 0)
            throw make_error(new Store.Compound("type_error",
                    new Object[]{"evaluable", make_indicator_term(template)}));
        Object[] args;
        if (Store.is_element(template)) {
            args = ((Store.Element) template).args;
        } else {
            args = VOID_ARGS;
        }
        return ((Handler.Funktion) peek.func).eval(args);
    }

    private static Object exec_test(Object template) {
        Store.Provable peek = lookup_pred(template);
        if (peek == null || (peek.flags & Store.MASK_PRED_TEST) == 0) {
            return exec_build(template);
        } else {
            Object[] args;
            if (Store.is_element(template)) {
                args = ((Store.Element) template).args;
            } else {
                args = VOID_ARGS;
            }
            gc_enter++;
            return Boolean.valueOf(((Handler.Check) peek.func).run(args));
        }
    }

    private static boolean exec_check(Object[] code, Object[] display) {
        temp_display = display;
        boolean check = true;
        Store.Compound back = null;
        Object res = null;
        for (int i = 0; i < code.length; i++) {
            Object goal = (check ? exec_test(code[i]) : exec_build(code[i]));
            if (goal == Boolean.TRUE)
                continue;
            if (goal == Boolean.FALSE) {
                temp_display = null;
                return false;
            }
            goal = new Store.Compound(".", new Object[]{goal, Store.UNDEF_OBJ});
            if (back == null) {
                res = goal;
            } else {
                back.args[1] = goal;
            }
            back = (Store.Compound)goal;
            check = false;
        }
        if (back == null) {
            res = ((Store.Structure) call).args[1];
        } else {
            back.args[1] = ((Store.Structure) call).args[1];
        }
        temp_display = null;
        cont(res);
        return true;
    }

    /**************************************************************/
    /* 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 boolean True if the two terms unify, otherwise false.
     */
    public static boolean unify(Object first, Object second) {
        List stack = null;
        List log = null;
        try {
            for (; ; ) {
                first = Store.deref(first);
                second = Store.deref(second);
                if (Store.is_variable(first)) {
                    if (!Store.is_variable(second) || first != second)
                        bind(second, (Store.Variable) first);
                } else if (Store.is_variable(second)) {
                    bind(first, (Store.Variable) second);
                } else if (!Store.is_structure(first)) {
                    if (!Objects.equals(first, second))
                        break;
                } else if (!Store.is_structure(second)) {
                    break;
                } else if (((Store.Structure) first).args.length !=
                        ((Store.Structure) second).args.length) {
                    break;
                } else {
                    first = Machine.union_find((Store.Structure) first);
                    second = Machine.union_find((Store.Structure) second);
                    if (first != second) {
                        if (is_frozen(first) && is_frozen(second) &&
                                ((Frozen)first).hash != ((Frozen)second).hash)
                            break;
                        if (!((Store.Structure) first).functor.equals(
                                ((Store.Structure) second).functor))
                            break;
                        log = Machine.union_add(log, (Store.Structure) first,
                                (Store.Structure) second);
                        if (0 != ((Store.Structure) first).args.length - 1) {
                            Store.Item item2 = new Store.Item((Store.Structure)first, second, 0);
                            stack = Store.stack_push(stack, item2);
                        }
                        first = ((Store.Structure) first).args[0];
                        second = ((Store.Structure) second).args[0];
                        continue;
                    }
                }
                Store.Item item = (Store.Item)Store.stack_peek(stack);
                if (item == null) {
                    return true;
                } else {
                    item.idx++;
                    first = item.first.args[item.idx];
                    second = ((Store.Structure)item.second).args[item.idx];
                    if (item.idx == item.first.args.length - 1)
                        Store.stack_pop(stack);
                }
            }
            return false;
        } finally {
            Machine.union_undo(log);
        }
    }

    /**
     * The function returns the representative of a structure.
     *
     * @param obj The structure.
     * @return The representative.
     */
    public static Store.Structure union_find(Store.Structure obj) {
        while (Store.is_structure(obj.functor))
            obj = (Store.Structure)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.
     */
    public static List union_add(List log, Store.Structure from,
                                 Store.Structure to) {
        from.functor = to;
        if (log == null)
            log = new ArrayList();
        log.add(from);
        return log;
    }

    /**
     * The routine uses the log L to undo modifications.
     *
     * @param log The log.
     */
    public static void union_undo(List log) {
        if (log == null)
            return;
        for (int i = log.size() - 1; i >= 0; i--) {
            Store.Structure elem = (Store.Structure)log.get(i);
            elem.functor = ((Store.Structure)elem.functor).functor;
        }
    }

    /**
     * Bind a variable to a term.
     *
     * @param source The Prolog term.
     * @param term   The variable.
     */
    public static void bind(Object source, Store.Variable term) {
        term.instantiated = source;
        term.tail = trail;
        if ((term.flags & Store.VAR_MASK_STATE) == gc_mask)
            term.flags |= Store.VAR_MASK_STATE;
        trail = term;
    }

    /**
     * Unbind variable binds.
     *
     * @param mark The trail mark.
     */
    public static void unbind(Store.Variable mark) {
        while (mark != trail) {
            Store.Variable term = trail;
            if (Store.engine.backtrail == term)
                Store.engine.backtrail = (Store.Variable)term.tail;
            trail = (Store.Variable)term.tail;
            term.instantiated = Store.UNDEF_OBJ;
            term.tail = null;
        }
    }

    /**************************************************************/
    /* Context                                                    */
    /**************************************************************/

    public static final ArrayList tasks = new ArrayList();

    public static final class Context {
        public Store.Variable trail;
        public Choice redo;
        public Object call;
        public int gc_mask;
        public Store.Engine engine;

        public Context() {
            this.trail = null;
            this.redo = null;
            this.call = "[]";
            this.gc_mask = Store.VAR_MASK_ODD;
            this.engine = new Store.Engine();
            this.engine.text_output = Store.engine.text_output;
            this.engine.text_error = Store.engine.text_error;
            this.engine.text_input = Store.engine.text_input;
            tasks.add(this);
        }

    }

    private static void ctx_ended(Context buf) {
        int k = tasks.lastIndexOf(buf);
        if (k != -1)
            tasks.remove(k);
    }

    /**************************************************************/
    /* Group                                                      */
    /**************************************************************/

    public static void group_teardown() {
        for (int i = 0; i < tasks.size(); i++) {
            Context buf = (Context)tasks.get(i);
            Object msg = new Store.Compound("system_error", new Object[]{"user_exit"});
            register_signal(buf, msg);
            invoke_interrupt(buf);
        }
    }

    /**************************************************************/
    /* Switching                                                  */
    /**************************************************************/

    public static Object ctx = CTX_MAIN;

    /**
     * Set the task context.
     *
     * @param buf The context.
     */
    public static void ctx_set(Object buf) {
        ctx = buf;
    }

    /**
     * Switch the task context.
     *
     * @param buf The context.
     */
    public static void ctx_switch(Context buf) {
        Store.Variable vtemp = trail;
        trail = buf.trail;
        buf.trail = vtemp;
        Choice ctemp = redo;
        redo = buf.redo;
        buf.redo = ctemp;
        Object otemp = call;
        call = buf.call;
        buf.call = otemp;
        int itemp = gc_mask;
        gc_mask = buf.gc_mask;
        buf.gc_mask = itemp;
        Store.Engine etemp = Store.engine;
        Store.set_engine(buf.engine);
        buf.engine = etemp;
    }

    /**************************************************************/
    /* 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.
     */
    public static boolean launch(Object form, Object buf, Object[] paras) {
        if (!CTX_MAIN.equals(buf)) {
            ctx_set(buf);
            ctx_switch((Context) buf);
        }
        int back = Store.engine.flags & SYS_MASK_FULL_ASYNC;
        Store.engine.flags &= ~SYS_MASK_FULL_ASYNC;
        Choice snap = snap_setup();
        if (Store.is_clause(form)) {
            call = melt_clause((Store.Clause) form, paras);
        } else if (Store.is_goal(form)) {
            call = melt_directive((Store.Goal) form);
        } else {
            call = form;
        }
        Object found;
        try {
            found = solve(snap, Boolean.TRUE);
        } finally {
            snap_cleanup(snap);
            Store.engine.flags &= ~SYS_MASK_FULL_ASYNC;
            Store.engine.flags |= back;
            if (!CTX_MAIN.equals(buf)) {
                ctx_switch((Context) buf);
                ctx_set(CTX_MAIN);
            }
        }
        return ((Boolean)found).booleanValue();
    }

    public static boolean callback(Object form, Object buf, Object[] paras) {
        try {
            return launch(form, buf, paras);
        } catch (Throwable err) {
            return false;
        }
    }

    public static Object melt_directive(Store.Goal goal) {
        Object[] display;
        if (goal.size != 0) {
            display = new Object[goal.size];
        } else {
            display = null;
        }
        int peek = goal.cutvar;
        if (peek != -1)
            display[peek] = redo;
        return exec_body(goal.body, display);
    }

    public static Object melt_clause(Store.Clause clause, Object[] paras) {
        Object[] display;
        if (clause.size != 0) {
            display = new Object[clause.size];
        } else {
            display = null;
        }
        if (exec_head(clause.head, display, paras)) {
            int 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.
     */
    public static boolean launch_async(Object form, Object buf, Object[] paras) {
        gc_last += real_time();
        if (!CTX_MAIN.equals(buf)) {
            ctx_set(buf);
            ctx_switch((Context) buf);
        }
        int back = Store.engine.flags & SYS_MASK_FULL_ASYNC;
        Store.engine.flags |= SYS_MASK_FULL_ASYNC;
        Object found = Boolean.TRUE;
        Choice snap = snap_setup();
        if (Store.is_clause(form)) {
            call = melt_clause((Store.Clause) form, paras);
        } else if (Store.is_goal(form)) {
            call = melt_directive((Store.Goal) form);
        } else {
            call = form;
        }
        try {
            for (; ; ) {
                found = solve(snap, found);
                if (found == Boolean.FALSE) {
                    break;
                } else if (found != Boolean.TRUE) {
                    if (!CTX_MAIN.equals(buf)) {
                        ctx_switch((Context) buf);
                        ctx_set(CTX_MAIN);
                    }
                    gc_last -= real_time();
                    ((Handler.Promise) found).await();
                    gc_last += real_time();
                    if (!CTX_MAIN.equals(buf)) {
                        ctx_set(buf);
                        ctx_switch((Context) buf);
                    }
                    found = Boolean.FALSE;
                } else {
                    break;
                }
            }
        } finally {
            snap_cleanup(snap);
            Store.engine.flags &= ~SYS_MASK_FULL_ASYNC;
            Store.engine.flags |= back;
            if (!CTX_MAIN.equals(buf)) {
                ctx_switch((Context) buf);
                ctx_set(CTX_MAIN);
                ctx_ended((Context) buf);
            }
        }
        gc_last -= real_time();
        return ((Boolean)found).booleanValue();
    }

    public static void task_async(Object form, Object buf, Object[] paras) {
        try {
            launch_async(form, buf, paras);
        } catch (Throwable err) {
            /* */
        }
    }

    /**
     * Register an interrupt function in a context.
     *
     * @param buf  The context.
     * @param func The function.
     */
    public static void register_interrupt(Object buf, Runnable func) {
        Store.Engine en = determine_engine(buf);
        en.abort = func;
    }

    /**
     * Register a signal in a context.
     *
     * @param buf     The context.
     * @param msg The signal.
     */
    public static void register_signal(Object buf, Object msg) {
        Store.Engine en = determine_engine(buf);
        en.signal = msg;
    }

    /**
     * Invoke the interrupt handler of a context.
     *
     * @param buf     The context.
     */
    public static void invoke_interrupt(Object buf) {
        Store.Engine en = determine_engine(buf);
        en.abort.run();
    }

    private static Store.Engine determine_engine(Object buf) {
        if (!CTX_MAIN.equals(buf)) {
            if (!buf.equals(ctx)) {
                return ((Context) buf).engine;
            } else {
                return Store.engine;
            }
        } else {
            if (!CTX_MAIN.equals(ctx)) {
                return ((Context) ctx).engine;
            } else {
                return Store.engine;
            }
        }
    }

}