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