		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-old

Process the old input.

Signature
(solve-process-old old verify-guards ctx state) → (mv erp result state)
Returns: result — (tuple (old symbolp) (?f symbolp) (x1...xn symbol-listp) (matrix pseudo-termp) result).

Definitions and Theorems

Function: solve-process-old

(defun solve-process-old (old verify-guards ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'solve-process-old))
  (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."
      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))
    (x1...xn (defun-sk-bound-vars old wrld))
    (imatrix (defun-sk-imatrix old wrld))
    (matrix (defun-sk-matrix old wrld))
    (calls (all-calls (list ?f) matrix nil nil))
    ((unless (= (len calls) 1))
     (er-soft+
      ctx t nil
      "The matrix ~x0 of the target function ~x1, ~
                   after translation and LET expansion, ~
                   must contains exactly one call of ~x2, ~
                   but it contains ~@3 instead."
      imatrix old ?f
      (if (consp calls)
          (msg "multiple calls ~&0" calls)
        "no calls")))
    (call (car calls))
    ((unless (equal (fargs call) x1...xn))
     (er-soft+
      ctx t nil
      "The matrix ~x0 of the target function ~x1, ~
                   after translation and LET expansion, ~
                   must call ~x2 on the variables ~x3, ~
                   but it calls it on ~x4 instead."
      imatrix old ?f x1...xn (fargs call))))
   (value (list old ?f x1...xn matrix)))))