		Search-engine friendly clone of the ACL2 documentation.

Constructor-preliminaries

Partition-macro-args

Partition the arguments of a macro into a list and an alist.

The XDOC constructors are macros. Some of them take a varying number of ``regular'' arguments and a varying number of keyword arguments, but the keywords are not predefined and the two kinds of arguments may be intermixed.

This function partitions these intermixed arguments into a list of regular arguments and an alist of keyword arguments. Each keyword encountered in the input list is regarded as starting a keyword argument (unless it follows one already); if a keyword is not followed by a value, it is an error. This function does not check for duplicate keywords. The output list and alists are in the same order as in the input.

Definitions and Theorems

Function: partition-macro-args

(defun partition-macro-args (args ctx)
  (declare (xargs :guard (true-listp args)))
  (cond ((endp args) (mv nil nil))
        ((keywordp (car args))
         (if (consp (cdr args))
             (mv-let (rest-list rest-alist)
                     (partition-macro-args (cddr args) ctx)
               (mv rest-list
                   (acons (car args)
                          (cadr args)
                          rest-alist)))
           (prog2$ (er hard?
                       ctx "Missing value for keyword ~x0."
                       (car args))
                   (mv nil nil))))
        (t (mv-let (rest-list rest-alist)
                   (partition-macro-args (cdr args) ctx)
             (mv (cons (car args) rest-list)
                 rest-alist)))))

Theorem: true-listp-of-mv-nth-0-partition-macro-args

(defthm true-listp-of-mv-nth-0-partition-macro-args
  (true-listp (mv-nth 0 (partition-macro-args args ctx))))

Theorem: alistp-of-mv-nth-1-partition-macro-args

(defthm alistp-of-mv-nth-1-partition-macro-args
  (alistp (mv-nth 1 (partition-macro-args args ctx))))