		Search-engine friendly clone of the ACL2 documentation.

Std/system/macro-queries

Macro-required-args

Required arguments of a macro, in order.

Signature
(macro-required-args mac wrld) → required-args
Arguments: mac — Guard (symbolp mac).; wrld — Guard (plist-worldp wrld).
Returns: required-args — A symbol-listp.

The arguments of a macro form a list that optionally starts with &whole followed by another symbol, continues with zero or more symbols that do not start with & (which are the required arguments) and possibly ends with a symbol starting with & followed by more things.

After removing &whole and the symbol following it (if the list of arguments starts with &whole), we collect all the arguments until either the end of the list is reached or a symbol starting with & is encountered.

See macro-required-args+ for an enhanced variant of this utility.

Definitions and Theorems

Function: macro-required-args-aux

(defun
   macro-required-args-aux (args)
   (declare (xargs :guard (true-listp args)))
   (let ((__function__ 'macro-required-args-aux))
        (declare (ignorable __function__))
        (if (endp args)
            nil
            (b* ((arg (car args)))
                (if (lambda-keywordp arg)
                    nil
                    (cons arg
                          (macro-required-args-aux (cdr args))))))))

Function: macro-required-args

(defun macro-required-args (mac wrld)
       (declare (xargs :guard (and (symbolp mac)
                                   (plist-worldp wrld))))
       (let ((__function__ 'macro-required-args))
            (declare (ignorable __function__))
            (b* ((all-args (macro-args mac wrld)))
                (if (endp all-args)
                    nil
                    (if (eq (car all-args) '&whole)
                        (macro-required-args-aux (cddr all-args))
                        (macro-required-args-aux all-args))))))