		Search-engine friendly clone of the ACL2 documentation.

Pattern-match

Def-pattern-match-constructor

Allow pattern-match to recognize a constructor.

Example:

(def-pattern-match-constructor cons consp (car cdr))

For a constructor cname, defines a macro named cname-pattern-matcher which will allow constructs using cname to be recognized by the pattern-match macro; see pattern-match. This macro takes three arguments: the name of the constructor, which is the symbol that pattern-match will recognize; the name of a recognizer function which returns t on objects produced by the constructor; and an ordered list of destructor function names, which when applied to the constructed object return the arguments to the constructor.

For example, say we define a function cons3 that combines three objects into a triple. We define a recognizer, cons3-p, for correctly-formed triples as created by cons3, as well as three accessors, cons3-first, cons3-second, cons3-third. Now we'd like to have a pattern match expression like this

(pattern-match x
       ((cons3 a b c) ... body ..)
       ... other clauses ...)

resolve to this:

(if (cons3-p x)
    (let ((a (cons3-first x))
          (b (cons3-second x))
          (c (cons3-third x)))
      ... body ...)
  ... other conditions ...)

Therefore the pattern match macro must know that the recognizer for a cons3 object is cons3-p, and that the destructors are cons3-first, etc - we don't want to have to write out those names anywhere in the untranslated body. Our solution is that when pattern-match sees a function symbol fun, it returns a call to a macro named fun-pattern-matcher. If this macro does not exist, pattern-match will fail. To easily define such macros, we provide def-pattern-match-constructor, which takes as arguments the constructor name, the recognizer name, and the ordered list of destructors. For example, to allow pattern-match to deal with cons3, we'd call

(def-pattern-match-constructor cons3 cons3-p
  (cons3-first cons3-second cons3-third))

Similarly for cons, the call would be

(def-pattern-match-constructor cons consp (car cdr))

but this is built into the pattern match book.

Pattern-matcher macros may be defined more flexibly without using def-pattern-match-constructor in order to support, for example, macros with variable numbers of arguments; see constructor-pattern-match-macros.