update docs
This commit is contained in:
parent
3009987985
commit
57ecd61b95
621
docs/chr.md
Normal file
621
docs/chr.md
Normal file
@ -0,0 +1,621 @@
|
|||||||
|
|
||||||
|
@section CHR CHR: Constraint Handling Rules
|
||||||
|
@ingroup SWILibrary
|
||||||
|
@{
|
||||||
|
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:
|
||||||
|
|
||||||
|
+ T. Schrijvers, and B. Demoen, <em>The K.U.Leuven CHR System: Implementation and Application</em>, First Workshop on Constraint Handling Rules: Selected
|
||||||
|
Contributions (Fruwirth, T. and Meister, M., eds.), pp. 1--5, 2004.
|
||||||
|
|
||||||
|
@defgroup CHR_Introduction Introduction
|
||||||
|
@ingroup CHR
|
||||||
|
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
@defgroup CHR_Syntax_and_Semantics Syntax and Semantics
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
We present informally the syntax and semantics of CHR.
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Syntax CHR Syntax
|
||||||
|
@ingroup CHR_Syntax_and_Semantics
|
||||||
|
@{
|
||||||
|
|
||||||
|
The syntax of CHR rules in hProlog is the following:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
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(`)`)].
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
Additional syntax-related terminology:
|
||||||
|
|
||||||
|
+ *head:* the constraints in an `actual_rule` before
|
||||||
|
the arrow (either `<=>` or `==>`)
|
||||||
|
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Semantics Semantics
|
||||||
|
@ingroup CHR_Syntax_and_Semantics
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Rule_Types Rules
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
There are three different kinds of rules, each with their specific semantics:
|
||||||
|
|
||||||
|
+ simplification
|
||||||
|
The simplification rule removes the constraints in its head and calls its body.
|
||||||
|
|
||||||
|
+ propagation
|
||||||
|
The propagation rule calls its body exactly once for the constraints in
|
||||||
|
its head.
|
||||||
|
|
||||||
|
+ simpagation
|
||||||
|
The simpagation rule removes the constraints in its head after the
|
||||||
|
`\` 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:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
constraints1 \ constraints2 <=> body
|
||||||
|
~~~~~
|
||||||
|
_constraints1_
|
||||||
|
constraints are not called in the body.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Rule_Names Rule Names
|
||||||
|
@ingroup CHR_Rule_Types
|
||||||
|
@{
|
||||||
|
|
||||||
|
Naming a rule is optional and has no semantical meaning. It only functions
|
||||||
|
as documentation for the programmer.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHRPragmas Pragmas
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
The semantics of the pragmas are:
|
||||||
|
|
||||||
|
+ passive(Identifier)
|
||||||
|
The constraint in the head of a rule _Identifier_ can only act as a
|
||||||
|
passive constraint in that rule.
|
||||||
|
|
||||||
|
|
||||||
|
Additional pragmas may be released in the future.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Options Options
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
It is possible to specify options that apply to all the CHR rules in the module.
|
||||||
|
Options are specified with the `option/2` declaration:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
option(Option,Value).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
Available options are:
|
||||||
|
|
||||||
|
+ check_guard_bindings
|
||||||
|
This option controls whether guards should be checked for illegal
|
||||||
|
variable bindings or not. Possible values for this option are
|
||||||
|
`on`, to enable the checks, and `off`, to disable the
|
||||||
|
checks.
|
||||||
|
|
||||||
|
+ optimize
|
||||||
|
This is an experimental option controlling the degree of optimization.
|
||||||
|
Possible values are `full`, to enable all available
|
||||||
|
optimizations, and `off` (default), to disable all optimizations.
|
||||||
|
The default is derived from the SWI-Prolog flag `optimise`, where
|
||||||
|
`true` is mapped to `full`. Therefore the commandline
|
||||||
|
option `-O` provides full CHR optimization.
|
||||||
|
If optimization is enabled, debugging should be disabled.
|
||||||
|
|
||||||
|
+ debug
|
||||||
|
This options enables or disables the possibility to debug the CHR code.
|
||||||
|
Possible values are `on` (default) and `off`. See
|
||||||
|
`debugging` for more details on debugging. The default is
|
||||||
|
derived from the prolog flag `generate_debug_info`, which
|
||||||
|
is `true` by default. See `-nodebug`.
|
||||||
|
If debugging is enabled, optimization should be disabled.
|
||||||
|
|
||||||
|
+ 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 `-`, `+` or `?`.
|
||||||
|
The latter is the default. The meaning is the following:
|
||||||
|
|
||||||
|
+ -
|
||||||
|
The corresponding argument of every occurrence
|
||||||
|
of the constraint is always unbound.
|
||||||
|
+ +
|
||||||
|
The corresponding argument of every occurrence
|
||||||
|
of the constraint is always ground.
|
||||||
|
+ ?
|
||||||
|
The corresponding argument of every occurrence
|
||||||
|
of the constraint can have any instantiation, which may change
|
||||||
|
over time. This is the default value.
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
+ 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:
|
||||||
|
|
||||||
|
+ int
|
||||||
|
The corresponding argument of every occurrence
|
||||||
|
of the constraint is an integer number.
|
||||||
|
+ float
|
||||||
|
...{} a floating point number.
|
||||||
|
+ number
|
||||||
|
...{} a number.
|
||||||
|
+ natural
|
||||||
|
...{} a positive integer.
|
||||||
|
+ any
|
||||||
|
The corresponding argument of every occurrence
|
||||||
|
of the constraint can have any type. This is the default value.
|
||||||
|
|
||||||
|
|
||||||
|
Currently, type declarations are only used to improve certain
|
||||||
|
optimizations (guard simplification, occurrence subsumption, ...{}).
|
||||||
|
|
||||||
|
+ 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
|
||||||
|
`type(` _name_`,` _list_`)`, where
|
||||||
|
_name_ is a term and _list_ is a list of alternatives.
|
||||||
|
Variables can be used to define generic types. Recursive definitions
|
||||||
|
are allowed. Examples are
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
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)]).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
The mode, type_declaration and type_definition options are provided
|
||||||
|
for backward compatibility. The new syntax is described below.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
@defgroup CHR_in_YAP_Programs CHR in Prolog Programs
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
The CHR constraints defined in a particulary chr file are
|
||||||
|
associated with a module. The default module is `user`. One should
|
||||||
|
never load different chr files with the same CHR module name.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Constraint_declaration Constraint declaration
|
||||||
|
@ingroup CHR_in_YAP_Programs
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
Every constraint used in CHR rules has to be declared.
|
||||||
|
There are two ways to do this. The old style is as follows:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
option(type_definition,type(list(T),[ [] , [T|list(T)] ]).
|
||||||
|
option(mode,foo(+,?)).
|
||||||
|
option(type_declaration,foo(list(int),float)).
|
||||||
|
:- constraints foo/2, bar/0.
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
The new style is as follows:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- chr_type list(T) ---> [] ; [T|list(T)].
|
||||||
|
:- constraints foo(+list(int),?float), bar.
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Compilation Compilation
|
||||||
|
@ingroup CHR_in_YAP
|
||||||
|
|
||||||
|
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 chr. They are activated if the compiled file
|
||||||
|
has the chr extension or after finding a declaration of the
|
||||||
|
format below.
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- constraints ...
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
It is adviced to define CHR rules in a module file, where the module
|
||||||
|
declaration is immediately followed by including the chr
|
||||||
|
library as examplified below:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- module(zebra, [ zebra/0 ]).
|
||||||
|
:- use_module(library(chr)).
|
||||||
|
|
||||||
|
:- constraints ...
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Debugging CHR Debugging
|
||||||
|
@ingroup CHR_in_YAP
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
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 debug, whose default is derived
|
||||||
|
from the SWI-Prolog flag `generate_debug_info`. Therefore debug
|
||||||
|
info is provided unless the `-nodebug` is used.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Ports Ports
|
||||||
|
@ingroup CHR_Debugging
|
||||||
|
|
||||||
|
|
||||||
|
For CHR constraints the four standard ports are defined:
|
||||||
|
|
||||||
|
+ call
|
||||||
|
A new constraint is called and becomes active.
|
||||||
|
+ 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.
|
||||||
|
+ fail
|
||||||
|
An active constraint fails.
|
||||||
|
+ redo
|
||||||
|
An active constraint starts looking for an alternative solution.
|
||||||
|
|
||||||
|
|
||||||
|
In addition to the above ports, CHR constraints have five additional
|
||||||
|
ports:
|
||||||
|
|
||||||
|
+ wake
|
||||||
|
A suspended constraint is woken and becomes active.
|
||||||
|
+ insert
|
||||||
|
An active constraint has tried all rules and is suspended in
|
||||||
|
the constraint store.
|
||||||
|
+ remove
|
||||||
|
An active or passive constraint is removed from the constraint
|
||||||
|
store, if it had been inserted.
|
||||||
|
+ try
|
||||||
|
An active constraints tries a rule with possibly
|
||||||
|
some passive constraints. The try port is entered
|
||||||
|
just before committing to the rule.
|
||||||
|
+ apply
|
||||||
|
An active constraints commits to a rule with possibly
|
||||||
|
some passive constraints. The apply port is entered
|
||||||
|
just after committing to the rule.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Tracing Tracing
|
||||||
|
@ingroup CHR_Debugging
|
||||||
|
|
||||||
|
|
||||||
|
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 `call`,
|
||||||
|
`exit`, `fail`, `wake` and `apply` ports,
|
||||||
|
accepting debug commands, and simply write out the other ports.
|
||||||
|
|
||||||
|
The following debug commans are currently supported:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
CHR debug options:
|
||||||
|
|
||||||
|
<cr> creep c creep
|
||||||
|
s skip
|
||||||
|
g ancestors
|
||||||
|
n nodebug
|
||||||
|
b break
|
||||||
|
a abort
|
||||||
|
f fail
|
||||||
|
? help h help
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
Their meaning is:
|
||||||
|
|
||||||
|
+ creep
|
||||||
|
Step to the next port.
|
||||||
|
+ skip
|
||||||
|
Skip to exit port of this call or wake port.
|
||||||
|
+ ancestors
|
||||||
|
Print list of ancestor call and wake ports.
|
||||||
|
+ nodebug
|
||||||
|
Disable the tracer.
|
||||||
|
+ break
|
||||||
|
Enter a recursive Prolog toplevel. See break/0.
|
||||||
|
+ abort
|
||||||
|
Exit to the toplevel. See abort/0.
|
||||||
|
+ fail
|
||||||
|
Insert failure in execution.
|
||||||
|
+ help
|
||||||
|
Print the above available debug options.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Debugging_Predicates CHR Debugging Predicates
|
||||||
|
@ingroup CHR_Debugging
|
||||||
|
|
||||||
|
|
||||||
|
The chr module contains several predicates that allow
|
||||||
|
inspecting and printing the content of the constraint store.
|
||||||
|
|
||||||
|
+ chr_trace
|
||||||
|
Activate the CHR tracer. By default the CHR tracer is activated and
|
||||||
|
deactivated automatically by the Prolog predicates trace/0 and
|
||||||
|
notrace/0.
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Examples Examples
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Here are two example constraint solvers written in CHR.
|
||||||
|
|
||||||
|
+
|
||||||
|
The program below defines a solver with one constraint,
|
||||||
|
`leq/2`, which is a less-than-or-equal constraint.
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- 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).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
+
|
||||||
|
The program below implements a simple finite domain
|
||||||
|
constraint solver.
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- 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).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Compatibility Compatibility with SICStus CHR
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
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:
|
||||||
|
|
||||||
|
+ [The handler/1 declaration]
|
||||||
|
In SICStus every CHR module requires a `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.
|
||||||
|
|
||||||
|
+ [The rules/1 declaration]
|
||||||
|
In SICStus, for every CHR module it is possible to only enable a subset
|
||||||
|
of the available rules through the `rules/1` declaration. The
|
||||||
|
declaration is valid syntax in SWI-Prolog, but has no effect. A
|
||||||
|
warning is given during compilation.
|
||||||
|
|
||||||
|
+ [Sourcefile naming]
|
||||||
|
SICStus uses a two-step compiler, where chr files are
|
||||||
|
first translated into pl files. For SWI-Prolog CHR
|
||||||
|
rules may be defined in a file with any extension.
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CHR_Guidelines Guidelines
|
||||||
|
@ingroup CHR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
In this section we cover several guidelines on how to use CHR to write
|
||||||
|
constraint solvers and how to do so efficiently.
|
||||||
|
|
||||||
|
+ [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:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
{constraint \ constraint <=> true}.
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
+ [Multi-headed rules]
|
||||||
|
Multi-headed rules are executed more efficiently when the constraints
|
||||||
|
share one or more variables.
|
||||||
|
|
||||||
|
+ [Mode and type declarations]
|
||||||
|
Provide mode and type declarations to get more efficient program execution.
|
||||||
|
Make sure to disable debug (`-nodebug`) and enable optimization
|
||||||
|
(`-O`).
|
||||||
|
|
||||||
|
@}
|
||||||
|
|
||||||
|
|
||||||
|
@}
|
132
docs/clpqr.md
Normal file
132
docs/clpqr.md
Normal file
@ -0,0 +1,132 @@
|
|||||||
|
|
||||||
|
/** @defgroup CLPQR Constraint Logic Programming over Reals
|
||||||
|
@ingroup SWILibrary
|
||||||
|
@{
|
||||||
|
|
||||||
|
YAP now uses the CLP(R) package developed by <em>Leslie De Koninck</em>,
|
||||||
|
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,
|
||||||
|
<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 *CLP(QR)*
|
||||||
|
implementation.
|
||||||
|
|
||||||
|
Please note that the clpr library is <em>not</em> an
|
||||||
|
`autoload` library and therefore this library must be loaded
|
||||||
|
explicitely before using it:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- use_module(library(clpr)).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
@defgroup CLPR_Solver_Predicates Solver Predicates
|
||||||
|
@ingroup CLPQR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
The following predicates are provided to work with constraints:
|
||||||
|
|
||||||
|
|
||||||
|
* @defgroup CLPR_Syntax Syntax of the predicate arguments
|
||||||
|
@ingroup YAPPackages
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
<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 \
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CLPR_Unification Use of unification
|
||||||
|
@ingroup CLPQR
|
||||||
|
@{
|
||||||
|
|
||||||
|
Instead of using the `{}/1` predicate, you can also use the standard
|
||||||
|
unification mechanism to store constraints. The following code samples
|
||||||
|
are equivalent:
|
||||||
|
|
||||||
|
+ Unification with a variable
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
{X =:= Y}
|
||||||
|
{X = Y}
|
||||||
|
X = Y
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
+ Unification with a number
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
{X =:= 5.0}
|
||||||
|
{X = 5.0}
|
||||||
|
X = 5.0
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup CLPR_NonhYlinear_Constraints Non-Linear Constraints
|
||||||
|
@ingroup CLPQR
|
||||||
|
@{
|
||||||
|
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
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)
|
||||||
|
~~~~~
|
515
docs/syntax.md
Normal file
515
docs/syntax.md
Normal file
@ -0,0 +1,515 @@
|
|||||||
|
@defgroup Syntax YAP Syntax
|
||||||
|
@ingroup YAPProgramming
|
||||||
|
@{
|
||||||
|
@page YAPSyntax Syntax
|
||||||
|
|
||||||
|
We will describe the syntax of YAP at two levels. We first will
|
||||||
|
describe the syntax for Prolog terms. In a second level we describe
|
||||||
|
the \a tokens from which Prolog \a terms are
|
||||||
|
built.
|
||||||
|
|
||||||
|
@section Formal_Syntax Syntax of Terms
|
||||||
|
|
||||||
|
Below, we describe the syntax of YAP terms from the different
|
||||||
|
classes of tokens defined above. The formalism used will be <em>BNF</em>,
|
||||||
|
extended where necessary with attributes denoting integer precedence or
|
||||||
|
operator type.
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
term ----> subterm(1200) end_of_term_marker
|
||||||
|
|
||||||
|
subterm(N) ----> term(M) [M <= N]
|
||||||
|
|
||||||
|
term(N) ----> op(N, fx) subterm(N-1)
|
||||||
|
| op(N, fy) subterm(N)
|
||||||
|
| subterm(N-1) op(N, xfx) subterm(N-1)
|
||||||
|
| subterm(N-1) op(N, xfy) subterm(N)
|
||||||
|
| subterm(N) op(N, yfx) subterm(N-1)
|
||||||
|
| subterm(N-1) op(N, xf)
|
||||||
|
| subterm(N) op(N, yf)
|
||||||
|
|
||||||
|
term(0) ----> atom '(' arguments ')'
|
||||||
|
| '(' subterm(1200) ')'
|
||||||
|
| '{' subterm(1200) '}'
|
||||||
|
| list
|
||||||
|
| string
|
||||||
|
| number
|
||||||
|
| atom
|
||||||
|
| variable
|
||||||
|
|
||||||
|
arguments ----> subterm(999)
|
||||||
|
| subterm(999) ',' arguments
|
||||||
|
|
||||||
|
list ----> '[]'
|
||||||
|
| '[' list_expr ']'
|
||||||
|
|
||||||
|
list_expr ----> subterm(999)
|
||||||
|
| subterm(999) list_tail
|
||||||
|
|
||||||
|
list_tail ----> ',' list_expr
|
||||||
|
| ',..' subterm(999)
|
||||||
|
| '|' subterm(999)
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
Notes:
|
||||||
|
|
||||||
|
+ \a op(N,T) denotes an atom which has been previously declared with type
|
||||||
|
\a T and base precedence \a N.
|
||||||
|
|
||||||
|
+ Since ',' is itself a pre-declared operator with type \a xfy and
|
||||||
|
precedence 1000, is \a subterm starts with a '(', \a op must be
|
||||||
|
followed by a space to avoid ambiguity with the case of a functor
|
||||||
|
followed by arguments, e.g.:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
+ (a,b) [the same as '+'(','(a,b)) of arity one]
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
versus
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
+(a,b) [the same as '+'(a,b) of arity two]
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
+
|
||||||
|
In the first rule for term(0) no blank space should exist between
|
||||||
|
\a atom and '('.
|
||||||
|
|
||||||
|
+
|
||||||
|
Each term to be read by the YAP parser must end with a single
|
||||||
|
dot, followed by a blank (in the sense mentioned in the previous
|
||||||
|
paragraph). When a name consisting of a single dot could be taken for
|
||||||
|
the end of term marker, the ambiguity should be avoided by surrounding the
|
||||||
|
dot with single quotes.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@section Tokens Prolog Tokens
|
||||||
|
|
||||||
|
Prolog tokens are grouped into the following categories:
|
||||||
|
|
||||||
|
@subsection Numbers Numbers
|
||||||
|
|
||||||
|
Numbers can be further subdivided into integer and floating-point numbers.
|
||||||
|
|
||||||
|
@subsubsection Integers
|
||||||
|
|
||||||
|
Integer numbers
|
||||||
|
are described by the following regular expression:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
<integer> := {<digit>+<single-quote>|0{xXo}}<alpha_numeric_char>+
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
where {...} stands for optionality, \a + optional repetition (one or
|
||||||
|
more times), \a \\\<digit\\\> denotes one of the characters 0 ... 9, \a |
|
||||||
|
denotes or, and \a \\\<single-quote\\\> denotes the character "'". The digits
|
||||||
|
before the \a \\\<single-quote\\\> character, when present, form the number
|
||||||
|
basis, that can go from 0, 1 and up to 36. Letters from `A` to
|
||||||
|
`Z` are used when the basis is larger than 10.
|
||||||
|
|
||||||
|
Note that if no basis is specified then base 10 is assumed. Note also
|
||||||
|
that the last digit of an integer token can not be immediately followed
|
||||||
|
by one of the characters 'e', 'E', or '.'.
|
||||||
|
|
||||||
|
Following the ISO standard, YAP also accepts directives of the
|
||||||
|
form `0x` to represent numbers in hexadecimal base and of the form
|
||||||
|
`0o` to represent numbers in octal base. For usefulness,
|
||||||
|
YAP also accepts directives of the form `0X` to represent
|
||||||
|
numbers in hexadecimal base.
|
||||||
|
|
||||||
|
Example:
|
||||||
|
the following tokens all denote the same integer
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
10 2'1010 3'101 8'12 16'a 36'a 0xa 0o12
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
Numbers of the form `0'a` are used to represent character
|
||||||
|
constants. So, the following tokens denote the same integer:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
0'd 100
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
YAP (version 6.3.4) supports integers that can fit
|
||||||
|
the word size of the machine. This is 32 bits in most current machines,
|
||||||
|
but 64 in some others, such as the Alpha running Linux or Digital
|
||||||
|
Unix. The scanner will read larger or smaller integers erroneously.
|
||||||
|
|
||||||
|
@subsubsection Floats
|
||||||
|
|
||||||
|
Floating-point numbers are described by:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
<float> := <digit>+{<dot><digit>+}
|
||||||
|
<exponent-marker>{<sign>}<digit>+
|
||||||
|
|<digit>+<dot><digit>+
|
||||||
|
{<exponent-marker>{<sign>}<digit>+}
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
where \a \\\<dot\\\> denotes the decimal-point character '.',
|
||||||
|
\a \\\<exponent-marker\\\> denotes one of 'e' or 'E', and \a \\\<sign\\\> denotes
|
||||||
|
one of '+' or '-'.
|
||||||
|
|
||||||
|
Examples:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
10.0 10e3 10e-3 3.1415e+3
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
Floating-point numbers are represented as a double in the target
|
||||||
|
machine. This is usually a 64-bit number.
|
||||||
|
|
||||||
|
@subsection Strings Character Strings
|
||||||
|
|
||||||
|
Strings are described by the following rules:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
string --> '"' string_quoted_characters '"'
|
||||||
|
|
||||||
|
string_quoted_characters --> '"' '"' string_quoted_characters
|
||||||
|
string_quoted_characters --> '\'
|
||||||
|
escape_sequence string_quoted_characters
|
||||||
|
string_quoted_characters -->
|
||||||
|
string_character string_quoted_characters
|
||||||
|
|
||||||
|
escape_sequence --> 'a' | 'b' | 'r' | 'f' | 't' | 'n' | 'v'
|
||||||
|
escape_sequence --> '\' | '"' | ''' | '`'
|
||||||
|
escape_sequence --> at_most_3_octal_digit_seq_char '\'
|
||||||
|
escape_sequence --> 'x' at_most_2_hexa_digit_seq_char '\'
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
where `string_character` in any character except the double quote
|
||||||
|
and escape characters.
|
||||||
|
|
||||||
|
Examples:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
"" "a string" "a double-quote:"""
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
The first string is an empty string, the last string shows the use of
|
||||||
|
double-quoting. The implementation of YAP represents strings as
|
||||||
|
lists of integers. Since YAP 4.3.0 there is no static limit on string
|
||||||
|
size.
|
||||||
|
|
||||||
|
Escape sequences can be used to include the non-printable characters
|
||||||
|
`a` (alert), `b` (backspace), `r` (carriage return),
|
||||||
|
`f` (form feed), `t` (horizontal tabulation), `n` (new
|
||||||
|
line), and `v` (vertical tabulation). Escape sequences also be
|
||||||
|
include the meta-characters `\\`, `"`, `'`, and
|
||||||
|
```. Last, one can use escape sequences to include the characters
|
||||||
|
either as an octal or hexadecimal number.
|
||||||
|
|
||||||
|
The next examples demonstrates the use of escape sequences in YAP:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
"\x0c\" "\01\" "\f" "\\"
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
The first three examples return a list including only character 12 (form
|
||||||
|
feed). The last example escapes the escape character.
|
||||||
|
|
||||||
|
Escape sequences were not available in C-Prolog and in original
|
||||||
|
versions of YAP up to 4.2.0. Escape sequences can be disable by using:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
:- yap_flag(character_escapes,false).
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
@subsection Atoms Atoms
|
||||||
|
|
||||||
|
Atoms are defined by one of the following rules:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
atom --> solo-character
|
||||||
|
atom --> lower-case-letter name-character*
|
||||||
|
atom --> symbol-character+
|
||||||
|
atom --> single-quote single-quote
|
||||||
|
atom --> ''' atom_quoted_characters '''
|
||||||
|
|
||||||
|
atom_quoted_characters --> ''' ''' atom_quoted_characters
|
||||||
|
atom_quoted_characters --> '\' atom_sequence string_quoted_characters
|
||||||
|
atom_quoted_characters --> character string_quoted_characters
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
where:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
<solo-character> denotes one of: ! ;
|
||||||
|
<symbol-character> denotes one of: # & * + - . / : <
|
||||||
|
= > ? @ \ ^ ~ `
|
||||||
|
<lower-case-letter> denotes one of: a...z
|
||||||
|
<name-character> denotes one of: _ a...z A...Z 0....9
|
||||||
|
<single-quote> denotes: '
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
and `string_character` denotes any character except the double quote
|
||||||
|
and escape characters. Note that escape sequences in strings and atoms
|
||||||
|
follow the same rules.
|
||||||
|
|
||||||
|
Examples:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
a a12x '$a' ! => '1 2'
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
Version `4.2.0` of YAP removed the previous limit of 256
|
||||||
|
characters on an atom. Size of an atom is now only limited by the space
|
||||||
|
available in the system.
|
||||||
|
|
||||||
|
@subsection Variables Variables
|
||||||
|
|
||||||
|
Variables are described by:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
<variable-starter><variable-character>+
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
where
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
<variable-starter> denotes one of: _ A...Z
|
||||||
|
<variable-character> denotes one of: _ a...z A...Z
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
If a variable is referred only once in a term, it needs not to be named
|
||||||
|
and one can use the character `_` to represent the variable. These
|
||||||
|
variables are known as anonymous variables. Note that different
|
||||||
|
occurrences of `_` on the same term represent <em>different</em>
|
||||||
|
anonymous variables.
|
||||||
|
|
||||||
|
@subsection Punctuation_Tokens Punctuation Tokens
|
||||||
|
|
||||||
|
Punctuation tokens consist of one of the following characters:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
( ) , [ ] { } |
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
These characters are used to group terms.
|
||||||
|
|
||||||
|
@subsection Layout Layout
|
||||||
|
Any characters with ASCII code less than or equal to 32 appearing before
|
||||||
|
a token are ignored.
|
||||||
|
|
||||||
|
All the text appearing in a line after the character \a % is taken to
|
||||||
|
be a comment and ignored (including \a %). Comments can also be
|
||||||
|
inserted by using the sequence `/\*` to start the comment and
|
||||||
|
`\*` followed by `/` to finish it. In the presence of any sequence of comments or
|
||||||
|
layout characters, the YAP parser behaves as if it had found a
|
||||||
|
single blank character. The end of a file also counts as a blank
|
||||||
|
character for this purpose.
|
||||||
|
|
||||||
|
@section Encoding Wide Character Support
|
||||||
|
|
||||||
|
YAP now implements a SWI-Prolog compatible interface to wide
|
||||||
|
characters and the Universal Character Set (UCS). The following text
|
||||||
|
was adapted from the SWI-Prolog manual.
|
||||||
|
|
||||||
|
YAP now supports wide characters, characters with character
|
||||||
|
codes above 255 that cannot be represented in a single byte.
|
||||||
|
<em>Universal Character Set</em> (UCS) is the ISO/IEC 10646 standard
|
||||||
|
that specifies a unique 31-bits unsigned integer for any character in
|
||||||
|
any language. It is a superset of 16-bit Unicode, which in turn is
|
||||||
|
a superset of ISO 8859-1 (ISO Latin-1), a superset of US-ASCII. UCS
|
||||||
|
can handle strings holding characters from multiple languages and
|
||||||
|
character classification (uppercase, lowercase, digit, etc.) and
|
||||||
|
operations such as case-conversion are unambiguously defined.
|
||||||
|
|
||||||
|
For this reason YAP, following SWI-Prolog, has two representations for
|
||||||
|
atoms. If the text fits in ISO Latin-1, it is represented as an array
|
||||||
|
of 8-bit characters. Otherwise the text is represented as an array of
|
||||||
|
wide chars, which may take 16 or 32 bits. This representational issue
|
||||||
|
is completely transparent to the Prolog user. Users of the foreign
|
||||||
|
language interface sometimes need to be aware of these issues though.
|
||||||
|
|
||||||
|
Character coding comes into view when characters of strings need to be
|
||||||
|
read from or written to file or when they have to be communicated to
|
||||||
|
other software components using the foreign language interface. In this
|
||||||
|
section we only deal with I/O through streams, which includes file I/O
|
||||||
|
as well as I/O through network sockets.
|
||||||
|
|
||||||
|
@subsection Stream_Encoding Wide character encodings on streams
|
||||||
|
|
||||||
|
Although characters are uniquely coded using the UCS standard
|
||||||
|
internally, streams and files are byte (8-bit) oriented and there are a
|
||||||
|
variety of ways to represent the larger UCS codes in an 8-bit octet
|
||||||
|
stream. The most popular one, especially in the context of the web, is
|
||||||
|
UTF-8. Bytes 0...127 represent simply the corresponding US-ASCII
|
||||||
|
character, while bytes 128...255 are used for multi-byte
|
||||||
|
encoding of characters placed higher in the UCS space. Especially on
|
||||||
|
MS-Windows the 16-bit Unicode standard, represented by pairs of bytes is
|
||||||
|
also popular.
|
||||||
|
|
||||||
|
Prolog I/O streams have a property called <em>encoding</em> which
|
||||||
|
specifies the used encoding that influence `get_code/2` and
|
||||||
|
`put_code/2` as well as all the other text I/O predicates.
|
||||||
|
|
||||||
|
The default encoding for files is derived from the Prolog flag
|
||||||
|
`encoding`, which is initialised from the environment. If the
|
||||||
|
environment variable `LANG` ends in "UTF-8", this encoding is
|
||||||
|
assumed. Otherwise the default is `text` and the translation is
|
||||||
|
left to the wide-character functions of the C-library (note that the
|
||||||
|
Prolog native UTF-8 mode is considerably faster than the generic
|
||||||
|
`mbrtowc()` one). The encoding can be specified explicitly in
|
||||||
|
load_files/2 for loading Prolog source with an alternative
|
||||||
|
encoding, `open/4` when opening files or using `set_stream/2` on
|
||||||
|
any open stream (not yet implemented). For Prolog source files we also
|
||||||
|
provide the `encoding/1` directive that can be used to switch
|
||||||
|
between encodings that are compatible to US-ASCII (`ascii`,
|
||||||
|
`iso_latin_1`, `utf8` and many locales).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
For
|
||||||
|
additional information and Unicode resources, please visit
|
||||||
|
<http://www.unicode.org/>.
|
||||||
|
|
||||||
|
YAP currently defines and supports the following encodings:
|
||||||
|
|
||||||
|
+ octet
|
||||||
|
Default encoding for <em>binary</em> streams. This causes
|
||||||
|
the stream to be read and written fully untranslated.
|
||||||
|
|
||||||
|
+ ascii
|
||||||
|
7-bit encoding in 8-bit bytes. Equivalent to `iso_latin_1`,
|
||||||
|
but generates errors and warnings on encountering values above
|
||||||
|
127.
|
||||||
|
|
||||||
|
+ iso_latin_1
|
||||||
|
8-bit encoding supporting many western languages. This causes
|
||||||
|
the stream to be read and written fully untranslated.
|
||||||
|
|
||||||
|
+ text
|
||||||
|
C-library default locale encoding for text files. Files are read and
|
||||||
|
written using the C-library functions `mbrtowc()` and
|
||||||
|
`wcrtomb()`. This may be the same as one of the other locales,
|
||||||
|
notably it may be the same as `iso_latin_1` for western
|
||||||
|
languages and `utf8` in a UTF-8 context.
|
||||||
|
|
||||||
|
+ utf8
|
||||||
|
Multi-byte encoding of full UCS, compatible to `ascii`.
|
||||||
|
See above.
|
||||||
|
|
||||||
|
+ unicode_be
|
||||||
|
Unicode Big Endian. Reads input in pairs of bytes, most
|
||||||
|
significant byte first. Can only represent 16-bit characters.
|
||||||
|
|
||||||
|
+ unicode_le
|
||||||
|
Unicode Little Endian. Reads input in pairs of bytes, least
|
||||||
|
significant byte first. Can only represent 16-bit characters.
|
||||||
|
|
||||||
|
|
||||||
|
Note that not all encodings can represent all characters. This implies
|
||||||
|
that writing text to a stream may cause errors because the stream
|
||||||
|
cannot represent these characters. The behaviour of a stream on these
|
||||||
|
errors can be controlled using `open/4` or `set_stream/2` (not
|
||||||
|
implemented). Initially the terminal stream write the characters using
|
||||||
|
Prolog escape sequences while other streams generate an I/O exception.
|
||||||
|
|
||||||
|
@subsection BOM BOM: Byte Order Mark
|
||||||
|
|
||||||
|
From Stream Encoding, you may have got the impression that
|
||||||
|
text-files are complicated. This section deals with a related topic,
|
||||||
|
making live often easier for the user, but providing another worry to
|
||||||
|
the programmer. *BOM* or <em>Byte Order Marker</em> is a technique
|
||||||
|
for identifying Unicode text-files as well as the encoding they
|
||||||
|
use. Such files start with the Unicode character `0xFEFF`, a
|
||||||
|
non-breaking, zero-width space character. This is a pretty unique
|
||||||
|
sequence that is not likely to be the start of a non-Unicode file and
|
||||||
|
uniquely distinguishes the various Unicode file formats. As it is a
|
||||||
|
zero-width blank, it even doesn't produce any output. This solves all
|
||||||
|
problems, or ...
|
||||||
|
|
||||||
|
Some formats start of as US-ASCII and may contain some encoding mark to
|
||||||
|
switch to UTF-8, such as the `encoding="UTF-8"` in an XML header.
|
||||||
|
Such formats often explicitly forbid the the use of a UTF-8 BOM. In
|
||||||
|
other cases there is additional information telling the encoding making
|
||||||
|
the use of a BOM redundant or even illegal.
|
||||||
|
|
||||||
|
The BOM is handled by the `open/4` predicate. By default, text-files are
|
||||||
|
probed for the BOM when opened for reading. If a BOM is found, the
|
||||||
|
encoding is set accordingly and the property `bom(true)` is
|
||||||
|
available through stream_property/2. When opening a file for
|
||||||
|
writing, writing a BOM can be requested using the option
|
||||||
|
`bom(true)` with `open/4`.
|
||||||
|
|
||||||
|
@subsection Operators Summary of YAP Predefined Operators
|
||||||
|
|
||||||
|
The Prolog syntax caters for operators of three main kinds:
|
||||||
|
|
||||||
|
+ prefix;
|
||||||
|
+ infix;
|
||||||
|
+ postfix.
|
||||||
|
|
||||||
|
|
||||||
|
Each operator has precedence in the range 1 to 1200, and this
|
||||||
|
precedence is used to disambiguate expressions where the structure of the
|
||||||
|
term denoted is not made explicit using brackets. The operator of higher
|
||||||
|
precedence is the main functor.
|
||||||
|
|
||||||
|
If there are two operators with the highest precedence, the ambiguity
|
||||||
|
is solved analyzing the types of the operators. The possible infix types are:
|
||||||
|
_xfx_, _xfy_, and _yfx_.
|
||||||
|
|
||||||
|
With an operator of type _xfx_ both sub-expressions must have lower
|
||||||
|
precedence than the operator itself, unless they are bracketed (which
|
||||||
|
assigns to them zero precedence). With an operator type _xfy_ only the
|
||||||
|
left-hand sub-expression must have lower precedence. The opposite happens
|
||||||
|
for _yfx_ type.
|
||||||
|
|
||||||
|
A prefix operator can be of type _fx_ or _fy_.
|
||||||
|
A postfix operator can be of type _xf_ or _yf_.
|
||||||
|
The meaning of the notation is analogous to the above.
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
a + b * c
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
means
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
a + (b * c)
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
as + and \* have the following types and precedences:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
:-op(500,yfx,'+').
|
||||||
|
:-op(400,yfx,'*').
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
Now defining
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
:-op(700,xfy,'++').
|
||||||
|
:-op(700,xfx,'=:=').
|
||||||
|
a ++ b =:= c
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
means
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
a ++ (b =:= c)
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
The following is the list of the declarations of the predefined operators:
|
||||||
|
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
:-op(1200,fx,['?-', ':-']).
|
||||||
|
:-op(1200,xfx,[':-','-->']).
|
||||||
|
:-op(1150,fx,[block,dynamic,mode,public,multifile,meta_predicate,
|
||||||
|
sequential,table,initialization]).
|
||||||
|
:-op(1100,xfy,[';','|']).
|
||||||
|
:-op(1050,xfy,->).
|
||||||
|
:-op(1000,xfy,',').
|
||||||
|
:-op(999,xfy,'.').
|
||||||
|
:-op(900,fy,['\+', not]).
|
||||||
|
:-op(900,fx,[nospy, spy]).
|
||||||
|
:-op(700,xfx,[@>=,@=<,@<,@>,<,=,>,=:=,=\=,\==,>=,=<,==,\=,=..,is]).
|
||||||
|
:-op(500,yfx,['\/','/\','+','-']).
|
||||||
|
:-op(500,fx,['+','-']).
|
||||||
|
:-op(400,yfx,['<<','>>','//','*','/']).
|
||||||
|
:-op(300,xfx,mod).
|
||||||
|
:-op(200,xfy,['^','**']).
|
||||||
|
:-op(50,xfx,same).
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
@}
|
189
docs/threads.md
Normal file
189
docs/threads.md
Normal file
@ -0,0 +1,189 @@
|
|||||||
|
|
||||||
|
@defgroup Threads Threads
|
||||||
|
@ingroup YAPExtensions
|
||||||
|
|
||||||
|
|
||||||
|
YAP implements a SWI-Prolog compatible multithreading
|
||||||
|
library. Like in SWI-Prolog, Prolog threads have their own stacks and
|
||||||
|
only share the Prolog <em>heap</em>: predicates, records, flags and other
|
||||||
|
global non-backtrackable data. The package is based on the POSIX thread
|
||||||
|
standard (Butenhof:1997:PPT) used on most popular systems except
|
||||||
|
for MS-Windows.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Creating_and_Destroying_Prolog_Threads Creating and Destroying Prolog Threads
|
||||||
|
@ingroup Threads
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@pred thread_create(: _Goal_, - _Id_, + _Options_)
|
||||||
|
|
||||||
|
|
||||||
|
Create a new Prolog thread (and underlying C-thread) and start it
|
||||||
|
by executing _Goal_. If the thread is created successfully, the
|
||||||
|
thread-identifier of the created thread is unified to _Id_.
|
||||||
|
_Options_ is a list of options. Currently defined options are:
|
||||||
|
|
||||||
|
+ stack
|
||||||
|
Set the limit in K-Bytes to which the Prolog stacks of
|
||||||
|
this thread may grow. If omitted, the limit of the calling thread is
|
||||||
|
used. See also the commandline `-S` option.
|
||||||
|
|
||||||
|
+ trail
|
||||||
|
Set the limit in K-Bytes to which the trail stack of this thread may
|
||||||
|
grow. If omitted, the limit of the calling thread is used. See also the
|
||||||
|
commandline option `-T`.
|
||||||
|
|
||||||
|
+ alias
|
||||||
|
Associate an alias-name with the thread. This named may be used to
|
||||||
|
refer to the thread and remains valid until the thread is joined
|
||||||
|
(see thread_join/2).
|
||||||
|
|
||||||
|
+ at_exit
|
||||||
|
Define an exit hook for the thread. This hook is called when the thread
|
||||||
|
terminates, no matter its exit status.
|
||||||
|
|
||||||
|
+ detached
|
||||||
|
If `false` (default), the thread can be waited for using
|
||||||
|
thread_join/2. thread_join/2 must be called on this thread
|
||||||
|
to reclaim the all resources associated to the thread. If `true`,
|
||||||
|
the system will reclaim all associated resources automatically after the
|
||||||
|
thread finishes. Please note that thread identifiers are freed for reuse
|
||||||
|
after a detached thread finishes or a normal thread has been joined.
|
||||||
|
See also thread_join/2 and thread_detach/1.
|
||||||
|
|
||||||
|
|
||||||
|
The _Goal_ argument is <em>copied</em> to the new Prolog engine.
|
||||||
|
This implies further instantiation of this term in either thread does
|
||||||
|
not have consequences for the other thread: Prolog threads do not share
|
||||||
|
data from their stacks.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Monitoring_Threads Monitoring Threads
|
||||||
|
@ingroup Threads
|
||||||
|
|
||||||
|
|
||||||
|
Normal multi-threaded applications should not need these the predicates
|
||||||
|
from this section because almost any usage of these predicates is
|
||||||
|
unsafe. For example checking the existence of a thread before signalling
|
||||||
|
it is of no use as it may vanish between the two calls. Catching
|
||||||
|
exceptions using catch/3 is the only safe way to deal with
|
||||||
|
thread-existence errors.
|
||||||
|
|
||||||
|
These predicates are provided for diagnosis and monitoring tasks.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Thread_Communication Thread communication
|
||||||
|
@ingroup Threads
|
||||||
|
|
||||||
|
|
||||||
|
Prolog threads can exchange data using dynamic predicates, database
|
||||||
|
records, and other globally shared data. These provide no suitable means
|
||||||
|
to wait for data or a condition as they can only be checked in an
|
||||||
|
expensive polling loop. <em>Message queues</em> provide a means for
|
||||||
|
threads to wait for data or conditions without using the CPU.
|
||||||
|
|
||||||
|
Each thread has a message-queue attached to it that is identified
|
||||||
|
by the thread. Additional queues are created using
|
||||||
|
`message_queue_create/2`.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@pred thread_send_message(+ _Term_)
|
||||||
|
|
||||||
|
|
||||||
|
Places _Term_ in the message-queue of the thread running the goal.
|
||||||
|
Any term can be placed in a message queue, but note that the term is
|
||||||
|
copied to the receiving thread and variable-bindings are thus lost.
|
||||||
|
This call returns immediately.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Signalling_Threads Signalling Threads
|
||||||
|
@ingroup Threadas
|
||||||
|
|
||||||
|
|
||||||
|
These predicates provide a mechanism to make another thread execute some
|
||||||
|
goal as an <em>interrupt</em>. Signalling threads is safe as these
|
||||||
|
interrupts are only checked at safe points in the virtual machine.
|
||||||
|
Nevertheless, signalling in multi-threaded environments should be
|
||||||
|
handled with care as the receiving thread may hold a <em>mutex</em>
|
||||||
|
(see with_mutex/2). Signalling probably only makes sense to start
|
||||||
|
debugging threads and to cancel no-longer-needed threads with throw/1,
|
||||||
|
where the receiving thread should be designed carefully do handle
|
||||||
|
exceptions at any point.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Threads_and_Dynamic_Predicates Threads and Dynamic Predicates
|
||||||
|
@ingroup Threads
|
||||||
|
|
||||||
|
|
||||||
|
Besides queues threads can share and exchange data using dynamic
|
||||||
|
predicates. The multi-threaded version knows about two types of
|
||||||
|
dynamic predicates. By default, a predicate declared <em>dynamic</em>
|
||||||
|
(see dynamic/1) is shared by all threads. Each thread may
|
||||||
|
assert, retract and run the dynamic predicate. Synchronisation inside
|
||||||
|
Prolog guarantees the consistency of the predicate. Updates are
|
||||||
|
<em>logical</em>: visible clauses are not affected by assert/retract
|
||||||
|
after a query started on the predicate. In many cases primitive from
|
||||||
|
thread synchronisation should be used to ensure application invariants on
|
||||||
|
the predicate are maintained.
|
||||||
|
|
||||||
|
Besides shared predicates, dynamic predicates can be declared with the
|
||||||
|
thread_local/1 directive. Such predicates share their
|
||||||
|
attributes, but the clause-list is different in each thread.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
@defgroup Thread_Synchronisation Thread Synchronisation
|
||||||
|
|
||||||
|
All
|
||||||
|
internal Prolog operations are thread-safe. This implies two Prolog
|
||||||
|
threads can operate on the same dynamic predicate without corrupting the
|
||||||
|
consistency of the predicate. This section deals with user-level
|
||||||
|
<em>mutexes</em> (called <em>monitors</em> in ADA or
|
||||||
|
<em>critical-sections</em> by Microsoft). A mutex is a
|
||||||
|
<em>MUT</em>ual <em>EX</em>clusive device, which implies at most one thread
|
||||||
|
can <em>hold</em> a mutex.
|
||||||
|
|
||||||
|
Mutexes are used to realise related updates to the Prolog database.
|
||||||
|
With `related', we refer to the situation where a `transaction' implies
|
||||||
|
two or more changes to the Prolog database. For example, we have a
|
||||||
|
predicate `address/2`, representing the address of a person and we want
|
||||||
|
to change the address by retracting the old and asserting the new
|
||||||
|
address. Between these two operations the database is invalid: this
|
||||||
|
person has either no address or two addresses, depending on the
|
||||||
|
assert/retract order.
|
||||||
|
|
||||||
|
Here is how to realise a correct update:
|
||||||
|
|
||||||
|
~~~~~
|
||||||
|
:- initialization
|
||||||
|
mutex_create(addressbook).
|
||||||
|
|
||||||
|
change_address(Id, Address) :-
|
||||||
|
mutex_lock(addressbook),
|
||||||
|
retractall(address(Id, _)),
|
||||||
|
asserta(address(Id, Address)),
|
||||||
|
mutex_unlock(addressbook).
|
||||||
|
~~~~~
|
||||||
|
|
||||||
|
|
||||||
|
|
15665
docs/yapdocs.md
Normal file
15665
docs/yapdocs.md
Normal file
File diff suppressed because it is too large
Load Diff
Reference in New Issue
Block a user