		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-name

Process the :solution-name input.

Signature
(solve-process-solution-name solution-name method ?f x1...xn verify-guards names-to-avoid ctx state) → (mv erp result state)
Arguments: method — Guard (keywordp method).; ?f — Guard (symbolp ?f).; x1...xn — Guard (symbol-listp x1...xn).; verify-guards — Guard (booleanp verify-guards).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: result — (tuple (f symbolp) (f-existsp booleanp) (updated-names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: solve-process-solution-name

(defun solve-process-solution-name
       (solution-name method ?f x1...xn
                      verify-guards names-to-avoid ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (keywordp method)
                             (symbolp ?f)
                             (symbol-listp x1...xn)
                             (booleanp verify-guards)
                             (symbol-listp names-to-avoid))))
 (let ((__function__ 'solve-process-solution-name))
  (declare (ignorable __function__))
  (b* (((er &)
        (ensure-value-is-symbol$ solution-name
                                 "The :SOLUTION-NAME input" t nil)))
   (if
    (function-symbolp solution-name (w state))
    (b*
     (((unless (eq method :manual))
       (er-soft+
        ctx t nil
        "The :SOLUTION-NAME input specifies ~
                         an existing function, ~x0. ~
                         This is allowed only if ~
                         the :METHOD input is :MANUAL, ~
                         but it is ~x1 instead."
        solution-name method))
      (desc (msg "The function ~x0 specified by the :SOLUTION-INPUT"
                 solution-name))
      ((er &)
       (ensure-function-is-logic-mode$ solution-name desc t nil))
      ((er &)
       (ensure-function-is-defined$ solution-name desc t nil))
      ((er &)
       (ensure-function-arity$ solution-name (len x1...xn)
                               desc t nil))
      ((er &)
       (ensure-function-number-of-results$
            solution-name 1 desc t nil))
      ((er &)
       (if verify-guards (ensure-function-is-guard-verified$
                              solution-name desc t nil)
         (value nil))))
     (value (list solution-name t names-to-avoid)))
    (b*
     (((er f)
       (if
        (eq solution-name :auto)
        (b*
         ((chars (explode (symbol-name ?f)))
          ((unless (and (consp chars)
                        (eql (car chars) #\?)))
           (er-soft+
            ctx t nil
            "The :SOLUTION-NAME input is :AUTO ~
                                        (perhaps by default). ~
                                        This is allowed only if ~
                                        the name of ~x0 starts with ?, ~
                                        but it does not."
            ?f)))
         (value (intern-in-package-of-symbol (implode (cdr chars))
                                             ?f)))
        (value solution-name)))
      ((er &)
       (ensure-symbol-is-fresh-event-name$
        f
        (msg
         "The name ~x0 specified ~
                                                      (perhaps by default) ~
                                                      by :SOLUTION-NAME"
         f)
        'function
        names-to-avoid t nil)))
     (value (list f nil names-to-avoid)))))))