		Search-engine friendly clone of the ACL2 documentation.

Std/system/macro-queries

Macro-keyword-args

Keyword arguments of a macro, in order, with their default values.

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

Starting from the full argument list of the macro, first we find &key in the list; if not found, we return nil (i.e. no keyword arguments). Otherwise, we scan and collect information from the remaining arguments, until we reach either the end of the macro argument list or a symbol starting with &....

Keyword arguments have one of the forms name, (name 'default), (name 'default predicate), where name is the argument name (a symbol) default its default value (quoted), and predicate is another symbol. When we find a keyword argument, we put name and default value as a pair into an alist.

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

Definitions and Theorems

Function: macro-keyword-args-aux

(defun macro-keyword-args-aux (args)
  (declare (xargs :guard (true-listp args)))
  (let ((__function__ 'macro-keyword-args-aux))
    (declare (ignorable __function__))
    (b* (((when (endp args)) nil)
         (arg (car args))
         ((when (lambda-keywordp arg)) nil)
         (name (if (atom arg) arg (first arg)))
         (default (if (atom arg)
                      nil
                    (unquote (second arg)))))
      (acons name default
             (macro-keyword-args-aux (cdr args))))))

Function: macro-keyword-args

(defun macro-keyword-args (mac wrld)
  (declare (xargs :guard (and (symbolp mac)
                              (plist-worldp wrld))))
  (let ((__function__ 'macro-keyword-args))
    (declare (ignorable __function__))
    (b* ((all-args (macro-args mac wrld))
         (args-after-&key (cdr (member-eq '&key all-args)))
         (keyword-args (macro-keyword-args-aux args-after-&key)))
      keyword-args)))