Next: lib-jasper, Previous: lib-heaps, Up: The Prolog Library [Contents][Index]
library(is_directives)This library module gives access to the information declared by
is/2 directives.
The is/2 declarations can be used for declaring arbitrary
predicate attributes, but the main application is for declaring
determinacy information, and this is what is described here.
Determinacy, i.e. whether a call to a predicate can produce more than one solution on backtracking, is an important property for understanding the predicate and the code that uses it. For this reason it is desirable to describe the behavior in the documentation that accompanies a predicate.
The determinacy properties of a predicate can also be used by various tools, and for this reason it is possible to declare the determinacy of a predicate in a way that can be automatically processed by such tools. One example is the determinacy analyzer in the SPIDER IDE (see SPIDER), which uses the declared determinacy of a called predicate to improve the precision of the analysis of the caller in the common case that the caller does not have any determinacy declaration of its own.
The SICStus libraries contain determinacy declarations for most exported predicates. These can serve as useful examples.
Determinacy declarations are hints, i.e. they are meant to
convey the expected behavior. Due to the dynamic nature of
Prolog, almost any call can fail, throw an exception, or succeed more
than once for reasons not directly related to the called
predicate. Examples where these things can happen are timeouts
(library(timeout)) and functionality that can cause goals to
run when a variable is bound, e.g. freeze/2. For this reason,
anything that uses determinacy declarations must be prepared to handle
any run-time behavior, not just the behavior specified by the
declarations.
The following determinacy attributes are available:
detA call will always succeed exactly once. I.e. the number of solutions is expected to be one. This is probably the most common behavior.
semidetA call will fail, or succeed exactly once. I.e. the number of
solutions is expected to be zero or one. This can be used for for
describing tests, e.g. X>Y.
multiA call will succeed more than once. I.e. the number of solutions is
expected to be one or more. This is uncommon, but could be used to
describe the builtin repeat/0.
nondetA call may fail or succeed any number of times. I.e. the number of solutions is expected to be zero or more. This is the most general determinacy information and is what must be assumed unless no other information is available.
failingA call will fail. I.e. the number of solutions is expected to be
zero. This is uncommon, but could be used to describe the builtin
false/0.
throwingA call is expected to throw an exception. This is similar to
failing in that the number of solutions is expected to be zero
but differs in situations where failure is treated specially, like
if-then-else. This is uncommon, but could be used to describe the
builtin throw/1 and some of the error reporting predicates in
library(types).
Determinacy is declared using directives that use is/2. Note
that in this usage, is/2 has nothing to do with the arithmetic
predicate of the same name.
The format of a determinacy directive is:
:- SPEC is ANNOTATION.
where ANNOTATION is one of the atoms used for
determinacy annotation. The SPEC describes the predicate and can
be either a predicate specification (like those used by the
abolish/1 predicate) or a skeletal goal (like those used
by the meta_predicate/1 directive).
Example:
% foo/2 is expected to always succeed, once, for any argument.
:- foo/2 is det.
foo(X, Y) :-
Y = hello(X).
% bar/2, when called with a non-variable first argument,
% is expected to succeed at most once.
:- bar(+, ?) is semidet.
% bar/2, when called with a variable first argument,
% is expected to succeed any number of times.
:- bar(-, ?) is nondet.
bar('a', lowercase).
bar('A', uppercase).
…
bar('z', lowercase).
bar('Z', uppercase).
The SPEC tells which predicate is being annotated and, if it is a skeletal goal, it can restrict the declaration to only apply for the specified instantiation of the arguments. It can have one of the following forms:
Module:Name/ArityName/ArityModule and Name should be atoms, Arity should be a non-negative integer. This predicate specification denotes the predicate Name with arity Arity in module Module, where Module defaults to the source module.
Module:Name(ARG1, ARG2, …, ARGN)Name(ARG1, ARG2, …, ARGN)This skeletal goal denotes the predicate Name with arity N in the module Module, where Module defaults to the source module. The argument positions is typically used to indicate an instantiation pattern.
Many predicates have different determinacy depending on how their arguments are instantiated. This can be indicated using the skeleton goal form of specification, with each argument of the skeleton goal being one of the following:
+Indicates that the argument is instantiated, i.e. it is not a variable when the predicate is called.
-Indicates that the argument is uninstantiated, i.e. it is a variable when the predicate is called.
?*Indicates that the argument can be anything, i.e. the declared determinism is not affected by the instantiation of this argument
if the argument is a compound term with one argument
(like + hello, or - Bar), only the functor is used when
interpreting the argument. This makes it possible to use variables as
descriptive names for the arguments, e.g.
:- parent_of(+Parent, -Child) is nondet.
Not only variables can be used as descriptions in this way, any term is accepted.
When declaring determinism, the skeleton argument only specifies
whether an argument is a variable or not. This is different from
whether the argument should be considered input or output
(var(X) has only an input argument, but will often be called
with a variable as input argument).
The declarations above is sufficient for most predicates. However,
they do not suffice for predicates whose determinism depends on an
argument goal, like lists:maplist/2.
For such predicates, i.e. meta predicates that take a single closure (goal) argument, it is possible to specify different determinacy for each of the possible determinacies of the closure argument, as in the following example:
% The last argument of dolist/3 is a closure with two
% suppressed arguments that will be supplied using call/3.
:- meta_predicate dolist(*, *, 2).
% This is the expected mode, a determinate producer. In this
% case dolist/3 will also succeed exactly once.
:- dolist(+, -, det) is det.
% If the closure can fail, then dolist/2 can also fail.
:- dolist(+, -, semidet) is semidet.
% If the closure succeeds more than once, then so will dolist/2.
:- dolist(+, -, multi) is multi.
% If the closure always fails (a strange usage, indeed) then dolist/3
% can nevertheless succeed, when the input is an empty list.
:- dolist(+, -, failing) is semidet.
% In general, dolist/3 will be nondeterminate if the closure is
% nondeterminate.
% This declaration may seem redundant, but it may not be for some tools.
:- dolist(+, -, nondet) is nondet.
% dolist/3 calls the argument closure, which expects two extra
% arguments, on each pair of corresponding list elements
dolist([], [], _G_2). % The closure is ignored here
dolist([X|Xs], [Y|Ys], G_2) :-
call(G_2, X, Y),
dolist(Xs, Ys, G_2).
:- square/2 is det. % always expected to succeed (once)
square(X, XX) :-
XX is X*X.
% Example use:
% | ?- square_list([1,2,3], Squares).
% Squares = [1,4,9] ?
%
% It can be inferred that this is expected to succeed exactly once.
square_list(Numbers, Squares) :-
% Calls square(X,Y) on each X in Numbers and Y in Squares.
% Since square/2 is 'det', the call do dolist/3 will
% be considered 'det' as well.
dolist(Numbers, Squares, square).
Since determinacy declarations by necessity are only hints, it is often better to focus on the expected behavior rather than the exact behavior when declaring determinism for a predicate.
Also, only very simple instantiation patterns can be specified, so it may be useful to pretend they indicate more than they actually do.
As an example, consider how to declare the determinacy of the builtin
length(List, Length):
semidet.
det.
multi.
… is
throwing is only meant for predicates expected to always throw
an exception).
However, it is not possible to specify “proper list”, “partial
list“ and non-list as instantiation patterns. On the other hand, it
would be unfortunate to not be able to say anything about the
determinacy of length/2.
In such cases it may make sense to pretend that ‘+’, the
non-variable argument instantiation, means “a properly/fully
instantiated input”, i.e. a “proper list” in the case of
length/2. Similarly, it may make sense to pretend that
‘?’, any instantiation, means “a partially instantiated input”,
i.e. a “partial list” in the case of length/2.
So, for the builtin length/2 it would make sense to specify the
following determinacy declarations:
:- length(*, +) is semidet. % this is precise :- length(+, -) is det. % pretend '+' means proper list :- length(?, -) is multi. % pretend '?' means partial list
It is up to the documentation accompanying the predicate, and any tools that use these declarations, to handle this appropriately.
The determinacy declarations are saved when code is compiled or
consulted and can be accessed when the code has been loaded. This
could be used by documentation generators, smart debuggers, and many
other purposes, not
all of which documented. New uses may be added without notice,
so you should ignore any recorded is/2 directive that you
do not understand.
The loaded is/2 directives can be accessed using the following,
non-determinate, predicate:
current_is_directive(Skel, M, Annotation, Spec, Directive, Context).
This is a compound term with the same name as the predicate and one anonymous variable in each argument position.
This is the module of the predicate specification. Typically the same as the source module.
This is the second argument of the is/2 directive.
This is the first argument of the is/2 directive, with module prefixes peeled off.
This is the entire is/2 directive (without the surrounding :- ...).
this is the source module.
Consider the following code:
:- module(example, [p1/3]). :- p1/3 is det. :- user:bar(+, +) is semidet.
This corresponds to the following two clauses of current_is_directive/6:
current_is_directive(p1(_,_,_),
example,
det,
p1/3,
(p1/3 is det),
example).
current_is_directive(bar(_,_),
user,
semidet,
bar(+,+),
(user:bar(+,+) is semidet),
example).
Exported predicates:
current_is_directive(Skel, M, Annotation, Spec, Directive, Context).Low-level access to the information recorded by is/2
directives. See the library documentation for details.
current_is_directive(:MSkel, Annotation, Spec).Like current_is_directive(Skel, M,
Annotation, Spec, _, _) where M and Skel
are the parts of the meta argument MSkel.