Process the inputs.
(specialize-process-inputs const-old const-new target param const wrld) → (mv er? tunits const-new$ target$ param$ const)
Function:
(defun specialize-process-inputs (const-old const-new target param const wrld) (declare (xargs :guard (plist-worldp wrld))) (b* (((reterr) (irr-transunit-ensemble) nil (c$::irr-ident) (c$::irr-ident) (irr-expr)) ((unless (symbolp const-old)) (retmsg$ "~x0 must be a symbol." const-old)) (tunits (constant-value const-old wrld)) ((unless (transunit-ensemblep tunits)) (retmsg$ "~x0 must be a translation unit ensemble." const-old)) ((unless (symbolp const-new)) (retmsg$ "~x0 must be a symbol." const-new)) ((unless (stringp target)) (retmsg$ "~x0 must be a string." target)) (target (ident target)) ((unless (stringp param)) (retmsg$ "~x0 must be a string." param)) (param (ident param)) ((unless (exprp const)) (retmsg$ "~x0 must be a C expression." const))) (retok tunits const-new target param const)))
Theorem:
(defthm maybe-msgp-of-specialize-process-inputs.er? (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (maybe-msgp er?)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemblep-of-specialize-process-inputs.tunits (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (transunit-ensemblep tunits)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-specialize-process-inputs.const-new$ (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (symbolp const-new$)) :rule-classes :rewrite)
Theorem:
(defthm identp-of-specialize-process-inputs.target$ (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (identp target$)) :rule-classes :rewrite)
Theorem:
(defthm identp-of-specialize-process-inputs.param$ (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (identp param$)) :rule-classes :rewrite)
Theorem:
(defthm exprp-of-specialize-process-inputs.const (b* (((mv ?er? ?tunits ?const-new$ ?target$ ?param$ ?const) (specialize-process-inputs const-old const-new target param const wrld))) (exprp const)) :rule-classes :rewrite)