Patterns
A representation for structured data.
A pattern is a simple kind of structure for representing
structured data.
Patterns were historically used in the EMOD hardware simulator, where they
played a large role. In esim we have largely moved toward just using
alists instead of patterns, but patterns are still used in a few places, most
notably the representation of module input and output lists.
A definition for patterns is:
- NIL is a special, empty pattern
- Any non-nil atom is a pattern variable (a kind of pattern), and
- A cons of two patterns is a pattern.
This means that any ACL2 object is a pattern, but here is perhaps a typical
example of a pattern:
(a (b0 b1) (c (d0 d1) e)) ;; example pattern
We say that this pattern is compatible with certain other ACL2
objects that have a similar cons structure, such as:
(1 (2 3) (4 (5 6) 7)) ;; example data
The general idea is that the example data "fits" into the pattern by
saying:
a = 1 b0 = 2 c = 4 d0 = 5 e = 7
b1 = 3 d1 = 6
Another way of thinking about patterns is as follows. Consider an alist
like ((a . 1) (b . 2) (c . 3)). It is often convenient to have the keys
and values together. But if you remember that your keys are (a b c), then
you could separately work with your values, (1 2 3). This is the basic
idea behind patterns, except that the keys and values can be structured instead
of just being lists.
This is a little awkward, and it would probably usually be better to just
work with alists everywhere.
Subtopics
- Pat->al
- (pat->al pat data al) extends the alist al by associating the
variables from pat with the data from data.
- Pat-flatten1
- Flatten a pattern into a list of atoms (without an accumulator).
- Member-of-pat-flatten
- (member-of-pat-flatten a pat) is an optimized way to ask if a is
a member of (pat-flatten1 pat).
- Similar-patternsp
- (similar-patternsp pat1 pat2) determines whether pat1 and pat2
are compatible with the same data.
- Pat-flatten
- Flatten a pattern into a list of atoms (with an accumulator).
- Al->pat
- (al->pat pat al default) builds a new data object that is compatible with
pat, using the data from al and providing the default value for
missing keys.
- Assoc-pat->al
- (assoc-pat->al key pat data) is an optimized way to look up a particular
key, given some pattern and data.
- Subsetp-of-pat-flatten
- (subsetp-of-pat-flatten x pat) is an optimized way to ask if x
is a subset of (pat-flatten1 pat).
- Pat->fal
- Alternative to pat->al that generates a fast alist.
- Data-for-patternp
- (data-for-patternp pat data) determines whether data is compatible
with the pattern pat.
