		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-input-processing

Defgrammar-process-inputs

Process all the inputs.

Signature
(defgrammar-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) (file common-lisp::stringp) (untranslate booleanp) (well-formed booleanp) (closed booleanp) (parents defgrammar-anyp) (short defgrammar-anyp) (long defgrammar-anyp) (other-events true-listp) val) , given (true-listp args).

Definitions and Theorems

Function: defgrammar-process-inputs

(defun defgrammar-process-inputs (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'defgrammar-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((fun (irr))
     (list nil "" nil nil nil nil nil nil nil))
    ((mv args other-events)
     (std::split-/// ctx args))
    ((mv erp name options)
     (partition-rest-and-keyword-args
          args *defgrammar-allowed-options*))
    ((when (or erp (not (consp name))
               (not (endp (cdr name)))))
     (er-soft+
      ctx t (irr)
      "The inputs must be the constant name ~
                   followed by the options ~&0 ~
                   and possibly /// followed by other events."
      *defgrammar-allowed-options*))
    (name (car name))
    ((er & :iferr (irr))
     (defgrammar-process-name name ctx state))
    (file-option (assoc-eq :file options))
    ((unless (consp file-option))
     (er-soft+ ctx t (irr)
               "The :FILE input must be supplied."))
    (file (cdr file-option))
    ((er &)
     (ensure-value-is-string$ file "The :FILE input" t (irr)))
    (untranslate-option (assoc-eq :untranslate options))
    (untranslate (if (consp untranslate-option)
                     (cdr untranslate-option)
                   nil))
    ((er &)
     (ensure-value-is-boolean$ untranslate
                               "The :UNTRANSLATE input" t (irr)))
    (well-formed-option (assoc-eq :well-formed options))
    (well-formed (if (consp well-formed-option)
                     (cdr well-formed-option)
                   nil))
    ((er &)
     (ensure-value-is-boolean$ well-formed
                               "The :WELL-FORMED input" t (irr)))
    (closed-option (assoc-eq :closed options))
    (closed (if (consp closed-option)
                (cdr closed-option)
              nil))
    ((er &)
     (ensure-value-is-boolean$ closed "The :CLOSED input" t (irr)))
    (parents-option (assoc-eq :parents options))
    (parents (if (consp parents-option)
                 (cdr parents-option)
               :absent))
    (short-option (assoc-eq :short options))
    (short (if (consp short-option)
               (cdr short-option)
             :absent))
    (long-option (assoc-eq :long options))
    (long (if (consp long-option)
              (cdr long-option)
            :absent)))
   (value (list name file untranslate well-formed closed
                parents short long other-events)))))

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

(defthm return-type-of-defgrammar-process-inputs.val
  (implies (true-listp args)
           (b* (((mv acl2::?erp ?val acl2::?state)
                 (defgrammar-process-inputs args ctx state)))
             (std::tuple (name common-lisp::symbolp)
                         (file common-lisp::stringp)
                         (untranslate booleanp)
                         (well-formed booleanp)
                         (closed booleanp)
                         (parents defgrammar-anyp)
                         (short defgrammar-anyp)
                         (long defgrammar-anyp)
                         (other-events true-listp)
                         val)))
  :rule-classes :rewrite)

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

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