		Search-engine friendly clone of the ACL2 documentation.

Tailrec-input-processing

Tailrec-process-inputs

Process all the inputs.

Signature
(tailrec-process-inputs old variant domain new-name new-enable accumulator wrapper wrapper-name wrapper-name-present wrapper-enable wrapper-enable-present old-to-new-name old-to-new-name-present old-to-new-enable old-to-new-enable-present new-to-old-name new-to-old-name-present new-to-old-enable new-to-old-enable-present old-to-wrapper-name old-to-wrapper-name-present old-to-wrapper-enable old-to-wrapper-enable-present wrapper-to-old-name wrapper-to-old-name-present wrapper-to-old-enable wrapper-to-old-enable-present verify-guards hints print show-only ctx state) → (mv erp result state)
Arguments: wrapper-name-present — Guard (booleanp wrapper-name-present).; wrapper-enable-present — Guard (booleanp wrapper-enable-present).; old-to-new-name-present — Guard (booleanp old-to-new-name-present).; old-to-new-enable-present — Guard (booleanp old-to-new-enable-present).; new-to-old-name-present — Guard (booleanp new-to-old-name-present).; new-to-old-enable-present — Guard (booleanp new-to-old-enable-present).; old-to-wrapper-name-present — Guard (booleanp old-to-wrapper-name-present).; old-to-wrapper-enable-present — Guard (booleanp old-to-wrapper-enable-present).; wrapper-to-old-name-present — Guard (booleanp wrapper-to-old-name-present).; wrapper-to-old-enable-present — Guard (booleanp wrapper-to-old-enable-present).
Returns: result — A tuple (old$ test<x1,...,xn> base<x1,...,xn> nonrec<x1,...,xn> (... update-xi<x1...,xn> ...) combine<q,r> q r domain$ new-name$ new-enable$ a wrapper-name$ wrapper-enable$ old-to-new-name$ old-to-new-enable$ new-to-old-name$ new-to-old-enable$ old-to-wrapper-name$ old-to-wrapper-enable$ wrapper-to-old-name$ wrapper-to-old-enable$ verify-guards$ hints$ names-to-avoid) satisfying (typed-tuplep symbolp pseudo-termp pseudo-termp pseudo-termp pseudo-term-listp pseudo-termp symbolp symbolp pseudo-termfnp symbolp booleanp symbolp symbolp booleanp symbolp booleanp symbolp booleanp symbolp booleanp symbolp booleanp booleanp evmac-input-hints-p symbol-listp result).

Definitions and Theorems

Function: tailrec-process-inputs

(defun tailrec-process-inputs
       (old variant domain
            new-name new-enable accumulator wrapper
            wrapper-name wrapper-name-present
            wrapper-enable wrapper-enable-present
            old-to-new-name old-to-new-name-present
            old-to-new-enable
            old-to-new-enable-present
            new-to-old-name new-to-old-name-present
            new-to-old-enable
            new-to-old-enable-present
            old-to-wrapper-name
            old-to-wrapper-name-present
            old-to-wrapper-enable
            old-to-wrapper-enable-present
            wrapper-to-old-name
            wrapper-to-old-name-present
            wrapper-to-old-enable
            wrapper-to-old-enable-present
            verify-guards
            hints print show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (booleanp wrapper-name-present)
                         (booleanp wrapper-enable-present)
                         (booleanp old-to-new-name-present)
                         (booleanp old-to-new-enable-present)
                         (booleanp new-to-old-name-present)
                         (booleanp new-to-old-enable-present)
                         (booleanp old-to-wrapper-name-present)
                         (booleanp old-to-wrapper-enable-present)
                         (booleanp wrapper-to-old-name-present)
                         (booleanp wrapper-to-old-enable-present))))
 (let ((__function__ 'tailrec-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (evmac-process-input-print print ctx state))
    (verbose (and (member-eq print '(:info :all)) t))
    ((er (list old$
               test base nonrec updates combine q r))
     (tailrec-process-old old variant
                          verify-guards verbose ctx state))
    ((er &)
     (tailrec-process-variant$ variant "The :VARIANT input" t nil))
    ((er verify-guards$)
     (process-input-verify-guards verify-guards old$ ctx state))
    ((er domain$)
     (tailrec-process-domain domain old$ combine q r variant
                             verify-guards$ verbose ctx state))
    ((er &)
     (ensure-value-is-boolean$ wrapper "The :WRAPPER input" t nil))
    ((er (list new-name$ wrapper-name$ names-to-avoid))
     (process-input-new/wrapper-names
          new-name
          wrapper-name wrapper-name-present
          wrapper old$ nil ctx state))
    ((er new-enable$)
     (process-input-new-enable new-enable old$ ctx state))
    ((er a)
     (tailrec-process-accumulator accumulator old$ r ctx state))
    ((er wrapper-enable$)
     (process-input-wrapper-enable
          wrapper-enable wrapper-enable-present
          wrapper ctx state))
    ((er (list old-to-new-name$ names-to-avoid))
     (process-input-old-to-new-name
          old-to-new-name
          old-to-new-name-present old$
          new-name$ names-to-avoid ctx state))
    ((er old-to-new-enable$)
     (process-input-old-to-new-enable
          old-to-new-enable
          old-to-new-enable-present ctx state))
    ((er (list new-to-old-name$ names-to-avoid))
     (process-input-new-to-old-name
          new-to-old-name
          new-to-old-name-present old$
          new-name$ names-to-avoid ctx state))
    ((er new-to-old-enable$)
     (process-input-new-to-old-enable
          new-to-old-enable
          new-to-old-enable-present ctx state))
    ((er (list old-to-wrapper-name$ names-to-avoid))
     (process-input-old-to-wrapper-name
          old-to-wrapper-name
          old-to-wrapper-name-present wrapper old$
          wrapper-name$ names-to-avoid ctx state))
    ((er old-to-wrapper-enable$)
     (process-input-old-to-wrapper-enable
          old-to-wrapper-enable
          old-to-wrapper-enable-present
          wrapper ctx state))
    ((er (list wrapper-to-old-name$ names-to-avoid))
     (process-input-wrapper-to-old-name
          wrapper-to-old-name
          wrapper-to-old-name-present wrapper old$
          wrapper-name$ names-to-avoid ctx state))
    ((er wrapper-to-old-enable$)
     (process-input-wrapper-to-old-enable
          wrapper-to-old-enable
          wrapper-to-old-enable-present
          wrapper ctx state))
    ((when (and old-to-new-enable$ new-to-old-enable$))
     (er-soft+
      ctx t nil
      "The :OLD-TO-NEW-ENABLE and :NEW-TO-OLD-ENABLE inputs ~
                   are (perhaps by default, for one of them) both T. ~
                   This is disallowed."))
    ((when (and wrapper old-to-wrapper-enable$
                wrapper-to-old-enable$))
     (er-soft+
      ctx t nil
      "The :OLD-TO-WRAPPER-ENABLE ~
                   and :WRAPPER-TO-OLD-ENABLE inputs ~
                   are (perhaps by default, for one of them) both T. ~
                   This is disallowed."))
    ((er hints$)
     (evmac-process-input-hints hints ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state)))
   (value (list old$ test
                base nonrec updates combine q r domain$
                new-name$ new-enable$ a wrapper-name$
                wrapper-enable$ old-to-new-name$
                old-to-new-enable$ new-to-old-name$
                new-to-old-enable$ old-to-wrapper-name$
                old-to-wrapper-enable$
                wrapper-to-old-name$
                wrapper-to-old-enable$ verify-guards$
                hints$ names-to-avoid)))))