###
# 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))