		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-process-inputs

Process all the inputs.

Signature
(parteval-process-inputs old static new-name new-enable thm-name thm-enable verify-guards untranslate print show-only ctx state) → (mv erp result state)
Returns: result — A tuple (old$ static$ new-name$ new-enable$ thm-name$ verify-guards$ case names-to-avoid) satisfying (typed-tuplep symbolp symbol-alistp symbolp booleanp symbolp booleanp natp symbol-listp result).

The inputs are processed in the order in which they appear in the documentation, except that :verify-guards is processed just before static because the result of processing :verify-guards is used to process static. old is processed before :verify-guards because the result of processing old is used to process :verify-guards. :verify-guards is also used to process old, but it is only tested for equality with t (see parteval-process-old).

Definitions and Theorems

Function: parteval-process-inputs

(defun parteval-process-inputs
       (old static new-name new-enable
            thm-name thm-enable verify-guards
            untranslate print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'parteval-process-inputs))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((er old$)
     (parteval-process-old old verify-guards ctx state))
    ((er verify-guards$)
     (process-input-verify-guards verify-guards old$ ctx state))
    ((er static$)
     (parteval-process-static static old$ verify-guards$ ctx state))
    (case (parteval-case-of-old old$ static$ wrld)
)
    ((er (list new-name$ names-to-avoid))
     (process-input-new-name new-name old$ nil ctx state))
    ((er new-enable$)
     (process-input-new-enable new-enable old$ ctx state))
    ((er thm-name$)
     (parteval-process-thm-name thm-name old$ new-name$ ctx state))
    (names-to-avoid (cons thm-name$ names-to-avoid))
    ((er &)
     (ensure-value-is-boolean$ thm-enable
                               "The :THM-ENABLE input" t nil))
    ((when (and (= case 3) new-enable$ thm-enable))
     (er-soft+
      ctx t nil
      "Since (i) the target function ~x0 ~
                   has the form of case 3 in :DOC PARTEVAL, ~
                   (ii) either the :NEW-ENABLE input is T, ~
                   or it is (perhaps by default) :AUTO ~
                   and (iii) the target function is enabled, ~
                   the :THM-ENABLE input cannot be T."
      old$))
    ((er &)
     (ensure-is-untranslate-specifier$
          untranslate
          "The :UNTRANSLATE input" t nil))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list old$
                static$ new-name$ new-enable$ thm-name$
                verify-guards$ case names-to-avoid)))))