		Search-engine friendly clone of the ACL2 documentation.

Std/system/macro-queries

Macro-keyword-args+

Enhanced variant of macro-keyword-args.

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

This returns the same result as macro-keyword-args, but it is guard-verified and includes run-time checks (which should always succeed) that allow us to prove the return type theorem and to verify the guards without strengthening the guard on wrld. Furthermore, this utility causes an error (via macro-args+) if called on a symbol that does not name a macro.

Definitions and Theorems

Function: macro-keyword-args+-aux

(defun macro-keyword-args+-aux (mac args)
 (declare (xargs :guard (and (symbolp mac) (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)
    ((when (symbolp arg))
     (acons arg nil
            (macro-keyword-args+-aux mac (cdr args))))
    ((unless (and (consp arg)
                  (symbolp (first arg))
                  (consp (cdr arg))
                  (consp (second arg))
                  (eq (car (second arg)) 'quote)
                  (consp (cdr (second arg)))))
     (raise
      "Internal error: ~
                   the keyword macro argument ~x0 of ~x1 ~
                   does not have the expected form."
      arg mac)))
   (acons (first arg)
          (unquote (second arg))
          (macro-keyword-args+-aux mac (cdr args))))))

Theorem: symbol-alistp-of-macro-keyword-args+-aux

(defthm symbol-alistp-of-macro-keyword-args+-aux
  (b* ((keyword-args (macro-keyword-args+-aux mac args)))
    (symbol-alistp keyword-args))
  :rule-classes :rewrite)

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 mac args-after-&key)))
    keyword-args)))

Theorem: symbol-alistp-of-macro-keyword-args+

(defthm symbol-alistp-of-macro-keyword-args+
  (b* ((keyword-args (macro-keyword-args+ mac wrld)))
    (symbol-alistp keyword-args))
  :rule-classes :rewrite)