/**
 * 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 {
    exec_build, Item, is_variable, Compound, exec_unify,
    is_structure, add, bind, deref, set_to_list,
    union_add, union_find, union_undo, VAR_MASK_SEEN,
    stack_peek, stack_pop, stack_push, walk_vars,
    make_check, assoc_get, assoc_set, is_compound,
    norm_smallint, object_hash_code, check_integer,
    is_integer, Variable
} from "../nova/core.mjs";

/*********************************************************************/
/* unify_with_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.
 */
function test_unify_checked(args) {
    let alpha = exec_build(args[0]);
    let beta = exec_build(args[1]);
    return unify_checked(alpha, beta);
}

/**
 * Determine whether two terms unify with occurs check.
 * As a side effect the trail is extended, even if unification fails.
 * Can handle cyclic terms and deep recursion.
 *
 * @param first The first term.
 * @param second The second term.
 * @return boolean True if the two terms unify, otherwise false.
 */
function unify_checked(first, second) {
    let stack = null;
    let log = null;
    try {
        for (; ;) {
            first = deref(first);
            second = deref(second);
            if (is_variable(first)) {
                if (!is_variable(second) || first !== second) {
                    if (has_var(first, second))
                        break;
                    bind(second, first);
                }
            } else if (is_variable(second)) {
                if (has_var(second, first))
                    break;
                bind(first, second);
            } else if (!is_structure(first)) {
                if (first !== second)
                    break;
            } else if (!is_structure(second)) {
                break;
            } else if (first.args.length !== second.args.length) {
                break;
            } else {
                first = union_find(first);
                second = union_find(second);
                if (first.functor !== second.functor) {
                    break;
                } else if (first !== second) {
                    log = union_add(log, first, second);
                    if (0 !== first.args.length - 1) {
                        let item = new Item(first, second, 0);
                        stack = stack_push(stack, item);
                    }
                    first = first.args[0];
                    second = second.args[0];
                    continue;
                }
            }
            let item = stack_peek(stack);
            if (item === null) {
                return true;
            } else {
                item.idx++;
                first = item.first.args[item.idx];
                second = item.second.args[item.idx];
                if (item.idx === item.first.args.length - 1)
                    stack_pop(stack);
            }
        }
        return false;
    } finally {
        union_undo(log);
    }
}

/**
 * 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.
 */
function has_var(vterm, first) {

    function has_var2(node) {
        return (node === vterm);
    }

    let res = walk_vars(first, has_var2, VAR_MASK_SEEN);
    walk_vars(first, has_var2, 0);
    return res;
}

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

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

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

    function subsumes2(first2, second2) {
        for (; ;) {
            first2 = deref(first2);
            second2 = deref(second2);
            if (is_variable(first2)) {
                if (is_variable(second2) && first2 === second2)
                    return true;
                if (has_var(first2, second))
                    return false;
                bind(second2, first2);
                return true;
            }
            if (is_variable(second2))
                return false;
            if (!is_structure(first2))
                return (first2 === second2);
            if (!is_structure(second2))
                return false;
            if (first2.args.length !== second2.args.length)
                return false;
            if (first2.functor !== second2.functor)
                return false;
            first2 = first2.args;
            second2 = second2.args;
            let i = 0;
            for (; i < first2.length - 1; i++) {
                if (!subsumes2(first2[i], second2[i]))
                    return false;
            }
            first2 = first2[i];
            second2 = second2[i];
        }
    }

    return subsumes2(first, second);
}

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

/**
 * term_singletons(T, L):
 * The built-in succeeds in L with the singleton variables of T.
 */
function test_term_singletons(args) {
    let alpha = exec_build(args[0]);
    alpha = walk_singletons(alpha);
    for (let [key, val] of alpha) {
        if (val)
            alpha.delete(key);
    }
    alpha = set_to_list(alpha.keys());
    return exec_unify(args[1], alpha);
}

/**
 * Walk a Prolog term completely.
 *
 * @param first The Prolog term.
 * @return The singletons.
 */
function walk_singletons(first) {
    let stack = null;
    let map = null;
    for (; ; ) {
        first = deref(first);
        if (is_variable(first)) {
            first = new Map([[first, false]]);
        } else if (is_compound(first)) {
            let peek = assoc_get(map, first);
            if (peek === undefined) {
                map = assoc_set(map, first, EMPTY_MAP);
                let item = new Item(first, EMPTY_MAP, 0);
                stack = stack_push(stack, item);
                first = first.args[0];
                continue;
            } else {
                first = peek;
            }
        } else {
            first = EMPTY_MAP;
        }
        let item = stack_peek(stack);
        while (item !== null &&
                item.idx  === item.first.args.length - 1) {
            first = union_map(item.second, first);
            map = assoc_set(map, item.first, first);
            stack_pop(stack);
            item = stack_peek(stack);
        }
        if (item == null) {
            return first;
        } else {
            item.second = union_map(item.second, first);
            item.idx++;
            first = item.first.args[item.idx];
        }
    }
}

let EMPTY_MAP = new Map();

function union_map(first, second) {
    if (first.size === 0)
        return second;
    if (second.size === 0)
        return first;
    first = new Map(first);
    for (let [key, val] of second) {
        let value = first.get(key);
        if (value !== undefined) {
            value = true;
        } else {
            value = val;
        }
        first.set(key, value);
    }
    return first;
}

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

/**
 * ground(T): [TC2 8.3.10]
 * The built-in succceeds if T is ground.
 */
function test_ground(args) {
    let alpha = exec_build(args[0]);
    let res = walk_vars(alpha, node => true, VAR_MASK_SEEN);
    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.
 */
function test_nonground(args) {
    let alpha = exec_build(args[0]);
    let hit = undefined;

    function nonground2(node) {
        hit = node;
        return true;
    }

    let res = walk_vars(alpha, nonground2, VAR_MASK_SEEN);
    walk_vars(alpha, node => true, 0);
    return res && exec_unify(args[1], hit);
}

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

/**
 * term_hash(X, H):
 * The predicate succeeds in H with the term hash of the term X.
 */
function test_term_hash(args) {
    try {
        let alpha = exec_build(args[0]);
        alpha = norm_smallint(walk_hash(alpha));
        return exec_unify(args[1], alpha);
    } catch (err) {
        console.trace("err="+err);
        return false;
    }
}

/**
 * Walk a Prolog term completely.
 *
 * @param first The Prolog term.
 * @return The hash.
 */
function walk_hash(first) {
    let stack = null;
    let map = null;
    for (; ; ) {
        first = deref(first);
        if (is_structure(first)) {
            let peek = assoc_get(map, first);
            if (peek === undefined) {
                map = assoc_set(map, first, 0);
                peek = object_hash_code(first.functor);
                let item = new Item(first, peek, 0);
                stack = stack_push(stack, item);
                first = first.args[0];
                continue;
            } else {
                first = peek;
            }
        } else {
            first = object_hash_code(first);
        }
        let item = stack_peek(stack);
        while (item !== null &&
        item.idx === item.first.args.length - 1) {
            first = (item.second * 31 + first) | 0;
            map = assoc_set(map, item.first, first);
            stack_pop(stack);
            item = stack_peek(stack);
        }
        if (item === null) {
            return first;
        } else {
            item.second = (item.second * 31 + first) | 0;
            item.idx++;
            first = item.first.args[item.idx];
        }
    }
}

/*********************************************************************/
/* numbervars/3                                                      */
/*********************************************************************/

/**
 * numbervars(X, N, M):
 * The predicate instantiates the un-instantiated variables of
 * the term X with compounds of the form ‘$VAR’(<index>). The
 * <index> starts with N. The predicate succeeds when M unifies
 * with the next available <index>.
 */
function test_numbervars(args) {
    let alpha = exec_build(args[0]);
    let beta = exec_build(args[1]);
    check_integer(beta);
    if (beta >= 0) {
        beta = numbervars("$VAR", alpha, beta);
    } else {
        beta = (-1) - beta;
        beta = numbervars("_", alpha, beta);
        beta = (-1) - beta;
    }
    return exec_unify(args[2], beta);
}

function numbervars(functor, alpha, beta) {

    function numbervars2(node) {
        bind(new Compound(functor, [beta]), node);
        beta++;
        return false;
    }

    walk_vars(alpha, node => false, VAR_MASK_SEEN);
    walk_vars(alpha, numbervars2, 0);
    return beta;
}

/******************************************************************/
/* unnumbervars/3                                                 */
/******************************************************************/

/**
 * unnumbervars(S, N, T):
 * The predicate succeeds in T with a copy of S with compounds of
 * the form ‘$VAR’(<index>) and <index> greater or equal N are
 * replaced by fresh variables.
 */
function test_unnumbervars(args) {
    let alpha = exec_build(args[0]);
    let beta = exec_build(args[1]);
    check_integer(beta);
    if (beta >= 0) {
        alpha = walk_unnumber("$VAR", beta, alpha);
    } else {
        beta = (-1) - beta;
        alpha = walk_unnumber("_", beta, alpha);
    }
    return exec_unify(args[2], alpha);
}

/**
 * Walk a Prolog term completely.
 *
 * @param functor The unary functor.
 * @param beta The lower bound.
 * @param first The Prolog term.
 * @return The unnumber.
 */
function walk_unnumber(functor, beta, first) {
    let stack = null;
    let map = null;
    for (; ; ) {
        first = deref(first);
        if (is_structure(first)) {
            if (functor === first.functor &&
                first.args.length === 1) {
                let peek = deref(first.args[0]);
                if (is_integer(peek) && beta <= peek) {
                    first = assoc_get(map, peek);
                    if (first === undefined) {
                        first = new Variable();
                        map = assoc_set(map, peek, first);
                    }
                }
            }
            if (is_structure(first)) {
                let peek = assoc_get(map, first);
                if (peek === undefined) {
                    peek = new Compound(first.functor,
                        new Array(first.args.length));
                    map = assoc_set(map, first, peek);
                    let item = new Item(first, peek, 0);
                    stack = stack_push(stack, item);
                    first = first.args[0];
                    continue;
                } else {
                    first = peek;
                }
            }
        }
        let item = stack_peek(stack);
        while (item !== null &&
        item.idx  === item.first.args.length - 1) {
            item.second.args[item.idx] = first;
            first = item.second;
            stack_pop(stack);
            item = stack_peek(stack);
        }
        if (item === null) {
            return first;
        } else {
            item.second.args[item.idx] = first;
            item.idx++;
            first = item.first.args[item.idx];
        }
    }
}

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

export function main() {
    add("unify_with_occurs_check", 2, make_check(test_unify_checked));
    add("subsumes", 2, make_check(test_subsumes));
    add("term_singletons", 2, make_check(test_term_singletons));
    add("ground", 1, make_check(test_ground));
    add("nonground", 2, make_check(test_nonground));
    add("term_hash", 2, make_check(test_term_hash));
    add("numbervars", 3, make_check(test_numbervars));
    add("unnumbervars", 3, make_check(test_unnumbervars));
}
