		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-input-processing

Defdefparse-process-inputs

Process all the inputs.

Signature
(defdefparse-process-inputs args ctx state) → (mv erp val state)
Arguments: args — Guard (true-listp args).; ctx — Guard (ctxp ctx).
Returns: val — Type (std::tuple (name common-lisp::symbolp) (pkg-wit common-lisp::symbolp) (grammar common-lisp::symbolp) (prefix common-lisp::symbolp) val) .

If successful, we return the inputs, except that we return the package witnesss instead of the package input.

Definitions and Theorems

Function: defdefparse-process-inputs

(defun defdefparse-process-inputs (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'defdefparse-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((fun (irr)) (list nil nil nil nil))
    ((mv erp name options)
     (partition-rest-and-keyword-args
          args *defdefparse-allowed-options*))
    ((when (or erp (not (consp name))
               (not (endp (cdr name)))))
     (er-soft+
      ctx t (irr)
      "The inputs must be the name (a symbol) ~
                   followed by the options ~&0."
      *defdefparse-allowed-options*))
    (name (car name))
    ((er name :iferr (irr))
     (defdefparse-process-name name ctx state))
    (package-option (assoc-eq :package options))
    ((unless (consp package-option))
     (er-soft+ ctx t (irr)
               "The :PACKAGE input is missing."))
    (package (cdr package-option))
    ((er pkg-wit :iferr (irr))
     (defdefparse-process-package package ctx state))
    (grammar-option (assoc-eq :grammar options))
    ((unless (consp grammar-option))
     (er-soft+ ctx t (irr)
               "The :GRAMMAR input is missing."))
    (grammar (cdr grammar-option))
    ((er grammar :iferr (irr))
     (defdefparse-process-grammar grammar ctx state))
    (prefix-option (assoc-eq :prefix options))
    ((unless (consp prefix-option))
     (er-soft+ ctx t (irr)
               "The :PREFIX input is missing."))
    (prefix (cdr prefix-option))
    ((er prefix :iferr (irr))
     (defdefparse-process-prefix prefix ctx state)))
   (value (list name pkg-wit grammar prefix)))))

Theorem: return-type-of-defdefparse-process-inputs.val

(defthm return-type-of-defdefparse-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defdefparse-process-inputs args ctx state)))
    (std::tuple (name common-lisp::symbolp)
                (pkg-wit common-lisp::symbolp)
                (grammar common-lisp::symbolp)
                (prefix common-lisp::symbolp)
                val))
  :rule-classes :rewrite)

Theorem: true-listp-of-defdefparse-process-inputs.val

(defthm true-listp-of-defdefparse-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defdefparse-process-inputs args ctx state)))
    (true-listp val))
  :rule-classes :type-prescription)