		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-wrapper-to-old-name

Process the :wrapper-to-old-name input of an APT transformation.

Signature
(process-input-wrapper-to-old-name wrapper-to-old-name wrapper-to-old-name-present gen-wrapper old wrapper names-to-avoid ctx state) → (mv erp result state)
Arguments: wrapper-to-old-name-present — Guard (booleanp wrapper-to-old-name-present).; gen-wrapper — Guard (booleanp gen-wrapper).; old — Guard (symbolp old).; wrapper — Guard (symbolp wrapper).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — A list (wrapper-to-old updated-names-to-avoid) satisfying (typed-tuplep symbolp symbol-listp result).

This is quite analogous to process-input-old-to-wrapper-name, but for the :wrapper-to-old-name input of an APT transformation.

Definitions and Theorems

Function: process-input-wrapper-to-old-name

(defun process-input-wrapper-to-old-name
       (wrapper-to-old-name wrapper-to-old-name-present gen-wrapper
                            old wrapper names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp wrapper-to-old-name-present)
                             (booleanp gen-wrapper)
                             (symbolp old)
                             (symbolp wrapper)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'process-input-wrapper-to-old-name))
  (declare (ignorable __function__))
  (if gen-wrapper
   (b*
    ((wrld (w state))
     ((er &)
      (if wrapper-to-old-name-present
          (ensure-value-is-symbol$
               wrapper-to-old-name
               "The :WRAPPER-TO-OLD-NAME input" t nil)
        (value nil)))
     (name
      (if
       (or (not wrapper-to-old-name-present)
           (keywordp wrapper-to-old-name))
       (b* ((kwd (if wrapper-to-old-name-present wrapper-to-old-name
                   (get-default-input-wrapper-to-old-name wrld))))
         (intern-in-package-of-symbol
              (concatenate 'string
                           (symbol-name wrapper)
                           (symbol-name kwd)
                           (symbol-name old))
              wrapper))
       wrapper-to-old-name))
     (description
      (msg
       "The name ~x0 of the theorem ~
                          that rewrites the wrapper function ~x1 ~
                          in terms of the old function ~x2, ~
                          specified (perhaps by default) ~
                          by the :WRAPPER-TO-OLD-NAME input ~x3,"
       name wrapper old wrapper-to-old-name))
     (error-msg? (fresh-namep-msg-weak name nil wrld))
     ((when error-msg?)
      (er-soft+ ctx t nil
                "~@0 must be a valid fresh theorem name.  ~@1"
                description error-msg?))
     ((er &)
      (ensure-value-is-not-in-list$
       name names-to-avoid
       (msg
        "among the names ~x0 of other events ~
                      generated by this transformation"
        names-to-avoid)
       description t nil)))
    (value (list name (cons name names-to-avoid))))
   (if wrapper-to-old-name-present
    (er-soft+
     ctx t nil
     "Since the :WRAPPER input is (perhaps by default) NIL, ~
                   no :WRAPPER-TO-OLD-NAME input may be supplied,
                   but ~x0 was supplied instead."
     wrapper-to-old-name)
    (value (list nil names-to-avoid))))))