Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the cl-unification Reference Manual, generated automatically by Declt version 4.0 beta 2 "William Riker" on Mon Aug 15 04:07:11 2022 GMT+0.
Next: Systems, Previous: The cl-unification Reference Manual, Up: The cl-unification Reference Manual [Contents][Index]
CL-UNIFICATION ============== Marco Antoniotti (c) 2004-2022 ------------------------------ The directory containing this file you are reading should contain the code and the documentation of the CL-UNIFICATION package. The package is a full-blown library to "unify" arbitrary CL objects while constructing bindings for placeholders (unification variables) in a "template" sublanguage. A NOTE ON FORKING ----------------- Of course you are free to fork the project subject to the current licensing scheme. However, before you do so, I ask you to consider plain old "cooperation" by asking me to become a developer. It helps keeping the entropy level at an acceptable level. Enjoy.
Next: Files, Previous: Introduction, Up: The cl-unification Reference Manual [Contents][Index]
The main system appears first, followed by any subsystem dependency.
The CL-UNIFICATION system.
The system contains the definitions for the ’unification’ machinery.
Marco Antoniotti
BSD
Next: Packages, Previous: Systems, Up: The cl-unification Reference Manual [Contents][Index]
Files are sorted by type and then listed depth-first from the systems components trees.
Next: cl-unification/cl-unification-pkg.lisp, Previous: Lisp, Up: Lisp [Contents][Index]
cl-unification (system).
source-file-type (method).
asdf-system-definition-file (class).
Next: cl-unification/variables.lisp, Previous: cl-unification/cl-unification.asd, Up: Lisp [Contents][Index]
cl-unification (system).
Next: cl-unification/substitutions.lisp, Previous: cl-unification/cl-unification-pkg.lisp, Up: Lisp [Contents][Index]
cl-unification-pkg.lisp (file).
cl-unification (system).
make-var-name (function).
Next: cl-unification/lambda-list-parsing.lisp, Previous: cl-unification/variables.lisp, Up: Lisp [Contents][Index]
variables.lisp (file).
cl-unification (system).
Next: cl-unification/templates-hierarchy.lisp, Previous: cl-unification/substitutions.lisp, Up: Lisp [Contents][Index]
substitutions.lisp (file).
cl-unification (system).
Next: cl-unification/unifier.lisp, Previous: cl-unification/lambda-list-parsing.lisp, Up: Lisp [Contents][Index]
lambda-list-parsing.lisp (file).
cl-unification (system).
Next: cl-unification/match-block.lisp, Previous: cl-unification/templates-hierarchy.lisp, Up: Lisp [Contents][Index]
templates-hierarchy.lisp (file).
cl-unification (system).
Next: cl-unification/apply-substitution.lisp, Previous: cl-unification/unifier.lisp, Up: Lisp [Contents][Index]
unifier.lisp (file).
cl-unification (system).
Previous: cl-unification/match-block.lisp, Up: Lisp [Contents][Index]
match-block.lisp (file).
cl-unification (system).
apply-substitution (generic function).
Next: Definitions, Previous: Files, Up: The cl-unification Reference Manual [Contents][Index]
Packages are listed by definition order.
Next: cl-unification-system, Previous: Packages, Up: Packages [Contents][Index]
The CL.EXT.DACF.UNIFICATION Package.
This package contains all the definitions necessary for the general
Common Lisp unifier to work.
The package also has the "UNIFY" nickname.
common-lisp.
Previous: it.unimib.disco.ma.cl.ext.dacf.unification, Up: Packages [Contents][Index]
asdf-system-definition-file (class).
Next: Indexes, Previous: Packages, Up: The cl-unification Reference Manual [Contents][Index]
Definitions are sorted by export status, category, package, and then by lexicographic order.
Next: Internals, Previous: Definitions, Up: Definitions [Contents][Index]
Next: Macros, Previous: Public Interface, Up: Public Interface [Contents][Index]
Next: Ordinary functions, Previous: Special variables, Up: Public Interface [Contents][Index]
Sets up a lexical environment to evaluate FORMS after an unification.
MATCH unifies a TEMPLATE and an OBJECT and then sets up a lexical
environment where the variables present in the template are bound
lexically. Note that both variable names ’?FOO’ and ’FOO’ are bound
for convenience.
The MATCH form returns the values returned by the evaluation of the
last of the FORMS.
If ERRORP is non-NIL (the default) then the form raises a
UNIFICATION-FAILURE, otherwise the result of evaluating ERROR-VALUE,
whose default is NIL is returned. (Note that UNIFICATION-FAILUREs
raising from the evaluation of FORMS will also be caught and handled
according to ERRORP settings.)
If MATCH-NAMED is not NIL, then a surrounding BLOCK named MATCH-NAMED
is set up around the matching code.
MATCH-CASE sets up a CASE-like environment for multiple template matching clauses.
The syntax of MATCH-CASE comprises a number of clauses of the form
<pre>
clause ::= regular-clause | default-clause
regular-clause ::= ’(’ template ’&body’ forms ’)’
default-clause ::= ’(’ t ’&body’ forms ’)’
| ’(’ ’otherwise’ ’&body’ forms ’)’
</pre>
’form’ and ’forms’ are regular Common Lisp forms.
’template’ is a unification template.
The full syntax of MATCH-CASE is
<pre>
match-case (object &key errorp default-substitution) clauses
</pre>
Each clause evaluates its forms in an environment where the variables
present in the template are bound lexically. Note that both variable
names ’?FOO’ and ’FOO’ are bound for convenience.
The values returned by the MATCH-CASE form are those of the last form in
the first clause that satisfies the match test.
If ERRORP is non-NIL then if none of the regular clauses matches, then
an error of type UNIFICATION-NON-EXAUSTIVE is signalled, regardless of
any default clause. Otherwise, the default clause behaves as a
standard CASE default clause. The default value of ERRORP is NIL.
MATCHING-NAMED is used as BLOCK name around the MATCHING machinery.
DEFAULT-SUBSTITUTION is the substitution to be used for the matching;
it defaults to the empty substitution.
Sets up a lexical environment to evaluate FORMS after an unification.
MATCHF unifies a TEMPLATE and an OBJECT and then sets up a lexical
environment where the variables present in the template are bound
lexically. Note that both variable names ’?FOO’ and ’FOO’ are bound
for convenience.
MATCHF does not ’evaluate’ TEMPLATE (note that using the #T syntax will
generate a template at read-time).
The MATCHF form returns the values returned by the evaluation of the
last of the FORMS.
If ERRORP is non-NIL (the default) then the form raises a
UNIFICATION-FAILURE, otherwise the result of evaluating ERROR-VALUE,
whose default is NIL is returned. (Note that UNIFICATION-FAILUREs
raising from the evaluation of FORMS will also be caught and handled
according to ERRORP settings.)
If MATCH-NAMED is not NIL, then a surrounding BLOCK named MATCH-NAMED
is set up around the matching code.
MATCHF-CASE sets up a CASE-like environment for multiple template matching clauses.
The syntax of MATCHF-CASE comprises a number of clauses of the form
<pre>
clause ::= regular-clause | default-clause
regular-clause ::= ’(’ template ’&body’ forms ’)’
default-clause ::= ’(’ t ’&body’ forms ’)’
| ’(’ ’otherwise’ ’&body’ forms ’)’
</pre>
’form’ and ’forms’ are regular Common Lisp forms.
’template’ is a unification template.
The full syntax of MATCHF-CASE is
matchf-case (object &key errorp default-substitution) clauses
Each clause evaluates its forms in an environment where the variables
present in the template are bound lexically. Note that both variable
names ’?FOO’ and ’FOO’ are bound for convenience.
The values returned by the MATCH-CASE form are those of the last form in
the first clause that satisfies the match test.
If ERRORP is non-NIL then if none of the regular clauses matches, then
an error of type UNIFICATION-NON-EXAUSTIVE is signalled, regardless of
any default clause. Otherwise, the default clause behaves as a
standard CASE default clause. The default value of ERRORP is NIL.
MATCHING-NAMED is used as BLOCK name around the MATCHING machinery.
DEFAULT-SUBSTITUTION is the substitution to be used for the matching;
it defaults to the empty substitution.
Notes:
MATCHF-CASE behaves like MATCH-CASE, but the patterns are not
evaluated; i.e., it relies on MATCHF instead of MATCH to construct the
macro expansion.
MATCHING sets up a COND-like environment for multiple template matching clauses.
The syntax of MATCHING comprises a number of clauses, collected in
MATCH-CLAUSES, of the form
<pre>
clause ::= regular-clause | default-clause
regular-clause ::= ’(’ ’(’ template form ’)’ ’&body’ forms ’)’
default-clause ::= ’(’ ’t’ ’&body’ forms ’)’
| ’(’ ’otherwise’ ’&body’ forms ’)’
</pre>
’form’ and ’forms’ are regular Common Lisp forms.
’template’ is a unification template.
The full syntax of MATCHING is
<pre>
matching (&key errorp default-substitution) clauses
</pre>
Each clause evaluates its forms in an environment where the variables
present in the template are bound lexically. Note that both variable
names ’?FOO’ and ’FOO’ are bound for convenience.
The values returned by the MATCHING form are those of the last form in
the first clause that satisfies the match test.
If ERRORP is non-NIL then if none of the regular clauses matches, then
an error of type UNIFICATION-NON-EXAUSTIVE is signalled, regardless of
any default clause. Otherwise, the default clause behaves as a
standard COND default clause. The default value of ERRORP is NIL.
MATCHING-NAMED is used as BLOCK name around the MATCHING machinery.
DEFAULT-SUBSTITUTION is the substitution to be used for the matching;
it defaults to the empty substitution.
Next: Generic functions, Previous: Macros, Up: Public Interface [Contents][Index]
Finds the value associated to VARIABLE in ENV.
VARIABLE is a unification variable; if ERRORP is non-null an error is
signaled if VARIABLE is not found in the environment ENV.
The function returns two values: the value associated to VARIABLE or
NIL, and an indication about whether an association was actually found
in ENV.
Arguments and Values:
VARIABLE : a unification variable
ENV : and ENVIRONMENT
ERRORP : a generalized Boolean
result : a T
foundp : a BOOLEAN
Exceptional Situations:
If an error is signaled, then it is an instance of UNIFICATION-VARIABLE-UNBOUND.
Notes:
FIND-VARIABLE-VALUE is almost symmetric to IS-VARIABLE-BOUND.
Finds the value associated to the variable S in ENV.
This function is essentialy a convenience wrapper around
FIND-VARIABLE-VALUE. If PLAIN-SYMBOL-P is non-NIL, then the symbol S
is ensured to be a ’unification variable’ (with a #? first
character).
Exceptional Situations:
A UNIFICATION-VARIABLE-UNBOUND may be signaled is ERRORP is non-nil and no association si found for S in ENV.
Next: Standalone methods, Previous: Ordinary functions, Up: Public Interface [Contents][Index]
Applies a SUBSTITUTION to an ITEM.
The ’template’ factory.
Creates a TEMPLATE instance based on the values of KIND and SPEC.
Arguments and Values:
KIND : a T
SPEC : a T
result : a TEMPLATE
Exceptional Situations:
May signal an error if a particular combination of KIND and SPEC is either not consistent or handled.
Returns T if the argument X is a TEMPLATE.
Arguments and Values:
X : any object
result : a BOOLEAN
Unifies two objects A and B given a substitution ENV.
A is a Common Lisp object and B is either a Common Lisp object or a
"template", A and B can be commuted.
The unification rules are rather complex. Each method of the generic
function implements a specific rule of unification.
The generic function returns a ‘substitution’ upon success or it signals a UNIFICATION-FAILURE condition upon failure.
Unifies two strings A and B.
Two strings A and B unify if and only if they satisfy either #’STRING= or
#’STRING-EQUAL. The choice of which of test to perform (#’STRING= or #’STRING-EQUAL)
is made according to the value of the variable
*UNIFY-STRING-CASE-SENSITIVE-P*, which defaults to T.
If A and B unify then an unmodified environment ENV is returned,
otherwise an error of type UNIFICATION-FAILURE is signaled.
Unifies two strings A and B.
Two CHARACTERs A and B unify if and only if they satisfy either #’CHAR= or
#’CHAR-EQUAL. The choice of which of test to perform (#’CHAR= or #’CHAR-EQUAL)
is made according to the value of the variable
*UNIFY-STRING-CASE-SENSITIVE-P*, which defaults to T.
If A and B unify then an unmodified environment ENV is returned,
otherwise an error of type UNIFICATION-FAILURE is signaled.
Unifies two numbers A and B.
Two numbers unify only if and only if they are equal as per the function #’=, in
which case an unmodified envirironment ENV is returned.
Otherwise an error of type UNIFICATION-FAILURE is signalled.
Of course, asking for unification of two floating point numbers may
not yield the expected result.
Unifies a list A and a list B in an environment ENV.
The unification procedure proceedes recursively on each element of
both lists. If two elements cannot be unified then an error of type
UNIFICATION-FAILURE is signaled. Otherwise a possibly extended
environment is returned.
Unifies a symbol B and a list A in an environment ENV.
If A is not a variable then an error of type UNIFICATION-FAILURE is
signaled. If A is a unification variable, then the environment ENV is
extended with a binding for A to B, unless the occurrence check is
called and fails, in which case an error is signaled.
Unifies a symbol A and a list B in an environment ENV.
If A is not a variable then an error of type UNIFICATION-FAILURE is
signaled. If A is a unification variable, then the environment ENV is
extended with a binding for A to B, unless the occurrence check is
called and fails, in which case an error is signaled.
Next: Conditions, Previous: Generic functions, Up: Public Interface [Contents][Index]
asdf/component.
Next: Structures, Previous: Standalone methods, Up: Public Interface [Contents][Index]
simple-error.
This is the condition that is signaled
unbound-variable.
Next: Classes, Previous: Conditions, Up: Public Interface [Contents][Index]
The ENVIRONMENT structure.
The data structure containing the associations (bindings) between variables and values.
structure-object.
list
Next: Types, Previous: Structures, Up: Public Interface [Contents][Index]
The AREF-TEMPLATE Class.
The instances of this class are those object that are used to unify
against a particular element of an ARRAY.
The syntax of these templates is the following:
<pre>
#T(<b>aref</b> (<i>index1</i> ... <i>indexN</i>) <i>item</i>)
</pre>
<pre>
#T(<b>aref</b> <i>index</i> <i>item</i>)
</pre>
The AREF-TEMPLATE syntax denotes the <i>item</i> at <i>index1</i> ...
<i>indexN</i> of an ARRAY. An AREF-TEMPLATE must be unified against a
ARRAY object. <i>item</i> is <em>unified</em> against the element
extracted from the sequence object at <i>index1</i> ... <i>indexN</i>
by the standard function AREF.
The second form is a shorthand.
<pre>
#T(<b>aref</b> <i>index</i> <i>item</i>) <==> #T(<b>aref</b> (<i>index</i>) <i>item</i>)
</pre>
Examples:
cl-prompt> (setf e (unify #(0 1 42 3 4 5) #T(aref 2 ?x)))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
42
cl-prompt> (setq e (unify #(0 1 42 3 4 5) #T(aref 42 ?x)))
==> Error: index 42 out of bounds.
cl-prompt> (setq e (unify 42 #T(aref 42 ?x)))
==> Error: UNIFICATION-FAILURE
cl-prompt> (setq e (unify "This is a string!" #T(aref 4 ?x)))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
#\Space
cl-prompt> (setq e (unify #2A((1 0) (foo bar)) #T(aref (1 1) ?x)))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
BAR
cl-prompt> (setq e (unify #2A((1 0) (foo bar)) #T(aref (1 1) baz)))
==> Error: UNIFICATION-FAILURE
cl-prompt> (setq e (unify #2A((1 0) (foo ?x)) #T(aref (1 1) baz)))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
BAZ
Exceptional Situations:
Unifying an AREF-TEMPLATE against a non-ARRAY object results in an
UNIFICATION-FAILURE error being signaled.
The ARRAY-TEMPLATE Class.
The instances of this class are objects that can be used to unify
against arrays.
The syntax of this particular template is the following:
<pre>
#T(array <shape-template>)
</pre>
<pre>
#T(<CL array type specifier> <shape-template>)
</pre>
<pre>
#T(array ([* | <CL type specifier>] [<dimension spec>]) <shape-template>)
</pre>
Where <shape-template> can be:
<pre>
<shape-template> ::= <sequence-template>
| <destructuring template lambda list>
| (<shape-template>)
</pre>
The ARRAY-TEMPLATE syntax denotes an ARRAY object. An ARRAY-TEMPLATE
must be unified against an ARRAY object. The elements of the array
must be unified against the <shape-template>. Each row of the
array is unified recursively against each element of the
<shape-template>.
Examples:
cl-prompt> (setf e (unify #(0 1 42 3 4 5) #T(array (0 1 ?x 3 4 5))))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
42
cl-prompt> (setq e (unify #(0 1 42 3 4 5) #T(array (0 1 "FOO" 3 4 5))))
==> Error: UNIFICATION-FAILURE
cl-prompt> (setq e (unify #2A((0 1 42) (3 4 5)) #T(array ((0 1 ?x) (3 4 5)))))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
42
cl-prompt> (setq e (unify #2A(("foo" "bar" 42) (3 4 5)) #T(array ((_ _ ?x) (3 4 5)))))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
42
cl-prompt> (setq e (unify #2A(("foo" "bar" 42) (3 4 5)) #T(array (#T(vector _ &rest ?x) (3 4 5)))))
#<ENVIRONMENT xxx>
cl-prompt> (find-variable-value ’?x e)
#("bar" 42)
Exceptional Situations:
Unifying an ARRAY-TEMPLATE against a non-ARRAY object results in an
UNIFICATION-FAILURE error being signaled.
Notes:
<h3>Syntax Note</h3>
The ARRAY-TEMPLATE syntax tries to be easy to use, at the cost of
being overloaded. There is no actual need to have the separate
forms <code>(<b>array</b> (fixnum) ...)</code> and
<code>((<b>array</b> fixnum) ...)</code>.
In a future release they may be conflated. For the time being
they are kept separate as it is unclear which would be better to
provide.
<h3>Elements Unification</h3>
It would be nice to have the possibility to unify against
<em>slices</em> of the array. Alas, this seems non trivial to get
right, and it is left as a future extension of the semantics of
<i><shape-template></i>.
<h3>ARRAY Structural Properties</h3>
For the time being, there is no way to "unify" against structural
properties of vectors like fill pointers and displacements.
The ELEMENT-TEMPLATE Class.
The instances of this class are those object that are used to unify against a particular element of an ARRAY or a SEQUENCE.
The EXPRESSION-TEMPLATE Class.
This class is the root of the ’expression template’ sub-hierarchy.
The TEMPLATE Class.
The root of the hierarchy of template objects.
| Initarg | Value |
|---|---|
| :spec | nil |
(or symbol cons)
:spec
Previous: Classes, Up: Public Interface [Contents][Index]
The SUBSTITUTION type.
The type representing the associations between variables and values.
Notes:
It is a synonim for the structure type ENVIRONMENT.
Previous: Public Interface, Up: Definitions [Contents][Index]
Next: Ordinary functions, Previous: Internals, Up: Internals [Contents][Index]
Next: Generic functions, Previous: Special variables, Up: Internals [Contents][Index]
Finds a BINDING for a VARIABLE in ENV.
The function returns a BINDING for VARIABLE in ENV, if it finds one.
Otherwise returns NIL.
Arguments and Values:
VARIABLE : a unification variable
ENV : and ENVIRONMENT
result : a BINDING or NIL.
Checks whether a VARIABLE is bound in ENV.
The function returns two values: a BOOLEAN that indicates whether
VARIABLE is bound in ENV and its value if so; otherwise the second
value is NIL.
Arguments and Values:
VARIABLE : a unification variable
ENV : and ENVIRONMENT
bounddp : a BOOLEAN
result : a T
Notes:
IS-VARIABLE-BOUND is almost symmetric to FIND-VARIABLE-VALUE.
Next: Conditions, Previous: Ordinary functions, Up: Internals [Contents][Index]
item.
Next: Structures, Previous: Generic functions, Up: Internals [Contents][Index]
program-error.
:item
This slot is read-only.
Condition thrown by ’match’ forms.
The condition UNIFICATION-FAILURE is thrown by ’match’ forms when it
can be established that there are other possible unifications for a
template.
simple-error.
Next: Classes, Previous: Conditions, Up: Internals [Contents][Index]
structure-object.
it.unimib.disco.ma.cl.ext.dacf.unification::bindings
This slot is read-only.
t
This slot is read-only.
Next: Types, Previous: Structures, Up: Internals [Contents][Index]
cl-source-file.
Previous: Definitions, Up: The cl-unification Reference Manual [Contents][Index]
| Jump to: | (
A B C D E F G I K L M N O P R S T U V |
|---|
| Jump to: | (
A B C D E F G I K L M N O P R S T U V |
|---|
Next: Data types, Previous: Functions, Up: Indexes [Contents][Index]
| Jump to: | *
B D E F I K N S T |
|---|
| Jump to: | *
B D E F I K N S T |
|---|
| Jump to: | A B C E F I K L M N O P R S T U V |
|---|
| Jump to: | A B C E F I K L M N O P R S T U V |
|---|