Process the input of an APT transformation that selects an input of the function variable call in a SOFT shallow pop-refinement specification of a certain form.
(process-input-select-old-soft-io select-input-value select-input-keyword old ?f x-x1...xn x-a1...am ctx state) → (mv erp x state)
This is related to process-input-old-soft-io-sel-mod, which checks that the target function of an APT transformation is a SOFT shallow pop-refinement specification of the form referenced in the documentation of that input processor. That documentation mentions that the selected input is specified via some other input of the transformation. This input processor serves to process that input.
Some of the arguments of this input processor are the homonymous results of process-input-old-soft-io-sel-mod, some of which are just for error messages. There are two arguments about the transformation input to process: its value and its keyword (the latter is just for error messages).
If the input being processed is
Function:
(defun process-input-select-old-soft-io (select-input-value select-input-keyword old ?f x-x1...xn x-a1...am ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (keywordp select-input-keyword) (symbolp old) (symbolp ?f) (symbol-listp x-x1...xn) (pseudo-term-listp x-a1...am)))) (let ((__function__ 'process-input-select-old-soft-io)) (declare (ignorable __function__)) (b* (((er x) (if (eq select-input-value :auto) (if (= (len x-a1...am) 1) (value (car x-a1...am)) (er-soft+ ctx t nil "The ~x0 input is ~ (perhaps by default) :AUTO, ~ but this is allowed only if ~ the call of ~x1 in ~x2 ~ has exactly one argument, ~ but it has ~x3 arguments instead." select-input-keyword ?f old (len x-a1...am))) (b* (((er &) (ensure-value-is-in-list$ select-input-value x-a1...am (msg "one of the arguments ~x0 of ~ the call of ~x1 in ~x2" x-a1...am ?f old) (msg "The ~x0 input" select-input-keyword) t nil))) (value select-input-value)))) ((unless (symbolp x)) (er-soft+ ctx t nil "The argument ~x0 of the call of ~x1 in ~x2, ~ specified (perhaps by default) by the ~x3 input, ~ must be a variable, but it is not." x ?f old select-input-keyword)) ((unless (member-eq x x-x1...xn)) (value (raise "Internal error: ~ the variable ~x0 in the call of ~x1 in ~x2 ~ is not among the bound variables ~x3." x ?f old x-x1...xn))) (a1...am (remove1-eq x x-a1...am)) ((when (member-eq x (all-vars (cons :dummy-fn a1...am)))) (er-soft+ ctx t nil "Aside from the argument ~x0 itself, ~ the other arguments ~x1 of the call of ~x2 ~ must not depend on ~x0, but they do." x a1...am ?f))) (value x))))
Theorem:
(defthm symbolp-of-process-input-select-old-soft-io.x (b* (((mv ?erp ?x acl2::?state) (process-input-select-old-soft-io select-input-value select-input-keyword old ?f x-x1...xn x-a1...am ctx state))) (symbolp x)) :rule-classes :rewrite)