Author(s): Manuel Hermenegildo, Pedro Lopez, Francisco Bueno.
Version: 1.10#7 (2006/4/26, 19:22:13 CEST)
Version of last change: 1.5#9 (1999/12/9, 21:57:42 MET)
This library package adds some new declaration definitions and new operator definitions to user programs. These new declarations and operators provide some very simple syntactic sugar to support
regular type definitions in source code. Regular types are just properties which have the additional characteristic of being
regular types (
basic_props:regtype/1).
For example, this library package allows writing:
:- regtype tree(X) # "X is a tree.".
instead of the more combersome:
:- prop tree(X) + regtype # "X is a tree.".
Regular types can be used as properties to describe predicates and play an essential role in program debugging (see the Ciao Prolog preprocessor (ciaopp) manual).
In this chapter we explain some general considerations worth taking into account when writing properties in general, not just regular types. The exact syntax of regular types is also described.
Given the classes of assertions in the Ciao assertion language, there are two fundamental classes of properties. Properties used in assertions which refer to execution states (i.e., calls/1, success/1, and the like) are called
properties of execution states. Properties used in assertions related to computations (i.e., comp/1) are called
properties of computations. Different considerations apply when writing a property of the former or of the later kind.
Consider a definition of the predicate string_concat/3 which concatenates two character strings (represented as lists of ASCII codes):
string_concat([],L,L). string_concat([X|Xs],L,[X|NL]):- string_concat(Xs,L,NL).
Assume that we would like to state in an assertion that each argument "is a list of integers." However, we must decide which one of the following two possibilities we mean exactly: "the argument is instantiated to a list of integers" (let us call this property instantiated_to_intlist/1), or "if any part of the argument is instantiated, this instantiation must be compatible with the argument being a list of integers" (we will call this property compatible_with_intlist/1). For example, instantiated_to_intlist/1 should be true for the terms [] and [1,2], but should not for X, [a,2], and [X,2]. In turn, compatible_with_intlist/1 should be true for [], X, [1,2], and [X,2], but should not be for [X|1], [a,2], and 1. We refer to properties such as instantiated_to_intlist/1 above as
instantiation properties and to those such as compatible_with_intlist/1 as
compatibility properties (corresponding to the traditional notions of "instantiation types" and "compatibility types").
It turns out that both of these notions are quite useful in practice. In the example above, we probably would like to use compatible_with_intlist/1 to state that on success of string_concat/3 all three argument must be compatible with lists of integers in an assertion like:
:- success string_concat(A,B,C) => ( compatible_with_intlist(A),
compatible_with_intlist(B),
compatible_with_intlist(C) ).
With this assertion, no error will be flagged for a call to string_concat/3 such as string_concat([20],L,R), which on success produces the resulting atom string_concat([20],L,[20|L]), but a call string_concat([],a,R) would indeed flag an error.
On the other hand, and assuming that we are running on a Prolog system, we would probably like to use instantiated_to_intlist/1 for sumlist/2 as follows:
:- calls sumlist(L,N) : instantiated_to_intlist(L). sumlist([],0). sumlist([X|R],S) :- sumlist(R,PS), S is PS+X.
to describe the type of calls for which the program has been designed, i.e., those in which the first argument of sumlist/2 is indeed a list of integers.
The property instantiated_to_intlist/1 might be written as in the following (Prolog) definition:
:- prop instantiated_to_intlist/1.
instantiated_to_intlist(X) :-
nonvar(X), instantiated_to_intlist_aux(X).
instantiated_to_intlist_aux([]).
instantiated_to_intlist_aux([X|T]) :-
integer(X), instantiated_to_intlist(T).
(Recall that the Prolog builtin integer/1 itself implements an instantiation check, failing if called with a variable as the argument.)
The property compatible_with_intlist/1 might in turn be written as follows (also in Prolog):
:- prop compatible_with_intlist/1.
compatible_with_intlist(X) :- var(X).
compatible_with_intlist(X) :-
nonvar(X), compatible_with_intlist_aux(X).
compatible_with_intlist_aux([]).
compatible_with_intlist_aux([X|T]) :-
int_compat(X), compatible_with_intlist(T).
int_compat(X) :- var(X).
int_compat(X) :- nonvar(X), integer(X).
Note that these predicates meet the criteria for being properties and thus the prop/1 declaration is correct.
Ensuring that a property meets the criteria for "not affecting the computation" can sometimes make its coding somewhat tedious. In some ways, one would like to be able to write simply:
intlist([]). intlist([X|R]) :- int(X), intlist(R).
(Incidentally, note that the above definition, provided that it suits the requirements for being a property and that int/1 is a regular type, meets the criteria for being a regular type. Thus, it could be declared :- regtype intlist/1.)
But note that (independently of the definition of int/1) the definition above is not the correct instantiation check, since it would succeed for a call such as intlist(X). In fact, it is not strictly correct as a compatibility property either, because, while it would fail or succeed as expected, it would perform instantiations (e.g., if called with intlist(X) it would bind X to []). In practice, it is convenient to provide some run-time support to aid in this task.
The run-time support of the Ciao system (see section Run-time checking of assertions) ensures that the execution of properties is performed in such a way that properties written as above can be used directly as instantiation checks. Thus, writing:
:- calls sumlist(L,N) : intlist(L).
has the desired effect. Also, the same properties can often be used as compatibility checks by writing them in the assertions as compat(Property) (basic_props:compat/1). Thus, writing:
:- success string_concat(A,B,C) => ( compat(intlist(A)),
compat(intlist(B)),
compat(intlist(C)) ).
also has the desired effect.
As a general rule, the properties that can be used directly for checking for compatibility should be downwards closed, i.e., once they hold they will keep on holding in every state accessible in forwards execution. There are certain predicates which are inherently instantiation checks and should not be used as compatibility properties nor appear in the definition of a property that is to be used with compat. Examples of such predicates (for Prolog) are ==, ground, nonvar, integer, atom, >, etc. as they require a certain instantiation degree of their arguments in order to succeed.
In contrast with properties of execution states, properties of computations refer to the entire execution of the call(s) that the assertion relates to. One such property is, for example, not_fail/1 (note that although it has been used as in :- comp append(Xs,Ys,Zs) + not_fail, it is in fact read as not_fail(append(Xs,Ys,Zs)); see assertions_props:complex_goal_property/1). For this property, which should be interpreted as "execution of the predicate either succeeds at least once or loops," we can use the following predicate not_fail/1 for run-time checking:
not_fail(Goal):-
if( call(Goal),
true, %% then
warning(Goal) ). %% else
where the warning/1 (library) predicate simply prints a warning message.
In this simple case, implementation of the predicate is not very difficult using the (non-standard) if/3 builtin predicate present in many Prolog systems.
However, it is not so easy to code predicates which check other properties of the computation and we may in general need to program a meta-interpreter for this purpose.
regtypes)regtypes)This assertion is similar to a pred assertion but it flags that the predicate being documented is also a " regular type." This allows for example checking whether it is in the class of types supported by the type checking and inference modules. Currently, types are properties whose definitions are regular programs.
A regular program is defined by a set of clauses, each of the form:
p(x, v_1, ..., v_n) :- body_1, ..., body_k.
where:
x is a term whose variables (which are called term variables) are unique, i.e., it is not allowed to introduce equality constraints between the variables of x.
For example, p(f(X, Y)) :- ... is valid, but p(f(X, X)) :- ... is not.
p/n+1 the terms x do not unify except maybe for one single clause in which x is a variable.
n >= 0 and p/n is a
parametric type functor (whereas the predicate defined by the clauses is p/n+1).
v_1, ..., v_n are unique variables, which are called parametric variables.
body_i is of the form:
t(z) where z is one of the term variables and t is a regular type expression;
q(y, t_1, ..., t_m) where m >= 0, q/m is a parametric type functor, not in the set of functors =/2, ^/2, ./3.
t_1, ..., t_m are regular type expressions, and y is a term variable.
A regular type expression is either a parametric variable or a parametric type functor applied to some of the parametric variables (but regular type abstractions might also be used in some cases, see @xref{Meta-properties}).
A parametric type functor is a regular type, defined by a regular program, or a basic type. Basic types are defined in section Basic data types and properties.
The set of types is thus a well defined subset of the set of properties. Note that types can be used to describe characteristics of arguments in assertions and they can also be executed (called) as any other predicates.
Usage: :- regtype(AssertionBody).
AssertionBody is an assertion body.
(assertions_props:assrt_body/1)
This assertion is similar to a
regtype/1 assertion but it is explicitely qualified. Non-qualified
regtype/1 assertions are assumed the qualifier check. Note that checking regular type definitions should be done with the ciaopp preprocessor.
Usage: :- regtype(AssertionStatus, AssertionBody).
AssertionStatus is an acceptable status for an assertion.
(assertions_props:assrt_status/1)
AssertionBody is an assertion body.
(assertions_props:assrt_body/1)
Go to the first, previous, next, last section, table of contents.