defmapping

(in-package "ACL2")

(evmac-topic-implementation defmapping
  :items (*evmac-topic-implementation-item-state* *evmac-topic-implementation-item-wrld*
    *evmac-topic-implementation-item-ctx*
    "@('name'),
   @('doma'),
   @('domb'),
   @('alpha'),
   @('beta'),
   @('beta-of-alpha-thm'),
   @('alpha-of-beta-thm'),
   @('guard-thms'),
   @('unconditional'),
   @('thm-names'),
   @('thm-enable'),
   @('hints'),
   @('print'), and
   @('show-only')
   are the homonymous inputs to @(tsee defmapping),
   before being validated.
   These variables have no types because they may be any values."
    "@('name$'),
   @('doma$'),
   @('domb$'),
   @('alpha$'),
   @('beta$'),
   @('beta-of-alpha-thm$'),
   @('alpha-of-beta-thm$'),
   @('guard-thms$'),
   @('unconditional$'),
   @('thm-name$'),
   @('thm-enable$'),
   @('hints$'),
   @('print$'), and
   @('show-only$')
   are the results of processing
   the homonymous inputs (without the @('$')) to @(tsee defmapping).
   Some are identical to the corresponding inputs,
   but they have types implied by their successful validation,
   performed when they are processed."
    "@('call') is the call of @(tsee defmapping) supplied by the user."
    "@('call$') is the result of removing
   @(':print') and @(':show-only') from @('call')."
    "@('expansion') is the @(tsee encapsulate) generated by @(tsee defmapping)."
    "@('a1...an') is the list of variables @('a1'), ..., @('an')
   described in the documentation."
    "@('b1...bm') is the list of variables @('b1'), ..., @('bm')
   described in the documentation."
    "@('stobjp') is a flag saying whether
   any of the domains has input or output stobjs."))

(defxdoc+ defmapping-table
  :parents (defmapping-implementation)
  :short "@(csee table) of recorded @(tsee defmapping) information."
  :long (topstring (p "For each successful call of @(tsee defmapping)
     whose @(':show-only') input is not @('t'),
     this table includes a pair
     whose key is the name supplied as first input to @(tsee defmapping)
     and whose value includes the information about
     the domains, conversions, and theorems
     (see @(tsee defmapping-infop)).")
    (p "This table is used
     not only to record the @(tsee defmapping) information,
     but also to support the redundancy check
     in @(tsee defmapping-check-redundancy)."))
  :order-subtopics t
  :default-parent t)

(defval *defmapping-table-name*
  'defmapping-table
  :short "Name of the @(tsee defmapping) table.")

(defaggregate defmapping-info
  :short "Information about a @(tsee defmapping) call,
          recorded as a pair's value in the @(tsee defmapping) table."
  ((call$ "The call to @(tsee defmapping),
           without @(':print') and @(':show-only')."
     pseudo-event-formp) (expansion "The @(tsee encapsulate) generated from
               the call to @(tsee defmapping)."
      pseudo-event-formp)
    (doma pseudo-termfnp "Domain @($A$), in translated form.")
    (domb pseudo-termfnp "Domain @($B$), in translated form.")
    (alpha pseudo-termfnp
      "Conversion @($\alpha$), in translated form.")
    (beta pseudo-termfnp
      "Conversion @($\beta$), in translated form.")
    (stobjp booleanp
      "Whether @($A$) or @($B$) has any input or output stobjs.")
    (alpha-image symbolp
      "Name of the @(':alpha-image') theorem.")
    (beta-image symbolp "Name of the @(':beta-image') theorem.")
    (beta-of-alpha symbolp
      "Name of the @(':beta-of-alpha') theorem,
                           if present (otherwise @('nil').")
    (alpha-of-beta symbolp
      "Name of the @(':alpha-of-beta') theorem,
                           if present (otherwise @('nil').")
    (alpha-injective symbolp
      "Name of the @(':alpha-injective') theorem,
                             if present (otherwise @('nil').")
    (beta-injective symbolp
      "Name of the @(':beta-injective') theorem,
                            if present (otherwise @('nil').")
    (doma-guard symbolp
      "Name of the @(':doma-guard') theorem,
                        if present (otherwise @('nil')).")
    (domb-guard symbolp
      "Name of the @(':domb-guard') theorem,
                        if present (otherwise @('nil')).")
    (alpha-guard symbolp
      "Name of the @(':alpha-guard') theorem,
                         if present (otherwise @('nil')).")
    (beta-guard symbolp
      "Name of the @(':beta-guard') theorem,
                        if present (otherwise @('nil')).")
    (unconditional booleanp
      "Value of the @(':unconditional') input,
                            i.e. whether some of the theorems
                            are unconditional or not."))
  :pred defmapping-infop)

(make-event `(table ,*DEFMAPPING-TABLE-NAME*
    nil
    nil
    :guard (and (symbolp key) (defmapping-infop val))))

(define maybe-defmapping-infop
  (x)
  :returns (yes/no booleanp)
  :short "Recognize information about a @(tsee defmapping) call, and @('nil')."
  (or (defmapping-infop x) (eq x nil)))

(define defmapping-lookup
  ((name symbolp) (wrld plist-worldp))
  :returns (info? "A @(tsee maybe-defmapping-infop).")
  :verify-guards nil
  :short "Return the information for the @(tsee defmapping) specified by name,
          or @('nil') if there is no @(tsee defmapping) with that name."
  (b* ((defmapping-table (table-alist *defmapping-table-name* wrld)) (pair? (assoc-eq name defmapping-table))
      ((when (null pair?)) nil)
      (info (cdr pair?)))
    info))

(define defmapping-filter-call
  ((call pseudo-event-formp))
  :guard (and (>= (len call) 6)
    (member-eq (car call) '(defmapping defiso defsurj definj)))
  :returns (call$ "A @(tsee pseudo-event-formp).")
  :verify-guards nil
  :short "Remove any @(':print') and @(':show-only') inputs
          from a call of @(tsee defmapping) or its wrappers."
  :long (topstring-p "As explained in the documentation,
    these two options are ignored when checking redundancy.")
  (b* ((number-of-required-args 5) (number-of-elements-before-options (1+ number-of-required-args))
      (options (nthcdr number-of-elements-before-options call))
      (options (remove-keyword :print options))
      (options (remove-keyword :show-only options))
      (call$ (append (take number-of-elements-before-options call)
          options)))
    call$))

(evmac-topic-input-processing defmapping)

(define defmapping-process-name
  (name ctx state)
  :returns (mv erp (nothing null) state)
  :verify-guards nil
  :short "Process the @('name') input."
  (b* (((er &) (ensure-value-is-symbol$ name "The first input" t nil)) ((er &) (ensure-symbol-not-keyword$ name "The first input" t nil)))
    (value nil)))

(define defmapping-process-function
  ((function "The @('doma'), @('domb'), @('alpha'), or @('beta')
              input to @(tsee defmapping).") (position (member position '(2 3 4 5))
      "Position of the input in
              the ordered inputs to @(tsee defmapping).")
    (guard-thms$ booleanp)
    ctx
    state)
  :returns (mv erp
    (result "A tuple @('(function$
                                    arity
                                    numres
                                    stobjp)')
                        satisfying
                        @('(typed-tuplep pseudo-termfnp
                                         natp
                                         posp
                                         booleanp
                                         result)').")
    state)
  :mode :program :short "Process one of the input functions
          (i.e. @('doma'), @('domb'), @('alpha'), or @('beta'))."
  :long (topstring-p "Return either the input unchanged (if it is a function name)
    or its translation (if it is a lambda expression).
    Also return the arity and the number of results.")
  (b* (((er (list fn/lambda stobjs-in stobjs-out description)) (ensure-function/macro/lambda$ function
         (msg "The ~n0 input" (list position))
         t
         nil)) ((er &) (ensure-function/lambda-logic-mode$ fn/lambda
          description
          t
          nil))
      ((er &) (ensure-function/lambda-closed$ fn/lambda description t nil))
      (stobjp (or (not (equal stobjs-in (repeat (len stobjs-in) nil)))
          (not (equal stobjs-out (repeat (len stobjs-out) nil)))))
      ((unless guard-thms$) (value (list fn/lambda (len stobjs-in) (len stobjs-out) stobjp)))
      ((er &) (ensure-function/lambda-guard-verified-exec-fns$ fn/lambda
          (msg "Since the :GUARD-THMS input is (perhaps by default) T, ~@0"
            (msg-downcase-first description))
          t
          nil)))
    (value (list fn/lambda (len stobjs-in) (len stobjs-out) stobjp))))

(define defmapping-process-functions
  (doma domb alpha beta guard-thms$ ctx state)
  :returns (mv erp
    (result "A tuple @('(doma$ domb$ alpha$ beta$ stobjp)')
                        satisfying @('(typed-tuplep pseudo-termfnp
                                                    pseudo-termfnp
                                                    pseudo-termfnp
                                                    pseudo-termfnp
                                                    booleanp
                                                    result)').")
    state)
  :mode :program :short "Process the @('doma'), @('domb'), @('alpha'), and @('beta') inputs."
  :long (topstring-p "We call @(tsee defmapping-process-function) on each
    and then we check the constraints on the arities and numbers of results.")
  (b* (((er (list doma$ doma-arity doma-numres doma-stobjp)) (defmapping-process-function doma 2 guard-thms$ ctx state)) ((er (list domb$ domb-arity domb-numres domb-stobjp)) (defmapping-process-function domb 3 guard-thms$ ctx state))
      ((er (list alpha$ alpha-arity alpha-numres &)) (defmapping-process-function alpha 4 guard-thms$ ctx state))
      ((er (list beta$ beta-arity beta-numres &)) (defmapping-process-function beta 5 guard-thms$ ctx state))
      ((unless (= doma-numres 1)) (er-soft+ ctx
          t
          nil
          "The number of results returned by the domain ~x0 ~
                   must be 1, but it is ~x1 instead."
          doma
          doma-numres))
      ((unless (= domb-numres 1)) (er-soft+ ctx
          t
          nil
          "The number of results returned by the domain ~x0 ~
                   must be 1, but it is ~x1 instead."
          domb
          domb-numres))
      ((unless (= alpha-arity doma-arity)) (er-soft+ ctx
          t
          nil
          "The arity of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
          alpha
          doma-arity
          doma
          alpha-arity))
      ((unless (= alpha-numres domb-arity)) (er-soft+ ctx
          t
          nil
          "The number of results of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
          alpha
          domb-arity
          domb
          alpha-numres))
      ((unless (= beta-arity domb-arity)) (er-soft+ ctx
          t
          nil
          "The arity of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
          beta
          domb-arity
          domb
          beta-arity))
      ((unless (= beta-numres doma-arity)) (er-soft+ ctx
          t
          nil
          "The number of results of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
          beta
          doma-arity
          doma
          beta-numres)))
    (value (list doma$ domb$ alpha$ beta$ (or doma-stobjp domb-stobjp)))))

(define defmapping-thm-keywords
  ((beta-of-alpha-thm$ booleanp) (alpha-of-beta-thm$ booleanp)
    (guard-thms$ booleanp))
  :returns (thm-keywords keyword-listp)
  :short "Keywords that identify all the theorems to generate."
  (append (list :alpha-image :beta-image)
    (and beta-of-alpha-thm$
      (list :beta-of-alpha :alpha-injective))
    (and alpha-of-beta-thm$
      (list :alpha-of-beta :beta-injective))
    (and guard-thms$
      (list :doma-guard :domb-guard :alpha-guard :beta-guard)))
  ///
  (more-returns (thm-keywords no-duplicatesp-equal
      :name no-duplicatesp-equal-of-defmapping-thm-keywords)))

(define defmapping-process-thm-names
  (thm-names (name$ symbolp)
    (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (guard-thms$ booleanp)
    ctx
    state)
  :returns (mv erp
    (thm-names$ "A @(tsee symbol-symbol-alistp).")
    state)
  :verify-guards nil
  :short "Process the @(':thm-names') input."
  :long (topstring (p "We compute the names of all the theorems to generate,
     and we return them as a complete alist
     from the keywords that identify the theorems
     to the corresponding theorem names.
     The alist has unique keys.")
    (p "If an explicit theorem name is supplied in the @(':thm-names') input,
     it is used;
     otherwise, the theorem name is generated as explained in the documentation.
     The theorem names, whether generated or supplied,
     must be valid fresh theorem names.
     They must also be all distinct;
     this is always the case if the theorem names are all generated,
     because the keywords used in their names are all distinct."))
  (b* (((er &) (ensure-keyword-value-list$ thm-names
         "The :THM-NAMES input"
         t
         nil)) (thm-names-alist (keyword-value-list-to-alist thm-names))
      (keys (strip-cars thm-names-alist))
      (description (msg "The list ~x0 of keywords of the :THM-NAMES input"
          keys))
      ((er &) (ensure-list-has-no-duplicates$ keys description t nil))
      (thm-keywords (defmapping-thm-keywords beta-of-alpha-thm$
          alpha-of-beta-thm$
          guard-thms$))
      ((er &) (ensure-list-subset$ keys thm-keywords description t nil))
      ((er thm-names$) (defmapping-process-thm-names-aux thm-keywords
          thm-names-alist
          name$
          ctx
          state))
      (names (strip-cdrs thm-names$))
      (description (msg "The list ~x0 of theorem names, ~
                          some of which may be supplied ~
                          in the :THM-NAMES input,"
          names))
      ((er &) (ensure-list-has-no-duplicates$ names description t nil)))
    (value thm-names$))
  :prepwork ((define defmapping-process-thm-names-aux
     ((thm-keywords symbol-listp) (thm-names-alist symbol-symbol-alistp)
       (name$ symbolp)
       ctx
       state)
     :returns (mv erp alist state)
     :verify-guards nil
     :parents nil
     (if (endp thm-keywords)
       (value nil)
       (b* ((thm-keyword (car thm-keywords)) (pair (assoc-eq thm-keyword thm-names-alist))
           (thm-name (if pair
               (cdr pair)
               (add-suffix-to-fn name$
                 (concatenate 'string "." (symbol-name thm-keyword)))))
           (description (msg "The name ~x0 of the ~x1 theorem, ~@2,"
               thm-name
               thm-keyword
               (if pair
                 "supplied in the :THM-NAMES input"
                 "automatically generated")))
           ((er &) (ensure-value-is-symbol$ thm-name description t nil))
           ((er &) (ensure-symbol-new-event-name$ thm-name description t nil))
           ((er alist) (defmapping-process-thm-names-aux (cdr thm-keywords)
               thm-names-alist
               name$
               ctx
               state)))
         (value (acons thm-keyword thm-name alist)))))))

(define defmapping-process-thm-enable
  (thm-enable (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (guard-thms$ booleanp)
    ctx
    state)
  :returns (mv erp (thm-enable$ keyword-listp) state)
  :short "Process the @(':thm-enable') input."
  :long (topstring (p "If the processing is successful,
     we return a normalized version of this input,
     namely a list of keywords that specifies which theorems must be enabled,
     among the ones that are generated."))
  (b* (((when (eq thm-enable :all)) (value (defmapping-thm-keywords beta-of-alpha-thm$
           alpha-of-beta-thm$
           guard-thms$))) ((when (eq thm-enable :all-nonguard)) (value (set-difference-eq (defmapping-thm-keywords beta-of-alpha-thm$
              alpha-of-beta-thm$
              guard-thms$)
            '(:doma-guard :domb-guard :alpha-guard :beta-guard))))
      ((unless (keyword-listp thm-enable)) (er-soft+ ctx
          t
          nil
          "The :THM-ENABLE input, ~x0, is not ~
                   :ALL, :ALL-NOGUARD, or a list of keywords."
          thm-enable))
      ((er &) (ensure-list-has-no-duplicates$ thm-enable
          (msg "The :THM-ENABLE list, ~x0," thm-enable)
          t
          nil))
      (thms (defmapping-thm-keywords beta-of-alpha-thm$
          alpha-of-beta-thm$
          guard-thms$))
      ((unless (subsetp-eq thm-enable thms)) (er-soft+ ctx
          t
          nil
          "The :THM-ENABLE input, ~x0, is not a subset of ~
                   the keywords ~x1 for the generated theorems."
          thm-enable
          thms)))
    (value thm-enable))
  :prepwork ((defrulel returns-lemma
     (implies (keyword-listp x)
       (keyword-listp (set-difference-equal x y)))) (defrulel verify-guards-lemma1
      (implies (keyword-listp x) (true-listp x)))
    (defrulel verify-guards-lemma2
      (implies (keyword-listp x) (symbol-listp x)))))

(define 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)
  :returns (mv erp
    (result "A tuple @('(doma$
                                    domb$
                                    alpha$
                                    beta$
                                    stobjp
                                    thm-names$
                                    thm-enable$
                                    hints$)')
                        satisfying
                        @('(typed-tuplep pseudo-termfnp
                                         pseudo-termfnp
                                         pseudo-termfnp
                                         pseudo-termfnp
                                         booleanp
                                         symbol-symbol-alistp
                                         keyword-listp
                                         symbol-truelist-alistp
                                         result)').")
    state)
  :mode :program :short "Process all the inputs."
  (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$ stobjp)) (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$
        stobjp
        thm-names$
        thm-enable$
        hints$))))

(evmac-topic-event-generation defmapping
  :some-local-nonlocal-p t)

(define defmapping-gen-var-a1...an
  ((alpha$ pseudo-termfnp) (wrld plist-worldp))
  :returns (a1...an "A @(tsee symbol-listp).")
  :verify-guards nil
  :short "Generate the list of variables @('(a1 ... an)')
          described in the documentation."
  :long (topstring (p "We use the formal parameters of the conversion @($\alpha$)."))
  (cond ((symbolp alpha$) (formals alpha$ wrld))
    (t (lambda-formals alpha$))))

(define defmapping-gen-var-b1...bm
  ((beta$ pseudo-termfnp) (wrld plist-worldp))
  :returns (b1...bm "A @(tsee symbol-listp).")
  :verify-guards nil
  :short "Generate the list of variables @('(b1 ... bm)')
          described in the documentation."
  :long (topstring (p "We use the formal parameters of the conversion @($\beta$)."))
  (cond ((symbolp beta$) (formals beta$ wrld))
    (t (lambda-formals beta$))))

(define defmapping-differentiate-a/b-vars
  ((a1/b1...an/bm symbol-listp) (b1/a1...bm/an symbol-listp))
  :returns (a1/b1...an/bm-differentiated "A @(tsee symbol-listp).")
  :mode :program :short "Ensure that the variables
          @('a1'), ..., @('an') or @('b1'), ..., @('bm')
          do not overlap with
          @('b1'), ..., @('bm') or @('a1'), ..., @('an')."
  :long (topstring (p "In the formula of the @(':alpha-of-beta') applicability condition,
     in certain cases @('a1'), ..., @('an') are bound by @(tsee mv-let),
     and @('b1'), ..., @('bm') are used in the body of the @(tsee mv-let):
     if any @('bj') were identical to any @('ai'),
     the formula would be incorrect in general.
     A similar situation occurs
     with the @(':beta-of-alpha') applicability condition,
     with the roles of @('a1'), ..., @('an') and @('b1'), ..., @('bm') swapped.
     Thus, in these cases we may need to differentiate
     @('a1'), ..., @('an') apart from @('b1'), ..., @('bm') or vice versa.
     We do that here, using @(tsee genvar)."))
  (cond ((endp a1/b1...an/bm) nil)
    (t (b* ((a2/b2...an/bm-differentiated (defmapping-differentiate-a/b-vars (cdr a1/b1...an/bm)
             b1/a1...bm/an)) (a1/b1 (car a1/b1...an/bm))
          (a1/b1-differentiated (genvar a1/b1
              (symbol-name a1/b1)
              nil
              (append b1/a1...bm/an a2/b2...an/bm-differentiated))))
        (cons a1/b1-differentiated a2/b2...an/bm-differentiated)))))

(define defmapping-gen-var-aa/bb
  ((a1/b1...an/bm symbol-listp))
  :returns (aa1/bb1...aan/bbm "A @(tsee symbol-listp).")
  :mode :program :short "Generate the list of variables
          @('(aa1 ... aan)') or @('(bb1 ... bbm)')
          described in the documentation."
  :long (topstring-p "We generate these by appending @('$') to each of
    @('(a1 ... an)') or @('(b1 ... bm)'),
    using @(tsee genvar) to ensure that we do not introduce clashes.")
  (cond ((endp a1/b1...an/bm) nil)
    (t (b* ((aa2/bb2...aan/bbm (defmapping-gen-var-aa/bb (cdr a1/b1...an/bm))) (a1/b1 (car a1/b1...an/bm))
          (aa1/bb1 (genvar a1/b1
              (cat (symbol-name a1/b1) "$")
              nil
              (append a1/b1...an/bm aa2/bb2...aan/bbm))))
        (cons aa1/bb1 aa2/bb2...aan/bbm)))))

(define defmapping-gen-appconds
  ((doma$ pseudo-termfnp) (domb$ pseudo-termfnp)
    (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (a1...an symbol-listp)
    (b1...bm symbol-listp)
    (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (guard-thms$ booleanp)
    (unconditional$ booleanp)
    state)
  :returns (appconds "A @(tsee evmac-appcond-listp).")
  :mode :program :short "Generate the applicability conditions."
  (b* ((wrld (w state)) (n (arity doma$ wrld))
      (m (arity domb$ wrld)))
    (append (make-evmac-appcond? :alpha-image (b* ((antecedent (apply-term doma$ a1...an)) (consequent (if (= m 1)
                (apply-term* domb$ (apply-term alpha$ a1...an))
                (make-mv-let-call 'mv
                  b1...bm
                  :all (apply-term alpha$ a1...an)
                  (apply-term domb$ b1...bm)))))
          (implicate antecedent consequent)))
      (make-evmac-appcond? :beta-image (b* ((antecedent (apply-term domb$ b1...bm)) (consequent (if (= n 1)
                (apply-term* doma$ (apply-term beta$ b1...bm))
                (make-mv-let-call 'mv
                  a1...an
                  :all (apply-term beta$ b1...bm)
                  (apply-term doma$ a1...an)))))
          (implicate antecedent consequent)))
      (make-evmac-appcond? :beta-of-alpha (b* ((antecedent (if unconditional$
               *t*
               (apply-term doma$ a1...an))) (consequent (if (= n 1)
                (if (= m 1)
                  (b* ((a (car a1...an)))
                    `(equal ,(APPLY-TERM* BETA$ (APPLY-TERM* ALPHA$ A)) ,A))
                  (b* ((b1...bm (defmapping-differentiate-a/b-vars b1...bm a1...an)))
                    (make-mv-let-call 'mv
                      b1...bm
                      :all (apply-term* alpha$ (car a1...an))
                      `(equal ,(APPLY-TERM BETA$ B1...BM) ,(CAR A1...AN)))))
                (if (= m 1)
                  (b* ((aa1...aan (defmapping-gen-var-aa/bb a1...an)))
                    (make-mv-let-call 'mv
                      aa1...aan
                      :all (apply-term* beta$ (apply-term alpha$ a1...an))
                      (conjoin-equalities aa1...aan a1...an)))
                  (b* ((aa1...aan (defmapping-gen-var-aa/bb a1...an)) (b1...bm (defmapping-differentiate-a/b-vars b1...bm a1...an)))
                    (make-mv-let-call 'mv
                      b1...bm
                      :all (apply-term alpha$ a1...an)
                      (make-mv-let-call 'mv
                        aa1...aan
                        :all (apply-term beta$ b1...bm)
                        (conjoin-equalities aa1...aan a1...an))))))))
          (implicate antecedent consequent))
        :when beta-of-alpha-thm$)
      (make-evmac-appcond? :alpha-of-beta (b* ((antecedent (if unconditional$
               *t*
               (apply-term domb$ b1...bm))) (consequent (if (= n 1)
                (if (= m 1)
                  (b* ((b (car b1...bm)))
                    `(equal ,(APPLY-TERM* ALPHA$ (APPLY-TERM* BETA$ B)) ,B))
                  (b* ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm)))
                    (make-mv-let-call 'mv
                      bb1...bbm
                      :all (apply-term* alpha$ (apply-term beta$ b1...bm))
                      (conjoin-equalities bb1...bbm b1...bm))))
                (if (= m 1)
                  (b* ((b (car b1...bm)) (a1...an (defmapping-differentiate-a/b-vars a1...an b1...bm)))
                    (make-mv-let-call 'mv
                      a1...an
                      :all (apply-term* beta$ b)
                      `(equal ,(APPLY-TERM ALPHA$ A1...AN) ,B)))
                  (b* ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm)) (a1...an (defmapping-differentiate-a/b-vars a1...an b1...bm)))
                    (make-mv-let-call 'mv
                      a1...an
                      :all (apply-term beta$ b1...bm)
                      (make-mv-let-call 'mv
                        bb1...bbm
                        :all (apply-term alpha$ a1...an)
                        (conjoin-equalities bb1...bbm b1...bm))))))))
          (implicate antecedent consequent))
        :when alpha-of-beta-thm$)
      (make-evmac-appcond? :doma-guard (cond ((symbolp doma$) (uguard doma$ wrld))
          (t (term-guard-obligation (lambda-body doma$) :limited state)))
        :when guard-thms$)
      (make-evmac-appcond? :domb-guard (cond ((symbolp domb$) (uguard domb$ wrld))
          (t (term-guard-obligation (lambda-body domb$) :limited state)))
        :when guard-thms$)
      (make-evmac-appcond? :alpha-guard (b* ((alpha-formals (cond ((symbolp alpha$) (formals alpha$ wrld))
               (t (lambda-formals alpha$)))) (alpha-guard (cond ((symbolp alpha$) (uguard alpha$ wrld))
                (t (term-guard-obligation (lambda-body alpha$) :limited state)))))
          (implicate (apply-term doma$ a1...an)
            (subcor-var alpha-formals a1...an alpha-guard)))
        :when guard-thms$)
      (make-evmac-appcond? :beta-guard (b* ((beta-formals (cond ((symbolp beta$) (formals beta$ wrld))
               (t (lambda-formals beta$)))) (beta-guard (cond ((symbolp beta$) (uguard beta$ wrld))
                (t (term-guard-obligation (lambda-body beta$) :limited state)))))
          (implicate (apply-term domb$ b1...bm)
            (subcor-var beta-formals b1...bm beta-guard)))
        :when guard-thms$))))

(define defmapping-gen-appcond-thm
  ((appcond evmac-appcondp) (appcond-thm-names symbol-symbol-alistp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (wrld plist-worldp))
  :returns (mv (local-event "A @(tsee pseudo-event-formp).")
    (exported-event "A @(tsee pseudo-event-formp)."))
  :mode :program :short "Generate a theorem event from an applicability condition."
  :long (topstring (p "All the applicability conditions
     that must hold for the @(tsee defmapping) call
     are turned into theorems exported from the @(tsee encapsulate).
     To keep the ACL2 history ``clean'',
     we generate the theorem in local form with a @(':by') hint
     (the references the local theorem name of the applicability condition;
     this name generally differs from
     the theorem name determined by @(':thm-names')),
     and in non-local, redundant form without hints."))
  (b* (((evmac-appcond appcond) appcond) (thm-name (cdr (assoc-eq appcond.name thm-names$)))
      (thm-formula (untranslate appcond.formula t wrld))
      (thm-hints `(("Goal" :by ,(CDR (ASSOC-EQ APPCOND.NAME APPCOND-THM-NAMES)))))
      (defthmr/defthmdr (if (member-eq appcond.name thm-enable$)
          'defthmr
          'defthmdr))
      (local-event `(local (,DEFTHMR/DEFTHMDR ,THM-NAME ,THM-FORMULA :hints ,THM-HINTS)))
      (exported-event `(,DEFTHMR/DEFTHMDR ,THM-NAME ,THM-FORMULA)))
    (mv local-event exported-event)))

(define defmapping-gen-appcond-thms
  ((appconds evmac-appcond-listp) (appcond-thm-names symbol-symbol-alistp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (wrld plist-worldp))
  :returns (mv (local-events "A @(tsee pseudo-event-form-listp).")
    (exported-events "A @(tsee pseudo-event-form-listp)."))
  :mode :program :short "Lift @(tsee defmapping-gen-appcond-thm) to
          lists of applicability conditions."
  (b* (((when (endp appconds)) (mv nil nil)) ((mv local-event exported-event) (defmapping-gen-appcond-thm (car appconds)
          appcond-thm-names
          thm-names$
          thm-enable$
          wrld))
      ((mv local-events exported-events) (defmapping-gen-appcond-thms (cdr appconds)
          appcond-thm-names
          thm-names$
          thm-enable$
          wrld)))
    (mv (cons local-event local-events)
      (cons exported-event exported-events))))

(define defmapping-gen-alpha-injective
  ((doma$ pseudo-termfnp) (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (a1...an symbol-listp)
    (b1...bm symbol-listp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (appcond-thm-names symbol-symbol-alistp)
    (wrld plist-worldp))
  :returns (mv (local-event "A @(tsee pseudo-event-formp).")
    (exported-event "A @(tsee pseudo-event-formp)."))
  :mode :program :short "Generate the @(':alpha-injective') theorem."
  :long (topstring (p "This function is called if only if
     the @(':beta-of-alpha-thm') input is @('t').")
    (p "We generate hints based on the proofs in the design notes.
     The @(':cases') hints correspond, in the proof in the design notes,
     to the inference step that applies @($\beta$)
     to both sides of the equality @($\alpha(a)=\alpha(a')$).
     The hints for these proofs are the same
     whether @(':unconditional') is @('t') or @('nil')."))
  (b* ((aa1...aan (defmapping-gen-var-aa/bb a1...an)) (name (cdr (assoc-eq :alpha-injective thm-names$)))
      (formula (b* ((antecedent (if unconditional$
               *t*
               (conjoin2 (apply-term doma$ a1...an)
                 (apply-term doma$ aa1...aan)))) (consequent `(equal (equal ,(APPLY-TERM ALPHA$ A1...AN)
                  ,(APPLY-TERM ALPHA$ AA1...AAN))
                ,(CONJOIN-EQUALITIES A1...AN AA1...AAN)))
            (formula (implicate antecedent consequent)))
          (untranslate formula t wrld)))
      (hints (b* ((beta-of-alpha (cdr (assoc-eq :beta-of-alpha appcond-thm-names))) (beta-of-alpha-instance `(:instance ,BETA-OF-ALPHA
                ,@(ALIST-TO-DOUBLETS (PAIRLIS$ A1...AN AA1...AAN))))
            (m (len b1...bm))
            (cases-hints-formula (if (= m 1)
                `(equal ,(APPLY-TERM* BETA$ (APPLY-TERM ALPHA$ A1...AN))
                  ,(APPLY-TERM* BETA$ (APPLY-TERM ALPHA$ AA1...AAN)))
                `(equal ,(APPLY-TERM BETA$ (MAKE-MV-NTH-CALLS (APPLY-TERM ALPHA$ A1...AN) M))
                  ,(APPLY-TERM BETA$ (MAKE-MV-NTH-CALLS (APPLY-TERM ALPHA$ AA1...AAN) M))))))
          `(("Goal" :in-theory nil
             :cases (,CASES-HINTS-FORMULA)
             :use (,BETA-OF-ALPHA ,BETA-OF-ALPHA-INSTANCE)))))
      (defthmr/defthmdr (if (member-eq :alpha-injective thm-enable$)
          'defthmr
          'defthmdr))
      (local-event `(local (,DEFTHMR/DEFTHMDR ,NAME ,FORMULA :hints ,HINTS)))
      (exported-event `(,DEFTHMR/DEFTHMDR ,NAME ,FORMULA)))
    (mv local-event exported-event)))

(define defmapping-gen-beta-injective
  ((domb$ pseudo-termfnp) (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (a1...an symbol-listp)
    (b1...bm symbol-listp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (appcond-thm-names symbol-symbol-alistp)
    (wrld plist-worldp))
  :returns (mv (local-event "A @(tsee pseudo-event-formp).")
    (exported-event "A @(tsee pseudo-event-formp)."))
  :mode :program :short "Generate the @(':beta-injective') theorem."
  :long (topstring (p "This function is called if only if
     the @(':alpha-of-beta-thm') input is @('t').")
    (p "We generate hints based on the proofs in the design notes.
     The @(':cases') hints correspond, in the proof in the design notes,
     to the inference step that applies @($\alpha$)
     to both sides of the equality @($\beta(b)=\beta(b')$).
     The hints for these proofs are the same
     whether @(':unconditional') is @('t') or @('nil')."))
  (b* ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm)) (name (cdr (assoc-eq :beta-injective thm-names$)))
      (formula (b* ((antecedent (if unconditional$
               *t*
               (conjoin2 (apply-term domb$ b1...bm)
                 (apply-term domb$ bb1...bbm)))) (consequent `(equal (equal ,(APPLY-TERM BETA$ B1...BM)
                  ,(APPLY-TERM BETA$ BB1...BBM))
                ,(CONJOIN-EQUALITIES B1...BM BB1...BBM)))
            (formula (implicate antecedent consequent)))
          (untranslate formula t wrld)))
      (hints (b* ((alpha-of-beta (cdr (assoc-eq :alpha-of-beta appcond-thm-names))) (alpha-of-beta-instance `(:instance ,ALPHA-OF-BETA
                ,@(ALIST-TO-DOUBLETS (PAIRLIS$ B1...BM BB1...BBM))))
            (n (len a1...an))
            (cases-hints-formula (if (= n 1)
                `(equal ,(APPLY-TERM* ALPHA$ (APPLY-TERM BETA$ B1...BM))
                  ,(APPLY-TERM* ALPHA$ (APPLY-TERM BETA$ BB1...BBM)))
                `(equal ,(APPLY-TERM ALPHA$ (MAKE-MV-NTH-CALLS (APPLY-TERM BETA$ B1...BM) N))
                  ,(APPLY-TERM ALPHA$ (MAKE-MV-NTH-CALLS (APPLY-TERM BETA$ BB1...BBM) N))))))
          `(("Goal" :in-theory nil
             :cases (,CASES-HINTS-FORMULA)
             :use (,ALPHA-OF-BETA ,ALPHA-OF-BETA-INSTANCE)))))
      (defthmr/defthmdr (if (member-eq :beta-injective thm-enable$)
          'defthmr
          'defthmdr))
      (local-event `(local (,DEFTHMR/DEFTHMDR ,NAME ,FORMULA :hints ,HINTS)))
      (exported-event `(,DEFTHMR/DEFTHMDR ,NAME ,FORMULA)))
    (mv local-event exported-event)))

(define defmapping-gen-nonappcond-thms
  ((doma$ pseudo-termfnp) (domb$ pseudo-termfnp)
    (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (a1...an symbol-listp)
    (b1...bm symbol-listp)
    (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (appcond-thm-names symbol-symbol-alistp)
    (wrld plist-worldp))
  :returns (mv (local-events "A @(tsee pseudo-event-form-listp).")
    (exported-events "A @(tsee pseudo-event-form-listp)."))
  :mode :program :short "Generate the theorems that are not applicability conditions."
  :long (topstring (p "These can be no, one, or two injectivity theorems,
     based on the @(':beta-of-alpha-thm') and @(':alpha-of-beta-thm') inputs."))
  (b* (((mv alpha-inj-local-event-singleton-list-or-nil
        alpha-inj-exported-event-singleton-list-or-nil) (if beta-of-alpha-thm$
         (b* (((mv local-event exported-event) (defmapping-gen-alpha-injective doma$
                alpha$
                beta$
                a1...an
                b1...bm
                unconditional$
                thm-names$
                thm-enable$
                appcond-thm-names
                wrld)))
           (mv (list local-event) (list exported-event)))
         (mv nil nil))) ((mv beta-inj-local-event-singleton-list-or-nil
         beta-inj-exported-event-singleton-list-or-nil) (if alpha-of-beta-thm$
          (b* (((mv local-event exported-event) (defmapping-gen-beta-injective domb$
                 alpha$
                 beta$
                 a1...an
                 b1...bm
                 unconditional$
                 thm-names$
                 thm-enable$
                 appcond-thm-names
                 wrld)))
            (mv (list local-event) (list exported-event)))
          (mv nil nil))))
    (mv (append alpha-inj-local-event-singleton-list-or-nil
        beta-inj-local-event-singleton-list-or-nil)
      (append alpha-inj-exported-event-singleton-list-or-nil
        beta-inj-exported-event-singleton-list-or-nil))))

(define defmapping-gen-thms
  ((doma$ pseudo-termfnp) (domb$ pseudo-termfnp)
    (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (a1...an symbol-listp)
    (b1...bm symbol-listp)
    (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (appconds evmac-appcond-listp)
    (appcond-thm-names symbol-symbol-alistp)
    (wrld plist-worldp))
  :returns (mv (local-events "A @(tsee pseudo-event-form-listp).")
    (exported-events "A @(tsee pseudo-event-form-listp)."))
  :mode :program :short "Generate all the theorems."
  (b* (((mv appcond-local-events appcond-exported-events) (defmapping-gen-appcond-thms appconds
         appcond-thm-names
         thm-names$
         thm-enable$
         wrld)) ((mv nonappcond-local-events nonappcond-exporte-events) (defmapping-gen-nonappcond-thms doma$
          domb$
          alpha$
          beta$
          a1...an
          b1...bm
          beta-of-alpha-thm$
          alpha-of-beta-thm$
          unconditional$
          thm-names$
          thm-enable$
          appcond-thm-names
          wrld)))
    (mv (append appcond-local-events nonappcond-local-events)
      (append appcond-exported-events nonappcond-exporte-events))))

(define defmapping-gen-ext-table
  ((name$ symbolp) (doma$ pseudo-termfnp)
    (domb$ pseudo-termfnp)
    (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (stobjp booleanp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (call$ pseudo-event-formp)
    (expansion pseudo-event-formp))
  :returns (event pseudo-event-formp)
  :verify-guards nil
  :short "Generate the event that extends the @(tsee defmapping) table."
  (b* ((alpha-image (cdr (assoc-eq :alpha-image thm-names$))) (beta-image (cdr (assoc-eq :beta-image thm-names$)))
      (beta-of-alpha (cdr (assoc-eq :beta-of-alpha thm-names$)))
      (alpha-of-beta (cdr (assoc-eq :alpha-of-beta thm-names$)))
      (alpha-injective (cdr (assoc-eq :alpha-injective thm-names$)))
      (beta-injective (cdr (assoc-eq :beta-injective thm-names$)))
      (doma-guard (cdr (assoc-eq :doma-guard thm-names$)))
      (domb-guard (cdr (assoc-eq :domb-guard thm-names$)))
      (alpha-guard (cdr (assoc-eq :alpha-guard thm-names$)))
      (beta-guard (cdr (assoc-eq :beta-guard thm-names$)))
      (info (make-defmapping-info :call$ call$
          :expansion expansion
          :doma doma$
          :domb domb$
          :alpha alpha$
          :beta beta$
          :stobjp stobjp
          :alpha-image alpha-image
          :beta-image beta-image
          :beta-of-alpha beta-of-alpha
          :alpha-of-beta alpha-of-beta
          :alpha-injective alpha-injective
          :beta-injective beta-injective
          :doma-guard doma-guard
          :domb-guard domb-guard
          :alpha-guard alpha-guard
          :beta-guard beta-guard
          :unconditional unconditional$)))
    `(table ,*DEFMAPPING-TABLE-NAME* ',NAME$ ',INFO)))

(define defmapping-gen-print-result
  ((thms pseudo-event-form-listp))
  :returns (cw-events pseudo-event-form-listp)
  :short "Generate the events that print the result."
  :long (topstring-p "This refers to the @(':result') value of the @(':print') input.
    The result to print consists of the generated theorems.
    These theorems are printed only if
    @(':print') is @(':result') or @(':info') or @(':all').")
  (if (endp thms)
    nil
    (cons `(cw-event "~x0~|" ',(CAR THMS))
      (defmapping-gen-print-result (cdr thms)))))

(define defmapping-gen-everything
  ((name$ symbolp) (doma$ pseudo-termfnp)
    (domb$ pseudo-termfnp)
    (alpha$ pseudo-termfnp)
    (beta$ pseudo-termfnp)
    (stobjp booleanp)
    (beta-of-alpha-thm$ booleanp)
    (alpha-of-beta-thm$ booleanp)
    (guard-thms$ booleanp)
    (unconditional$ booleanp)
    (thm-names$ symbol-symbol-alistp)
    (thm-enable$ keyword-listp)
    (hints$ symbol-truelist-alistp)
    (print$ evmac-input-print-p)
    (show-only$ booleanp)
    (call pseudo-event-formp)
    ctx
    state)
  :returns (mv erp (event "A @(tsee pseudo-event-formp).") state)
  :mode :program :verify-guards nil
  :short "Generate the top-level event."
  :long (topstring (p "This is a @(tsee progn) that consists of
     the expansion of @(tsee defmapping) (the @(tsee encapsulate)),
     followed by an event to extend the @(tsee defmapping) table,
     optionally followed by events to print the generated theorems.
     The @(tsee progn) ends with @(':invisible')
     to avoid printing a return value.")
    (p "The expansion starts with an implicitly local event to
     ensure logic mode.
     After the events to proof
     Other implicitly local event forms remove any default and override hints,
     to prevent such hints from sabotaging the generated proofs
     for the theorems that are not applicability conditions;
     this removal is done after proving the applicability conditions,
     in case their proofs rely on the default or override hints.
     We also add an explicitly local event to prevent @(tsee mv-nth)
     from being expanded in the generated proofs,
     which is accomplished via a system attachment.")
    (p "If @(':print') is @(':all'),
     the expansion is wrapped to show ACL2's output
     in response to the submitted events.
     If @(':print') is @(':info') or @(':all'),
     a blank line is printed just before the result, for visual separation;
     if @(':print') is @(':result'),
     the blank line is not printed.")
    (p "If @(':show-only') is @('t'),
     the expansion is printed on the screen
     and not returned as part of the event to submit,
     which is in this case is just an @(':invisible') form.
     In this case, if @(':print') is @(':info') or @(':all'),
     a blank line is printed just before the @(tsee encapsulate),
     for visual separation."))
  (b* ((wrld (w state)) (a1...an (defmapping-gen-var-a1...an alpha$ wrld))
      (b1...bm (defmapping-gen-var-b1...bm beta$ wrld))
      (appconds (defmapping-gen-appconds doma$
          domb$
          alpha$
          beta$
          a1...an
          b1...bm
          beta-of-alpha-thm$
          alpha-of-beta-thm$
          guard-thms$
          unconditional$
          state))
      ((er (list appcond-events appcond-thm-names &)) (evmac-appcond-theorems-no-extra-hints appconds
          hints$
          nil
          print$
          ctx
          state))
      ((mv local-thm-events exported-thm-events) (defmapping-gen-thms doma$
          domb$
          alpha$
          beta$
          a1...an
          b1...bm
          beta-of-alpha-thm$
          alpha-of-beta-thm$
          unconditional$
          thm-names$
          thm-enable$
          appconds
          appcond-thm-names
          wrld))
      (expansion `(encapsulate nil
          (logic)
          (set-ignore-ok t)
          ,@APPCOND-EVENTS
          (evmac-prepare-proofs)
          ,@LOCAL-THM-EVENTS
          ,@EXPORTED-THM-EVENTS))
      ((when show-only$) (if (member-eq print$ '(:info :all))
          (cw "~%~x0~|" expansion)
          (cw "~x0~|" expansion))
        (value '(value-triple :invisible)))
      (expansion+ (restore-output? (eq print$ :all) expansion))
      (call$ (defmapping-filter-call call))
      (extend-table (defmapping-gen-ext-table name$
          doma$
          domb$
          alpha$
          beta$
          stobjp
          unconditional$
          thm-names$
          call$
          expansion))
      (print-result (and (member-eq print$ '(:result :info :all))
          (append (and (member-eq print$ '(:info :all)) '((cw-event "~%")))
            (defmapping-gen-print-result exported-thm-events)))))
    (value `(progn ,EXPANSION+
        ,EXTEND-TABLE
        ,@PRINT-RESULT
        (value-triple :invisible)))))

(define defmapping-check-redundancy
  (name print show-only (call pseudo-event-formp) ctx state)
  :returns (mv erp (yes/no "A @(tsee booleanp).") state)
  :verify-guards nil
  :parents (defmapping-implementation)
  :short "Check if a call to @(tsee defmapping) is redundant."
  :long (topstring (p "If the @(tsee defmapping) table has no entry for @('name'),
     we return @('nil'): the call is not redundant.")
    (p "If the table has an entry for @('name') but the call differs
     (after removing any @(':print') and @(':show-only')),
     an error occurs.")
    (p "If the call is redundant,
     we know that all the inputs except possibly @(':print') and @(':show-only')
     are valid
     (because they are the same as the ones of the recorded successful call);
     we validate these two inputs, for better error checking.
     If @(':show-only') is @('t'),
     we print the recorded expansion of the call.
     Unless @(':print') is @('nil'),
     we print a message saying that the call is redundant."))
  (b* ((table (table-alist *defmapping-table-name* (w state))) (pair (assoc-equal name table))
      ((unless pair) (value nil))
      (info (cdr pair))
      (call$ (defmapping-filter-call call))
      ((unless (equal call$ (defmapping-info->call$ info))) (er-soft+ ctx
          t
          nil
          "A different call to DEFMAPPING with name ~x0 ~
                   has already been performed."
          name))
      ((er &) (evmac-process-input-print print ctx state))
      ((er &) (evmac-process-input-show-only show-only ctx state))
      ((run-when show-only) (cw "~x0~|" (defmapping-info->expansion info)))
      ((run-when print) (cw "~%The call ~x0 is redundant.~%" call)))
    (value t)))

(define 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 pseudo-event-formp)
    ctx
    state)
  :returns (mv erp (event "A @(tsee pseudo-event-formp).") state)
  :parents (defmapping-implementation)
  :mode :program :short "Check redundancy,
          process the inputs,
          and generate the event to submit."
  (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$
           stobjp
           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$
      stobjp
      beta-of-alpha-thm
      alpha-of-beta-thm
      guard-thms
      unconditional
      thm-names$
      thm-enable$
      hints$
      print
      show-only
      call
      ctx
      state)))

(defsection defmapping-macro-definition
  :parents (defmapping-implementation)
  :short "Definition of the @(tsee defmapping) macro."
  :long (topstring (p "Submit the event form generated by @(tsee defmapping-fn).")
    (@def "defmapping"))
  (defmacro defmapping
    (&whole call
      name
      doma
      domb
      alpha
      beta
      &key
      (beta-of-alpha-thm 'nil)
      (alpha-of-beta-thm 'nil)
      (guard-thms 't)
      (unconditional 'nil)
      (thm-names 'nil)
      (thm-enable 'nil)
      (hints 'nil)
      (print ':result)
      (show-only 'nil))
    `(make-event-terse (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
        (cons 'defmapping ',NAME)
        state)
      :suppress-errors ,(NOT PRINT))))