### # 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. ## from nova.core import (bind, make_check, exec_build, deref, is_structure, set, is_frozen, union_find, union_add, VAR_MASK_SEEN, VAR_MASK_SERNO, Item, MAX_ARITY, stack_pop, stack_peek, stack_push, check_nil, Triple, is_triple, walk_uncompute, exec_unify, Compound, Variable, is_compound, is_variable, object_equals, walk_vars, union_undo) ################################################################ # 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. ## def test_unify_checked(args): alpha = exec_build(args[0]) 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 True if the two terms unify, otherwise false. ## def unify_checked(first, second): stack = None log = None try: while True: first = deref(first) second = deref(second) if is_variable(first): if not is_variable(second) or first is not second: if has_var(first, second): break bind(second, first) elif is_variable(second): if has_var(second, first): break bind(first, second) elif not is_structure(first): if not object_equals(first, second): break elif not is_structure(second): break elif len(first.args) != len(second.args): break else: first = union_find(first) second = union_find(second) if first is not second: if (is_frozen(first) and is_frozen(second) and first.hash != second.hash): break if first.functor != second.functor: break log = union_add(log, first, second) if 0 != len(first.args) - 1: item = Item(first, second, 0) stack = stack_push(stack, item) first = first.args[0] second = second.args[0] continue item = stack_peek(stack) if item is None: return True else: item.idx += 1 first = item.first.args[item.idx] second = item.second.args[item.idx] if item.idx == len(item.first.args) - 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. ## def test_has_var(args): alpha = exec_build(args[0]) beta = exec_build(args[1]) return is_variable(alpha) and 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 True if vterm occurs in alpha, otherwise false. ## def has_var(vterm, first): def has_var2(node): return node is vterm 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. ## def test_acyclic_term(args): alpha = exec_build(args[0]) res = walk_cyclic(alpha, VAR_MASK_SEEN) walk_cyclic(alpha, 0) return not res def walk_cyclic(first, state): stack = None while True: 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 elif ((first.walk & VAR_MASK_SERNO) != len(first.args)): return True item = stack_peek(stack) while (item is not None and (item.walk & VAR_MASK_SERNO) == len(item.args) - 1): item.walk += 1 stack_pop(stack) item = stack_peek(stack) if item is None: return False else: item.walk += 1 first = item.args[item.walk & VAR_MASK_SERNO] ################################################################ # acyclic_decompose/2 # ################################################################ ### # acyclic_decompose(X, T, L): # 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. ## def test_acyclic_decompose(args): alpha = exec_build(args[0]) res = None try: back = None i = 0 peek = alpha while (is_structure(peek) and peek.functor == "." and len(peek.args) == 2 and i < MAX_ARITY): temp = deref(peek.args[0]) temp = walk_decom(temp) temp = Compound(".", [temp, NotImplemented]) if back is None: res = temp else: back.args[1] = temp back = temp i += 1 peek = deref(peek.args[1]) check_nil(peek) if back is None: res = "[]" else: back.args[1] = "[]" finally: peek = alpha while (is_structure(peek) and peek.functor == "." and len(peek.args) == 2): temp = deref(peek.args[0]) walk_uncompute(temp) peek = deref(peek.args[1]) return exec_unify(args[1], res) def walk_decom(first): stack = None subst = "[]" while True: first = deref(first) if is_compound(first): if not is_triple(first.functor): first.functor = Triple(first.functor, NotImplemented, [NotImplemented] * len(first.args)) first.walk &= ~VAR_MASK_SERNO stack = stack_push(stack, first) first = first.args[0] continue else: peek = first.functor.accum if peek is NotImplemented: peek = Variable() first.functor.accum = peek first = peek item = stack_peek(stack) while (item is not None and (item.walk & VAR_MASK_SERNO) == len(item.args) - 1): item.functor.children[item.walk & VAR_MASK_SERNO] = first first = Compound(item.functor.backup, item.functor.children) peek = item.functor.accum if peek is NotImplemented: item.functor.accum = first else: first = Compound("=", [peek, first]) subst = Compound(".", [first, subst]) first = peek stack_pop(stack) item = stack_peek(stack) if item is None: return Compound(".", [first,subst]) else: item.functor.children[item.walk & VAR_MASK_SERNO] = first item.walk += 1 first = item.args[item.walk & VAR_MASK_SERNO] ####################################################################### # Cyc Lib Init # ####################################################################### def 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))