Process the
(process-input-old-soft-io-sel-mod old verify-guards ctx state) → (mv erp result state)
The form that the specification must have is the one described in Section `Input/Output Relation with Selected Input and Modified Inputs' of specification-forms.
We check that
This input processor also takes as input
the
We check that the function denoted by
If all the checks are successful,
we return, as second and subsequent results:
the (only) function variable that the function depends on;
the quantified variables,
where the selected one
In the first error message below,
the
Function:
(defun process-input-old-soft-io-sel-mod (old verify-guards ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'process-input-old-soft-io-sel-mod)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((er old) (ensure-function-name-or-numbered-wildcard$ old "The first input" t nil)) ((when (and (eq verify-guards t) (not (guard-verified-p old wrld)))) (er-soft+ ctx t nil "Since the :VERIFY-GUARDS input is T, ~ the target function ~x0 must be guard-verified, ~ but it is not." old)) ((unless (soft::quant-sofunp old wrld)) (er-soft+ ctx t nil "The target function ~x0 ~ must be a SOFT quantifier function, but it is not." old)) (funvars (soft::sofun-funvars old wrld)) ((unless (= (len funvars) 1)) (er-soft+ ctx t nil "The target function ~x0 ~ must depend on exactly one function variable, ~ but instead it depends on ~x1." old funvars)) (??f (car funvars)) ((when (consp (formals old wrld))) (er-soft+ ctx t nil "The target function ~x0 ~ must have no parameters, but instead it has parameters ~x1." old (formals old wrld))) ((unless (eq (defun-sk-quantifier old wrld) 'forall)) (er-soft+ ctx t nil "The quantifier of the target function ~x0 ~ must be universal, but it is existential instead." old)) (x-x1...xn (defun-sk-bound-vars old wrld)) (matrix (defun-sk-matrix old wrld)) (??f-calls (all-calls (list ?f) matrix nil nil)) ((unless (= (len ?f-calls) 1)) (er-soft+ ctx t nil "The matrix ~x0 of the target function ~x1 ~ must have exactly one call of the function variable ~x2, ~ but it has ~x3 calls instead." matrix old ?f (len ?f-calls))) (??f-call (car ?f-calls)) (x-a1...am (fargs ?f-call)) ((unless (consp x-a1...am)) (er-soft+ ctx t nil "The call ~x0 in the matrix ~x1 of ~x2 ~ must have at least one argument, ~ but it has none instead." ?f-call matrix old)) (??f-call-string (concatenate 'string (symbol-name ?f) "-CALL")) (y (genvar old ?f-call-string nil x-x1...xn)) (iorel-body (subst-expr y ?f-call matrix)) (iorel (make-lambda (append x-x1...xn (list y)) iorel-body))) (value (list old ?f x-x1...xn x-a1...am y iorel)))))