package foreign;

import nova.*;

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 fastlib {

    /******************************************************************/
    /* unify_with_occurs_check/2 and occurs_check/2                   */
    /******************************************************************/

    /**
     * unify_with_occurs_check(S, T): [ISO 8.2.2]
     * The built-in succeeds when the Prolog terms S and T unify
     * with occurs check, otherwise the built-in fails.
     */
    private static boolean test_unify_checked(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        Object beta = Machine.exec_build(args[1]);
        return unify_checked(alpha, beta);
    }

    /**
     * Determine whether two terms unify with occurs check.
     * As a side effect the trail is extended, even if unification fails.
     * Can handle cyclic terms.
     *
     * @param first  The first term.
     * @param second The second term.
     * @return boolean True if the two terms unify, otherwise false.
     */
    private static boolean unify_checked(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) {
                        if (has_var((Store.Variable) first, second))
                            break;
                        Machine.bind(second, (Store.Variable) first);
                    }
                } else if (Store.is_variable(second)) {
                    if (has_var((Store.Variable) second, first))
                        break;
                    Machine.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 (!((Store.Structure) first).functor.equals(
                            ((Store.Structure) second).functor)) {
                        break;
                    } else if (first != second) {
                        log = Machine.union_add(log, (Store.Structure) first,
                                (Store.Structure) second);
                        if (0 != ((Store.Structure) first).args.length - 1) {
                            Machine.Item item = new Machine.Item((Store.Structure)first, second, 0);
                            stack = Store.stack_push(stack, item);
                        }
                        first = ((Store.Structure) first).args[0];
                        second = ((Store.Structure) second).args[0];
                        continue;
                    }
                }
                Machine.Item item = (Machine.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);
        }
    }

    /**
     * occurs_check(S, T): [ISO 7.3.3]
     * The built-in succeeds when the Prolog variable S occurs
     * in the Prolog term T, otherwise the built-in fails.
     */
    private static boolean test_has_var(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        Object beta = Machine.exec_build(args[1]);
        return Store.is_variable(alpha) && has_var((Store.Variable)alpha, beta);
    }

    /**
     * Check whether a variable occurs in a term.
     * Can handle cyclic terms and deep recursion.
     *
     * @param vterm The Prolog variable.
     * @param first The Prolog term.
     * @return boolean True if vterm occurs in first, otherwise false.
     */
    private static boolean has_var(Store.Variable vterm, Object first) {
        has_var2 h = new has_var2(vterm);
        boolean res = special.walk_vars(first, h, Store.VAR_MASK_SEEN);
        special.walk_vars(first, h, 0);
        return res;
    }

    private static class has_var2 implements Handler.Acceptor {
        private final Store.Variable vterm;

        private has_var2(Store.Variable vterm)  {
            this.vterm = vterm;
        }

        public boolean run(Object node) {
            return (node == vterm);
        }

    }

    /******************************************************************/
    /* subsumes/2                                                     */
    /******************************************************************/

    /**
     * subsumes(X, Y): [N208 8.2.4]
     * The built-in succeeds if X subsumes Y.
     */
    private static boolean test_subsumes(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        Object beta = Machine.exec_build(args[1]);
        return subsumes(beta, alpha, beta);
    }

    /**
     * Determine whether two terms single side unify.
     * As a side effect the trail is extended, even if unification fails.
     * Tail recursive solution.
     *
     * @param root   The root of the second term.
     * @param first  The first term.
     * @param second The second term.
     * @return boolean True if the two terms single side unify, otherwise false.
     */
    private static boolean subsumes(Object root, Object first, Object second) {
        for (; ; ) {
            first = Store.deref(first);
            second = Store.deref(second);
            if (Store.is_variable(first)) {
                if (Store.is_variable(second) && first == second)
                    return true;
                if (has_var((Store.Variable) first, root))
                    return false;
                Machine.bind(second, (Store.Variable) first);
                return true;
            }
            if (Store.is_variable(second))
                return false;
            if (!Store.is_structure(first))
                return Objects.equals(first, second);
            if (!Store.is_structure(second))
                return false;
            Object[] t1 = ((Store.Structure) first).args;
            Object[] t2 = ((Store.Structure) second).args;
            if (t1.length != t2.length)
                return false;
            if (!((Store.Structure) first).functor.equals(((Store.Structure) second).functor))
                return false;
            int i = 0;
            for (; i < t1.length - 1; i++) {
                if (!subsumes(root, t1[i], t2[i]))
                    return false;
            }
            first = t1[i];
            second = t2[i];
        }
    }

    /******************************************************************/
    /* term_singletons/2                                              */
    /******************************************************************/

    /**
     * term_singletons(T, L):
     * The built-in succeeds in L with the singleton variables of T.
     */
    private static boolean test_term_singletons(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        alpha = walk_singletons(alpha);
        Iterator it = ((Map)alpha).entrySet().iterator();
        while (it.hasNext()) {
            Map.Entry entry = (Map.Entry)it.next();
            if (((Boolean)entry.getValue()).booleanValue())
                it.remove();
        }
        alpha = theatre.set_to_list(((Map)alpha).keySet());
        return Machine.exec_unify(args[1], alpha);
    }

    /**
     * Walk a Prolog term completely.
     *
     * @param first The Prolog term.
     * @return The singletons.
     */
    private static Object walk_singletons(Object first) {
        List stack = null;
        Map map = null;
        for (; ; ) {
            first = Store.deref(first);
            if (Store.is_variable(first)) {
                first = Collections.singletonMap(first, Boolean.FALSE);
            } else if (Store.is_compound(first)) {
                Object peek = Store.assoc_get(map, first);
                if (peek == null) {
                    map = Store.assoc_set(map, first, EMPTY_MAP);
                    Machine.Item item = new Machine.Item((Store.Structure)first, EMPTY_MAP, 0);
                    stack = Store.stack_push(stack, item);
                    first = ((Store.Structure) first).args[0];
                    continue;
                } else {
                    first = peek;
                }
            } else {
                first = EMPTY_MAP;
            }
            Machine.Item item = (Machine.Item)Store.stack_peek(stack);
            while (item != null &&
                    item.idx  == item.first.args.length - 1) {
                first = union_map((Map)item.second, (Map)first);
                map = Store.assoc_set(map, item.first, first);
                Store.stack_pop(stack);
                item = (Machine.Item)Store.stack_peek(stack);
            }
            if (item == null) {
                return first;
            } else {
                item.second = union_map((Map)item.second, (Map)first);
                item.idx++;
                first = item.first.args[item.idx];
            }
        }
    }

    private static final Map EMPTY_MAP = new LinkedHashMap();

    private static Map union_map(Map first, Map second) {
        if (first.size() == 0)
            return second;
        if (second.size() == 0)
            return first;
        first = new LinkedHashMap(first);
        Iterator it = second.entrySet().iterator();
        while (it.hasNext()) {
            Map.Entry entry = (Map.Entry)it.next();
            Object value = first.get(entry.getKey());
            if (value != null) {
                value = Boolean.TRUE;
            } else {
                value = entry.getValue();
            }
            first.put(entry.getKey(), value);
        }
        return first;
    }

    /******************************************************************/
    /* ground/1 and nonground/2                                       */
    /******************************************************************/

    /**
     * ground(T): [TC2 8.3.10]
     * The built-in succceeds if T is ground.
     */
    private static boolean test_ground(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        boolean res = special.walk_vars(alpha, node -> true, Store.VAR_MASK_SEEN);
        special.walk_vars(alpha, node -> true, 0);
        return !res;
    }

    /**
     * nonground(T, V):
     * The built-in succeeds if T is non-ground and V is the first variable.
     */
    private static boolean test_nonground(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        nonground2 h = new nonground2();
        boolean res = special.walk_vars(alpha, h, Store.VAR_MASK_SEEN);
        special.walk_vars(alpha, node -> true, 0);
        return res && Machine.exec_unify(args[1], h.hit);
    }

    private static class nonground2 implements Handler.Acceptor {
        private Object hit = null;

        public boolean run(Object node) {
            hit = node;
            return true;
        }

    }

    /******************************************************************/
    /* term_hash/2                                                    */
    /******************************************************************/

    /**
     * term_hash(X, H):
     * The predicate succeeds in H with the term hash of the term X.
     */
    private static boolean test_term_hash(Object[] args) {
        Object alpha = Machine.exec_build(args[0]);
        alpha = walk_hash(alpha);
        return Machine.exec_unify(args[1], alpha);
    }

    /**
     * Walk a Prolog term completely.
     *
     * @param first The Prolog term.
     * @return The hash.
     */
    private static Object walk_hash(Object first) {
        List stack = null;
        Map map = null;
        for (; ; ) {
            first = Store.deref(first);
            if (Store.is_structure(first)) {
                Object peek = Store.assoc_get(map, first);
                if (peek == null) {
                    map = Store.assoc_set(map, first, Integer.valueOf(0));
                    peek = eval.object_hash_code(((Store.Structure) first).functor);
                    Machine.Item item = new Machine.Item((Store.Structure)first, peek, 0);
                    stack = Store.stack_push(stack, item);
                    first = ((Store.Structure) first).args[0];
                    continue;
                } else {
                    first = peek;
                }
            } else {
                first = eval.object_hash_code(first);
            }
            Machine.Item item = (Machine.Item)Store.stack_peek(stack);
            while (item != null &&
                    item.idx  == item.first.args.length - 1) {
                first = Integer.valueOf(((Integer)item.second).intValue() * 31 + ((Integer)first).intValue());
                map = Store.assoc_set(map, item.first, first);
                Store.stack_pop(stack);
                item = (Machine.Item)Store.stack_peek(stack);
            }
            if (item == null) {
                return first;
            } else {
                item.second = Integer.valueOf(((Integer)item.second).intValue() * 31 + ((Integer)first).intValue());
                item.idx++;
                first = item.first.args[item.idx];
            }
        }
    }

    /******************************************************************/
    /* Fast Lib Init                                                  */
    /******************************************************************/

    public static void main() {
        Store.add("unify_with_occurs_check", 2, special.make_check(fastlib::test_unify_checked));
        Store.add("occurs_check", 2, special.make_check(fastlib::test_has_var));
        Store.add("subsumes", 2, special.make_check(fastlib::test_subsumes));
        Store.add("term_singletons", 2, special.make_check(fastlib::test_term_singletons));
        Store.add("ground", 1, special.make_check(fastlib::test_ground));
        Store.add("nonground", 2, special.make_check(fastlib::test_nonground));
        Store.add("term_hash", 2, special.make_check(fastlib::test_term_hash));
    }

}
