• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • 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
          • Defaults-table
          • Xdoc::apt-constructors
          • Input-processors
            • Process-input-old-soft-io-sel-mod
            • Process-input-new/wrapper-names
            • Process-input-select-old-soft-io
            • Process-input-old-to-new-name
            • Process-input-old-if-new-name
            • Process-input-old-to-wrapper-name
            • Process-input-wrapper-enable
            • Process-input-wrapper-to-old-name
            • Process-input-old-to-new-enable
            • Process-input-old-to-wrapper-enable
            • Process-input-old-if-new-enable
            • Process-input-new-name
            • Process-input-new-to-old-name
            • Process-input-wrapper-to-old-enable
            • Process-input-verify-guards
            • Process-input-new-enable
            • Process-input-new-to-old-enable
          • Transformation-table
          • Find-base-cases
          • Untranslate-specifier-utilities
          • Print-specifier-utilities
          • Hints-specifier-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
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Utilities

Input-processors

Utilities to process inputs that are common to multiple APT transformations.

Subtopics

Process-input-old-soft-io-sel-mod
Process the old input of an APT transformation, when that input must denote a SOFT shallow pop-refinement specification of a certain form.
Process-input-new/wrapper-names
Process the :new-name and :wrapper-name inputs.
Process-input-select-old-soft-io
Process the input of an APT transformation that selects an input of the function variable call in a SOFT shallow pop-refinement specification of a certain form.
Process-input-old-to-new-name
Process the :old-to-new-name input of an APT transformation.
Process-input-old-if-new-name
Process the :old-if-new-name input of an APT transformation.
Process-input-old-to-wrapper-name
Process the :old-to-wrapper-name input of an APT transformation.
Process-input-wrapper-enable
Process the :wrapper-enable input of an APT transformation.
Process-input-wrapper-to-old-name
Process the :wrapper-to-old-name input of an APT transformation.
Process-input-old-to-new-enable
Process the :old-to-new-enable input of an APT transformation.
Process-input-old-to-wrapper-enable
Process the :old-to-wrapper-enable input of an APT transformation.
Process-input-old-if-new-enable
Process the :old-if-new-enable input of an APT transformation.
Process-input-new-name
Process the :new-name input of an APT transformation.
Process-input-new-to-old-name
Process the :new-to-old-name input of an APT transformation.
Process-input-wrapper-to-old-enable
Process the :wrapper-to-old-enable input of an APT transformation.
Process-input-verify-guards
Process the :verify-guards input of an APT transformation.
Process-input-new-enable
Process the :new-enable input of an APT transformation.
Process-input-new-to-old-enable
Process the :new-to-old-enable input of an APT transformation.