/usr/lib/swi-prolog/doc/Manual/practical.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">

<HTML>
<HEAD>
<TITLE>SWI-Prolog 5.11.18 Reference Manual: Section 7.3</TITLE><LINK REL=home HREF="index.html">
<LINK REL=contents HREF="Contents.html">
<LINK REL=index HREF="DocIndex.html">
<LINK REL=summary HREF="summary.html">
<LINK REL=previous HREF="SyntaxAndSemantics.html">
<LINK REL=next HREF="debugging.html">
<STYLE type="text/css">
/* Style sheet for SWI-Prolog latex2html
*/

dd.defbody
{ margin-bottom: 1em;
}

dt.pubdef
{ background-color: #c5e1ff;
}

dt.multidef
{ background-color: #c8ffc7;
}

.bib dd
{ margin-bottom: 1em;
}

.bib dt
{ float: left;
margin-right: 1.3ex;
}

pre.code
{ margin-left: 1.5em;
margin-right: 1.5em;
border: 1px dotted;
padding-top: 5px;
padding-left: 5px;
padding-bottom: 5px;
background-color: #f8f8f8;
}

div.navigate
{ text-align: center;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
}

div.title
{ text-align: center;
padding-bottom: 1em;
font-size: 200%;
font-weight: bold;
}

div.author
{ text-align: center;
font-style: italic;
}

div.abstract
{ margin-top: 2em;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
margin-left: 10%; margin-right:10%;
}

div.abstract-title
{ text-align: center;
padding: 5px;
font-size: 120%;
font-weight: bold;
}

div.toc-h1
{ font-size: 200%;
font-weight: bold;
}

div.toc-h2
{ font-size: 120%;
font-weight: bold;
margin-left: 2em;
}

div.toc-h3
{ font-size: 100%;
font-weight: bold;
margin-left: 4em;
}

div.toc-h4
{ font-size: 100%;
margin-left: 6em;
}

span.sec-nr
{
}

span.sec-title
{
}

span.pred-ext
{ font-weight: bold;
}

span.pred-tag
{ float: right;
padding-top: 0.2em;
font-size: 80%;
font-style: italic;
color: #202020;
}

/* Footnotes */

sup.fn { color: blue; text-decoration: underline; }
span.fn-text { display: none; }
sup.fn span {display: none;}
sup:hover span
{ display: block !important;
position: absolute; top: auto; left: auto; width: 80%;
color: #000; background: white;
border: 2px solid;
padding: 5px; margin: 10px; z-index: 100;
font-size: smaller;
}
</STYLE>
</HEAD>
<BODY BGCOLOR="white">
<DIV class="navigate"><A class="nav" href="index.html"><IMG SRC="home.gif" BORDER=0 ALT="Home"></A>
<A class="nav" href="Contents.html"><IMG SRC="index.gif" BORDER=0 ALT="Contents"></A>
<A class="nav" href="DocIndex.html"><IMG SRC="yellow_pages.gif" BORDER=0 ALT="Index"></A>
<A class="nav" href="summary.html"><IMG SRC="info.gif" BORDER=0 ALT="Summary"></A>
<A class="nav" href="SyntaxAndSemantics.html"><IMG SRC="prev.gif" BORDER=0 ALT="Previous"></A>
<A class="nav" href="debugging.html"><IMG SRC="next.gif" BORDER=0 ALT="Next"></A>
</DIV>

<H2><A NAME="sec:7.3"><SPAN class="sec-nr">7.3</SPAN> <SPAN class="sec-title">CHR 
in SWI-Prolog Programs</SPAN></A></H2>

<A NAME="sec:practical"></A>

<H3><A NAME="sec:7.3.1"><SPAN class="sec-nr">7.3.1</SPAN> <SPAN class="sec-title">Embedding 
in Prolog Programs</SPAN></A></H3>

<P>The CHR constraints defined in a <CODE>.pl</CODE> file are associated 
with a module. The default module is <CODE>user</CODE>. One should never 
load different <CODE>.pl</CODE> files with the same CHR module name.

<H3><A NAME="sec:7.3.2"><SPAN class="sec-nr">7.3.2</SPAN> <SPAN class="sec-title">Constraint 
declaration</SPAN></A></H3>

<DL class="latex">
<DT class="pubdef"><A NAME="chr_constraint/1">:- <STRONG>chr_constraint</STRONG>(<VAR>+Specifier</VAR>)</A></DT>
<DD class="defbody">
Every constraint used in CHR rules has to be declared with a
<A NAME="idx:chrconstraint1:1349"></A><A class="pred" href="practical.html#chr_constraint/1">chr_constraint/1</A> 
declaration by the <EM>constraint specifier</EM>. For convenience 
multiple constraints may be declared at once with the same
<A class="pred" href="practical.html#chr_constraint/1">chr_constraint/1</A> 
declaration followed by a comma-separated list of constraint specifiers.

<P>A constraint specifier is, in its compact form, <TT><VAR>F</VAR>/<VAR>A</VAR></TT> 
where
<VAR>F</VAR> and <VAR>A</VAR> are respectively the functor name and 
arity of the constraint, e.g.:

<PRE class="code">
:- chr_constraint foo/1.
:- chr_constraint bar/2, baz/3.
</PRE>

<P>In its extended form, a constraint specifier is
<TT><VAR>c</VAR>(<VAR>A_1</VAR>, ... ,<VAR>A_n</VAR>)</TT> where <VAR>c</VAR> 
is the constraint's functor,
<VAR>n</VAR> its arity and the <VAR>A_i</VAR> are argument specifiers. 
An argument specifier is a mode, optionally followed by a type. E.g.

<PRE class="code">
:- chr_constraint get_value(+,?).
:- chr_constraint domain(?int, +list(int)), 
                  alldifferent(?list(int)).
</PRE>

<P></DD>
</DL>

<P><B>Modes</B> 

<P>A mode is one of:

<DL class="latex">
<DT><STRONG><CODE>-</CODE></STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint is 
always unbound.
</DD>
<DT><STRONG><CODE>+</CODE></STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint is 
always ground.
</DD>
<DT><STRONG><CODE>?</CODE></STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint can 
have any instantiation, which may change over time. This is the default 
value.
</DD>
</DL>

<P><B>Types</B> 

<P>A type can be a user-defined type or one of the built-in types. A 
type comprises a (possibly infinite) set of values. The type declaration 
for a constraint argument means that for every instance of that 
constraint the corresponding argument is only ever bound to values in 
that set. It does not state that the argument necessarily has to be 
bound to a value.

<P>The built-in types are:

<DL class="latex">
<DT><STRONG>int</STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint is an 
integer number.
</DD>
<DT><STRONG>dense_int</STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint is an 
integer that can be used as an array index. Note that if this argument 
takes values in <VAR>[0,n]</VAR>, the array takes
<VAR>O(n)</VAR> space.
</DD>
<DT><STRONG>float</STRONG></DT>
<DD class="defbody">
... a floating point number.
</DD>
<DT><STRONG>number</STRONG></DT>
<DD class="defbody">
... a number.
</DD>
<DT><STRONG>natural</STRONG></DT>
<DD class="defbody">
... a positive integer.
</DD>
<DT><STRONG>any</STRONG></DT>
<DD class="defbody">
The corresponding argument of every occurrence of the constraint can 
have any type. This is the default value.
</DD>
</DL>

<DL class="latex">
<DT class="pubdef"><A NAME="chr_type/1">:- <STRONG>chr_type</STRONG>(<VAR>+TypeDeclaration</VAR>)</A></DT>
<DD class="defbody">
User-defined types are algebraic data types, similar to those in Haskell 
or the discriminated unions in Mercury. An algebraic data type is 
defined using <A NAME="idx:chrtype1:1350"></A><A class="pred" href="practical.html#chr_type/1">chr_type/1</A>:

<PRE class="code">
:- chr_type type ---&gt; body. 
</PRE>

<P>If the type term is a functor of arity zero (i.e. one having zero 
arguments), it names a monomorphic type. Otherwise, it names a 
polymorphic type; the arguments of the functor must be distinct type 
variables. The body term is defined as a sequence of constructor 
definitions separated by semi-colons.

<P>Each constructor definition must be a functor whose arguments (if 
any) are types. Discriminated union definitions must be transparent: all 
type variables occurring in the body must also occur in the type.

<P>Here are some examples of algebraic data type definitions:

<PRE class="code">
:- chr_type color ---&gt; red ; blue ; yellow ; green.

:- chr_type tree ---&gt;  empty ; leaf(int) ; branch(tree, tree).

:- chr_type list(T) ---&gt; [] ; [T | list(T)].

:- chr_type pair(T1, T2) ---&gt; (T1 - T2).
</PRE>

<P>Each algebraic data type definition introduces a distinct type. Two 
algebraic data types that have the same bodies are considered to be 
distinct types (name equivalence).

<P>Constructors may be overloaded among different types: there may be 
any number of constructors with a given name and arity, so long as they 
all have different types.

<P>Aliases can be defined using ==. For example, if your program uses 
lists of lists of integers, you can define an alias as follows:

<PRE class="code">
:- chr_type lli == list(list(int)).
</PRE>

<P></DD>
</DL>

<P><B>Type Checking</B> 

<P>Currently two complementary forms of type checking are performed:
<OL class="latex">
<LI>Static type checking is always performed by the compiler. It is 
limited to CHR rule heads and CHR constraint calls in rule bodies.

<P>Two kinds of type error are detected. The first is where a variable 
has to belong to two types. For example, in the program:

<PRE class="code">
:-chr_type foo ---&gt; foo.
:-chr_type bar ---&gt; bar.

:-chr_constraint abc(?foo).
:-chr_constraint def(?bar).

foobar @ abc(X) &lt;=&gt; def(X).
</PRE>

<P>the variable <TT>X</TT> has to be of both type <TT>foo</TT> and <TT>bar</TT>. 
This is reported by the type clash error:

<PRE class="code">
CHR compiler ERROR:
    `--&gt; Type clash for variable _G5398 in rule foobar:
                expected type foo in body goal def(_G5398, _G5448)
                expected type bar in head def(_G5448, _G5398)
</PRE>

<P>The second kind of error is where a functor is used that does not 
belong to the declared type. For example in:

<PRE class="code">
:-chr_type foo ---&gt; foo.
:-chr_type bar ---&gt; bar.

:-chr_constraint abc(?foo).

foo @ abc(bar) &lt;=&gt; true.
</PRE>

<P>in the head of the rule <TT>bar</TT> appears where something of type <TT>foo</TT> 
is expected. This is reported as:

<PRE class="code">
CHR compiler ERROR:
    `--&gt; Invalid functor in head abc(bar) of rule foo:
                found `bar',
                expected type `foo'!
</PRE>

<P>No runtime overhead is incurred in static type checking.

<P>
<LI>Dynamic type checking checks at runtime, during program execution, 
whether the arguments of CHR constraints respect their declared types. 
The <A class="pred" href="coroutining.html#when/2">when/2</A> 
co-routining library is used to delay dynamic type checks until 
variables are instantiated.

<P>The kind of error detected by dynamic type checking is where a 
functor is used that does not belong to the declared type. E.g. for the 
program:

<PRE class="code">	
:-chr_type foo ---&gt; foo.

:-chr_constraint abc(?foo).
</PRE>

<P>we get the following error in an erroneous query:

<PRE class="code">
?- abc(bar).
ERROR: Type error: `foo' expected, found `bar' (CHR Runtime Type Error)
</PRE>

<P>Dynamic type checking is weaker than static type checking in the 
sense that it only checks the particular program execution at hand 
rather than all possible executions. It is stronger in the sense that it 
tracks types throughout the whole program.

<P>Note that it is enabled only in debug mode, as it incurs some (minor) 
runtime overhead.
</OL>

<H3><A NAME="sec:7.3.3"><SPAN class="sec-nr">7.3.3</SPAN> <SPAN class="sec-title">Compilation</SPAN></A></H3>

The SWI-Prolog CHR compiler exploits <A NAME="idx:termexpansion2:1351"></A><A class="pred" href="consulting.html#term_expansion/2">term_expansion/2</A> 
rules to translate the constraint handling rules to plain Prolog. These 
rules are loaded from the library <CODE>library(chr)</CODE>. They are 
activated if the compiled file has the <CODE>.chr</CODE> extension or 
after finding a declaration of the format below.

<PRE class="code">
:- chr_constraint ...
</PRE>

<P>It is advised to define CHR rules in a module file, where the module 
declaration is immediately followed by including the library(chr) 
library as exemplified below:

<PRE class="code">
:- module(zebra, [ zebra/0 ]).
:- use_module(library(chr)).

:- chr_constraint ...
</PRE>

<P>Using this style CHR rules can be defined in ordinary Prolog .pl 
files and the operator definitions required by CHR do not leak into 
modules where they might cause conflicts.

<P></BODY></HTML>
swi-prolog-nox 5.10.4-3ubuntu1 / usr / lib / swi-prolog / doc / Manual / practical.html
