		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-new-name

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

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

The APT transformations that use this utility have a :new-name input but not a :wrapper and :wrapper-name input (the ones with these additional two inputs should use the utility process-input-new/wrapper-names instead). This utility processes (and validates) the :new-name inputs, as described in function-name-generation.

Definitions and Theorems

Function: process-input-new-name

(defun process-input-new-name
       (new-name old names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'process-input-new-name))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((er &)
     (ensure-value-is-symbol$ new-name "The :NEW-NAME input" t nil))
    ((mv numbered-name-p base index)
     (check-numbered-name old wrld))
    ((mv base index)
     (if numbered-name-p (mv base index)
       (mv old 0))))
   (if (eq new-name :auto)
       (b* (((mv new-name names-to-avoid)
             (next-fresh-numbered-name base (1+ index)
                                       names-to-avoid wrld)))
         (value (list new-name names-to-avoid)))
    (b*
     ((msg/nil (fresh-namep-msg-weak new-name 'function
                                     wrld))
      ((when msg/nil)
       (er-soft+
        ctx t nil
        "The name ~x0 specified by :NEW-NAME ~
                       is already in use.  ~@1"
        new-name msg/nil))
      ((when (member-eq new-name names-to-avoid))
       (er-soft+
        ctx t nil
        "The name ~x0 specified by :NEW-NAME ~
                       must be distinct form the names ~&1 ~
                       that are also being generated."
        new-name names-to-avoid)))
     (value (list new-name
                  (cons new-name names-to-avoid))))))))