		Search-engine friendly clone of the ACL2 documentation.

Input-processors

Process-input-select-old-soft-io

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.

Signature
(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)
Arguments: select-input-keyword — Guard (keywordp select-input-keyword).; old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-a1...am — Guard (pseudo-term-listp x-a1...am).
Returns: x — Type (symbolp x).

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 :auto, which must be the default (this is assumed by an error messages below), then the call of the function variable must have a single argument, which must necessarily be a variable because of the checks performed by process-input-select-old-soft-io; in this case, this is the argument selected by the input being processed. Otherwise, the input being processed must be a variable among the arguments of the call of the function variable.

Definitions and Theorems

Function: process-input-select-old-soft-io

(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: symbolp-of-process-input-select-old-soft-io.x

(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)