Enhanced variant of macro-required-args.
(macro-required-args+ mac wrld) → 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
Function:
(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:
(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:
(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:
(defthm symbol-listp-of-macro-required-args+ (b* ((required-args (macro-required-args+ mac wrld))) (symbol-listp required-args)) :rule-classes :rewrite)