Classical Prolog modes

Author(s): Manuel Hermenegildo.

This package defines a number of modes which are frequently useful in programs when describing predicates, e.g., via pred assertions (or doccomments, see below). They correspond to the modes used in many classical Prolog texts and code as documentation, with some additions. In Ciao these modes are actually syntactic sugar for assertions, so that they can be checked either statically or dynamically. Note that some of these modes use the same symbol as one of the basicmodes and isomodes packages (see Some basic Prolog modes and ISO-Prolog modes) but have in some cases subtly different meaning.

As an example, the following declaration:

:- pred is(-,+).

Expresses that is/2 should be called with the second argument bound and it will bind the first argument. Also:

:- pred is(-num,+arithexpression).

(more precise than the above), expresses that is/2 should be called with the second argument instantiated to an arithmetic expression and that on success it will bind the first argument to a number. The argument of a mode as above can be any property, including, e.g., regular types.

The first declaration is equivalent to (and is in fact translated to) the assertion:

:- pred is(X,Y) : nonvar(Y) => nonvar(X).

and the second one to:

:- pred is(X,Y) : arithexpression(Y) => num(X).

Modes can also be included inside comments in markdown format (see the doccomments and markdown libraries). For example:

%! pred is(-,+):
%  Evaluates the expression in the second argument
%  and binds the first argument with the result.

which are also translated to the corresponding assertions.

Usage and interface

Library usage:
:- use_package(modes). or :- module(...,...,[modes]).
New operators defined:
?/1 [500,fx], @/1 [500,fx].
New modes defined:
+/1, -/1, --/1, ?/1, @/1, in/1, ++/1, out/1, go/1, +/2, -/2, --/2, ?/2, @/2, in/2, ++/2, out/2, go/2.
Implicit imports:
- System library modules:
  meta_props.
- Packages:
  prelude, initial, condcomp, assertions, assertions/assertions_basic, metaprops, hiord.

Documentation on new modes

MODE+/1

The argument should be bound (nonvar) when the predicate is called. For example:

:- pred + > +.

expresses that both arguments of >/2 should be bound when the predicate is called.

Usage:+A

The following properties are added at call time:
(term_typing:nonvar/1)A is currently a term which is not a free variable.

MODE-/1

The argument is an output argument. It may be bound or not at call time. It will be bound (nonvar) if the predicate succeeds.

Usage:-A

The following properties are added upon exit:
(term_typing:nonvar/1)A is currently a term which is not a free variable.

MODE--/1

The argument should be a free variable (i.e., unbound) when the predicate is called.

Usage:--A

The following properties are added at call time:
(term_typing:var/1)A is a free variable.

MODE?/1

No information is given on this argument.

MODE@/1

The argument will not be further instantiated, i.e., will not be more instantiated than when the predicate is called.

Usage:@(A)

The following properties are added globally:
(basic_props:not_further_inst/2)A is not further instantiated.

MODEin/1

The argument is ground at call time.

Usage:in(A)

The following properties are added at call time:
(term_typing:ground/1)A is currently ground (it contains no variables).
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODE++/1

Same as in: the argument is ground at call time.

Usage:++A

The following properties are added at call time:
(term_typing:ground/1)A is currently ground (it contains no variables).
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODEout/1

The argument is a variable when the predicate is called and will be ground if the predicate succeeds.

Usage:out(A)

The following properties are added at call time:
(term_typing:var/1)A is a free variable.
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODEgo/1

The argument is ground by the predicate, if it succeeds.

Usage:go(A)

The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODE+/2

This argument should be instantiated when the predicate is called. For example:

:- pred +arithexpression > +arithexpression.

expresses that both arguments of >/2 should be bound to arithmetic expressions (have the arithexpression property) when the predicate is called.

Usage:A+P

The following properties are added at call time:
(term_typing:nonvar/1)A is currently a term which is not a free variable.
(meta_props:call/2)A has property P.

MODE-/2

The argument is an output argument. It may be bound or not at call time. It will be instantiated to a term that has the indicated type or property if the predicate succeeds. For example, this assertion:

:- pred length(-list,-int).

expresses that length/2 can be called in any mode, but on output the second argument will be instantiated to a number and the first one will be instantiated to a list. Note that this does not mean that the list will be ground, but rather that it will be a complete list but whose elements can be any term, including variables (see the discussion of instantitation and compatibility types in Declaring regular types.

Usage:A-P

The following properties are added upon exit:
(term_typing:nonvar/1)A is currently a term which is not a free variable.
(meta_props:call/2)A has property P.

MODE--/2

The argument should be a free variable (i.e., unbound) when the predicate is called and will be bound to a term that has the indicated type or property in general, if the predicate succeeds.

Usage:--(A,P)

The following properties are added at call time:
(term_typing:var/1)A is a free variable.
The following properties are added upon exit:
(meta_props:call/2)A has property P.

MODE?/2

The argument can be a variable or, if it is instantiated, it is to a term that is compatible with the indicated type or property.

Usage:?(A,P)

Call and exit are compatible with:
(meta_props:call/2)A has property P.

MODE@/2

The argument will not be further instantiated, i.e., will not be more instantiated than when the predicate is called, and the term is compatible with the indicated type or property.

Usage:@(A,P)

Call and exit are compatible with:
(meta_props:call/2)A has property P.
The following properties are added globally:
(basic_props:not_further_inst/2)A is not further instantiated.

MODEin/2

The argument is ground at call time and is compatible with the indicated type or property.

Usage:in(A,P)

The following properties are added at call time:
(term_typing:ground/1)A is currently ground (it contains no variables).
(meta_props:call/2)A has property P.
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODE++/2

Same as in: the argument is ground at call time and is compatible with the indicated type or property.

Usage:++(A,P)

The following properties are added at call time:
(term_typing:ground/1)A is currently ground (it contains no variables).
(meta_props:call/2)A has property P.
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).

MODEout/2

The argument is a variable when the predicate is called and will be bound to a ground term that is compatible with the indicated type or property, if the predicate succeeds.

Usage:out(A,P)

The following properties are added at call time:
(term_typing:var/1)A is a free variable.
The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).
(meta_props:call/2)A has property P.

MODEgo/2

The argument is ground by the predicate to a ground term that is compatible with the indicated type or property, if the predicate succeeds.

Usage:go(A,P)

The following properties are added upon exit:
(term_typing:ground/1)A is currently ground (it contains no variables).
(meta_props:call/2)A has property P.