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
This function returns two results.
The first result is an alist
from the keywords
Function:
(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:
(defthm alistp-of-mv-nth-0-of-defmacro+-find-parents/short/long (alistp (mv-nth 0 (defmacro+-find-parents/short/long rest))))
Theorem:
(defthm true-listp-of-mv-nth-1-of-defmacro+-find-parents/short/long (true-listp (mv-nth 1 (defmacro+-find-parents/short/long rest))))