Many predicates can sensibly be called in different ways, e.g. with a
specific argument as input or as output. The header of the documentation
of a predicate consists of one or more templates, each
representing a specific way of calling the predicate.
A template can contain information about types, argument
instantiation patterns, determinism and more. The syntax is informally
described below:
| <template> | ::= | <head>[’//’]’is’ <determinism> |
| | | <head>[’//’] |
| <determinism> | ::= | ’det’ |
| | | ’semidet’ |
| | | ’failure’ |
| | | ’nondet’ |
| | | ’multi’ |
| | | ’undefined’ |
| <head> | ::= | <functor>’(’<argspec> ’,’ <argspec>’)’ |
| | | <functor> |
| <argspec> | ::= | [<instantiation>]<argname>[’:’<type>] |
| <instantiation> | ::= | ’++’ | ’+’ | ’-’ | ’--’ | ’?’
| ’:’ | ’@’ | ’!’ |
| <type> | ::= | <term> |
The determinism values originate from Mercury. Their meaning
is explained in the table below. Informally, det is used
for deterministic transformations (e.g. arithmetic), semidet
for tests, nondet and multi for generators.
The
failure indicator is rarely used. It mostly appears in
hooks or the recovery goal of catch/3.
| Determinism | Predicate behaviour |
det | Succeeds exactly once
without a choice point |
semidet | Fails or Succeeds exactly once
without a choice-point |
failure | Always fails |
nondet | No constraints on the number of
times the predicate succeeds and whether or not it leaves choice-points
on the last success. |
multi | As nondet, but succeeds
at least one time. |
undefined | Well founded semantics third
value. See undefined/0. |
The meanings of the instantiation patterns for individual
arguments are:
| ++ | Argument is ground at call-time, i.e., the argument
does not contain a variable anywhere. |
| + | Argument is fully instantiated at call-time, to a term
that satisfies the type. This is not necessarily ground, e.g.,
the term
[_] is a list, although its only member is
unbound. |
| - | Argument is an output argument. It may be
unbound at call-time, or it may be bound to a term. In the latter case,
the predicate behaves as if the argument was unbound, and then unified
with that term after the goal succeeds. For example, the goal findall(X,
Goal, [T]) is good style and equivalent to findall(X, Goal,
Xs), Xs = [T]3The ISO
standard dictates that findall(X, Goal, 1) raises a type_error
exception, breaking this semantic relation. SWI-Prolog does not follow
the standard here. Determinism declarations assume that the
argument is a free variable at call-time. For the case where the
argument is bound or involved in constraints,
det effectively becomes semidet, and multi
effectively becomes nondet. |
| -- | Argument is unbound at call-time. Typically used by
predicates that create‘something’and return a handle to the
created object, such as open/3
which creates a stream. |
| ? | Argument is bound to a partial term of the
indicated type at call-time. Note that a variable is a partial term for
any type. |
| : | Argument is a meta-argument. Implies + |
| @ | Argument will not be further instantiated than it is
at call-time. Typically used for type tests. |
| ! | Argument contains a mutable structure that may be
modified using
setarg/3 or nb_setarg/3. |
Users should be aware that calling a predicate with arguments
instantiated in a way other than specified by one of the templates may
result in errors or unexpected behavior.
Developers should ensure that predicates are steadfast with
respect to output arguments (marked - in the template). This means that
instantiation of output arguments at call-time does not change the
semantics of the goal (it may be used for optimization, though). If this
steadfast behavior cannot be guaranteed, -- should be used instead.
In the current version, argument types are represented by an
arbitrary term without formal semantics. In future versions we may adopt
a formal type system that allows for runtime verification and static
type analysis
Hermenegildo,
2000, Mycroft &
O'Keefe, 1984, Jeffery et
al., 2000
Examples
%! length(+List:list, -Length:int) is det.
%! length(?List:list, -Length:int) is nondet.
%! length(?List:list, +Length:int) is det.
%
% True if List is a list of length Length.
%
% @compat iso
