• 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-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-implementation

Defmapping-fn

Check redundancy, process the inputs, and generate the event to submit.

Signature

(defmapping-fn name 
               doma domb alpha beta beta-of-alpha-thm 
               alpha-of-beta-thm guard-thms 
               unconditional thm-names thm-enable 
               hints print show-only call ctx state) 
 
  → 
(mv erp event state)

Arguments

call — Guard (pseudo-event-formp call).

Returns

event — A pseudo-event-formp.

Definitions and Theorems

Function: defmapping-fn

(defun defmapping-fn (name doma domb alpha beta beta-of-alpha-thm
                           alpha-of-beta-thm guard-thms
                           unconditional thm-names thm-enable
                           hints print show-only call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (pseudo-event-formp call)))
  (let ((__function__ 'defmapping-fn))
    (declare (ignorable __function__))
    (b* (((er redundant?)
          (defmapping-check-redundancy
               name print show-only call ctx state))
         ((when redundant?)
          (value '(value-triple :invisible)))
         ((er (list doma$ domb$ alpha$
                    beta$ thm-names$ thm-enable$ hints$))
          (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)))
      (defmapping-gen-everything name doma$ domb$ alpha$ beta$
                                 beta-of-alpha-thm alpha-of-beta-thm
                                 guard-thms unconditional
                                 thm-names$ thm-enable$ hints$
                                 print show-only call ctx state))))