This package allows the execution under the Basic Andorra Model [War88]. The model classifies goals as a determinate goal, if at most one clause matches the goal, or nondeterminate goal, otherwise. In this model a goal is delayed until either it becomes determinate or it becomes the leftmost goal and no determinate goal is available. The implementation of this selection rule is based on the use of attributed variables [Hol92,Hol90].
In order to test determinacy we verify only the heads of clauses and builtins in the bodies of clauses before the first cut, if any. By default, determinacy of a goal is detected dynamically: when called, if at most one clause matches, it is executed; otherwise, it is delayed. For goals delayed the test is repeated each time a variable appearing in the goal is instantiated. In addition, efficiency can be improved by using declarations that specify the determinacy conditions. These will be considered for testing instead of the generic test on all clauses that can match.
As with any other Ciao package, the andorra computation rule affects only the module that uses the package. If execution passes across two modules that use the computation rule, determinate goals are run in advance within one module and also within the other module. But determinate goals of one module do not run ahead of goals of the other module.
It is however possible to preserve the computation rule for calls to predicates defined in other modules. These modules should obviously also use this package. In addition all predicates from such modules should imported, i.e., the directive :- use_module(module), should be used in this case instead of :- use_module(module,[...]). Otherwise calls to predicates outside the module will only be called when they became the leftmost goal.
Declares determinacy conditions for a predicate. Conditions Cond are on variables of arguments of Pred. For example, in:
:- determinate(member(A,B,C), ( A ?= term(B,) ; C?=[_|_]) ). member(A,[A|B],B). member(A,[B|C],[B|D]) :- A==B, member(A,C,D).the declaration states that a call member(A,B,C) is determinate when either A doesn't unify with the first argument of B or C doesn't unify with [_|_].
States that the predicate Pred is determinate when Cond holds.
detcond(ground(X)) :- var(X). detcond(nonvar(X)) :- var(X). detcond(instatiated(A,Path)) :- var(A), list(int,Path). detcond(?\=(Term1,Term2)) :- path(Term1), path(Term2). detcond(?=(Term1,Term2)) :- path(Term1), path(Term2). detcond(Test) :- test(Test).
X is a determinacy condition.
path(X) :- var(X). path(X) :- list(int,X).