Admin User, created Apr 26. 2025
###
# 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 struct
from collections import OrderedDict
from nova.core import (make_check, exec_build, Variable,
check_integer, is_variable, set_to_list, check_callable,
is_atom, VOID_ARGS, Compound, is_compound, add, get_cont,
make_error, is_number, bind, atomic_equal, exec_unify,
deref, is_integer, VAR_MASK_STATE, make_special, cont)
#######################################################################
# 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>.
##
def test_numbervars(args):
alpha = exec_build(args[0])
beta = deref(exec_build(args[1]))
check_integer(beta)
if beta < 0:
raise make_error(Compound("domain_error",
["not_less_than_zero", beta]))
beta = numbervars(alpha, beta)
return exec_unify(args[2], beta)
def numbervars(alpha, beta):
def numbervars2(alpha2):
nonlocal beta
while True:
alpha2 = deref(alpha2)
if is_variable(alpha2):
bind(Compound("$VAR", [beta]), alpha2)
beta += 1
break
elif is_compound(alpha2):
alpha2 = alpha2.args
i = 0
while i < len(alpha2) - 1:
numbervars2(alpha2[i])
i += 1
alpha2 = alpha2[i]
else:
break
numbervars2(alpha)
return beta
################################################################
# 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.
# Tail recursive solution.
#
# @param first The first term.
# @param second The second term.
# @return True if the two terms unify, otherwise false.
##
def unify_checked(first, second):
while True:
first = deref(first)
second = deref(second)
if is_variable(first):
if is_variable(second) and first is 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 not is_compound(first):
return atomic_equal(first, second)
if not is_compound(second):
return False
if len(first.args) != len(second.args):
return False
if first.functor != second.functor:
return False
first = first.args
second = second.args
i = 0
while i < len(first) - 1:
if not unify_checked(first[i], second[i]):
return False
i += 1
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 True if term occurs in source, otherwise false.
##
def has_var(term, source):
def has_var2(source2):
while True:
source2 = deref(source2)
if is_variable(source2):
return term is source2
elif is_compound(source2):
source2 = source2.args
i = 0
while i < len(source2) - 1:
if has_var2(source2[i]):
return True
i += 1
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.
##
def test_subsumes(args):
alpha = exec_build(args[0])
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 True if the two terms single side unify, otherwise false.
##
def subsumes(first, second):
def subsumes2(first2, second2):
nonlocal second
while True:
first2 = deref(first2)
second2 = deref(second2)
if is_variable(first2):
if is_variable(second2) and first2 is second2:
return True
if has_var(first2, second):
return False
bind(second2, first2)
return True
if is_variable(second2):
return False
if not is_compound(first2):
return atomic_equal(first2, second2)
if not is_compound(second2):
return False
if len(first2.args) != len(second2.args):
return False
if first2.functor != second2.functor:
return False
first2 = first2.args
second2 = second2.args
i = 0
while i < len(first2) - 1:
if not subsumes2(first2[i], second2[i]):
return False
i += 1
first2 = first2[i]
second2 = second2[i]
return subsumes2(first, second)
################################################################
# term_hash/2 #
################################################################
###
# term_hash(X, H):
# The predicate succeeds in H with the variant hash of the term X.
##
def test_term_hash(args):
alpha = exec_build(args[0])
res = term_hash(alpha)
return exec_unify(args[1], res)
def term_hash(alpha):
res = 0
def term_hash2(alpha2):
nonlocal res
while True:
alpha2 = deref(alpha2)
if is_variable(alpha2):
res = int32(res * 31 + (alpha2.flags & ~VAR_MASK_STATE))
return
if not is_compound(alpha2):
res = int32(res * 31 + hash_code(alpha2))
return
args = alpha2.args
res = int32(res * 31 + hash_code(alpha2.functor))
i = 0
while i < len(args) - 1:
term_hash2(args[i])
i += 1
alpha2 = args[i]
term_hash2(alpha)
return res
###
# Compute the hash code of an atomic
#
# @param alpha The term.
# @return The hash code, a signed 32-bit integer
##
def hash_code(alpha):
if is_atom(alpha):
res = 0
i = 0
while i < len(alpha):
res = int32(res * 31 + ord(alpha[i]))
i += 1
return res
elif is_number(alpha):
if is_integer(alpha):
if -0x8000000 < alpha <= 0x7FFFFFFF:
return alpha
else:
if alpha < 0:
sign = -1
alpha = -alpha
else:
sign = 1
alpha = "%x" % alpha
res = 0
i = len(alpha) % 8
if i > 0:
res = int32(int(alpha[0:i], 16))
while i < len(alpha):
res = int32(res * 31 + int(alpha[i:i+8], 16))
i += 8
return res*sign
else:
beta = struct.pack(">d", alpha)
gamma = struct.unpack(">l", beta[0:4]) + struct.unpack(">l", beta[4:8])
return gamma[0] ^ gamma[1]
else:
if alpha is True:
return 1
elif alpha is False:
return 0
elif alpha is None:
return -1
else:
return -2
def int32(alpha):
alpha &= 0xFFFFFFFF
if alpha >= 0x80000000:
return alpha - 0x100000000
else:
return alpha
################################################################
# term_singletons/2 and nonground/2 #
################################################################
###
# term_singletons(T, L):
# The built-in succeeds in L with the singleton variables of T.
##
def test_term_singletons(args):
alpha = exec_build(args[0])
alpha = term_singletons(alpha)
alpha = set_to_list(alpha)
return exec_unify(args[1], alpha)
###
# Collect the singleton variables of a Prolog term.
#
# @param alpha The Prolog term.
# @return The set with the singleton variables.
##
def term_singletons(alpha):
res = None
anon = None
def term_singletons2(alpha2):
nonlocal res
nonlocal anon
while True:
alpha2 = deref(alpha2)
if is_variable(alpha2):
if res is None:
res = OrderedDict()
anon = OrderedDict()
if alpha2 in res:
del anon[alpha2]
else:
res[alpha2] = None
anon[alpha2] = None
break
elif is_compound(alpha2):
alpha2 = alpha2.args
i = 0
while i < len(alpha2) - 1:
term_singletons2(alpha2[i])
i += 1
alpha2 = alpha2[i]
else:
break
term_singletons2(alpha)
return anon
###
# nonground(T, V):
# The built-in succeeds if T is non-ground and V is the first variable.
##
def test_nonground(args):
alpha = exec_build(args[0])
alpha = first_variable(alpha)
if alpha is NotImplemented:
return False
return exec_unify(args[1], alpha)
###
# Find the first variable of a Prolog term.
#
# @param alpha The Prolog term.
# @return The first variable or undefined.
##
def first_variable(alpha):
while True:
alpha = deref(alpha)
if is_variable(alpha):
return alpha
elif is_compound(alpha):
alpha = alpha.args
i = 0
while i < len(alpha) - 1:
res = first_variable(alpha[i])
if res is not NotImplemented:
return res
i += 1
alpha = alpha[i]
else:
return NotImplemented
################################################################
# unnumbervars/2 #
################################################################
###
# unnumbervars(S, N, T):
# The predicate succeeds in T with a copy of S with compounds of
# the form ‘$VAR’(<index>) and <index> greater or equal N are
# replaced by fresh variables.
##
def test_unnumbervars(args):
alpha = exec_build(args[0])
beta = deref(exec_build(args[1]))
check_integer(beta)
if beta < 0:
raise make_error(Compound("domain_error",
["not_less_than_zero", beta]))
alpha = unnumbervars(alpha, beta)
return exec_unify(args[2], alpha)
def unnumbervars(alpha, beta):
assoc = None
def unnumbervars2(alpha2):
nonlocal assoc
nonlocal beta
back = None
while True:
alpha2 = deref(alpha2)
if is_variable(alpha2):
break
elif is_compound(alpha2):
if ("$VAR" == alpha2.functor and
len(alpha2.args) == 1):
beta2 = deref(alpha2.args[0])
if is_integer(beta2) and beta <= beta2:
beta2 = beta2 - beta
if assoc is None:
assoc = []
while len(assoc) <= beta2:
assoc.append(Variable())
alpha2 = assoc[beta2]
break
t1 = alpha2.args
args = [NotImplemented] * len(t1)
alpha2 = Compound(alpha2.functor, args)
i = 0
while i < len(args) - 1:
args[i] = unnumbervars2(t1[i])
i += 1
args[i] = back
back = alpha2
alpha2 = t1[i]
else:
break
while back is not None:
peek = back.args[len(back.args) - 1]
back.args[len(back.args) - 1] = alpha2
alpha2 = back
back = peek
return alpha2
return unnumbervars2(alpha)
#######################################################################
# call/2-4 #
#######################################################################
###
# call(F, A1, .., An): [Corr.2 8.15.4.4]
# The predicate succeeds in calling the goal which results from
# appending the arguments A1, .., An to the callable F.
##
def special_call(args):
alpha = deref(args[0])
check_callable(alpha)
if is_compound(alpha):
functor = alpha.functor
oldargs = alpha.args
else:
functor = alpha
oldargs = VOID_ARGS
arity = len(oldargs) + len(args) - 1
if arity == 0:
goal = functor
else:
newargs = [NotImplemented] * arity
i = 0
while i < len(oldargs):
newargs[i] = deref(oldargs[i])
i += 1
i = 0
while i < len(args) - 1:
newargs[i + len(oldargs)] = deref(args[i + 1])
i += 1
goal = Compound(functor, newargs)
res = get_cont().args[1]
res = Compound(".", [goal, res])
cont(res)
return True
#######################################################################
# Fast Lib Init #
#######################################################################
def 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))
add("term_hash", 2, make_check(test_term_hash))
add("term_singletons", 2, make_check(test_term_singletons))
add("nonground", 2, make_check(test_nonground))
add("unnumbervars", 3, make_check(test_unnumbervars))
add("call", 2, make_special(special_call))
add("call", 3, make_special(special_call))
add("call", 4, make_special(special_call))
add("call", 5, make_special(special_call))
add("call", 6, make_special(special_call))
add("call", 7, make_special(special_call))
add("call", 8, make_special(special_call))