macro-args

(defund macro-argp
  (arg)
  (declare (xargs :guard t))
  (or (symbolp arg)
    (and (true-listp arg)
      (or (and (= 1 (len arg)) (symbolp (first arg)))
        (and (= 2 (len arg))
          (symbolp (first arg))
          (myquotep (second arg)))
        (and (= 3 (len arg))
          (symbolp (first arg))
          (myquotep (second arg))
          (symbolp (third arg)))))))

(defund macro-arg-listp
  (args)
  (declare (xargs :guard t))
  (if (atom args)
    (null args)
    (and (macro-argp (first args))
      (macro-arg-listp (rest args)))))

(defund keyword-or-optional-arg-name-and-default
  (macro-arg)
  (declare (xargs :guard (macro-argp macro-arg)
      :guard-hints (("Goal" :in-theory (enable macro-argp)))))
  (if (symbolp macro-arg)
    (mv macro-arg nil)
    (if (< (len macro-arg) 2)
      (mv (first macro-arg) nil)
      (mv (first macro-arg) (unquote (second macro-arg))))))

(defund maybe-skip-whole-arg
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (if (and (consp macro-args) (eq '&whole (first macro-args)))
    (cddr macro-args)
    macro-args))

(defund remove-rest-and-body-from-macro-args
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (if (endp macro-args)
    nil
    (let ((arg (first macro-args)))
      (if (or (eq '&rest arg) (eq '&body arg))
        (remove-rest-and-body-from-macro-args (rest (rest macro-args)))
        (cons arg
          (remove-rest-and-body-from-macro-args (rest macro-args)))))))

(defund remove-allow-other-keys-from-macro-args
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (if (endp macro-args)
    nil
    (let ((arg (first macro-args)))
      (if (eq '&allow-other-keys arg)
        (remove-allow-other-keys-from-macro-args (rest macro-args))
        (cons arg
          (remove-allow-other-keys-from-macro-args (rest macro-args)))))))

(defun lambda-list-keywordp
  (macro-arg)
  (declare (xargs :guard t))
  (member-eq macro-arg
    '(&whole &optional &rest &body &key &allow-other-keys)))

(defund split-args-at-lambda-list-keyword
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (if (endp macro-args)
    (mv nil nil)
    (let ((macro-arg (first macro-args)))
      (if (lambda-list-keywordp macro-arg)
        (mv nil macro-args)
        (mv-let (args-before remaining-args)
          (split-args-at-lambda-list-keyword (rest macro-args))
          (mv (cons macro-arg args-before) remaining-args))))))

(defun split-macro-args
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (mv-let (required-args remaining-args)
    (split-args-at-lambda-list-keyword macro-args)
    (if (not (symbol-listp required-args))
      (prog2$ (er hard?
          'split-macro-args
          "Found a non-symbol required arg among: ~x0."
          required-args)
        (mv nil nil nil))
      (if (endp remaining-args)
        (mv required-args nil nil)
        (mv-let (optional-args remaining-args)
          (if (eq '&optional (first remaining-args))
            (split-args-at-lambda-list-keyword (rest remaining-args))
            (mv nil remaining-args))
          (if (endp remaining-args)
            (mv required-args optional-args nil)
            (if (eq '&key (first remaining-args))
              (mv required-args optional-args (rest remaining-args))
              (prog2$ (er hard?
                  'split-macro-args
                  "Unexpected lambda-list-keyword: ~x0."
                  (first remaining-args))
                (mv nil nil nil)))))))))

(defun keyword-or-optional-arg-names
  (keyword-args)
  (declare (xargs :guard (macro-arg-listp keyword-args)
      :guard-hints (("Goal" :in-theory (enable macro-arg-listp macro-argp)))))
  (if (atom keyword-args)
    nil
    (let ((keyword-arg (first keyword-args)))
      (mv-let (name default)
        (keyword-or-optional-arg-name-and-default keyword-arg)
        (declare (ignore default))
        (cons name
          (keyword-or-optional-arg-names (rest keyword-args)))))))

(defund extract-required-and-optional-and-keyword-args
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (let* ((macro-args (maybe-skip-whole-arg macro-args)) (macro-args (remove-rest-and-body-from-macro-args macro-args))
      (macro-args (remove-allow-other-keys-from-macro-args macro-args)))
    (split-macro-args macro-args)))

(defund macro-arg-names
  (macro-args)
  (declare (xargs :guard (macro-arg-listp macro-args)))
  (mv-let (required-args optional-args keyword-args)
    (extract-required-and-optional-and-keyword-args macro-args)
    (append required-args
      (keyword-or-optional-arg-names optional-args)
      (keyword-or-optional-arg-names keyword-args))))