package liblet;
         

         
import nova.envir.ComputeCompare;
         
import nova.envir.ComputeElem;
         
import nova.Machine;
         
import nova.Special;
         
import nova.Store;
         

         
import java.util.Objects;
         

         
public final class fastlib {
         

         

         
    private static boolean test_numbervars(Object[] args) {
         
        Object alpha = Machine.exec_build(args[0]);
         
        Object beta = Machine.deref(Machine.exec_build(args[1]));
         
        Special.check_integer(beta);
         
        if (ComputeCompare.integer_signum((Number) beta) < 0)
         
            throw Machine.make_error(new Store.Compound("domain_error",
         
                    new Object[]{"not_less_than_zero", beta}));
         
        beta = numbervars(alpha, (Number) beta);
         
        if (beta == null)
         
            return false;
         
        return Machine.exec_unify(args[2], beta);
         
    }
         

         
    private static Number numbervars(Object alpha, Number val) {
         
        for (; ; ) {
         
            alpha = Machine.deref(alpha);
         
            if (Store.is_variable(alpha)) {
         
                if (!Machine.unify(alpha, new Store.Compound("$VAR",
         
                        new Object[]{val}))) {
         
                    val = null;
         
                } else {
         
                    val = ComputeElem.add(val, Integer.valueOf(1));
         
                }
         
                break;
         
            } else if (Store.is_compound(alpha)) {
         
                Object[] temp = ((Store.Compound) alpha).args;
         
                int i = 0;
         
                for (; i < temp.length - 1; i++) {
         
                    val = numbervars(temp[i], val);
         
                    if (val == null)
         
                        break;
         
                }
         
                alpha = temp[i];
         
            } else {
         
                break;
         
            }
         
        }
         
        return val;
         
    }
         

         

         
    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);
         
    }
         

         
    private static boolean unify_checked(Object first, Object second) {
         
        for (; ; ) {
         
            first = Machine.deref(first);
         
            second = Machine.deref(second);
         
            if (Store.is_variable(first)) {
         
                if (Store.is_variable(second) && first == second)
         
                    return true;
         
                if (has_var(first, second))
         
                    return false;
         
                Machine.bind(second, (Store.Variable) first);
         
                return true;
         
            }
         
            if (Store.is_variable(second)) {
         
                if (has_var(second, first))
         
                    return false;
         
                Machine.bind(first, (Store.Variable) second);
         
                return true;
         
            }
         
            if (!Store.is_compound(first))
         
                return Objects.equals(first, second);
         
            if (!Store.is_compound(second))
         
                return false;
         
            Object[] t1 = ((Store.Compound) first).args;
         
            Object[] t2 = ((Store.Compound) second).args;
         
            if (t1.length != t2.length)
         
                return false;
         
            if (!((Store.Compound) first).functor.equals(((Store.Compound) second).functor))
         
                return false;
         
            int i = 0;
         
            for (; i < t1.length - 1; i++) {
         
                if (!unify_checked(t1[i], t2[i]))
         
                    return false;
         
            }
         
            first = t1[i];
         
            second = t2[i];
         
        }
         
    }
         

         
    private static boolean has_var(Object term, Object source) {
         
        for (; ; ) {
         
            source = Machine.deref(source);
         
            if (Store.is_variable(source)) {
         
                return (term == source);
         
            } else if (Store.is_compound(source)) {
         
                Object[] temp = ((Store.Compound) source).args;
         
                int i = 0;
         
                for (; i < temp.length - 1; i++)
         
                    if (has_var(term, temp[i]))
         
                        return true;
         
                source = temp[i];
         
            } else {
         
                return false;
         
            }
         
        }
         
    }
         

         

         
    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);
         
    }
         

         
    private static boolean subsumes(Object root, Object first, Object second) {
         
        for (; ; ) {
         
            first = Machine.deref(first);
         
            second = Machine.deref(second);
         
            if (Store.is_variable(first)) {
         
                if (Store.is_variable(second) && first == second)
         
                    return true;
         
                if (has_var(first, root))
         
                    return false;
         
                Machine.bind(second, (Store.Variable) first);
         
                return true;
         
            }
         
            if (Store.is_variable(second))
         
                return false;
         
            if (!Store.is_compound(first))
         
                return Objects.equals(first, second);
         
            if (!Store.is_compound(second))
         
                return false;
         
            Object[] t1 = ((Store.Compound) first).args;
         
            Object[] t2 = ((Store.Compound) second).args;
         
            if (t1.length != t2.length)
         
                return false;
         
            if (!((Store.Compound) first).functor.equals(((Store.Compound) 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];
         
        }
         
    }
         

         

         
    public static void main() {
         
        Store.add("numbervars", 3, Special.make_check(fastlib::test_numbervars));
         
        Store.add("unify_with_occurs_check", 2, Special.make_check(fastlib::test_unify_checked));
         
        Store.add("subsumes", 2, Special.make_check(fastlib::test_subsumes));
         
    }
         

         
}