		Search-engine friendly clone of the ACL2 documentation.

Defmapping-input-processing

Defmapping-process-inputs

Process all the inputs.

Signature
(defmapping-process-inputs name doma domb alpha beta beta-of-alpha-thm alpha-of-beta-thm guard-thms unconditional thm-names thm-enable hints print show-only ctx state) → (mv erp result state)
Returns: result — A tuple (doma$ domb$ alpha$ beta$ thm-names$ thm-enable$ hints$) satisfying (typed-tuplep pseudo-termfnp pseudo-termfnp pseudo-termfnp pseudo-termfnp symbol-symbol-alistp keyword-listp symbol-truelist-alistp result).

Definitions and Theorems

Function: defmapping-process-inputs

(defun defmapping-process-inputs
       (name doma domb alpha beta beta-of-alpha-thm
             alpha-of-beta-thm guard-thms
             unconditional thm-names thm-enable
             hints print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defmapping-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (defmapping-process-name name ctx state))
    ((er &)
     (ensure-value-is-boolean$ guard-thms
                               "The :GUARD-THMS input" t nil))
    ((er (list doma$ domb$ alpha$ beta$))
     (defmapping-process-functions
          doma
          domb alpha beta guard-thms ctx state))
    ((er &)
     (ensure-value-is-boolean$
          beta-of-alpha-thm
          "The :BETA-OF-ALPHA-THM input" t nil))
    ((er &)
     (ensure-value-is-boolean$
          alpha-of-beta-thm
          "The :ALPHA-OF-BETA-THM input" t nil))
    ((er &)
     (ensure-value-is-boolean$ unconditional
                               "The :UNCONDITIONAL input" t nil))
    ((when (and unconditional (not beta-of-alpha-thm)
                (not alpha-of-beta-thm)))
     (er-soft+
      ctx t nil
      "The :UNCONDITIONAL input cannot be T when ~
                   both :BETA-OF-ALPHA-THM and :ALPHA-OF-BETA-THM are NIL."))
    ((er thm-names$)
     (defmapping-process-thm-names
          thm-names name beta-of-alpha-thm
          alpha-of-beta-thm guard-thms ctx state))
    ((er thm-enable$)
     (defmapping-process-thm-enable
          thm-enable beta-of-alpha-thm
          alpha-of-beta-thm guard-thms ctx state))
    ((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 doma$ domb$ alpha$
                beta$ thm-names$ thm-enable$ hints$)))))