		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-iso

Process an iso component of the isomaps input.

Signature
(isodata-process-iso iso k old$ verify-guards$ names-to-avoid ctx state) → (mv erp result state)
Arguments: iso — The isok component of isomaps.; k — The k in isok.
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 (isomap updated-names-to-avoid) satisfying (typed-tuplep isodata-isomapp symbol-listp result).

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

If instead iso 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 defiso.

When iso is the name of an existing defiso, 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 defiso is not nil. We pick doma-guard, but any of the other three would work as well.

When iso is not the name of an existing defiso, and instead we generate a local one as part of isodata, we use defiso's input processing code, and then we check that the functions are all unary and single-valued; given the constraints already checked by the defiso input processing code, here it suffices to check that the two domains are unary. We cannot just generate the defiso later; we need the actual (translated) functions to use them in the events generated by isodata proper. When we call defiso's input processing functions, we set the context ctx to the one for the defiso call, so that the error message is appropriate. (When the generated defiso 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 defiso is a combination that involves old and k, to make the name of the defiso readable (in case of errors due to failed applicability conditions) and unique within the encapsulate generated by isodata.

If the processing is successful, we return the isomorphic mapping record specified by iso.

Definitions and Theorems

Function: isodata-process-iso

(defun isodata-process-iso
       (iso 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__ 'isodata-process-iso))
  (declare (ignorable __function__))
  (if
   (atom iso)
   (b*
    (((er &)
      (ensure-value-is-symbol$
       iso
       (msg
        "The ~n0 ISO component ~x1 ~
                          of the second input ~
                          must be a symbol or a list. ~
                          Since it is an atom,"
        (list k)
        iso)
       t nil))
     (info (defiso-lookup iso (w state)))
     ((unless info)
      (er-soft+
       ctx t nil
       "The ~n0 ISO component of the second input, ~
                       which is the symbol ~x1, ~
                       must be the name of an existing DEFISO, ~
                       but no DEFISO with this name exists.  ~
                       See :DOC DEFISO."
       (list k)
       iso))
     ((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 DEFISO ~x1 must include ~
                       the guard-related theorems, ~
                       but it does not.  ~
                       See :DOC DEFISO."
       old$ iso))
     (isomap
          (make-isodata-isomap :isoname iso
                               :localp nil
                               :oldp info.doma
                               :newp info.domb
                               :forth info.alpha
                               :back info.beta
                               :forth-image info.alpha-image
                               :back-image info.beta-image
                               :back-of-forth info.beta-of-alpha
                               :forth-of-back info.alpha-of-beta
                               :forth-injective info.alpha-injective
                               :back-injective info.beta-injective
                               :oldp-guard info.doma-guard
                               :newp-guard info.domb-guard
                               :forth-guard info.alpha-guard
                               :back-guard info.beta-guard
                               :hints nil)))
    (value (list isomap names-to-avoid)))
   (b*
    ((wrld (w state))
     (isoname (packn-pos (list 'defiso-isodata- old$ '- k)
                         old$))
     (isoname
          (isodata-fresh-defiso-name-with-*s-suffix isoname wrld))
     ((mv forth-image back-image back-of-forth
          forth-of-back oldp-guard newp-guard
          forth-guard back-guard forth-injective
          back-injective names-to-avoid)
      (isodata-fresh-defiso-thm-names
           isoname
           verify-guards$ names-to-avoid wrld))
     ((unless (true-listp iso))
      (er-soft+
       ctx t nil
       "The ~n0 ISO 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)
       iso))
     ((unless (or (= (len iso) 4) (= (len iso) 6)))
      (er-soft+
       ctx t nil
       "The ~n0 ISO component ~x1 of the second input ~
                     must be a list of length 4 or 6."
       (list k)
       iso))
     (oldp (first iso))
     (newp (second iso))
     (forth (third iso))
     (back (fourth iso))
     ((unless (or (= (len iso) 4)
                  (eq (fifth iso) :hints)))
      (er-soft+
       ctx t nil
       "The fifth component ~x0 ~
                     of the ~n1 ISO component ~x2 ~
                     of the second input ~
                     must be the keyword :HINTS."
       (fifth iso)
       (list k)
       iso))
     (hints (and (= (len iso) 6) (sixth iso)))
     (ctx-defiso (cons 'defiso isoname))
     ((er (list oldp$ newp$ forth$ back$))
      (acl2::defmapping-process-functions
           oldp newp forth
           back verify-guards$ ctx-defiso state))
     (oldp-arity (arity oldp$ wrld))
     ((unless (= oldp-arity 1))
      (er-soft+
       ctx t nil
       "The first component ~x0 ~
                     of the ~n1 ISO 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 ISO component ~
                     of the third input ~
                     must have one argument, but it has ~x2 arguments instead."
       newp (list k)
       newp-arity))
     (isomap (make-isodata-isomap :isoname isoname
                                  :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-of-back forth-of-back
                                  :forth-injective forth-injective
                                  :back-injective back-injective
                                  :oldp-guard oldp-guard
                                  :newp-guard newp-guard
                                  :forth-guard forth-guard
                                  :back-guard back-guard
                                  :hints hints)))
    (value (list isomap names-to-avoid))))))