• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
        • Defsurj
        • Defiso
        • Defmapping-implementation
          • Defmapping-event-generation
          • Defmapping-check-redundancy
          • Defmapping-table
          • Defmapping-fn
          • Defmapping-input-processing
            • Defmapping-process-thm-names
            • Defmapping-process-inputs
            • Defmapping-process-function
            • Defmapping-process-functions
            • Defmapping-process-thm-enable
            • Defmapping-thm-keywords
            • Defmapping-process-name
          • Defmapping-macro-definition
        • Definj
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Define-sk
      • Defines
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Support
      • Defthm-signed-byte-p
      • Defthm-unsigned-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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$)))))