		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-inputs

Process all the inputs.

Signature
(expdata-process-inputs old surjmaps predicate new-name new-enable old-to-new-name old-to-new-name-suppliedp old-to-new-enable old-to-new-enable-suppliedp new-to-old-name new-to-old-name-suppliedp new-to-old-enable new-to-old-enable-suppliedp newp-of-new-name newp-of-new-name-suppliedp newp-of-new-enable newp-of-new-enable-suppliedp verify-guards untranslate hints print show-only ctx state) → (mv erp result state)
Arguments: old-to-new-name-suppliedp — Guard (booleanp old-to-new-name-suppliedp).; old-to-new-enable-suppliedp — Guard (booleanp old-to-new-enable-suppliedp).; new-to-old-name-suppliedp — Guard (booleanp new-to-old-name-suppliedp).; new-to-old-enable-suppliedp — Guard (booleanp new-to-old-enable-suppliedp).; newp-of-new-name-suppliedp — Guard (booleanp newp-of-new-name-suppliedp).; newp-of-new-enable-suppliedp — Guard (booleanp newp-of-new-enable-suppliedp).
Returns: result — A tuple (old$ arg-surjmaps res-surjmaps new$ new-enable$ old-to-new$ old-to-new-enable$ new-to-old$ new-to-old-enable$ newp-of-new$ newp-of-new-enable$ verify-guards$ hints$ names-to-avoid) satisfying (typed-tuplep symbolp expdata-symbol-surjmap-alistp expdata-pos-surjmap-alistp symbolp booleanp symbolp booleanp symbolp booleanp symbolp booleanp booleanp evmac-input-hints-p symbol-listp result).

Definitions and Theorems

Function: expdata-process-inputs

(defun expdata-process-inputs
       (old surjmaps predicate
            new-name new-enable old-to-new-name
            old-to-new-name-suppliedp
            old-to-new-enable
            old-to-new-enable-suppliedp
            new-to-old-name
            new-to-old-name-suppliedp
            new-to-old-enable
            new-to-old-enable-suppliedp
            newp-of-new-name
            newp-of-new-name-suppliedp
            newp-of-new-enable
            newp-of-new-enable-suppliedp
            verify-guards untranslate
            hints print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (booleanp old-to-new-name-suppliedp)
                         (booleanp old-to-new-enable-suppliedp)
                         (booleanp new-to-old-name-suppliedp)
                         (booleanp new-to-old-enable-suppliedp)
                         (booleanp newp-of-new-name-suppliedp)
                         (booleanp newp-of-new-enable-suppliedp))))
 (let ((__function__ 'expdata-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er old$)
     (expdata-process-old old predicate verify-guards ctx state))
    ((er (list new$ names-to-avoid))
     (process-input-new-name new-name old$ nil ctx state))
    ((er (list old-to-new$ names-to-avoid))
     (process-input-old-to-new-name
          old-to-new-name
          old-to-new-name-suppliedp
          old$ new$ names-to-avoid ctx state))
    ((er (list new-to-old$ names-to-avoid))
     (process-input-new-to-old-name
          new-to-old-name
          new-to-old-name-suppliedp
          old$ new$ names-to-avoid ctx state))
    ((er (list newp-of-new$ names-to-avoid))
     (expdata-process-newp-of-new-name
          newp-of-new-name
          new$ names-to-avoid ctx state))
    ((er verify-guards$)
     (process-input-verify-guards verify-guards old$ ctx state))
    ((er (list arg-surjmaps
               res-surjmaps names-to-avoid))
     (expdata-process-surjmaps surjmaps old$ verify-guards$
                               names-to-avoid ctx state))
    ((er &)
     (ensure-value-is-boolean$
          predicate "The :PREDICATE input" t nil))
    ((er new-enable$)
     (process-input-new-enable new-enable old$ ctx state))
    ((er old-to-new-enable$)
     (process-input-old-to-new-enable
          old-to-new-enable
          old-to-new-enable-suppliedp ctx state))
    ((er new-to-old-enable$)
     (process-input-new-to-old-enable
          new-to-old-enable
          new-to-old-enable-suppliedp ctx state))
    ((when (and old-to-new-enable$ new-to-old-enable$))
     (er-soft+
      ctx t nil
      (if old-to-new-enable-suppliedp
       (if new-to-old-enable-suppliedp
        "The :OLD-TO-NEW-ENABLE input ~
                           and the :NEW-TO-OLD-ENABLE inputs ~
                           cannot be both T."
        "Since the default :NEW-TO-OLD-ENABLE input is T, ~
                         the :OLD-TO-NEW-ENABLE input cannot be T.")
       (if new-to-old-enable-suppliedp
        "Since the default :OLD-TO-NEW-ENABLE input is T, ~
                         the :NEW-TO-OLD-ENABLE input cannot be T."
        "Internal error: ~
                       the default :OLD-TO-NEW-ENABLE and :NEW-TO-OLD-ENABLE ~
                       are both T."))))
    ((er &)
     (ensure-value-is-boolean$
          newp-of-new-enable
          "The :NEWP-OF-NEW-ENABLE input" t nil))
    ((when (and newp-of-new-name-suppliedp
                (not res-surjmaps)))
     (er-soft+
      ctx t nil
      "Since no results are being transformed, ~
                   it is an error to supply the :NEWP-OF-NEW-NAME input."))
    ((when (and newp-of-new-enable-suppliedp
                (not res-surjmaps)))
     (er-soft+
      ctx t nil
      "Since no results are being transformed, ~
                   it is an error to supply the :NEWP-OF-NEW-ENABLE input."))
    ((er &)
     (ensure-is-untranslate-specifier$
          untranslate
          "The :UNTRANSLATE input" t nil))
    ((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 old$ arg-surjmaps res-surjmaps
                new$ new-enable$ old-to-new$
                old-to-new-enable$ new-to-old$
                new-to-old-enable$ newp-of-new$
                newp-of-new-enable verify-guards$
                hints$ names-to-avoid)))))