<HTML>
<HEAD>
<!-- Created by texi2html 1.56k + clip patches and <A href="http://www.clip.dia.fi.upm.es/Software">lpdoc</A> from ciao.texi on 28 January 2007 -->
<LINK rel="stylesheet" href="ciao.css" type="text/css">
<TITLE>The Ciao Prolog System - Declaring regular types</TITLE>
</HEAD>
<BODY>
Go to the <A HREF="ciao_1.html">first</A>, <A HREF="ciao_60.html">previous</A>, <A HREF="ciao_62.html">next</A>, <A HREF="ciao_241.html">last</A> section, <A HREF="ciao_toc.html">table of contents</A>.
<P><HR><P>
<H1><A NAME="SEC275" HREF="ciao_toc.html#TOC275">Declaring regular types</A></H1>
<P>
<A NAME="IDX3986"></A>
<P>
<STRONG>Author(s):</STRONG> Manuel Hermenegildo, Pedro Lopez, Francisco Bueno.
<P>
<STRONG>Version:</STRONG> 1.10#7 (2006/4/26, 19:22:13 CEST)
<P>
<STRONG>Version of last change:</STRONG> 1.5#9 (1999/12/9, 21:57:42 MET)
<P>
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
<A NAME="IDX3987"></A>
regular type definitions in source code. Regular types are just properties which have the additional characteristic of being
<A NAME="IDX3988"></A>
regular types (
<A NAME="IDX3989"></A>
<CODE>basic_props:regtype/1</CODE>).
<P>
For example, this library package allows writing:
<PRE>
:- regtype tree(X) # "<CODE>X</CODE> is a tree.".
</PRE>
<P>
instead of the more combersome:
<PRE>
:- prop tree(X) + regtype # "<CODE>X</CODE> is a tree.".
</PRE>
<P>
Regular types can be used as properties to describe predicates and play an essential role in program debugging (see the Ciao Prolog preprocessor (<CODE>ciaopp</CODE>) manual).
<P>
In this chapter we explain some general considerations worth taking into account when writing properties in general, not just regular types. The exact
<A NAME="IDX3990"></A>
syntax of regular types is also described.
<P>
<UL>
<LI><A HREF="ciao_61.html#SEC276">Defining properties</A>
<LI><A HREF="ciao_61.html#SEC277">Usage and interface (regtypes)</A>
<LI><A HREF="ciao_61.html#SEC278">Documentation on new declarations (regtypes)</A>
</UL>
<H2><A NAME="SEC276" HREF="ciao_toc.html#TOC276">Defining properties</A></H2>
<P>
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., <CODE>calls/1</CODE>, <CODE>success/1</CODE>, and the like) are called
<A NAME="IDX3991"></A>
<A NAME="IDX3992"></A>
<EM>properties of execution states</EM>. Properties used in assertions related to computations (i.e., <CODE>comp/1</CODE>) are called
<A NAME="IDX3993"></A>
<A NAME="IDX3994"></A>
<EM>properties of computations</EM>. Different considerations apply when writing a property of the former or of the later kind.
<P>
Consider a definition of the predicate <CODE>string_concat/3</CODE> which concatenates two character strings (represented as lists of ASCII codes):
<PRE>
string_concat([],L,L).
string_concat([X|Xs],L,[X|NL]):- string_concat(Xs,L,NL).
</PRE>
<P>
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 <EM>instantiated</EM> to a list of integers" (let us call this property <CODE>instantiated_to_intlist/1</CODE>), 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 <CODE>compatible_with_intlist/1</CODE>). For example, <CODE>instantiated_to_intlist/1</CODE> should be true for the terms <CODE>[]</CODE> and <CODE>[1,2]</CODE>, but should not for <CODE>X</CODE>, <CODE>[a,2]</CODE>, and <CODE>[X,2]</CODE>. In turn, <CODE>compatible_with_intlist/1</CODE> should be true for <CODE>[]</CODE>, <CODE>X</CODE>, <CODE>[1,2]</CODE>, and <CODE>[X,2]</CODE>, but should not be for <CODE>[X|1]</CODE>, <CODE>[a,2]</CODE>, and <CODE>1</CODE>. We refer to properties such as <CODE>instantiated_to_intlist/1</CODE> above as
<A NAME="IDX3995"></A>
<A NAME="IDX3996"></A>
<EM>instantiation properties</EM> and to those such as <CODE>compatible_with_intlist/1</CODE> as
<A NAME="IDX3997"></A>
<A NAME="IDX3998"></A>
<EM>compatibility properties</EM> (corresponding to the traditional notions of "instantiation types" and "compatibility types").
<P>
It turns out that both of these notions are quite useful in practice. In the example above, we probably would like to use <CODE>compatible_with_intlist/1</CODE> to state that on success of <CODE>string_concat/3</CODE> all three argument must be compatible with lists of integers in an assertion like:
<PRE>
:- success string_concat(A,B,C) => ( compatible_with_intlist(A),
compatible_with_intlist(B),
compatible_with_intlist(C) ).
</PRE>
<P>
With this assertion, no error will be flagged for a call to <CODE>string_concat/3</CODE> such as <CODE>string_concat([20],L,R)</CODE>, which on success produces the resulting atom <CODE>string_concat([20],L,[20|L])</CODE>, but a call <CODE>string_concat([],a,R)</CODE> would indeed flag an error.
<P>
On the other hand, and assuming that we are running on a Prolog system, we would probably like to use <CODE>instantiated_to_intlist/1</CODE> for <CODE>sumlist/2</CODE> as follows:
<PRE>
:- calls sumlist(L,N) : instantiated_to_intlist(L).
sumlist([],0).
sumlist([X|R],S) :- sumlist(R,PS), S is PS+X.
</PRE>
<P>
to describe the type of calls for which the program has been designed, i.e., those in which the first argument of <CODE>sumlist/2</CODE> is indeed a list of integers.
<P>
The property <CODE>instantiated_to_intlist/1</CODE> might be written as in the following (Prolog) definition:
<PRE>
:- 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).
</PRE>
<P>
(Recall that the Prolog builtin <CODE>integer/1</CODE> itself implements an instantiation check, failing if called with a variable as the argument.)
<P>
The property <CODE>compatible_with_intlist/1</CODE> might in turn be written as follows (also in Prolog):
<PRE>
:- 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).
</PRE>
<P>
Note that these predicates meet the criteria for being properties and thus the <CODE>prop/1</CODE> declaration is correct.
<P>
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:
<PRE>
intlist([]).
intlist([X|R]) :- int(X), intlist(R).
</PRE>
<P>
(Incidentally, note that the above definition, provided that it suits the requirements for being a property and that <CODE>int/1</CODE> is a regular type, meets the criteria for being a regular type. Thus, it could be declared <CODE>:- regtype intlist/1</CODE>.)
<P>
But note that (independently of the definition of <CODE>int/1</CODE>) the definition above is not the correct instantiation check, since it would succeed for a call such as <CODE>intlist(X)</CODE>. 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 <CODE>intlist(X)</CODE> it would bind <CODE>X</CODE> to <CODE>[]</CODE>). In practice, it is convenient to provide some run-time support to aid in this task.
<P>
The run-time support of the Ciao system (see section <A HREF="ciao_65.html#SEC288">Run-time checking of assertions</A>) 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:
<PRE>
:- calls sumlist(L,N) : intlist(L).
</PRE>
<P>
has the desired effect. Also, the same properties can often be used as compatibility checks by writing them in the assertions as <CODE>compat(Property)</CODE> (<CODE>basic_props:compat/1</CODE>). Thus, writing:
<PRE>
:- success string_concat(A,B,C) => ( compat(intlist(A)),
compat(intlist(B)),
compat(intlist(C)) ).
</PRE>
<P>
also has the desired effect.
<P>
As a general rule, the properties that can be used directly for checking for compatibility should be <EM>downwards closed</EM>, i.e., once they hold they will keep on holding in every state accessible in forwards execution. There are certain predicates which are inherently <EM>instantiation</EM> checks and should not be used as <EM>compatibility</EM> properties nor appear in the definition of a property that is to be used with <CODE>compat</CODE>. Examples of such predicates (for Prolog) are <CODE>==</CODE>, <CODE>ground</CODE>, <CODE>nonvar</CODE>, <CODE>integer</CODE>, <CODE>atom</CODE>, <CODE>></CODE>, etc. as they require a certain instantiation degree of their arguments in order to succeed.
<P>
In contrast with properties of execution states, <EM>properties of computations</EM> refer to the entire execution of the call(s) that the assertion relates to. One such property is, for example, <CODE>not_fail/1</CODE> (note that although it has been used as in <CODE>:- comp append(Xs,Ys,Zs) + not_fail</CODE>, it is in fact read as <CODE>not_fail(append(Xs,Ys,Zs))</CODE>; see <CODE>assertions_props:complex_goal_property/1</CODE>). 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 <CODE>not_fail/1</CODE> for run-time checking:
<PRE>
not_fail(Goal):-
if( call(Goal),
true, %% then
warning(Goal) ). %% else
</PRE>
<P>
where the <CODE>warning/1</CODE> (library) predicate simply prints a warning message.
<P>
In this simple case, implementation of the predicate is not very difficult using the (non-standard) <CODE>if/3</CODE> builtin predicate present in many Prolog systems.
<P>
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.
<H2><A NAME="SEC277" HREF="ciao_toc.html#TOC277">Usage and interface (<CODE>regtypes</CODE>)</A></H2>
<div class="cartouche">
<UL>
<LI><STRONG>Library usage:</STRONG>
<CODE>:- use_package(regtypes).</CODE>
or
<CODE>:- module(...,...,[regtypes]).</CODE>
<LI><STRONG>New operators defined:</STRONG>
<A NAME="IDX3999"></A>
<CODE>regtype/1</CODE> [1150,fx],
<A NAME="IDX4000"></A>
<CODE>regtype/2</CODE> [1150,xfx].
<LI><STRONG>New declarations defined:</STRONG>
<A NAME="IDX4001"></A>
<CODE>regtype/1</CODE>,
<A NAME="IDX4002"></A>
<CODE>regtype/2</CODE>.
<LI><STRONG>Other modules used:</STRONG>
<UL>
<LI><EM>System library modules:</EM>
<A NAME="IDX4003"></A>
<CODE>assertions/assertions_props</CODE>.
</UL>
</UL>
</div class="cartouche">
<H2><A NAME="SEC278" HREF="ciao_toc.html#TOC278">Documentation on new declarations (<CODE>regtypes</CODE>)</A></H2>
<P>
<A NAME="IDX4004"></A>
<A NAME="IDX4005"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>regtype/1:</B>
<DD><A NAME="IDX4006"></A>
<P>
<A NAME="IDX4007"></A>
<A NAME="IDX4008"></A>
This assertion is similar to a pred assertion but it flags that the predicate being documented is also a "
<A NAME="IDX4009"></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 <EM>regular programs</EM>.
<P>
A regular program is defined by a set of clauses, each of the form:
<PRE>
p(x, v_1, ..., v_n) :- body_1, ..., body_k.
</PRE>
<P>
where:
<OL>
<LI><CODE>x</CODE> is a term whose variables (which are called <EM>term variables</EM>) are unique, i.e., it is not allowed to introduce equality constraints between the variables of <CODE>x</CODE>.
For example, <CODE>p(f(X, Y)) :- ...</CODE> is valid, but <CODE>p(f(X, X)) :- ...</CODE> is not.
<LI>in all clauses defining <CODE>p/n+1</CODE> the terms <CODE>x</CODE> do not unify except maybe for one single clause in which <CODE>x</CODE> is a variable.
<LI><CODE>n</CODE> >= 0 and <CODE>p/n</CODE> is a
<A NAME="IDX4010"></A>
<A NAME="IDX4011"></A>
<EM>parametric type functor</EM> (whereas the predicate defined by the clauses is <CODE>p/n</CODE>+1).
<LI><CODE>v_1</CODE>, ..., <CODE>v_n</CODE> are unique variables, which are called <EM>parametric variables</EM>.
<LI>Each <CODE>body_i</CODE> is of the form:
<OL>
<LI><CODE>t(z)</CODE> where <CODE>z</CODE> is one of the <EM>term variables</EM> and <CODE>t</CODE> is a <EM>regular type expression</EM>;
<LI><CODE>q(y, t_1, ..., t_m)</CODE> where <CODE>m</CODE> >= 0, <CODE>q/m</CODE> is a <EM>parametric type functor</EM>, not in the set of functors <CODE>=/2</CODE>, <CODE>^/2</CODE>, <CODE>./3</CODE>.
<CODE>t_1, ..., t_m</CODE> are <EM>regular type expressions</EM>, and <CODE>y</CODE> is a <EM>term variable</EM>.
</OL>
<LI>Each term variable occurs at most once in the clause's body (and should be as the first argument of a literal).
</OL>
<P>
A
<A NAME="IDX4012"></A>
<A NAME="IDX4013"></A>
<EM>regular type expression</EM> is either a parametric variable or a parametric type functor applied to some of the parametric variables (but
<A NAME="IDX4014"></A>
regular type abstractions might also be used in some cases, see @xref{Meta-properties}).
<P>
A parametric type functor is a regular type, defined by a regular program, or a basic type. Basic types are defined in section <A HREF="ciao_18.html#SEC135">Basic data types and properties</A>.
<P>
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.
<P>
<STRONG>Usage:</STRONG> :- <CODE>regtype(AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P>
<A NAME="IDX4015"></A>
<A NAME="IDX4016"></A>
<DL>
<DT><span class="define">DECLARATION:</span> <B>regtype/2:</B>
<DD><A NAME="IDX4017"></A>
<P>
<A NAME="IDX4018"></A>
<A NAME="IDX4019"></A>
This assertion is similar to a
<A NAME="IDX4020"></A>
<CODE>regtype/1</CODE> assertion but it is explicitely qualified. Non-qualified
<A NAME="IDX4021"></A>
<CODE>regtype/1</CODE> assertions are assumed the qualifier <CODE>check</CODE>. Note that checking regular type definitions should be done with the <CODE>ciaopp</CODE> preprocessor.
<P>
<STRONG>Usage:</STRONG> :- <CODE>regtype(AssertionStatus, AssertionBody)</CODE>.
<UL>
<LI><EM>The following properties should hold at call time:</EM>
<CODE>AssertionStatus</CODE> is an acceptable status for an assertion.
(<CODE>assertions_props:assrt_status/1</CODE>)
<CODE>AssertionBody</CODE> is an assertion body.
(<CODE>assertions_props:assrt_body/1</CODE>)
</UL>
</DL>
<P><HR><P>
Go to the <A HREF="ciao_1.html">first</A>, <A HREF="ciao_60.html">previous</A>, <A HREF="ciao_62.html">next</A>, <A HREF="ciao_241.html">last</A> section, <A HREF="ciao_toc.html">table of contents</A>.
</BODY>
</HTML>
