Andorra execution

Author(s): Claudio Vaucheret, Francisco Bueno.

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.

Usage and interface

Library usage:
:- use_package(andorra). or :- module(...,...,[andorra]).
Exports:
- Regular Types:
  detcond/1, path/1.
New operators defined:
?\=/2 [700,xfx], ?=/2 [700,xfx].
New declarations defined:
determinate/2.
Implicit imports:
- Packages:
  prelude, initial, condcomp, assertions, assertions/assertions_basic.

Documentation on new declarations

DECLARATIONdeterminate/2

:- determinate(Pred,Cond).

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,[1])  ; 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 [_|_].

Usage::- determinate(Pred,Cond).

States that the predicate Pred is determinate when Cond holds.

The following properties should hold at call time:
(basic_props:predname/1)Pred is a predicate name.
(user(... /andorra_doc):detcond/1)Cond is a determinacy condition.

Documentation on exports

REGTYPEdetcond/1

Defined by:

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

ground/1 and nonvar/1 have the usual meaning.
instatiated(A,Path) means that the subterm of A addressed by Path is not a variable. Path is a list of integer numbers describing a path to the subterm regarding the whole term A as a tree. For example, instantiated(f(g(X),h(i(Z),Y)),[2,1]) tests whether i(Z) is not a variable.
Term1 ?\= Term2 means ``terms Term1 and Term2 do not unify (when instantiated)''. Term1 and Term2 can be either an argument of the predicate or a term term(V,Path), which refers to the subterm of V addressed by Path.
Term1 ?= Term2 means ``terms Term1 and Term2 unify (when instantiated)''. The same considerations above apply to Term1 and Term2.
any other test that does not unify variables can also be used ( ==/2, \==/2, atomic/1).

Usage:detcond(X)

X is a determinacy condition.

REGTYPEpath/1

Defined by:

path(X) :-
    var(X).
path(X) :-
    list(int,X).

Other information

The andorra transformation will include the following predicates into the code of the module that uses the package. Be careful not to define predicates by these names:

detcond_andorra/4
path_andorra/4
detcond_susp/4
path_susp/4
list_andorra2/5
test_andorra2/4