		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-old-if-new-name

Process the :old-if-new-name input of an APT transformation.

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

The APT transformations that use this utility have an input :old-if-new-name that specifies the name of the generated theorem asserting that the old function is implied by the new function. This input must be either a symbol to use directly as the theorem name (in which case the symbol must not be a keyword), or a keyword used as a separator between the names of the old and new functions as expained in set-default-input-old-if-new-name. If also explained there, if this input is absent, it is taken from the APT defaults table.

This utility processes the :old-if-new-name input of an APT transformation, validating that the input specifies a valid name for the new theorem. The names-to-avoid parameter contains names of other events that are generated by the transformation but do not yet exist: they are used to ensure that the name of this theorem is distinct from them; this theorem's name is added to the list, which is also returned.

The caller of this utility must set the parameter old-if-new-name-present to t iff the :old-if-new-name input is present. If this is nil, the parameter old-if-new-name is ignored.

Definitions and Theorems

Function: process-input-old-if-new-name

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