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