		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-body

Process the body input.

Signature
(defarbrec-process-body body fn$ x1...xn$ ctx state) → (mv erp result state)
Returns: result — A tuple (body$ test updates) satisfying (typed-tuplep pseudo-termp pseudo-termp pseudo-term-listp result).

We submit the program-mode function to ACL2, so that any errors in the body will be caught and will stop execution with an error. If the submission succeeds, the ACL2 state now includes the function, which we further validate and decompose.

If the function has the form assumed in the documentation of defarbrec, the exit test is test<x1,...,xn> and the updated arguments are update-x1<x1,...,xn>, ..., update-xn<x1,...xn>. If the function has a different form, the exit test is the negation of the conjunction of the tests that control the recursive call.

Note that the wrld variable is bound after calling trans-eval-error-triple, to ensure that the program-mode function is in that world.

Definitions and Theorems

Function: defarbrec-process-body

(defun defarbrec-process-body (body fn$ x1...xn$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defarbrec-process-body))
  (declare (ignorable __function__))
  (b*
   ((program-mode-fn
         (cons 'defun
               (cons fn$
                     (cons x1...xn$
                           (cons '(declare (xargs :mode :program))
                                 (cons body 'nil))))))
    ((er &)
     (trans-eval-error-triple program-mode-fn ctx state))
    (wrld (w state))
    (body$ (ubody fn$ wrld))
    (description (msg "The function ~x0" fn$))
    ((er &)
     (ensure-function-number-of-results$ fn$ 1 description t nil))
    ((er &)
     (ensure-function-no-stobjs$ fn$ description t nil))
    (rec-calls-with-tests (recursive-calls fn$ wrld))
    (num-rec-calls (len rec-calls-with-tests))
    ((when (/= num-rec-calls 1))
     (er-soft+
      ctx t nil
      "The function ~x0 must make exactly one recursive call, ~
                   but it makes ~x1 recursive calls instead."
      fn$ num-rec-calls))
    (program-mode-fns (all-program-ffn-symbs body$ nil wrld))
    (program-mode-fns (remove-eq fn$ program-mode-fns))
    ((unless (null program-mode-fns))
     (er-soft+
      ctx t nil
      "The function ~x0 must call ~
                   only logic-mode functions besides itself, ~
                   but it also calls the program-mode ~@1 instead."
      fn$
      (if (= (len program-mode-fns) 1)
          (msg "function ~x0" (car program-mode-fns))
        (msg "functions ~&0" program-mode-fns))))
    (rec-call-with-tests (car rec-calls-with-tests))
    (tests (access tests-and-call
                   rec-call-with-tests :tests))
    (rec-call (access tests-and-call
                      rec-call-with-tests :call))
    (test (dumb-negate-lit (conjoin tests)))
    (updates (fargs rec-call)))
   (value (list body$ test updates)))))