		Search-engine friendly clone of the ACL2 documentation.

Casesplit-input-processing

Casesplit-process-inputs

Process all the inputs.

Signature
(casesplit-process-inputs old conditions theorems new-name new-enable thm-name thm-enable verify-guards hints print show-only ctx state) → (mv erp result state)
Returns: result — A tuple (old$ conditions$ hyps news new-name$ new-enable$ thm-name$ verify-guards$ hints$ names-to-avoid) satisfying (typed-tuplep symbolp pseudo-term-listp pseudo-term-listp pseudo-term-listp symbolp booleanp symbolp booleanp evmac-input-hints-p 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 conditions because the result of processing :verify-guards is used to process conditions. 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 casesplit-process-old).

Definitions and Theorems

Function: casesplit-process-inputs

(defun casesplit-process-inputs
       (old conditions theorems new-name new-enable
            thm-name thm-enable verify-guards
            hints print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'casesplit-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er old$)
     (casesplit-process-old old verify-guards ctx state))
    ((er verify-guards$)
     (process-input-verify-guards verify-guards old$ ctx state))
    ((er conditions$)
     (casesplit-process-conditions conditions
                                   old$ verify-guards$ ctx state))
    ((er (list hyps news))
     (casesplit-process-theorems
          theorems old$ conditions$ ctx state))
    ((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$)
     (casesplit-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))
    ((er hints$)
     (evmac-process-input-hints hints ctx state))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list old$ conditions$ hyps news new-name$
                new-enable$ thm-name$ verify-guards$
                hints$ names-to-avoid)))))