package doglet;
import nova.Machine;
import nova.Store;
import nova.eval;
import nova.special;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Objects;
/**
* 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.
*/
public final class cyclib {
/******************************************************************/
/* 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.
*/
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);
}
/**
* Determine whether two terms unify with occurs check.
* As a side effect the trail is extended, even if unification fails.
* Can handle cyclic terms.
*
* @param first The first term.
* @param second The second term.
* @return boolean True if the two terms unify, otherwise false.
*/
private static boolean unify_checked(Object first, Object second) {
List stack = null;
List log = null;
try {
for (; ; ) {
first = Store.deref(first);
second = Store.deref(second);
if (Store.is_variable(first)) {
if (!Store.is_variable(second) || first != second) {
if (has_var((Store.Variable) first, second))
break;
Machine.bind(second, (Store.Variable) first);
}
} else if (Store.is_variable(second)) {
if (has_var((Store.Variable) second, first))
break;
Machine.bind(first, (Store.Variable) second);
} else if (!Store.is_structure(first)) {
if (!Objects.equals(first, second))
break;
} else if (!Store.is_structure(second)) {
break;
} else if (((Store.Structure) first).args.length !=
((Store.Structure) second).args.length) {
break;
} else {
first = Machine.union_find((Store.Structure) first);
second = Machine.union_find((Store.Structure) second);
if (first != second) {
if (Machine.is_frozen(first) && Machine.is_frozen(second) &&
((Machine.Frozen)first).hash != ((Machine.Frozen)second).hash)
break;
if (!((Store.Structure) first).functor.equals(
((Store.Structure) second).functor))
break;
log = Machine.union_add(log, (Store.Structure) first,
(Store.Structure) second);
if (0 != ((Store.Structure) first).args.length - 1) {
Store.Item item = new Store.Item((Store.Structure)first, second, 0);
stack = Store.stack_push(stack, item);
}
first = ((Store.Structure) first).args[0];
second = ((Store.Structure) second).args[0];
continue;
}
}
Store.Item item = (Store.Item)Store.stack_peek(stack);
if (item == null) {
return true;
} else {
item.idx++;
first = item.first.args[item.idx];
second = ((Store.Structure)item.second).args[item.idx];
if (item.idx == item.first.args.length - 1)
Store.stack_pop(stack);
}
}
return false;
} finally {
Machine.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.
*/
private static boolean test_has_var(Object[] args) {
Object alpha = Machine.exec_build(args[0]);
Object beta = Machine.exec_build(args[1]);
return Store.is_variable(alpha) && has_var((Store.Variable)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.
*/
private static boolean has_var(Store.Variable vterm, Object first) {
has_var2 h = new has_var2(vterm);
boolean res = special.walk_vars(first, h::run, Store.VAR_MASK_SEEN);
special.walk_vars(first, h::run, 0);
return res;
}
private static class has_var2 {
private final Store.Variable vterm;
private has_var2(Store.Variable vterm) {
this.vterm = vterm;
}
public boolean run(Object node) {
return (node == vterm);
}
}
/******************************************************************/
/* 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.
*/
private static boolean test_acyclic_term(Object[] args) {
Object alpha = Machine.exec_build(args[0]);
boolean res = walk_cyclic(alpha, Store.VAR_MASK_SEEN);
walk_cyclic(alpha, 0);
return !res;
}
private static boolean walk_cyclic(Object first, int state) {
List stack = null;
for (; ; ) {
first = Store.deref(first);
if (Store.is_compound(first)) {
if ((((Store.Compound) first).walk & Store.VAR_MASK_SEEN) != state) {
((Store.Compound)first).walk = (((Store.Compound)first).walk & ~Store.VAR_MASK_SEEN) | state;
((Store.Compound) first).walk &= ~Store.VAR_MASK_SERNO;
stack = Store.stack_push(stack, first);
first = ((Store.Structure) first).args[0];
continue;
} else if ((((Store.Compound)first).walk & Store.VAR_MASK_SERNO)
!= ((Store.Structure) first).args.length) {
return true;
}
}
Store.Compound item = (Store.Compound)Store.stack_peek(stack);
while (item != null &&
(item.walk & Store.VAR_MASK_SERNO) == item.args.length - 1) {
item.walk++;
Store.stack_pop(stack);
item = (Store.Compound)Store.stack_peek(stack);
}
if (item == null) {
return false;
} else {
item.walk++;
first = item.args[item.walk & Store.VAR_MASK_SERNO];
}
}
}
/******************************************************************/
/* acyclic_decompose/2 */
/******************************************************************/
/**
* acyclic_decompose(S, T):
* The built-in succeeds in R with skeleton and substitution
* list cells so that the substitions applied to the skeletons
* gives identical the elements of the Prolog list L.
*/
private static boolean test_acyclic_decompose(Object[] args) {
Object alpha = Machine.exec_build(args[0]);
Object res = null;
try {
Store.Structure back = null;
int i = 0;
Object peek = alpha;
while (Store.is_structure(peek) &&
".".equals(((Store.Structure) peek).functor) &&
((Store.Structure) peek).args.length == 2 &&
i < special.MAX_ARITY) {
Object temp = Store.deref(((Store.Structure) peek).args[0]);
temp = walk_decom(temp);
temp = new Store.Compound(".",
new Object[]{temp, Store.UNDEF_OBJ});
if (back == null) {
res = temp;
} else {
back.args[1] = temp;
}
back = (Store.Structure) temp;
i++;
peek = Store.deref(((Store.Structure) peek).args[1]);
}
special.check_nil(peek);
if (back == null) {
res = "[]";
} else {
back.args[1] = "[]";
}
} finally {
Object peek = alpha;
while (Store.is_structure(peek) &&
".".equals(((Store.Structure) peek).functor) &&
((Store.Structure) peek).args.length == 2) {
Object temp = Store.deref(((Store.Structure) peek).args[0]);
eval.walk_uncompute(temp);
peek = Store.deref(((Store.Structure) peek).args[1]);
}
}
return Machine.exec_unify(args[1], res);
}
/**
* Walk a Prolog term completely.
*
* @param first The Prolog term.
* @return The decomp.
*/
private static Object walk_decom(Object first) {
List stack = null;
Object subst = "[]";
for (; ; ) {
first = Store.deref(first);
if (Store.is_compound(first)) {
if (!eval.is_triple(((Store.Structure) first).functor)) {
((Store.Structure) first).functor = new eval.Triple(
((Store.Structure) first).functor, Store.UNDEF_OBJ,
new Object[((Store.Structure) first).args.length]);
((Store.Compound) first).walk &= ~Store.VAR_MASK_SERNO;
stack = Store.stack_push(stack, first);
first = ((Store.Structure) first).args[0];
continue;
} else {
Object peek = ((eval.Triple) ((Store.Structure) first).functor).accum;
if (peek == Store.UNDEF_OBJ) {
peek = new Store.Variable();
((eval.Triple) ((Store.Structure) first).functor).accum = peek;
}
first = peek;
}
}
Store.Compound item = (Store.Compound) Store.stack_peek(stack);
while (item != null &&
(item.walk & Store.VAR_MASK_SERNO) == item.args.length - 1) {
((eval.Triple) item.functor).children[item.walk & Store.VAR_MASK_SERNO] = first;
first = new Store.Compound(((eval.Triple) item.functor).backup, ((eval.Triple) item.functor).children);
Object peek = ((eval.Triple) item.functor).accum;
if (peek == Store.UNDEF_OBJ) {
((eval.Triple) item.functor).accum = first;
} else {
first = new Store.Compound("=", new Object[]{peek, first});
subst = new Store.Compound(".", new Object[]{first, subst});
first = peek;
}
Store.stack_pop(stack);
item = (Store.Compound) Store.stack_peek(stack);
}
if (item == null) {
return new Store.Compound(".", new Object[]{first,subst});
} else {
((eval.Triple) item.functor).children[item.walk & Store.VAR_MASK_SERNO] = first;
item.walk++;
first = item.args[item.walk & Store.VAR_MASK_SERNO];
}
}
}
/******************************************************************/
/* Cyc Lib Init */
/******************************************************************/
public static void main() {
Store.set("unify_with_occurs_check", 2, special.make_check(cyclib::test_unify_checked));
Store.set("occurs_check", 2, special.make_check(cyclib::test_has_var));
Store.set("acyclic_term", 1, special.make_check(cyclib::test_acyclic_term));
Store.set("acyclic_decompose", 2, special.make_check(cyclib::test_acyclic_decompose));
}
}