		Search-engine friendly clone of the ACL2 documentation.

Patterns

Pat->al

(pat->al pat data al) extends the alist al by associating the variables from pat with the data from data.

The cars of the new pairs are precisely all the non-NIL atoms of the pattern pat. The cdrs of the new pairs are the objects at corresponding locations in data. For instance,

(pat->al '(a (b) (c d))
          '(1 (2) (3 4))
          nil)
  -->
((a . 1) (b . 2) (c . 3) (d . 4))

The alist is extended with ordinary cons operations; that is, it probably doesn't make much sense for al to be a fast alist, because the new alist won't be fast. See pat->fal for an alternative.

Definitions and Theorems

Function: pat->al

(defun pat->al (pat data al)
  (declare (xargs :guard (data-for-patternp pat data)))
  (if pat (if (atom pat)
              (cons (cons pat data) al)
            (pat->al (car pat)
                     (car data)
                     (pat->al (cdr pat) (cdr data) al)))
    al))

Theorem: pat->al-to-append

(defthm pat->al-to-append
  (implies (syntaxp (not (equal acc ''nil)))
           (equal (pat->al a b acc)
                  (append (pat->al a b nil) acc))))

Theorem: alist-keys-pat->al

(defthm alist-keys-pat->al
  (equal (alist-keys (pat->al p1 p2 nil))
         (pat-flatten1 p1)))