/**
 * 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, is_structure, set, deref, make_check,
    exec_unify, Compound, Variable, VAR_MASK_SEEN,
    VAR_MASK_SERNO, stack_push, is_frozen, Triple,
    stack_peek, stack_pop, is_compound, Item, is_triple,
    is_variable, bind, walk_vars, MAX_ARITY, check_nil,
    union_find, union_add, union_undo, walk_uncompute
} 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 (!Object.is(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 !== second) {
                    if (is_frozen(first) && is_frozen(second) &&
                        first.hash !== second.hash)
                        break;
                    if (first.functor !== second.functor)
                        break;
                    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);
    }
}

/*********************************************************************/
/* occurs_check/2                                                    */
/*********************************************************************/

/**
 * 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.
 */
function test_has_var(args) {
    let alpha = exec_build(args[0]);
    let beta = exec_build(args[1]);
    return is_variable(alpha) && has_var(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.
 */
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;
}

/*********************************************************************/
/* acyclic_term/1                                                    */
/*********************************************************************/

/**
 * acyclic_term(T): [TC2 8.3.11]
 * The predicate succeeds when the Prolog term T is an acyclic term,
 * otherwise the predicate fails.
 */
function test_acyclic_term(args) {
    let alpha = exec_build(args[0]);
    let res = walk_cyclic(alpha, VAR_MASK_SEEN);
    walk_cyclic(alpha, 0);
    return !res;
}

function walk_cyclic(first, state) {
    let stack = null;
    for (; ; ) {
        first = deref(first);
        if (is_compound(first)) {
            if ((first.walk & VAR_MASK_SEEN) !== state) {
                first.walk = (first.walk & ~VAR_MASK_SEEN) | state;
                first.walk &= ~VAR_MASK_SERNO;
                stack = stack_push(stack, first);
                first = first.args[0];
                continue;
            } else if ((first.walk & VAR_MASK_SERNO)
                     !== first.args.length) {
                return true;
            }
        }
        let item = stack_peek(stack);
        while (item !== null &&
                (item.walk & VAR_MASK_SERNO) === item.args.length - 1) {
            item.walk++;
            stack_pop(stack);
            item = stack_peek(stack);
        }
        if (item === null) {
            return false;
        } else {
            item.walk++;
            first = item.args[item.walk & VAR_MASK_SERNO];
        }
    }
}

/******************************************************************/
/* acyclic_decompose/2                                            */
/******************************************************************/

/**
 * acyclic_decompose(L, R):
 * The built-in succeeds in R with skeleton and substitution
 * list cells so that the substitions applied to the skeletons
 * identical the elements of the Prolog list L.
 */
function test_acyclic_decompose(args) {
    let alpha = exec_build(args[0]);
    let res = null;
    try {
        let back = null;
        let i = 0;
        let peek = alpha;
        while (is_structure(peek) &&
        peek.functor === "." &&
        peek.args.length === 2 &&
        i < MAX_ARITY) {
            let temp = deref(peek.args[0]);
            temp = walk_decom(temp);
            temp = new Compound(".", [temp, undefined]);
            if (back === null) {
                res = temp;
            } else {
                back.args[1] = temp;
            }
            back = temp;
            i++;
            peek = deref(peek.args[1]);
        }
        check_nil(peek);
        if (back === null) {
            res = "[]";
        } else {
            back.args[1] = "[]";
        }
    } finally {
        let peek = alpha;
        while (is_structure(peek) &&
        peek.functor === "." &&
        peek.args.length === 2) {
            let temp = deref(peek.args[0]);
            walk_uncompute(temp);
            peek = deref(peek.args[1]);
        }
    }
    return exec_unify(args[1], res);
}

function walk_decom(first) {
    let stack = null;
    let subst = "[]";
    for (; ; ) {
        first = deref(first);
        if (is_compound(first)) {
            if (!is_triple(first.functor)) {
                first.functor = new Triple(first.functor, undefined,
                    new Array(first.args.length));
                first.walk &= ~VAR_MASK_SERNO;
                stack = stack_push(stack, first);
                first = first.args[0];
                continue;
            } else {
                let peek = first.functor.accum;
                if (peek === undefined) {
                    peek = new Variable();
                    first.functor.accum = peek;
                }
                first = peek;
            }
        }
        let item = stack_peek(stack);
        while (item !== null &&
        (item.walk & VAR_MASK_SERNO) === item.args.length - 1) {
            item.functor.children[item.walk & VAR_MASK_SERNO] = first;
            first = new Compound(item.functor.backup, item.functor.children);
            let peek = item.functor.accum;
            if (peek === undefined) {
                item.functor.accum = first;
            } else {
                first = new Compound("=", [peek, first]);
                subst = new Compound(".", [first, subst]);
                first = peek;
            }
            stack_pop(stack);
            item = stack_peek(stack);
        }
        if (item === null) {
            return new Compound(".", [first,subst]);
        } else {
            item.functor.children[item.walk & VAR_MASK_SERNO] = first;
            item.walk++;
            first = item.args[item.walk & VAR_MASK_SERNO];
        }
    }
}

/*********************************************************************/
/* Cyc Lib Init                                                      */
/*********************************************************************/

export function main() {
    set("unify_with_occurs_check", 2, make_check(test_unify_checked));
    set("occurs_check", 2, make_check(test_has_var));
    set("acyclic_term", 1, make_check(test_acyclic_term));
    set("acyclic_decompose", 2, make_check(test_acyclic_decompose));
}
