		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-inputs

Process all the inputs.

Signature
(solve-process-inputs old method method? method-rules solution-name solution-enable solution-enable? solution-guard solution-guard? solution-guard-hints solution-guard-hints? solution-body solution-body? solution-hints solution-hints? new-name new-enable old-if-new-name old-if-new-name? old-if-new-enable old-if-new-enable? verify-guards print show-only ctx state) → (mv erp result state)
Arguments: method? — Guard (booleanp method?).; solution-enable? — Guard (booleanp solution-enable?).; solution-guard? — Guard (booleanp solution-guard?).; solution-guard-hints? — Guard (booleanp solution-guard-hints?).; solution-body? — Guard (booleanp solution-body?).; solution-hints? — Guard (booleanp solution-hints?).; old-if-new-name? — Guard (booleanp old-if-new-name?).; old-if-new-enable? — Guard (booleanp old-if-new-enable?).
Returns: result — (tuple (old symbolp) (?f symbolp) (x1...xn symbol-listp) (matrix pseudo-termp) (f symbolp) (f-existsp symbolp) (new symbolp) (new-enable booleanp) (old-if-new symbolp) (old-if-new-enable booleanp) (verify-guards booleanp) (names-to-avoid symbol-listp) result).

Definitions and Theorems

Function: solve-process-inputs

(defun solve-process-inputs
       (old method method? method-rules
            solution-name solution-enable
            solution-enable? solution-guard
            solution-guard? solution-guard-hints
            solution-guard-hints? solution-body
            solution-body? solution-hints
            solution-hints? new-name new-enable
            old-if-new-name old-if-new-name?
            old-if-new-enable old-if-new-enable?
            verify-guards print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp method?)
                             (booleanp solution-enable?)
                             (booleanp solution-guard?)
                             (booleanp solution-guard-hints?)
                             (booleanp solution-body?)
                             (booleanp solution-hints?)
                             (booleanp old-if-new-name?)
                             (booleanp old-if-new-enable?))))
 (let ((__function__ 'solve-process-inputs))
  (declare (ignorable __function__))
  (b*
   ((names-to-avoid nil)
    ((er (list old ??f x1...xn matrix))
     (solve-process-old old verify-guards ctx state))
    ((er verify-guards)
     (process-input-verify-guards verify-guards old ctx state))
    ((er &)
     (solve-process-method method method? ctx state))
    ((er &)
     (solve-process-method-rules method-rules ctx state))
    ((er (list f f-existsp names-to-avoid))
     (solve-process-solution-name
          solution-name method ?f x1...xn
          verify-guards names-to-avoid ctx state))
    ((er &)
     (solve-process-solution-enable
          solution-enable
          solution-enable? f-existsp ctx state))
    ((er &)
     (solve-process-solution-guard solution-guard solution-guard?
                                   x1...xn f-existsp ctx state))
    ((er &)
     (solve-process-solution-guard-hints solution-guard-hints
                                         solution-guard-hints?
                                         f-existsp ctx state))
    ((er &)
     (solve-process-solution-body
          solution-body solution-body?
          method x1...xn f-existsp ctx state))
    ((er &)
     (solve-process-solution-hints
          solution-hints
          solution-hints? method ctx state))
    ((er (list new names-to-avoid))
     (process-input-new-name new-name old names-to-avoid ctx state))
    ((er new-enable)
     (process-input-new-enable new-enable old ctx state))
    ((er (list old-if-new names-to-avoid))
     (process-input-old-if-new-name
          old-if-new-name old-if-new-name?
          old new names-to-avoid ctx state))
    ((er old-if-new-enable)
     (process-input-old-if-new-enable old-if-new-enable
                                      old-if-new-enable? ctx state))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list old ?f x1...xn matrix f f-existsp new
                new-enable old-if-new old-if-new-enable
                verify-guards names-to-avoid)))))