The notion of unification originated in the field of formal logic (e.g. [R65],) and has been used extensively in Computer Science and Programming Languages. Most notably, Prolog uses the full power of unification.

Unification is also at the core of type checking algorithms in the tradition of Milner's, and a limited form - pattern matching - is available to the user in languages of the ML and Haskell family.

The library presented in these pages provides a full blown unification framework for Common Lisp.

Writing a pattern matcher or a an unifier in Common Lisp is easy, as long as we limit ourselves to manipulate only ATOMs and CONSes.

Alas, it would be much nicer if we could manipulate arbitrary Common Lisp objects as the ML programmer can with arbitrary ML objects.

The library presented here is the first one (to the best of the author's knowledge) that is capable of manipulating arbitrary Common Lisp objects.

To reach the project page, click this link to CL Unification

Pattern matching algorithm