		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-old-to-wrapper-name

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

Signature
(process-input-old-to-wrapper-name old-to-wrapper-name old-to-wrapper-name-present gen-wrapper old wrapper names-to-avoid ctx state) → (mv erp result state)
Arguments: old-to-wrapper-name-present — Guard (booleanp old-to-wrapper-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 (old-to-wrapper updated-names-to-avoid) satisfying (typed-tuplep symbolp symbol-listp result).

This is quite analogous to process-input-old-to-new-name, but for the :old-to-wrapper-name input of an APT transformation. The gen-wrapper parameter is t iff the wrapper is generated, i.e. if the :wrapper input of the transformation is t. If this is nil, we ensure that :old-to-wrapper-name is absent.

Definitions and Theorems

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

(defun process-input-old-to-wrapper-name
       (old-to-wrapper-name old-to-wrapper-name-present gen-wrapper
                            old wrapper names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp old-to-wrapper-name-present)
                             (booleanp gen-wrapper)
                             (symbolp old)
                             (symbolp wrapper)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'process-input-old-to-wrapper-name))
  (declare (ignorable __function__))
  (if gen-wrapper
   (b*
    ((wrld (w state))
     ((er &)
      (if old-to-wrapper-name-present
          (ensure-value-is-symbol$
               old-to-wrapper-name
               "The :OLD-TO-WRAPPER-NAME input" t nil)
        (value nil)))
     (name
      (if
       (or (not old-to-wrapper-name-present)
           (keywordp old-to-wrapper-name))
       (b* ((kwd (if old-to-wrapper-name-present old-to-wrapper-name
                   (get-default-input-old-to-wrapper-name wrld))))
         (intern-in-package-of-symbol
              (concatenate 'string
                           (symbol-name old)
                           (symbol-name kwd)
                           (symbol-name wrapper))
              wrapper))
       old-to-wrapper-name))
     (description
      (msg
       "The name ~x0 of the theorem ~
                              that rewrites the old function ~x1 ~
                              in terms of the wrapper function ~x2, ~
                              specified (perhaps by default) ~
                              by the :OLD-TO-WRAPPER-NAME input ~x3,"
       name old wrapper old-to-wrapper-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 old-to-wrapper-name-present
    (er-soft+
     ctx t nil
     "Since the :WRAPPER input is (perhaps by default) NIL, ~
                   no :OLD-TO-WRAPPER-NAME input may be supplied,
                   but ~x0 was supplied instead."
     old-to-wrapper-name)
    (value (list nil names-to-avoid))))))