Home Page
Site Map
Login/out
Message Board
Download(c) 2005-2024 XLOG Technologies AG
/**
* 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 {
check_integer, exec_build,
unify, is_variable, Compound, exec_unify,
is_compound, is_bigint, norm_smallint, make_error,
norm_bigint, add, make_check, bind, deref
} from "../dogelog.mjs";
/*********************************************************************/
/* 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 = deref(exec_build(args[1]));
check_integer(beta);
if (beta < 0)
throw make_error(new Compound("domain_error",
["not_less_than_zero", beta]));
beta = numbervars(alpha, beta);
if (beta === undefined)
return false;
return exec_unify(args[2], beta);
}
function numbervars(alpha, beta) {
function numbervars2(alpha2) {
for (; ;) {
alpha2 = deref(alpha2);
if (is_variable(alpha2)) {
if (!unify(alpha2, new Compound("$VAR", [beta]))) {
beta = undefined;
} else {
beta = succ(beta);
}
break;
} else if (is_compound(alpha2)) {
alpha2 = alpha2.args;
let i = 0;
for (; i < alpha2.length - 1; i++) {
numbervars2(alpha2[i]);
if (beta === undefined)
break;
}
alpha2 = alpha2[i];
} else {
break;
}
}
}
numbervars2(alpha);
return beta;
}
function succ(beta) {
if (!is_bigint(beta)) {
return norm_smallint(beta + 1);
} else {
return norm_bigint(beta + BigInt(1));
}
}
/*********************************************************************/
/* 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.
* Tail recursive solution.
*
* @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) {
for (; ;) {
first = deref(first);
second = deref(second);
if (is_variable(first)) {
if (is_variable(second) && first === second)
return true;
if (has_var(first, second))
return false;
bind(second, first);
return true;
}
if (is_variable(second)) {
if (has_var(second, first))
return false;
bind(first, second);
return true;
}
if (!is_compound(first))
return (first === second);
if (!is_compound(second))
return false;
if (first.args.length !== second.args.length)
return false;
if (first.functor !== second.functor)
return false;
first = first.args;
second = second.args;
let i = 0;
for (; i < first.length - 1; i++) {
if (!unify_checked(first[i], second[i]))
return false;
}
first = first[i];
second = second[i];
}
}
/**
* Check whether a variable occurs in a term.
* Tail recursive solution.
*
* @param term The variable.
* @param source The Prolog term.
* @return boolean True if term occurs in source, otherwise false.
*/
function has_var(term, source) {
function has_var2(source2) {
for (; ;) {
source2 = deref(source2);
if (is_variable(source2)) {
return (term === source2);
} else if (is_compound(source2)) {
source2 = source2.args;
let i = 0;
for (; i < source2.length - 1; i++)
if (has_var2(source2[i]))
return true;
source2 = source2[i];
} else {
return false;
}
}
}
return has_var2(source);
}
/*********************************************************************/
/* 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_compound(first2))
return (first2 === second2);
if (!is_compound(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);
}
/*********************************************************************/
/* Fast Lib Init */
/*********************************************************************/
export function main() {
add("numbervars", 3, make_check(test_numbervars));
add("unify_with_occurs_check", 2, make_check(test_unify_checked));
add("subsumes", 2, make_check(test_subsumes));
}