		Search-engine friendly clone of the ACL2 documentation.

Std/system/macro-queries

Macro-required-args+

Enhanced variant of macro-required-args.

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

This returns the same result as macro-required-args, but it is guard-verified and includes run-time checks (which should always succeed) that allows us to prove the return type theorem and to verify 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-required-args+-aux

(defun
 macro-required-args+-aux (mac args)
 (declare (xargs :guard (and (symbolp mac) (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
     (if
      (symbolp arg)
      (cons arg
            (macro-required-args+-aux mac (cdr args)))
      (raise
       "Internal error: ~
                     the required macro argument ~x0 of ~x1 is not a symbol."
       arg mac)))))))

Theorem: symbol-listp-of-macro-required-args+-aux

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

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 mac (cddr all-args))
                      (macro-required-args+-aux mac all-args))))))

Theorem: symbol-listp-of-macro-required-args+

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