		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-process-old

Process the old input.

Signature
(tailrec-process-old old variant verify-guards verbose ctx state) → (mv erp result state)
Arguments: verbose — Guard (booleanp verbose).
Returns: result — A tuple (old$ test<x1,...,xn> base<x1,...,xn> nonrec<x1,...,xn> (... update-xi<x1...,xn> ...) combine<q,r> q r), satisfying (typed-tuplep symbolp pseudo-termp pseudo-termp pseudo-termp pseudo-term-listp pseudo-termp symbolp symbolp result), where old$ is the name of the target function of the transformation (denoted by the old input) and the other components are described in the documentation.

Show the components of the function denoted by old if verbose is t.

Definitions and Theorems

Function: tailrec-process-old

(defun tailrec-process-old
       (old variant verify-guards verbose ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (booleanp verbose)))
 (let ((__function__ 'tailrec-process-old))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((er old$)
     (ensure-function-name-or-numbered-wildcard$
          old "The first input" t nil))
    (description (msg "The target function ~x0" old$))
    ((er &)
     (ensure-function-is-logic-mode$ old$ description t nil))
    ((er &)
     (ensure-function-is-defined$ old$ description t nil))
    ((er &)
     (ensure-function-number-of-results$ old$ 1 description t nil))
    ((er &)
     (ensure-function-no-stobjs$ old$ description t nil))
    ((er &)
     (ensure-function-singly-recursive$ old$ description t nil))
    ((er &)
     (ensure-function-known-measure$ old$ description t nil))
    (body (if (non-executablep old$ wrld)
              (unwrapped-nonexec-body old$ wrld)
            (ubody old$ wrld)))
    (body (remove-lambdas body))
    ((er (list test then else))
     (ensure-term-if-call$
      body
      (msg
       "After translation and LET expansion, ~
                                    the body ~x0 of the target function ~x1"
       body old$)
      t nil))
    (then-calls-old-p (ffnnamep old$ then))
    (else-calls-old-p (ffnnamep old$ else))
    ((when (and then-calls-old-p else-calls-old-p))
     (er-soft+
      ctx t nil
      "After translation and LET expansion, ~
                   the body ~x0 of the target fuction ~x1 ~
                   must have one non-recursive top-level IF branch;
                   however, both branches call ~x1."
      body old$))
    ((mv test base combine-nonrec-reccall)
     (if then-calls-old-p (mv (dumb-negate-lit test) else then)
       (mv test then else)))
    ((er &)
     (ensure-term-does-not-call$
      test old$
      (msg
       "After translation and LET expansion, ~
                      the exit test ~x0 ~
                      of the target function ~x1"
       test old$)
      t nil))
    ((er &)
     (if
      (member-eq variant '(:monoid :monoid-alt))
      (ensure-term-ground$
       base
       (msg
        "Since the :VARIANT input is ~s0~x1, ~
                          after translation and LET expansion, ~
                          the non-recursive branch ~x2 ~
                          of the target function ~x3"
        (if (eq variant :monoid)
            "(perhaps by default) "
          "")
        variant base old$)
       t nil)
      (value nil)))
    ((er (list nonrec updates combine q r))
     (tailrec-decompose-recursive-branch
          old$ combine-nonrec-reccall ctx state))
    ((er &)
     (if
      (eq verify-guards t)
      (ensure-function-is-guard-verified$
       old$
       (msg
        "Since the :VERIFY-GUARDS input is T, ~
                          the target function ~x0"
        old$)
       t nil)
      (value nil)))
    ((run-when verbose)
     (cw "~%")
     (cw "Components of the target function ~x0:~%"
         old$)
     (cw "- Exit test: ~x0.~%"
         (untranslate test nil wrld))
     (cw "- Base value: ~x0.~%"
         (untranslate base nil wrld))
     (cw "- Non-recursive computation: ~x0.~%"
         (untranslate nonrec nil wrld))
     (cw "- Argument updates: ~x0.~%"
         (untranslate-lst updates nil wrld))
     (cw "- Combination operator: ~x0.~%"
         (untranslate combine nil wrld))
     (cw "- Fresh variable for non-recursive computation: ~x0.~%"
         q)
     (cw "- Fresh variable for recursive call: ~x0.~%"
         r)))
   (value (list old$ test
                base nonrec updates combine q r)))))