  This paper proposes a pattern-matching system that enables non-linear
pattern-matching against unfree data types. The system allows multiple
occurrences of the same variables in a pattern, multiple results of
pattern-matching and modularization of the way of pattern-matching for each
data type at the same time. It enables us to represent pattern-matching against
not only algebraic data types but also unfree data types such as sets, graphs
and any other data types whose data have no canonical form and multiple ways of
decomposition. I have realized that with a rule that pattern-matching is
executed from the left side of a pattern and a rule that a binding to a
variable in a pattern can be referred to in its right side of the pattern.
Furthermore, I have realized modularization of these patterns with lexical
scoping. In my system, a pattern is not a first class object, but a
pattern-function that obtains only patterns and returns a pattern is a first
class object. This restriction simplifies the non-linear pattern-matching
system with lexical scoping. I have already implemented the pattern-matching
system in the Egison programming language.
