		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-input-processing

Deftreeops-process-inputs

Process all the inputs.

Signature
(deftreeops-process-inputs args call wrld) → (mv erp redundantp grammar rules prefix print)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: redundantp — Type (booleanp redundantp).; grammar — Type (common-lisp::symbolp grammar).; rules — Type (rulelistp rules).; prefix — Type (common-lisp::symbolp prefix).; print — Type (evmac-input-print-p print).

If the redundantp result is t, the grammar, rules, and prefix results are irrelevant.

Definitions and Theorems

Function: deftreeops-process-inputs

(defun deftreeops-process-inputs (args call wrld)
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__ 'deftreeops-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil nil :error)
    ((mv erp grammar options)
     (partition-rest-and-keyword-args
          args *deftreeops-allowed-options*))
    ((when (or erp (not (consp grammar))
               (not (endp (cdr grammar)))))
     (reterr
      (msg
       "The inputs must be the constant name for the grammar ~
                      followed by the options ~&0."
       *deftreeops-allowed-options*)))
    (grammar (car grammar))
    ((erp redundantp grammar rules)
     (deftreeops-process-grammar grammar call wrld))
    ((when redundantp)
     (retok t nil nil nil :error))
    (prefix-option (assoc-eq :prefix options))
    ((unless (consp prefix-option))
     (reterr (msg "The :PREFIX input must be supplied.")))
    (prefix (cdr prefix-option))
    ((erp prefix)
     (deftreeops-process-prefix prefix))
    (print-option (assoc-eq :print options))
    (print (if print-option (cdr print-option)
             :result))
    ((erp print)
     (deftreeops-process-print print)))
   (retok nil grammar rules prefix print))))

Theorem: booleanp-of-deftreeops-process-inputs.redundantp

(defthm booleanp-of-deftreeops-process-inputs.redundantp
  (b* (((mv acl2::?erp ?redundantp ?grammar
            ?rules ?prefix common-lisp::?print)
        (deftreeops-process-inputs args call wrld)))
    (booleanp redundantp))
  :rule-classes :rewrite)

Theorem: symbolp-of-deftreeops-process-inputs.grammar

(defthm symbolp-of-deftreeops-process-inputs.grammar
  (b* (((mv acl2::?erp ?redundantp ?grammar
            ?rules ?prefix common-lisp::?print)
        (deftreeops-process-inputs args call wrld)))
    (common-lisp::symbolp grammar))
  :rule-classes :rewrite)

Theorem: rulelistp-of-deftreeops-process-inputs.rules

(defthm rulelistp-of-deftreeops-process-inputs.rules
  (b* (((mv acl2::?erp ?redundantp ?grammar
            ?rules ?prefix common-lisp::?print)
        (deftreeops-process-inputs args call wrld)))
    (rulelistp rules))
  :rule-classes :rewrite)

Theorem: symbolp-of-deftreeops-process-inputs.prefix

(defthm symbolp-of-deftreeops-process-inputs.prefix
  (b* (((mv acl2::?erp ?redundantp ?grammar
            ?rules ?prefix common-lisp::?print)
        (deftreeops-process-inputs args call wrld)))
    (common-lisp::symbolp prefix))
  :rule-classes :rewrite)

Theorem: evmac-input-print-p-of-deftreeops-process-inputs.print

(defthm evmac-input-print-p-of-deftreeops-process-inputs.print
  (b* (((mv acl2::?erp ?redundantp ?grammar
            ?rules ?prefix common-lisp::?print)
        (deftreeops-process-inputs args call wrld)))
    (evmac-input-print-p print))
  :rule-classes :rewrite)