		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-surj

Process a surj component of the surjmaps input.

Signature
(expdata-process-surj surj k old$ verify-guards$ names-to-avoid ctx state) → (mv erp result state)
Arguments: surj — The surjk component of surjmaps.; k — The k in surjk.
Guard (posp k).; old$ — Guard (symbolp old$).; verify-guards$ — Guard (booleanp verify-guards$).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A tuple (surjmap updated-names-to-avoid) satisfying (typed-tuplep expdata-surjmapp symbol-listp result).

If surj is the name of an existing defsurj, the names-to-avoid argument is returned unchanged, because we are not generating any fresh theorem names in this case.

If instead surj is a list (oldp newp forth back) or (oldp newp forth back :hints ...), the names-to-avoid argument is augmented with the names of the theorems that will be generated by the local defsurj.

When surj is the name of an existing defsurj, to check whether its :guard-thms is t, which is required when verify-guards$ is t, we check whether one of the ...-guard theorems recorded in the defsurj is not nil. We pick doma-guard, but any of the other three would work as well.

When surj is not the name of an existing defsurj, and instead we generate a local one as part of expdata, we use defsurj's input processing code, and then we check that the functions are all unary and single-valued; given the constraints already checked by the defsurj input processing code, here it suffices to check that the two domains are unary. We cannot just generate the defsurj later; we need the actual (translated) functions to use them in the events generated by expdata proper. When we call defsurj's input processing functions, we set the context ctx to the one for the defsurj call, so that the error message is appropriate. (When the generated defsurj call is actually submitted, these input processing steps will be repeated, but will succeed since they have been already performed here; and they should be quite fast to execute.) The name of this local defsurj is a combination that involves old and k, to make the name of the defsurj readable (in case of errors due to failed applicability conditions) and unique within the encapsulate generated by expdata.

If the processing is successful, we return the surjective mapping record specified by surj.

Definitions and Theorems

Function: expdata-process-surj

(defun expdata-process-surj
       (surj k old$
             verify-guards$ names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (posp k)
                             (symbolp old$)
                             (booleanp verify-guards$)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'expdata-process-surj))
  (declare (ignorable __function__))
  (if
   (atom surj)
   (b*
    (((er &)
      (ensure-value-is-symbol$
       surj
       (msg
        "The ~n0 SURJ component ~x1 ~
                          of the second input ~
                          must be a symbol or a list. ~
                          Since it is an atom,"
        (list k)
        surj)
       t nil))
     (info (defsurj-lookup surj (w state)))
     ((unless info)
      (er-soft+
       ctx t nil
       "The ~n0 SURJ component of the second input, ~
                       which is the symbol ~x1, ~
                       must be the name of an existing DEFSURJ, ~
                       but no DEFSURJ with this name exists.  ~
                       See :DOC DEFSURJ."
       (list k)
       surj))
     ((defmapping-info info) info)
     ((when (and verify-guards$ (null info.doma-guard)))
      (er-soft+
       ctx t nil
       "Since the :VERIFY-GUARDS input is T, ~
                       or it is (perhaps by default) :AUTO ~
                       and the target function ~x0 is guard-verified, ~
                       the DEFSURJ ~x1 must include ~
                       the guard-related theorems, ~
                       but it does not.  ~
                       See :DOC DEFSURJ."
       old$ surj))
     (surjmap
         (make-expdata-surjmap :surjname surj
                               :localp nil
                               :oldp info.domb
                               :newp info.doma
                               :forth info.beta
                               :back info.alpha
                               :forth-image info.beta-image
                               :back-image info.alpha-image
                               :back-of-forth info.alpha-of-beta
                               :forth-injective info.alpha-injective
                               :oldp-guard info.domb-guard
                               :newp-guard info.doma-guard
                               :forth-guard info.beta-guard
                               :back-guard info.alpha-guard
                               :hints nil)))
    (value (list surjmap names-to-avoid)))
   (b*
    ((wrld (w state))
     (surjname (packn-pos (list 'defsurj-expdata- old$ '- k)
                          old$))
     (surjname
          (expdata-fresh-defsurj-name-with-*s-suffix surjname wrld))
     ((mv forth-image
          back-image back-of-forth oldp-guard
          newp-guard forth-guard back-guard
          forth-injective names-to-avoid)
      (expdata-fresh-defsurj-thm-names
           surjname
           verify-guards$ names-to-avoid wrld))
     ((unless (true-listp surj))
      (er-soft+
       ctx t nil
       "The ~n0 SURJ component ~x1 of the second input ~
                     must be a symbol or a list. ~
                     Since it is not an atom, it must be a list."
       (list k)
       surj))
     ((unless (or (= (len surj) 4) (= (len surj) 6)))
      (er-soft+
       ctx t nil
       "The ~n0 SURJ component ~x1 of the second input ~
                     must be a list of length 4 or 6."
       (list k)
       surj))
     (oldp (first surj))
     (newp (second surj))
     (forth (third surj))
     (back (fourth surj))
     ((unless (or (= (len surj) 4)
                  (eq (fifth surj) :hints)))
      (er-soft+
       ctx t nil
       "The fifth component ~x0 ~
                     of the ~n1 SURJ component ~x2 ~
                     of the second input ~
                     must be the keyword :HINTS."
       (fifth surj)
       (list k)
       surj))
     (hints (and (= (len surj) 6) (sixth surj)))
     (ctx-defsurj (cons 'defsurj surjname))
     ((er (list newp$ oldp$ back$ forth$))
      (acl2::defmapping-process-functions
           newp oldp back
           forth verify-guards$ ctx-defsurj state))
     (oldp-arity (arity oldp$ wrld))
     ((unless (= oldp-arity 1))
      (er-soft+
       ctx t nil
       "The first component ~x0 ~
                     of the ~n1 SURJ component ~
                     of the third input ~
                     must have one argument, but it has ~x2 arguments instead."
       oldp (list k)
       oldp-arity))
     (newp-arity (arity newp$ wrld))
     ((unless (= newp-arity 1))
      (er-soft+
       ctx t nil
       "The second component ~x0 ~
                     of the ~n1 SURJ component ~
                     of the third input ~
                     must have one argument, but it has ~x2 arguments instead."
       newp (list k)
       newp-arity))
     (surjmap (make-expdata-surjmap :surjname surjname
                                    :localp t
                                    :oldp oldp$
                                    :newp newp$
                                    :forth forth$
                                    :back back$
                                    :forth-image forth-image
                                    :back-image back-image
                                    :back-of-forth back-of-forth
                                    :forth-injective forth-injective
                                    :oldp-guard oldp-guard
                                    :newp-guard newp-guard
                                    :forth-guard forth-guard
                                    :back-guard back-guard
                                    :hints hints)))
    (value (list surjmap names-to-avoid))))))