update documentation.
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1434 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
This commit is contained in:
parent
61d9980cf3
commit
5cfad07c92
@ -37,10 +37,10 @@ clpbn_not_var_member([V1|Vs], V) :- V1 \== V,
|
||||
clpbn_not_var_member(Vs, V).
|
||||
|
||||
|
||||
sort_vars_by_key(AVars, SortedAVars, Keys) :-
|
||||
sort_vars_by_key(AVars, SortedAVars, UnifiableVars) :-
|
||||
get_keys(AVars, KeysVars),
|
||||
keysort(KeysVars, KVars),
|
||||
merge_same_key(KVars, SortedAVars, Keys).
|
||||
merge_same_key(KVars, SortedAVars, [], UnifiableVars).
|
||||
|
||||
get_keys([], []).
|
||||
get_keys([V|AVars], [K-V|KeysVars]) :-
|
||||
@ -49,15 +49,24 @@ get_keys([V|AVars], [K-V|KeysVars]) :-
|
||||
get_keys([_|AVars], KeysVars) :- % may be non-CLPBN vars.
|
||||
get_keys(AVars, KeysVars).
|
||||
|
||||
merge_same_key([], [], []).
|
||||
merge_same_key([K1-V1|KVs], [V1|Vs], [K1|Ks]) :-
|
||||
eat_same_key(KVs,K1,V1,RKVs),
|
||||
merge_same_key(RKVs, Vs, Ks).
|
||||
|
||||
eat_same_key([K-V|KVs],K,V,RKVs) :- !,
|
||||
eat_same_key(KVs,K,V,RKVs).
|
||||
eat_same_key(KVs,_,_,KVs).
|
||||
merge_same_key([], [], _, []).
|
||||
merge_same_key([K1-V1,K2-V2|Vs], SortedAVars, Ks, UnifiableVars) :-
|
||||
K1 == K2, !, V1 = V2,
|
||||
merge_same_key([K1-V1|Vs], SortedAVars, Ks, UnifiableVars).
|
||||
merge_same_key([K1-V1,K2-V2|Vs], [V1|SortedAVars], Ks, [K1|UnifiableVars]) :-
|
||||
(in_keys(K1, Ks) ; \+ \+ K1 == K2), !,
|
||||
add_to_keys(K1, Ks, NKs),
|
||||
merge_same_key([K2-V2|Vs], SortedAVars, NKs, UnifiableVars).
|
||||
merge_same_key([K-V|Vs], [V|SortedAVars], Ks, UnifiableVars) :-
|
||||
add_to_keys(K, Ks, NKs),
|
||||
merge_same_key(Vs, SortedAVars, NKs, UnifiableVars).
|
||||
|
||||
in_keys(K1,[K|_]) :- \+ \+ K1 = K, !.
|
||||
in_keys(K1,[_|Ks]) :-
|
||||
in_keys(K1,Ks).
|
||||
|
||||
add_to_keys(K1, Ks, Ks) :- ground(K1), !.
|
||||
add_to_keys(K1, Ks, [K1|Ks]).
|
||||
|
||||
sort_vars_by_key_and_parents(AVars, SortedAVars, UnifiableVars) :-
|
||||
get_keys_and_parents(AVars, KeysVars),
|
||||
|
@ -297,7 +297,7 @@ divide_by_sum([P|Ps0],Sum,[PN|Ps]) :-
|
||||
% what is actually output
|
||||
%
|
||||
attribute_goal(V, G) :-
|
||||
get_atts(V, [posterior(Vs,Vals,Ps,AllDiffs)]), !,
|
||||
get_atts(V, [posterior(Vs,Vals,Ps,AllDiffs)]),
|
||||
massage_out(Vs, Vals, Ps, G, AllDiffs, V).
|
||||
|
||||
massage_out([], Ev, _, V=Ev, _, V) :- !.
|
||||
|
11
Makefile.in
11
Makefile.in
@ -184,6 +184,9 @@ PL_SOURCES= \
|
||||
$(srcdir)/pl/utils.yap \
|
||||
$(srcdir)/pl/yapor.yap $(srcdir)/pl/yio.yap
|
||||
|
||||
YAPDOCS=$(srcdir)/docs/yap.tex $(srcdir)/docs/chr.tex \
|
||||
$(srcdir)/docs/clpr.tex $(srcdir)/docs/swi.tex
|
||||
|
||||
ENGINE_OBJECTS = \
|
||||
agc.o absmi.o adtdefs.o alloc.o amasm.o analyst.o arrays.o \
|
||||
arith0.o arith1.o arith2.o attvar.o bb.o \
|
||||
@ -616,7 +619,7 @@ install_info:
|
||||
|
||||
info: yap.info
|
||||
|
||||
yap.info: $(srcdir)/docs/yap.tex
|
||||
yap.info: $(YAPDOCS)
|
||||
$(MAKEINFO) $(srcdir)/docs/yap.tex
|
||||
|
||||
html: yap.html
|
||||
@ -626,17 +629,17 @@ yap.html: $(srcdir)/docs/yap.tex
|
||||
|
||||
dvi: yap.dvi
|
||||
|
||||
yap.dvi: $(srcdir)/docs/yap.tex
|
||||
yap.dvi: $(YAPDOCS)
|
||||
$(TEXI2DVI) $(srcdir)/docs/yap.tex
|
||||
|
||||
ps: yap.ps
|
||||
|
||||
yap.ps: $(srcdir)/docs/yap.dvi
|
||||
yap.ps: $(YAPDOCS)
|
||||
dvips -o yap.ps $(srcdir)/docs/yap
|
||||
|
||||
pdf: yap.pdf
|
||||
|
||||
yap.pdf: $(srcdir)/docs/yap.tex
|
||||
yap.pdf: $(YAPDOCS)
|
||||
$(TEXI2PDF) $(srcdir)/docs/yap.tex
|
||||
|
||||
clean_docs:
|
||||
|
@ -16,6 +16,8 @@
|
||||
|
||||
<h2>Yap-5.1.0:</h2>
|
||||
<ul>
|
||||
<li> NEW: update documentation to support new CLP(R) and CHR packages. </li>
|
||||
<li> FIXED: regression in clpbn/utils.yap. </li>
|
||||
<li> NEW: put_attrs/2. </li>
|
||||
<li> FIXED: don't install CLP unless coroutining && rational trees are
|
||||
active. </li>
|
||||
|
597
docs/chr.tex
Normal file
597
docs/chr.tex
Normal file
@ -0,0 +1,597 @@
|
||||
@chapter CHR: Constraint Handling Rules
|
||||
@c \label{sec:chr}
|
||||
|
||||
This chapter is written by Tom Schrijvers, K.U. Leuven for the hProlog
|
||||
system. Adjusted by Jan Wielemaker to fit the SWI-Prolog documentation
|
||||
infrastructure and remove hProlog specific references.
|
||||
|
||||
The CHR system of SWI-Prolog is the K.U.Leuven CHR system. The runtime
|
||||
environment is written by Christian Holzbaur and Tom Schrijvers while the
|
||||
compiler is written by Tom Schrijvers. Both are integrated with SWI-Prolog
|
||||
and licenced under compatible conditions with permission from the authors.
|
||||
|
||||
The main reference for SWI-Prolog's CHR system is:
|
||||
@itemize
|
||||
@item T. Schrijvers, and B. Demoen, @emph{The K.U.Leuven CHR System: Implementation
|
||||
and Application}, First Workshop on Constraint Handling Rules: Selected
|
||||
Contributions (Fruwirth, T. and Meister, M., eds.), pp. 1--5, 2004.
|
||||
@end itemize
|
||||
|
||||
@node CHR Introduction, CHR Syntax and Semantics, , CHR
|
||||
@section Introduction
|
||||
@c =====================
|
||||
|
||||
Constraint Handling Rules (CHR) is a committed-choice bottom-up language
|
||||
embedded in Prolog. It is designed for writing constraint solvers and is
|
||||
particularily useful for providing application-specific constraints.
|
||||
It has been used in many kinds of applications, like scheduling,
|
||||
model checking, abduction, type checking among many others.
|
||||
|
||||
CHR has previously been implemented in other Prolog systems (SICStus,
|
||||
Eclipse, Yap), Haskell and Java. This CHR system is based on the
|
||||
compilation scheme and runtime environment of CHR in SICStus.
|
||||
|
||||
In this documentation we restrict ourselves to giving a short overview
|
||||
of CHR in general and mainly focus on elements specific to this
|
||||
implementation. For a more thorough review of CHR we refer the reader to
|
||||
[Freuhwirth:98]. More background on CHR can be found at the CHR web site.
|
||||
|
||||
@c \secref{SyntaxAndSemantics} we present the syntax of CHR in Prolog and
|
||||
@c explain informally its operational semantics. Next, \secref{practical}
|
||||
@c deals with practical issues of writing and compiling hProlog programs
|
||||
@c containing CHR. \Secref{debugging} explains the currently primitive CHR
|
||||
@c debugging facilities. \Secref{predicates} provides a few useful predicates
|
||||
@c to inspect the constraint store and \secref{examples} illustrates CHR with
|
||||
@c two example programs. In \secref{sicstus-chr} some compatibility issues with
|
||||
@c SICStus CHR are listed. Finally, \secref{guidelines} concludes with a few
|
||||
@c practical guidelines for using CHR.
|
||||
|
||||
|
||||
@node CHR Syntax and Semantics, CHR in YAP Programs, CHR Introduction, CHR
|
||||
@section Syntax and Semantics
|
||||
@c \label{sec:SyntaxAndSemantics}
|
||||
@c=============================
|
||||
|
||||
@subsection Syntax
|
||||
@c -----------------
|
||||
|
||||
The syntax of CHR rules in hProlog is the following:
|
||||
|
||||
@example
|
||||
rules --> rule, rules.
|
||||
rules --> [].
|
||||
|
||||
rule --> name, actual_rule, pragma, [atom('.')].
|
||||
|
||||
name --> atom, [atom('@')].
|
||||
name --> [].
|
||||
|
||||
actual_rule --> simplification_rule.
|
||||
actual_rule --> propagation_rule.
|
||||
actual_rule --> simpagation_rule.
|
||||
|
||||
simplification_rule --> constraints, [atom('<=>')], guard, body.
|
||||
propagation_rule --> constraints, [atom('==>')], guard, body.
|
||||
simpagation_rule --> constraints, [atom('\')], constraints, [atom('<=>')],
|
||||
guard, body.
|
||||
|
||||
constraints --> constraint, constraint_id.
|
||||
constraints --> constraint, [atom(',')], constraints.
|
||||
|
||||
constraint --> compound_term.
|
||||
|
||||
constraint_id --> [].
|
||||
constraint_id --> [atom('#')], variable.
|
||||
|
||||
guard --> [].
|
||||
guard --> goal, [atom('|')].
|
||||
|
||||
body --> goal.
|
||||
|
||||
pragma --> [].
|
||||
pragma --> [atom('pragma')], actual_pragmas.
|
||||
|
||||
actual_pragmas --> actual_pragma.
|
||||
actual_pragmas --> actual_pragma, [atom(',')], actual_pragmas.
|
||||
|
||||
actual_pragma --> [atom('passive(')], variable, [atom(')')].
|
||||
|
||||
@end example
|
||||
|
||||
Additional syntax-related terminology:
|
||||
|
||||
@itemize
|
||||
@item @strong{head:} the constraints in an @code{actual_rule} before
|
||||
the arrow (either @code{<=>} or @code{==>})
|
||||
@end itemize
|
||||
|
||||
@subsection Semantics
|
||||
@c --------------------
|
||||
|
||||
In this subsection the operational semantics of CHR in Prolog are presented
|
||||
informally. They do not differ essentially from other CHR systems.
|
||||
|
||||
When a constraint is called, it is considered an active constraint and
|
||||
the system will try to apply the rules to it. Rules are tried and executed
|
||||
sequentially in the order they are written.
|
||||
|
||||
A rule is conceptually tried for an active constraint in the following
|
||||
way. The active constraint is matched with a constraint in the head of
|
||||
the rule. If more constraints appear in the head they are looked for
|
||||
among the suspended constraints, which are called passive constraints in
|
||||
this context. If the necessary passive constraints can be found and all
|
||||
match with the head of the rule and the guard of the rule succeeds, then
|
||||
the rule is committed and the body of the rule executed. If not all the
|
||||
necessary passive constraint can be found, the matching fails or the
|
||||
guard fails, then the body is not executed and the process of trying and
|
||||
executing simply continues with the following rules. If for a rule,
|
||||
there are multiple constraints in the head, the active constraint will
|
||||
try the rule sequentially multiple times, each time trying to match with
|
||||
another constraint.
|
||||
|
||||
This process ends either when the active constraint disappears, i.e. it
|
||||
is removed by some rule, or after the last rule has been processed. In
|
||||
the latter case the active constraint becomes suspended.
|
||||
|
||||
A suspended constraint is eligible as a passive constraint for an active
|
||||
constraint. The other way it may interact again with the rules, is when
|
||||
a variable appearing in the constraint becomes bound to either a nonvariable
|
||||
or another variable involved in one or more constraints. In that case the
|
||||
constraint is triggered, i.e. it becomes an active constraint and all
|
||||
the rules are tried.
|
||||
|
||||
@unnumberedsubsubsec Rule Types
|
||||
@c - - - - - - - - - -
|
||||
|
||||
There are three different kinds of rules, each with their specific semantics:
|
||||
|
||||
@table @code
|
||||
@item simplification
|
||||
The simplification rule removes the constraints in its head and calls its body.
|
||||
|
||||
@item propagation
|
||||
The propagation rule calls its body exactly once for the constraints in
|
||||
its head.
|
||||
|
||||
@item simpagation
|
||||
The simpagation rule removes the constraints in its head after the
|
||||
@code{\} and then calls its body. It is an optimization of
|
||||
simplification rules of the form: \[constraints_1, constraints_2 <=>
|
||||
constraints_1, body \] Namely, in the simpagation form:
|
||||
|
||||
@example
|
||||
constraints1 \ constraints2 <=> body
|
||||
@end example
|
||||
@noindent
|
||||
@var{constraints1}
|
||||
constraints are not called in the body.
|
||||
@end table
|
||||
|
||||
@unnumberedsubsubsec Rule Names
|
||||
@c - - - - - - - - - -
|
||||
Naming a rule is optional and has no semantical meaning. It only functions
|
||||
as documentation for the programmer.
|
||||
|
||||
@unnumberedsubsubsec Pragmas
|
||||
@c - - - - - - - - -
|
||||
The semantics of the pragmas are:
|
||||
|
||||
@table @option
|
||||
@item passive(Identifier)
|
||||
The constraint in the head of a rule @var{Identifier} can only act as a
|
||||
passive constraint in that rule.
|
||||
@end table
|
||||
|
||||
Additional pragmas may be released in the future.
|
||||
|
||||
@unnumberedsubsubsec Options
|
||||
@c - - - - - - - - -
|
||||
It is possible to specify options that apply to all the CHR rules in the module.
|
||||
Options are specified with the @code{option/2} declaration:
|
||||
|
||||
@example
|
||||
option(Option,Value).
|
||||
@end example
|
||||
|
||||
Available options are:
|
||||
@table @code
|
||||
@item check_guard_bindings
|
||||
This option controls whether guards should be checked for illegal
|
||||
variable bindings or not. Possible values for this option are
|
||||
@code{on}, to enable the checks, and @code{off}, to disable the
|
||||
checks.
|
||||
|
||||
@item optimize
|
||||
This is an experimental option controlling the degree of optimization.
|
||||
Possible values are @code{full}, to enable all available
|
||||
optimizations, and @code{off} (default), to disable all optimizations.
|
||||
The default is derived from the SWI-Prolog flag @code{optimise}, where
|
||||
@code{true} is mapped to @code{full}. Therefore the commandline
|
||||
option @option{-O} provides full CHR optimization.
|
||||
If optimization is enabled, debugging should be disabled.
|
||||
|
||||
@item debug
|
||||
This options enables or disables the possibility to debug the CHR code.
|
||||
Possible values are @code{on} (default) and @code{off}. See
|
||||
@option{debugging} for more details on debugging. The default is
|
||||
derived from the prolog flag @code{generate_debug_info}, which
|
||||
is @code{true} by default. See @option{-nodebug}.
|
||||
If debugging is enabled, optimization should be disabled.
|
||||
|
||||
@item mode
|
||||
This option specifies the mode for a particular constraint. The
|
||||
value is a term with functor and arity equal to that of a constraint.
|
||||
The arguments can be one of @code{-}, @code{+} or @code{?}.
|
||||
The latter is the default. The meaning is the following:
|
||||
@table @code
|
||||
@item -
|
||||
The corresponding argument of every occurrence
|
||||
of the constraint is always unbound.
|
||||
@item +
|
||||
The corresponding argument of every occurrence
|
||||
of the constraint is always ground.
|
||||
@item ?
|
||||
The corresponding argument of every occurrence
|
||||
of the constraint can have any instantiation, which may change
|
||||
over time. This is the default value.
|
||||
@end table
|
||||
The declaration is used by the compiler for various optimizations.
|
||||
Note that it is up to the user the ensure that the mode declaration
|
||||
is correct with respect to the use of the constraint.
|
||||
This option may occur once for each constraint.
|
||||
|
||||
@item type_declaration
|
||||
This option specifies the argument types for a particular constraint. The
|
||||
value is a term with functor and arity equal to that of a constraint.
|
||||
The arguments can be a user-defined type or one of
|
||||
the built-in types:
|
||||
@table @code
|
||||
@item int
|
||||
The corresponding argument of every occurrence
|
||||
of the constraint is an integer number.
|
||||
@item float
|
||||
@dots{} a floating point number.
|
||||
@item number
|
||||
@dots{} a number.
|
||||
@item natural
|
||||
@dots{} a positive integer.
|
||||
@item any
|
||||
The corresponding argument of every occurrence
|
||||
of the constraint can have any type. This is the default value.
|
||||
@end table
|
||||
|
||||
Currently, type declarations are only used to improve certain
|
||||
optimizations (guard simplification, occurrence subsumption, @dots{}).
|
||||
|
||||
@item type_definition
|
||||
This option defines a new user-defined type which can be used in
|
||||
type declarations. The value is a term of the form
|
||||
@code{type(}@var{name}@code{,}@var{list}@code{)}, where
|
||||
@var{name} is a term and @var{list} is a list of alternatives.
|
||||
Variables can be used to define generic types. Recursive definitions
|
||||
are allowed. Examples are
|
||||
|
||||
@example
|
||||
type(bool,[true,false]).
|
||||
type(complex_number,[float + float * i]).
|
||||
type(binary_tree(T),[ leaf(T) | node(binary_tree(T),binary_tree(T)) ]).
|
||||
type(list(T),[ [] | [T | list(T)]).
|
||||
@end example
|
||||
|
||||
|
||||
@end table
|
||||
|
||||
The mode, type_declaration and type_definition options are provided
|
||||
for backward compatibility. The new syntax is described below.
|
||||
|
||||
@node CHR in YAP Programs, CHR Debugging, CHR Syntax and Semantics, CHR
|
||||
@section CHR in YAP Programs
|
||||
@c \label{sec:practical}
|
||||
@c===========================
|
||||
|
||||
|
||||
@subsection Embedding in Prolog Programs
|
||||
|
||||
The CHR constraints defined in a particulary @file{chr} file are
|
||||
associated with a module. The default module is @code{user}. One should
|
||||
never load different @file{chr} files with the same CHR module name.
|
||||
|
||||
@subsection Constraint declaration
|
||||
|
||||
Every constraint used in CHR rules has to be declared.
|
||||
There are two ways to do this. The old style is as follows:
|
||||
|
||||
@example
|
||||
option(type_definition,type(list(T),[ [] , [T|list(T)] ]).
|
||||
option(mode,foo(+,?)).
|
||||
option(type_declaration,foo(list(int),float)).
|
||||
:- constraints foo/2, bar/0.
|
||||
@end example
|
||||
|
||||
The new style is as follows:
|
||||
|
||||
@example
|
||||
:- chr_type list(T) ---> [] ; [T|list(T)].
|
||||
:- constraints foo(+list(int),?float), bar.
|
||||
@end example
|
||||
|
||||
|
||||
@subsection Compilation
|
||||
|
||||
The SWI-Prolog CHR compiler exploits term_expansion/2 rules to translate
|
||||
the constraint handling rules to plain Prolog. These rules are loaded
|
||||
from the library @file{chr}. They are activated if the compiled file
|
||||
has the @file{chr} extension or after finding a declaration of the
|
||||
format below.
|
||||
|
||||
@example
|
||||
:- constraints ...
|
||||
@end example
|
||||
|
||||
It is adviced to define CHR rules in a module file, where the module
|
||||
declaration is immediately followed by including the @file{chr}
|
||||
library as examplified below:
|
||||
|
||||
@example
|
||||
:- module(zebra, [ zebra/0 ]).
|
||||
:- use_module(library(chr)).
|
||||
|
||||
:- constraints ...
|
||||
@end example
|
||||
|
||||
Using this style CHR rules can be defined in ordinary Prolog
|
||||
@file{pl} files and the operator definitions required by CHR do not
|
||||
leak into modules where they might cause conflicts.
|
||||
|
||||
|
||||
@node CHR Debugging, CHR Examples,CHR in YAP Programs, CHR
|
||||
@section Debugging
|
||||
@c \label{sec:debugging}
|
||||
@c=================
|
||||
|
||||
The CHR debugging facilities are currently rather limited. Only tracing
|
||||
is currently available. To use the CHR debugging facilities for a CHR
|
||||
file it must be compiled for debugging. Generating debug info is
|
||||
controlled by the CHR option @code{debug}, whose default is derived
|
||||
from the SWI-Prolog flag @code{generate_debug_info}. Therefore debug
|
||||
info is provided unless the @option{-nodebug} is used.
|
||||
|
||||
|
||||
@subsection Ports
|
||||
@c \label{sec:chrports
|
||||
@c===============
|
||||
|
||||
For CHR constraints the four standard ports are defined:
|
||||
|
||||
@table @code
|
||||
@item call
|
||||
A new constraint is called and becomes active.
|
||||
@item exit
|
||||
An active constraint exits: it has either been inserted in the store after
|
||||
trying all rules or has been removed from the constraint store.
|
||||
@item fail
|
||||
An active constraint fails.
|
||||
@item redo
|
||||
An active constraint starts looking for an alternative solution.
|
||||
@end table
|
||||
|
||||
In addition to the above ports, CHR constraints have five additional
|
||||
ports:
|
||||
|
||||
@table @code
|
||||
@item wake
|
||||
A suspended constraint is woken and becomes active.
|
||||
@item insert
|
||||
An active constraint has tried all rules and is suspended in
|
||||
the constraint store.
|
||||
@item remove
|
||||
An active or passive constraint is removed from the constraint
|
||||
store, if it had been inserted.
|
||||
@item try
|
||||
An active constraints tries a rule with possibly
|
||||
some passive constraints. The try port is entered
|
||||
just before committing to the rule.
|
||||
@item apply
|
||||
An active constraints commits to a rule with possibly
|
||||
some passive constraints. The apply port is entered
|
||||
just after committing to the rule.
|
||||
@end table
|
||||
|
||||
@subsection Tracing
|
||||
@c=================
|
||||
|
||||
Tracing is enabled with the chr_trace/0 predicate
|
||||
and disabled with the chr_notrace/0 predicate.
|
||||
|
||||
When enabled the tracer will step through the @code{call},
|
||||
@code{exit}, @code{fail}, @code{wake} and @code{apply} ports,
|
||||
accepting debug commands, and simply write out the other ports.
|
||||
|
||||
The following debug commans are currently supported:
|
||||
|
||||
@example
|
||||
CHR debug options:
|
||||
|
||||
<cr> creep c creep
|
||||
s skip
|
||||
g ancestors
|
||||
n nodebug
|
||||
b break
|
||||
a abort
|
||||
f fail
|
||||
? help h help
|
||||
@end example
|
||||
|
||||
Their meaning is:
|
||||
|
||||
@table @code
|
||||
@item creep
|
||||
Step to the next port.
|
||||
@item skip
|
||||
Skip to exit port of this call or wake port.
|
||||
@item ancestors
|
||||
Print list of ancestor call and wake ports.
|
||||
@item nodebug
|
||||
Disable the tracer.
|
||||
@item break
|
||||
Enter a recursive Prolog toplevel. See break/0.
|
||||
@item abort
|
||||
Exit to the toplevel. See abort/0.
|
||||
@item fail
|
||||
Insert failure in execution.
|
||||
@item help
|
||||
Print the above available debug options.
|
||||
@end table
|
||||
|
||||
@subsection CHR Debugging Predicates
|
||||
@c \label{sec:predicates
|
||||
@c====================================
|
||||
|
||||
The @file{chr} module contains several predicates that allow
|
||||
inspecting and printing the content of the constraint store.
|
||||
|
||||
@table @code
|
||||
@item chr_trace/0
|
||||
Activate the CHR tracer. By default the CHR tracer is activated and
|
||||
deactivated automatically by the Prolog predicates trace/0 and
|
||||
notrace/0.
|
||||
|
||||
@item chr_notrace/0
|
||||
De-activate the CHR tracer. By default the CHR tracer is activated and
|
||||
deactivated automatically by the Prolog predicates trace/0 and
|
||||
notrace/0.
|
||||
|
||||
@item chr_leash/0
|
||||
|
||||
Define the set of CHR ports on which the CHR
|
||||
tracer asks for user intervention (i.e. stops). @var{Spec} is either a
|
||||
list of ports or a predefined `alias'. Defined aliases are:
|
||||
@code{full} to stop at all ports, @code{none} or @code{off} to never
|
||||
stop, and @code{default} to stop at the @code{call}, @code{exit},
|
||||
@code{fail}, @code{wake} and @code{apply} ports. See also leash/1.
|
||||
|
||||
@item chr_show_store(+@var{Mod})
|
||||
Prints all suspended constraints of module @var{Mod} to the standard
|
||||
output. This predicate is automatically called by the SWI-Prolog toplevel at
|
||||
the end of each query for every CHR module currently loaded. The prolog-flag
|
||||
@code{chr_toplevel_show_store} controls whether the toplevel shows the
|
||||
constraint stores. The value @code{true} enables it. Any other value
|
||||
disables it.
|
||||
|
||||
|
||||
@end table
|
||||
|
||||
|
||||
@node CHR Examples, CHR Compatibility,CHR Debugging, CHR
|
||||
@section Examples
|
||||
@c \label{sec:examples}
|
||||
@c================
|
||||
|
||||
Here are two example constraint solvers written in CHR.
|
||||
|
||||
@itemize
|
||||
@item
|
||||
The program below defines a solver with one constraint,
|
||||
@code{leq/2}, which is a less-than-or-equal constraint.
|
||||
|
||||
@example
|
||||
:- module(leq,[cycle/3, leq/2]).
|
||||
:- use_module(library(chr)).
|
||||
|
||||
:- constraints leq/2.
|
||||
reflexivity @ leq(X,X) <=> true.
|
||||
antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
|
||||
idempotence @ leq(X,Y) \ leq(X,Y) <=> true.
|
||||
transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).
|
||||
|
||||
cycle(X,Y,Z):-
|
||||
leq(X,Y),
|
||||
leq(Y,Z),
|
||||
leq(Z,X).
|
||||
@end example
|
||||
|
||||
@item
|
||||
The program below implements a simple finite domain
|
||||
constraint solver.
|
||||
|
||||
@example
|
||||
:- module(dom,[dom/2]).
|
||||
:- use_module(library(chr)).
|
||||
|
||||
:- constraints dom/2.
|
||||
|
||||
dom(X,[]) <=> fail.
|
||||
dom(X,[Y]) <=> X = Y.
|
||||
dom(X,L1), dom(X,L2) <=> intersection(L1,L2,L3), dom(X,L3).
|
||||
|
||||
intersection([],_,[]).
|
||||
intersection([H|T],L2,[H|L3]) :-
|
||||
member(H,L2), !,
|
||||
intersection(T,L2,L3).
|
||||
intersection([_|T],L2,L3) :-
|
||||
intersection(T,L2,L3).
|
||||
@end example
|
||||
|
||||
@end itemize
|
||||
|
||||
@node CHR Compatibility, CHR Guidelines,CHR Examples, CHR
|
||||
@section Compatibility with SICStus CHR
|
||||
@c \label{sec:sicstus-chr}
|
||||
@c==================
|
||||
|
||||
There are small differences between CHR in SWI-Prolog and newer
|
||||
YAPs and SICStus and older versions of YAP. Besides differences in
|
||||
available options and pragmas, the following differences should be
|
||||
noted:
|
||||
|
||||
@table @code
|
||||
@item [The handler/1 declaration]
|
||||
In SICStus every CHR module requires a @code{handler/1}
|
||||
declaration declaring a unique handler name. This declaration is valid
|
||||
syntax in SWI-Prolog, but will have no effect. A warning will be given
|
||||
during compilation.
|
||||
|
||||
@item [The rules/1 declaration]
|
||||
In SICStus, for every CHR module it is possible to only enable a subset
|
||||
of the available rules through the @code{rules/1} declaration. The
|
||||
declaration is valid syntax in SWI-Prolog, but has no effect. A
|
||||
warning is given during compilation.
|
||||
|
||||
@item [Sourcefile naming]
|
||||
SICStus uses a two-step compiler, where @file{chr} files are
|
||||
first translated into @file{pl} files. For SWI-Prolog CHR
|
||||
rules may be defined in a file with any extension.
|
||||
@end table
|
||||
|
||||
|
||||
@node CHR Guidelines, ,CHR Compatibility, CHR
|
||||
@section Guidelines
|
||||
@c \label{sec:guidelines}
|
||||
@c ==================
|
||||
|
||||
In this section we cover several guidelines on how to use CHR to write
|
||||
constraint solvers and how to do so efficiently.
|
||||
|
||||
@table @code
|
||||
@item [Set semantics]
|
||||
The CHR system allows the presence of identical constraints, i.e.
|
||||
multiple constraints with the same functor, arity and arguments. For
|
||||
most constraint solvers, this is not desirable: it affects efficiency
|
||||
and possibly termination. Hence appropriate simpagation rules should be
|
||||
added of the form:
|
||||
|
||||
@example
|
||||
@{constraint \ constraint <=> true@}.
|
||||
@end example
|
||||
|
||||
@item [Multi-headed rules]
|
||||
Multi-headed rules are executed more efficiently when the constraints
|
||||
share one or more variables.
|
||||
|
||||
@item [Mode and type declarations]
|
||||
Provide mode and type declarations to get more efficient program execution.
|
||||
Make sure to disable debug (@option{-nodebug}) and enable optimization
|
||||
(@option{-O}).
|
||||
@end table
|
||||
|
||||
|
180
docs/clpr.tex
Normal file
180
docs/clpr.tex
Normal file
@ -0,0 +1,180 @@
|
||||
@chapter Constraint Logic Programming over Reals
|
||||
|
||||
YAP now uses the CLP(R) package developed by @emph{Leslie De Koninck},
|
||||
K.U. Leuven as part of a thesis with supervisor Bart Demoen and daily
|
||||
advisor Tom Schrijvers, and distributed with SWI-Prolog.
|
||||
|
||||
This CLP(R) system is a port of the CLP(Q,R) system of Sicstus Prolog
|
||||
and YAP by Christian Holzbaur: Holzbaur C.: OFAI clp(q,r) Manual,
|
||||
Edition 1.3.3, Austrian Research Institute for Artificial
|
||||
Intelligence, Vienna, TR-95-09, 1995,
|
||||
@url{http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09} This
|
||||
port only contains the part concerning real arithmetics. This manual
|
||||
is roughly based on the manual of the above mentioned @strong{CLP(QR)}
|
||||
implementation.
|
||||
|
||||
Please note that the @file{clpr} library is @emph{not} an
|
||||
@code{autoload} library and therefore this library must be loaded
|
||||
explicitely before using it:
|
||||
|
||||
@example
|
||||
:- use_module(library(clpr)).
|
||||
@end example
|
||||
|
||||
@node CLPR Solver Predicates, CLPR Syntax , , CLPR
|
||||
@section Solver Predicates
|
||||
@c =============================
|
||||
|
||||
The following predicates are provided to work with constraints:
|
||||
|
||||
@table @code
|
||||
@item @{+@var{Constraints}@}
|
||||
Adds the constraints given by @var{Constraints} to the constraint store.
|
||||
|
||||
@item entailed(+@var{Constraint})
|
||||
Succeeds if @var{Constraint} is necessarily true within the current
|
||||
constraint store. This means that adding the negation of the constraint
|
||||
to the store results in failure.
|
||||
|
||||
@item inf(+@var{Expression},-@var{Inf})
|
||||
Computes the infimum of @var{Expression} within the current state of the
|
||||
constraint store and returns that infimum in @var{Inf}. This predicate
|
||||
does not change the constraint store.
|
||||
|
||||
@item inf(+@var{Expression},-@var{Sup})
|
||||
Computes the supremum of @var{Expression} within the current state of
|
||||
the constraint store and returns that supremum in @var{Sup}. This
|
||||
predicate does not change the constraint store.
|
||||
|
||||
@item min(+@var{Expression})
|
||||
Minimizes @var{Expression} within the current constraint store. This is
|
||||
the same as computing the infimum and equation the expression to that
|
||||
infimum.
|
||||
|
||||
@item max(+@var{Expression})
|
||||
Maximizes @var{Expression} within the current constraint store. This is
|
||||
the same as computing the supremum and equating the expression to that
|
||||
supremum.
|
||||
|
||||
@item bb_inf(+@var{Ints},+@var{Expression},-@var{Inf},-@var{Vertext},+@var{Eps})
|
||||
Computes the infimum of @var{Expression} within the current constraint
|
||||
store, with the additional constraint that in that infimum, all
|
||||
variables in @var{Ints} have integral values. @var{Vertex} will contain
|
||||
the values of @var{Ints} in the infimum. @var{Eps} denotes how much a
|
||||
value may differ from an integer to be considered an integer. E.g. when
|
||||
@var{Eps} = 0.001, then X = 4.999 will be considered as an integer (5 in
|
||||
this case). @var{Eps} should be between 0 and 0.5.
|
||||
|
||||
@item bb_inf(+@var{Ints},+@var{Expression},-@var{Inf})
|
||||
The same as bb_inf/5 but without returning the values of the integers
|
||||
and with an eps of 0.001.
|
||||
|
||||
@item bb_inf(+@var{Target},+@var{Newvars},-@var{CodedAnswer})
|
||||
Returns the constraints on @var{Target} in the list @var{CodedAnswer}
|
||||
where all variables of @var{Target} have veen replaced by @var{NewVars}.
|
||||
This operation does not change the constraint store. E.g. in
|
||||
|
||||
@example
|
||||
dump([X,Y,Z],[x,y,z],Cons)
|
||||
@end example
|
||||
|
||||
@var{Cons} will contain the constraints on @var{X}, @var{Y} and
|
||||
@var{Z} where these variables have been replaced by atoms @code{x}, @code{y} and @code{z}.
|
||||
|
||||
@end table
|
||||
|
||||
@node CLPR Syntax, CLPR Unification, CLPR Solver Predicates, CLPR
|
||||
@section Syntax of the predicate arguments
|
||||
@c =============================================
|
||||
|
||||
The arguments of the predicates defined in the subsection above are
|
||||
defined in the following table. Failing to meet the syntax rules will
|
||||
result in an exception.
|
||||
|
||||
@example
|
||||
<Constraints> ---> <Constraint> \\ single constraint \\
|
||||
| <Constraint> , <Constraints> \\ conjunction \\
|
||||
| <Constraint> ; <Constraints> \\ disjunction \\
|
||||
|
||||
<Constraint> ---> <Expression> @{<@} <Expression> \\ less than \\
|
||||
| <Expression> @{>@} <Expression> \\ greater than \\
|
||||
| <Expression> @{=<@} <Expression> \\ less or equal \\
|
||||
| @{<=@}(<Expression>, <Expression>) \\ less or equal \\
|
||||
| <Expression> @{>=@} <Expression> \\ greater or equal \\
|
||||
| <Expression> @{=\=@} <Expression> \\ not equal \\
|
||||
| <Expression> =:= <Expression> \\ equal \\
|
||||
| <Expression> = <Expression> \\ equal \\
|
||||
|
||||
<Expression> ---> <Variable> \\ Prolog variable \\
|
||||
| <Number> \\ Prolog number (float, integer) \\
|
||||
| +<Expression> \\ unary plus \\
|
||||
| -<Expression> \\ unary minus \\
|
||||
| <Expression> + <Expression> \\ addition \\
|
||||
| <Expression> - <Expression> \\ substraction \\
|
||||
| <Expression> * <Expression> \\ multiplication \\
|
||||
| <Expression> / <Expression> \\ division \\
|
||||
| abs(<Expression>) \\ absolute value \\
|
||||
| sin(<Expression>) \\ sine \\
|
||||
| cos(<Expression>) \\ cosine \\
|
||||
| tan(<Expression>) \\ tangent \\
|
||||
| exp(<Expression>) \\ exponent \\
|
||||
| pow(<Expression>) \\ exponent \\
|
||||
| <Expression> @{^@} <Expression> \\ exponent \\
|
||||
| min(<Expression>, <Expression>) \\ minimum \\
|
||||
| max(<Expression>, <Expression>) \\ maximum \\
|
||||
@end example
|
||||
|
||||
@node CLPR Unification, CLPR Non-linear Constraints, CLPR Syntax, CLPR
|
||||
@section Use of unification
|
||||
|
||||
Instead of using the @code{@{@}/1} predicate, you can also use the standard
|
||||
unification mechanism to store constraints. The following code samples
|
||||
are equivalent:
|
||||
|
||||
@table @option
|
||||
@item Unification with a variable
|
||||
|
||||
@example
|
||||
@{X =:= Y@}
|
||||
@{X = Y@}
|
||||
X = Y
|
||||
@end example
|
||||
|
||||
@item Unification with a number
|
||||
|
||||
@example
|
||||
@{X =:= 5.0@}
|
||||
@{X = 5.0@}
|
||||
X = 5.0
|
||||
@end example
|
||||
|
||||
@end table
|
||||
|
||||
@node CLPR Non-linear Constraints, , CLPR Unification, CLPR
|
||||
@section Non-Linear Constraints
|
||||
@c ==================================
|
||||
|
||||
In this version, non-linear constraints do not get solved until certain
|
||||
conditions are satisfied. We call these conditions the isolation axioms.
|
||||
They are given in the following table.
|
||||
|
||||
@example
|
||||
A = B * C when B or C is ground or // A = 5 * C or A = B * 4 \\
|
||||
A and (B or C) are ground // 20 = 5 * C or 20 = B * 4 \\
|
||||
|
||||
A = B / C when C is ground or // A = B / 3
|
||||
A and B are ground // 4 = 12 / C
|
||||
|
||||
X = min(Y,Z) when Y and Z are ground or // X = min(4,3)
|
||||
X = max(Y,Z) Y and Z are ground // X = max(4,3)
|
||||
X = abs(Y) Y is ground // X = abs(-7)
|
||||
|
||||
X = pow(Y,Z) when X and Y are ground or // 8 = 2 ^ Z
|
||||
X = exp(Y,Z) X and Z are ground // 8 = Y ^ 3
|
||||
X = Y ^ Z Y and Z are ground // X = 2 ^ 3
|
||||
|
||||
X = sin(Y) when X is ground or // 1 = sin(Y)
|
||||
X = cos(Y) Y is ground // X = sin(1.5707)
|
||||
X = tan(Y)
|
||||
@end example
|
||||
|
495
docs/swi.tex
Normal file
495
docs/swi.tex
Normal file
@ -0,0 +1,495 @@
|
||||
@chapter SWI-Prolog Emulation
|
||||
|
||||
This library provides a number of SWI-Prolog builtins that are not by
|
||||
default in YAP. This library is loaded with the
|
||||
@code{use_module(library(swi))} command.
|
||||
|
||||
@table @code
|
||||
|
||||
@item append(?@var{List1},?@var{List2},?@var{List3})
|
||||
@findex append/3
|
||||
@snindex append/3
|
||||
@cnindex append/3
|
||||
Succeeds when @var{List3} unifies with the concatenation of @var{List1}
|
||||
and @var{List2}. The predicate can be used with any instantiation
|
||||
pattern (even three variables).
|
||||
|
||||
@item between(+@var{Low},+@var{High},?@var{Value})
|
||||
@findex between/3
|
||||
@snindex between/3
|
||||
@cnindex between/3
|
||||
|
||||
@var{Low} and @var{High} are integers, @var{High} less or equal than
|
||||
@var{Low}. If @var{Value} is an integer, @var{Low} less or equal than
|
||||
@var{Value} less or equal than @var{High}. When @var{Value} is a
|
||||
variable it is successively bound to all integers between @var{Low} and
|
||||
@var{High}. If @var{High} is @code{inf}, @code{between/3} is true iff
|
||||
@var{Value} less or equal than @var{Low}, a feature that is particularly
|
||||
interesting for generating integers from a certain value.
|
||||
|
||||
@item chdir(+@var{Dir})
|
||||
@findex chdir/1
|
||||
@snindex chdir/1
|
||||
@cnindex chdir/1
|
||||
|
||||
Compatibility predicate. New code should use @code{working_directory/2}.
|
||||
|
||||
@item concat_atom(+@var{List},-@var{Atom})
|
||||
@findex concat_atom/2
|
||||
@snindex concat_atom/2
|
||||
@cnindex concat_atom/2
|
||||
|
||||
@var{List} is a list of atoms, integers or floating point numbers. Succeeds
|
||||
if @var{Atom} can be unified with the concatenated elements of @var{List}. If
|
||||
@var{List} has exactly 2 elements it is equivalent to @code{atom_concat/3},
|
||||
allowing for variables in the list.
|
||||
|
||||
@item concat_atom(?@var{List},+@var{Separator},?@var{Atom})
|
||||
@findex concat_atom/3
|
||||
@snindex concat_atom/3
|
||||
@cnindex concat_atom/3
|
||||
|
||||
Creates an atom just like concat_atom/2, but inserts @var{Separator}
|
||||
between each pair of atoms. For example:
|
||||
\@example
|
||||
?- concat_atom([gnu, gnat], ', ', A).
|
||||
|
||||
A = 'gnu, gnat'
|
||||
@end example
|
||||
|
||||
(Unimplemented) This predicate can also be used to split atoms by
|
||||
instantiating @var{Separator} and @var{Atom}:
|
||||
|
||||
@example
|
||||
?- concat_atom(L, -, 'gnu-gnat').
|
||||
|
||||
L = [gnu, gnat]
|
||||
@end example
|
||||
|
||||
@item nth1(+@var{Index},?@var{List},?@var{Elem})
|
||||
@findex nth1/3
|
||||
@snindex nth1/3
|
||||
@cnindex nth1/3
|
||||
Succeeds when the @var{Index}-th element of @var{List} unifies with
|
||||
@var{Elem}. Counting starts at 1.
|
||||
|
||||
Set environment variable. @var{Name} and @var{Value} should be
|
||||
instantiated to atoms or integers. The environment variable will be
|
||||
passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
|
||||
They also influence @code{expand_file_name/2}.
|
||||
|
||||
@item setenv(+@var{Name},+@var{Value})
|
||||
@findex setenv/2
|
||||
@snindex setenv/2
|
||||
@cnindex setenv/2
|
||||
Set environment variable. @var{Name} and @var{Value} should be
|
||||
instantiated to atoms or integers. The environment variable will be
|
||||
passed to @code{shell/[0-2]} and can be requested using @code{getenv/2}.
|
||||
They also influence @code{expand_file_name/2}.
|
||||
|
||||
@item term_to_atom(?@var{Term},?@var{Atom})
|
||||
@findex term_to_atom/2
|
||||
@snindex term_to_atom/2
|
||||
@cnindex term_to_atom/2
|
||||
Succeeds if @var{Atom} describes a term that unifies with @var{Term}. When
|
||||
@var{Atom} is instantiated @var{Atom} is converted and then unified with
|
||||
@var{Term}. If @var{Atom} has no valid syntax, a @code{syntax_error}
|
||||
exception is raised. Otherwise @var{Term} is ``written'' on @var{Atom}
|
||||
using @code{write/1}.
|
||||
|
||||
@item working_directory(-@var{Old},+@var{New})
|
||||
@findex working_directory/2
|
||||
@snindex working_directory/2
|
||||
@cnindex working_directory/2
|
||||
|
||||
Unify @var{Old} with an absolute path to the current working directory
|
||||
and change working directory to @var{New}. Use the pattern
|
||||
@code{working_directory(CWD, CWD)} to get the current directory. See
|
||||
also @code{absolute_file_name/2} and @code{chdir/1}.
|
||||
|
||||
@end table
|
||||
|
||||
@node Invoking Predicates on all Members of a List,Forall, , SWI-Prolog
|
||||
@section Invoking Predicates on all Members of a List
|
||||
@c \label{sec:applylist}
|
||||
|
||||
All the predicates in this section call a predicate on all members of a
|
||||
list or until the predicate called fails. The predicate is called via
|
||||
@code{call/[2..]}, which implies common arguments can be put in
|
||||
front of the arguments obtained from the list(s). For example:
|
||||
|
||||
@example
|
||||
?- maplist(plus(1), [0, 1, 2], X).
|
||||
|
||||
X = [1, 2, 3]
|
||||
@end example
|
||||
|
||||
we will phrase this as ``@var{Predicate} is applied on ...''
|
||||
|
||||
@table @code
|
||||
|
||||
@item maplist(+@var{Pred},+@var{List})
|
||||
@findex maplist/2
|
||||
@snindex maplist/2
|
||||
@cnindex maplist/2
|
||||
@var{Pred} is applied successively on each element of @var{List} until
|
||||
the end of the list or @var{Pred} fails. In the latter case
|
||||
@code{maplist/2} fails.
|
||||
|
||||
@item maplist(+@var{Pred},+@var{List1},+@var{List2})
|
||||
@findex maplist/3
|
||||
@snindex maplist/3
|
||||
@cnindex maplist/3
|
||||
Apply @var{Pred} on all successive triples of elements from
|
||||
@var{List1} and
|
||||
@var{List2}. Fails if @var{Pred} can not be applied to a
|
||||
pair. See the example above.
|
||||
|
||||
@item maplist(+@var{Pred},+@var{List1},+@var{List2},+@var{List4})
|
||||
@findex maplist/4
|
||||
@snindex maplist/4
|
||||
@cnindex maplist/4
|
||||
Apply @var{Pred} on all successive triples of elements from @var{List1},
|
||||
@var{List2} and @var{List3}. Fails if @var{Pred} can not be applied to a
|
||||
triple. See the example above.
|
||||
|
||||
@c @item findlist(+@var{Pred},+@var{List1},?@var{List2})
|
||||
@c @findex findlist/3
|
||||
@c @snindex findlist/3
|
||||
@c @cnindex findlist/3
|
||||
@c Unify @var{List2} with a list of all elements of @var{List1} to which
|
||||
@c @var{Pred} applies.
|
||||
@end table
|
||||
|
||||
@node Forall,hProlog and SWI-Prolog Attributed Variables,Invoking Predicates on all Members of a List, SWI-Prolog
|
||||
@section Forall
|
||||
@c \label{sec:forall2}
|
||||
|
||||
@table @code
|
||||
@item forall(+@var{Cond},+@var{Action})
|
||||
@findex forall/2
|
||||
@snindex forall/2
|
||||
@cnindex forall/2
|
||||
|
||||
For all alternative bindings of @var{Cond} @var{Action} can be proven.
|
||||
The next example verifies that all arithmetic statements in the list
|
||||
@var{L} are correct. It does not say which is wrong if one proves wrong.
|
||||
|
||||
@example
|
||||
?- forall(member(Result = Formula, [2 = 1 + 1, 4 = 2 * 2]),
|
||||
Result =:= Formula).
|
||||
@end example
|
||||
|
||||
@end table
|
||||
|
||||
@node hProlog and SWI-Prolog Attributed Variables, SWI-Prolog Global Variables, Forall,SWI-Prolog
|
||||
@section hProlog and SWI-Prolog Attributed Variables
|
||||
@cindex hProlog Attributed Variables
|
||||
|
||||
Attributed variables
|
||||
@c @ref{Attributed variables}
|
||||
provide a technique for extending the
|
||||
Prolog unification algorithm by hooking the binding of attributed
|
||||
variables. There is little consensus in the Prolog community on the
|
||||
exact definition and interface to attributed variables. Yap Prolog
|
||||
traditionally implements a SICStus-like interface, but to enable
|
||||
SWI-compatibility we have implemented the SWI-Prolog interface,
|
||||
identical to the one realised by Bart Demoen for hProlog.
|
||||
|
||||
Binding an attributed variable schedules a goal to be executed at the
|
||||
first possible opportunity. In the current implementation the hooks are
|
||||
executed immediately after a successful unification of the clause-head
|
||||
or successful completion of a foreign language (builtin) predicate. Each
|
||||
attribute is associated to a module and the hook (attr_unify_hook/2) is
|
||||
executed in this module. The example below realises a very simple and
|
||||
incomplete finite domain reasoner.
|
||||
|
||||
@example
|
||||
:- module(domain,
|
||||
[ domain/2 % Var, ?Domain
|
||||
]).
|
||||
:- use_module(library(oset)).
|
||||
|
||||
domain(X, Dom) :-
|
||||
var(Dom), !,
|
||||
get_attr(X, domain, Dom).
|
||||
domain(X, List) :-
|
||||
sort(List, Domain),
|
||||
put_attr(Y, domain, Domain),
|
||||
X = Y.
|
||||
|
||||
% An attributed variable with attribute value Domain has been
|
||||
% assigned the value Y
|
||||
|
||||
attr_unify_hook(Domain, Y) :-
|
||||
( get_attr(Y, domain, Dom2)
|
||||
-> oset_int(Domain, Dom2, NewDomain),
|
||||
( NewDomain == []
|
||||
-> fail
|
||||
; NewDomain = [Value]
|
||||
-> Y = Value
|
||||
; put_attr(Y, domain, NewDomain)
|
||||
)
|
||||
; var(Y)
|
||||
-> put_attr( Y, domain, Domain )
|
||||
; memberchk(Y, Domain)
|
||||
).
|
||||
@end example
|
||||
|
||||
|
||||
Before explaining the code we give some example queries:
|
||||
|
||||
@table @code
|
||||
@item ?- domain(X, [a,b]), X = c
|
||||
no
|
||||
@item ?- domain(X, [a,b]), domain(X, [a,c]).
|
||||
X = a
|
||||
@item ?- domain(X, [a,b,c]), domain(X, [a,c]).
|
||||
X = _D0
|
||||
@end table
|
||||
|
||||
The predicate @code{domain/2} fetches (first clause) or assigns
|
||||
(second clause) the variable a @emph{domain}, a set of values it can
|
||||
be unified with. In the second clause first associates the domain
|
||||
with a fresh variable and then unifies X to this variable to deal
|
||||
with the possibility that X already has a domain. The
|
||||
predicate @code{attr_unify_hook/2} is a hook called after a variable with
|
||||
a domain is assigned a value. In the simple case where the variable
|
||||
is bound to a concrete value we simply check whether this value is in
|
||||
the domain. Otherwise we take the intersection of the domains and either
|
||||
fail if the intersection is empty (first example), simply assign the
|
||||
value if there is only one value in the intersection (second example) or
|
||||
assign the intersection as the new domain of the variable (third
|
||||
example).
|
||||
|
||||
|
||||
@table @code
|
||||
|
||||
@item put_attr(+@var{Var},+@var{Module},+@var{Value})
|
||||
@findex put_attr/3
|
||||
@snindex put_attr/3
|
||||
@cnindex put_attr/3
|
||||
If @var{Var} is a variable or attributed variable, set the value for the
|
||||
attribute named @var{Module} to @var{Value}. If an attribute with this
|
||||
name is already associated with @var{Var}, the old value is replaced.
|
||||
Backtracking will restore the old value (i.e. an attribute is a mutable
|
||||
term. See also @code{setarg/3}). This predicate raises a type error if
|
||||
@var{Var} is not a variable or @var{Module} is not an atom.
|
||||
|
||||
@item get_attr(+@var{Var},+@var{Module},+@var{Value})
|
||||
@findex get_attr/3
|
||||
@snindex get_attr/3
|
||||
@cnindex get_attr/3
|
||||
Request the current @var{value} for the attribute named @var{Module}. If
|
||||
@var{Var} is not an attributed variable or the named attribute is not
|
||||
associated to @var{Var} this predicate fails silently. If @var{Module}
|
||||
is not an atom, a type error is raised.
|
||||
|
||||
@item del_attr(+@var{Var},+@var{Module})
|
||||
@findex del_attr/2
|
||||
@snindex del_attr/2
|
||||
@cnindex del_attr/2
|
||||
Delete the named attribute. If @var{Var} loses its last attribute it
|
||||
is transformed back into a traditional Prolog variable. If @var{Module}
|
||||
is not an atom, a type error is raised. In all other cases this
|
||||
predicate succeeds regarless whether or not the named attribute is
|
||||
present.
|
||||
|
||||
@item attr_unify_hook(+@var{AttValue},+@var{VarValue})
|
||||
@findex attr_unify_hook/2
|
||||
@snindex attr_unify_hook/2
|
||||
@cnindex attr_unify_hook/2
|
||||
Hook that must be defined in the module an attributed variable refers
|
||||
to. Is is called @emph{after} the attributed variable has been
|
||||
unified with a non-var term, possibly another attributed variable.
|
||||
@var{AttValue} is the attribute that was associated to the variable
|
||||
in this module and @var{VarValue} is the new value of the variable.
|
||||
Normally this predicate fails to veto binding the variable to
|
||||
@var{VarValue}, forcing backtracking to undo the binding. If
|
||||
@var{VarValue} is another attributed variable the hook often combines
|
||||
the two attribute and associates the combined attribute with
|
||||
@var{VarValue} using @code{put_attr/3}.
|
||||
|
||||
@c \predicate{attr_portray_hook}{2}{+AttValue, +Var}
|
||||
@c Called by write_term/2 and friends for each attribute if the option
|
||||
@c \term{attributes}{portray} is in effect. If the hook succeeds the
|
||||
@c attribute is considered printed. Otherwise \exam{Module = ...} is
|
||||
@c printed to indicate the existence of a variable.
|
||||
@end table
|
||||
|
||||
@subsection Special Purpose SWI Predicates for Attributes
|
||||
|
||||
Normal user code should deal with @code{put_attr/3}, @code{get_attr/3}
|
||||
and @code{del_attr/2}. The routines in this section fetch or set the
|
||||
entire attribute list of a variables. Use of these predicates is
|
||||
anticipated to be restricted to printing and other special purpose
|
||||
operations.
|
||||
|
||||
@table @code
|
||||
@item get_attrs(+@var{Var},-@var{Attributes})
|
||||
@findex get_attrs/2
|
||||
@snindex get_attrs/2
|
||||
@cnindex get_attrs/2
|
||||
Get all attributes of @var{Var}. @var{Attributes} is a term of the form
|
||||
@code{att(Module, Value, MoreAttributes)}, where @var{MoreAttributes} is
|
||||
@code{[]} for the last attribute.
|
||||
|
||||
@item put_attrs(+@var{Var},+@var{Attributes})
|
||||
@findex put_attrs/2
|
||||
@snindex put_attrs/2
|
||||
@cnindex put_attrs/2
|
||||
Set all attributes of @var{Var}. See get_attrs/2 for a description of
|
||||
@var{Attributes}.
|
||||
|
||||
@item copy_term_nat(?@var{TI},-@var{TF})
|
||||
@findex copy_term_nat/2
|
||||
@snindex copy_term_nat/2
|
||||
@cnindex copy_term_nat/2
|
||||
As @code{copy_term/2}. Attributes however, are @emph{not} copied but replaced
|
||||
by fresh variables.
|
||||
@end table
|
||||
|
||||
|
||||
@node SWI-Prolog Global Variables, ,hProlog and SWI-Prolog Attributed Variables,SWI-Prolog
|
||||
@section SWI Global variables
|
||||
@c \label{sec:gvar}
|
||||
|
||||
SWI-Prolog global variables are associations between names (atoms) and
|
||||
terms. They differ in various ways from storing information using
|
||||
@code{assert/1} or @code{recorda/3}.
|
||||
|
||||
@itemize @bullet
|
||||
@item The value lives on the Prolog (global) stack. This implies
|
||||
that lookup time is independent from the size of the term.
|
||||
This is particulary interesting for large data structures
|
||||
such as parsed XML documents or the CHR global constraint
|
||||
store.
|
||||
|
||||
@item They support both global assignment using @code{nb_setval/2} and
|
||||
backtrackable assignment using @code{b_setval/2}.
|
||||
|
||||
@item Only one value (which can be an arbitrary complex Prolog
|
||||
term) can be associated to a variable at a time.
|
||||
|
||||
@item Their value cannot be shared among threads. Each thread
|
||||
has its own namespace and values for global variables.
|
||||
|
||||
@item Currently global variables are scoped globally. We may
|
||||
consider module scoping in future versions.
|
||||
@end itemize
|
||||
|
||||
Both @code{b_setval/2} and @code{nb_setval/2} implicitely create a variable if the
|
||||
referenced name does not already refer to a variable.
|
||||
|
||||
Global variables may be initialised from directives to make them
|
||||
available during the program lifetime, but some considerations are
|
||||
necessary for saved-states and threads. Saved-states to not store global
|
||||
variables, which implies they have to be declared with @code{initialization/1}
|
||||
to recreate them after loading the saved state. Each thread has
|
||||
its own set of global variables, starting with an empty set. Using
|
||||
@code{thread_inititialization/1} to define a global variable it will be
|
||||
defined, restored after reloading a saved state and created in all
|
||||
threads that are created @emph{after} the registration.
|
||||
|
||||
|
||||
@table @code
|
||||
@item b_setval(+@var{Name},+@var{Value})
|
||||
@findex b_setval/2
|
||||
@snindex b_setval/2
|
||||
@cnindex b_setval/2
|
||||
Associate the term @var{Value} with the atom @var{Name} or replaces
|
||||
the currently associated value with @var{Value}. If @var{Name} does
|
||||
not refer to an existing global variable a variable with initial value
|
||||
@code{[]} is created (the empty list). On backtracking the
|
||||
assignment is reversed.
|
||||
|
||||
@item b_getval(+@var{Name},-@var{Value})
|
||||
@findex b_getval/2
|
||||
@snindex b_getval/2
|
||||
@cnindex b_getval/2
|
||||
Get the value associated with the global variable @var{Name} and unify
|
||||
it with @var{Value}. Note that this unification may further instantiate
|
||||
the value of the global variable. If this is undesirable the normal
|
||||
precautions (double negation or @code{copy_term/2}) must be taken. The
|
||||
@code{b_getval/2} predicate generates errors if @var{Name} is not an atom or
|
||||
the requested variable does not exist.
|
||||
@end table
|
||||
|
||||
@table @code
|
||||
|
||||
@item nb_setval(+@var{Name},+@var{Value})
|
||||
@findex nb_setval/2
|
||||
@snindex nb_setval/2
|
||||
@cnindex nb_setval/2
|
||||
Associates a copy of @var{Value} created with @code{duplicate_term/2}
|
||||
with the atom @var{Name}. Note that this can be used to set an
|
||||
initial value other than @code{[]} prior to backtrackable assignment.
|
||||
|
||||
@item nb_getval(+@var{Name},-@var{Value})
|
||||
@findex nb_getval/2
|
||||
@snindex nb_getval/2
|
||||
@cnindex nb_getval/2
|
||||
The @code{nb_getval/2} predicate is a synonym for b_getval/2, introduced for
|
||||
compatibility and symetry. As most scenarios will use a particular
|
||||
global variable either using non-backtracable or backtrackable
|
||||
assignment, using @code{nb_getval/2} can be used to document that the
|
||||
variable is used non-backtracable.
|
||||
|
||||
@c \predicate{nb_linkval}{2}{+Name, +Value}
|
||||
@c Associates the term @var{Value} with the atom @var{Name} without copying
|
||||
@c it. This is a fast special-purpose variation of nb_setval/2 intended for
|
||||
@c expert users only because the semantics on backtracking to a point
|
||||
@c before creating the link are poorly defined for compound terms. The
|
||||
@c principal term is always left untouched, but backtracking behaviour on
|
||||
@c arguments is undone if the orginal assignment was \jargon{trailed} and
|
||||
@c left alone otherwise, which implies that the history that created the
|
||||
@c term affects the behaviour on backtracking. Please consider the
|
||||
@c following example:
|
||||
|
||||
@c \begin{code}
|
||||
@c demo_nb_linkval :-
|
||||
@c T = nice(N),
|
||||
@c ( N = world,
|
||||
@c nb_linkval(myvar, T),
|
||||
@c fail
|
||||
@c ; nb_getval(myvar, V),
|
||||
@c writeln(V)
|
||||
@c ).
|
||||
@c \end{code}
|
||||
|
||||
@item nb_current(?@var{Name},?@var{Value})
|
||||
@findex nb_current/2
|
||||
@snindex nb_current/2
|
||||
@cnindex nb_current/2
|
||||
Enumerate all defined variables with their value. The order of
|
||||
enumeration is undefined.
|
||||
|
||||
@item nb_delete(?@var{Name})
|
||||
@findex nb_delete/1
|
||||
@snindex nb_delete/1
|
||||
@cnindex nb_delete/1
|
||||
Delete the named global variable.
|
||||
@end table
|
||||
|
||||
@subsection Compatibility of SWI-Prolog Global Variables
|
||||
|
||||
Global variables have been introduced by various Prolog
|
||||
implementations recently. The implementation of them in SWI-Prolog is
|
||||
based on hProlog by Bart Demoen. In discussion with Bart it was
|
||||
decided that the semantics if hProlog @code{nb_setval/2}, which is
|
||||
equivalent to @code{nb_linkval/2} is not acceptable for normal Prolog
|
||||
users as the behaviour is influenced by how builtin predicates
|
||||
constructing terms (@code{read/1}, @code{=../2}, etc.) are implemented.
|
||||
|
||||
GNU-Prolog provides a rich set of global variables, including arrays.
|
||||
Arrays can be implemented easily in SWI-Prolog using @code{functor/3} and
|
||||
@code{setarg/3} due to the unrestricted arity of compound terms.
|
||||
|
||||
|
||||
@node Extensions,Debugging,SWI-Prolog,Top
|
||||
@chapter Extensions to Prolog
|
||||
|
||||
YAP includes several extensions that are not enabled by
|
||||
default, but that can be used to extend the functionality of the
|
||||
system. These options can be set at compilation time by enabling the
|
||||
related compilation flag, as explained in the @code{Makefile}
|
3492
docs/yap.tex
3492
docs/yap.tex
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user