Process the
(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)
This is quite analogous to process-input-old-to-wrapper-name,
but for the
Function:
(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))))))