		Search-engine friendly clone of the ACL2 documentation.

Defmacro+-implementation

Defmacro+-extract-parents/short/long

Extract the XDOC keyword options from defmacro+.

This is similar to std::extract-keywords, but more restricted. We introduce a new function here, instead of using std::extract-keywords, to reduce the book inclusions in the defmacro+ book. If std::extract-keywords is refactored at some point, we could use that here and eliminate this more restricted function.

The argument rest of this function consists of the arguments of defmacro+ after the name and macro arguments. See the definition of defmacro+.

This function returns two results. The first result is an alist from the keywords :parents, :short, and :long to their corresponding values; if a keyword is not supplied, it is not in the alist. The second result consists of rest without the keyword options.

Definitions and Theorems

Function: defmacro+-find-parents/short/long

(defun defmacro+-find-parents/short/long (rest)
 (declare (xargs :guard (true-listp rest)))
 (if (endp rest)
     (mv nil nil)
  (let ((next (car rest)))
   (if (member-eq next '(:parents :short :long))
       (if (consp (cdr rest))
           (let ((val (cadr rest)))
             (mv-let (alist rest)
                     (defmacro+-find-parents/short/long (cddr rest))
               (if (assoc-eq next alist)
                   (prog2$ (er hard? 'defmacro+
                               "Duplicate keyword ~x0." next)
                           (mv nil nil))
                 (mv (acons next val alist) rest))))
         (prog2$ (er hard? 'defmacro+
                     "Keyword ~x0 without a value." next)
                 (mv nil nil)))
     (mv-let (alist rest)
             (defmacro+-find-parents/short/long (cdr rest))
       (mv alist (cons next rest)))))))

Theorem: alistp-of-mv-nth-0-of-defmacro+-find-parents/short/long

(defthm alistp-of-mv-nth-0-of-defmacro+-find-parents/short/long
  (alistp (mv-nth 0
                  (defmacro+-find-parents/short/long rest))))

Theorem: true-listp-of-mv-nth-1-of-defmacro+-find-parents/short/long

(defthm true-listp-of-mv-nth-1-of-defmacro+-find-parents/short/long
  (true-listp (mv-nth 1
                      (defmacro+-find-parents/short/long rest))))