Process the
(process-input-old-to-new-name old-to-new-name old-to-new-name-present old new names-to-avoid ctx state) → (mv erp result state)
The APT transformations that use this utility
have an input
This utility processes the
The caller of this utility must set
the parameter
Function:
(defun process-input-old-to-new-name (old-to-new-name old-to-new-name-present old new names-to-avoid ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (booleanp old-to-new-name-present) (symbolp old) (symbolp new) (symbol-listp names-to-avoid)))) (let ((__function__ 'process-input-old-to-new-name)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((er &) (if old-to-new-name-present (ensure-value-is-symbol$ old-to-new-name "The :OLD-TO-NEW-NAME input" t nil) (value nil))) (name (if (or (not old-to-new-name-present) (keywordp old-to-new-name)) (b* ((kwd (if old-to-new-name-present old-to-new-name (get-default-input-old-to-new-name wrld)))) (intern-in-package-of-symbol (concatenate 'string (symbol-name old) (symbol-name kwd) (symbol-name new)) new)) old-to-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-TO-NEW-NAME input ~x3," name old new old-to-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))))))