• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
          • Tailrec-implementation
            • Tailrec-event-generation
            • Tailrec-fn
            • Tailrec-macro-definition
            • Tailrec-input-processing
              • Tailrec-process-inputs
                • Tailrec-process-old
                • Tailrec-process-domain
                • Tailrec-decompose-recursive-branch
                • Tailrec-check-nonrec-conditions
                • Tailrec-process-variant
                • Tailrec-infer-domain
                • Tailrec-find-nonrec-term-in-term/terms
                • Tailrec-process-accumulator
                • Tailrec-variantp
          • Schemalg
          • Restrict
          • Expdata
          • Casesplit
          • Simplify-term
          • Simplify-defun-sk
          • Parteval
          • Solve
          • Wrap-output
          • Propagate-iso
          • Simplify
          • Finite-difference
          • Drop-irrelevant-params
          • Copy-function
          • Lift-iso
          • Rename-params
          • Utilities
          • Simplify-term-programmatic
          • Simplify-defun-sk-programmatic
          • Simplify-defun-programmatic
          • Simplify-defun+
          • Common-options
          • Common-concepts
        • Std/util
        • Defdata
        • Defrstobj
        • Seq
        • Match-tree
        • Defrstobj
        • With-supporters
        • Def-partial-measure
        • Template-subst
        • Soft
        • Defthm-domain
        • Event-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
        • Theories
        • Rule-classes
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
          • Make-event
          • Defmacro
          • Untranslate-patterns
          • Tc
          • Trans*
          • Macro-aliases-table
          • Macro-args
          • Defabbrev
          • User-defined-functions-table
          • Trans
          • Untranslate-for-execution
          • Add-macro-fn
          • Check-vars-not-free
          • Safe-mode
          • Macro-libraries
            • B*
            • Defunc
            • Fty
            • Apt
              • Simplify-defun
              • Isodata
              • Tailrec
                • Tailrec-implementation
                  • Tailrec-event-generation
                  • Tailrec-fn
                  • Tailrec-macro-definition
                  • Tailrec-input-processing
                    • Tailrec-process-inputs
                      • Tailrec-process-old
                      • Tailrec-process-domain
                      • Tailrec-decompose-recursive-branch
                      • Tailrec-check-nonrec-conditions
                      • Tailrec-process-variant
                      • Tailrec-infer-domain
                      • Tailrec-find-nonrec-term-in-term/terms
                      • Tailrec-process-accumulator
                      • Tailrec-variantp
                • Schemalg
                • Restrict
                • Expdata
                • Casesplit
                • Simplify-term
                • Simplify-defun-sk
                • Parteval
                • Solve
                • Wrap-output
                • Propagate-iso
                • Simplify
                • Finite-difference
                • Drop-irrelevant-params
                • Copy-function
                • Lift-iso
                • Rename-params
                • Utilities
                • Simplify-term-programmatic
                • Simplify-defun-sk-programmatic
                • Simplify-defun-programmatic
                • Simplify-defun+
                • Common-options
                • Common-concepts
              • Std/util
              • Defdata
              • Defrstobj
              • Seq
              • Match-tree
              • Defrstobj
              • With-supporters
              • Def-partial-measure
              • Template-subst
              • Soft
              • Defthm-domain
              • Event-macros
              • Def-universal-equiv
              • Def-saved-obligs
              • With-supporters-after
              • Definec
              • Sig
              • Outer-local
              • Data-structures
            • Trans1
            • Defmacro-untouchable
            • Set-duplicate-keys-action
            • Add-macro-alias
            • Magic-macroexpand
            • Defmacroq
            • Trans!
            • Remove-macro-fn
            • Remove-macro-alias
            • Add-binop
            • Untrans-table
            • Trans*-
            • Remove-binop
            • Tcp
            • Tca
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • 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)))))