		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))))))