• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • 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
              • Isodata-implementation
                • Isodata-event-generation
                • Isodata-fn
                • Isodata-input-processing
                  • Isodata-symbol-isomap-alistp
                  • Isodata-isomapp
                  • Isodata-pos-isomap-alistp
                  • Isodata-process-iso
                  • Isodata-process-inputs
                  • Isodata-process-arg/res-list-iso
                  • Isodata-process-isomaps
                  • Isodata-fresh-defiso-thm-names
                  • Isodata-process-arg/res-list
                  • Isodata-process-arg/res-list-iso-list
                  • Isodata-process-res
                  • Isodata-fresh-defiso-name-with-*s-suffix
                  • Isodata-process-newp-of-new-name
                  • Isodata-process-isomaps-ress
                  • Isodata-process-isomaps-args
                  • Isodata-process-arg/res-list-iso-add-ress
                  • Isodata-process-arg/res-list-iso-add-args
                  • Isodata-process-old
                  • Isodata-process-undefined
                  • Isodata-process-arg/res-list-aux
                  • Isodata-isomap-listp
                  • Isodata-fresh-defiso-name-with-*s-suffix-aux
                • Isodata-macro-definition
            • 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
            • 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
      • Mailing-lists
      • Interfacing-tools
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
        • Simplify-defun
        • Isodata
          • Isodata-implementation
            • Isodata-event-generation
            • Isodata-fn
            • Isodata-input-processing
              • Isodata-symbol-isomap-alistp
              • Isodata-isomapp
              • Isodata-pos-isomap-alistp
              • Isodata-process-iso
              • Isodata-process-inputs
              • Isodata-process-arg/res-list-iso
              • Isodata-process-isomaps
              • Isodata-fresh-defiso-thm-names
              • Isodata-process-arg/res-list
              • Isodata-process-arg/res-list-iso-list
              • Isodata-process-res
              • Isodata-fresh-defiso-name-with-*s-suffix
              • Isodata-process-newp-of-new-name
              • Isodata-process-isomaps-ress
              • Isodata-process-isomaps-args
              • Isodata-process-arg/res-list-iso-add-ress
              • Isodata-process-arg/res-list-iso-add-args
              • Isodata-process-old
              • Isodata-process-undefined
              • Isodata-process-arg/res-list-aux
              • Isodata-isomap-listp
              • Isodata-fresh-defiso-name-with-*s-suffix-aux
            • Isodata-macro-definition
        • 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
        • 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
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Isodata-implementation

Isodata-input-processing

Input processing performed by isodata.

See input processing for general background.

Subtopics

Isodata-symbol-isomap-alistp
Recognize alists from symbols to isomorphic mapping records.
Isodata-isomapp
Information about an isomorphic mapping according to which (some of) the target function's arguments and results are transformed.
Isodata-pos-isomap-alistp
Recognize alists from positive integers to isomorphic mapping records.
Isodata-process-iso
Process an iso component of the isomaps input.
Isodata-process-inputs
Process all the inputs.
Isodata-process-arg/res-list-iso
Process an (arg/res-list iso) component of the isomaps input.
Isodata-process-isomaps
Process the isomaps input.
Isodata-fresh-defiso-thm-names
Return fresh defiso theorem names.
Isodata-process-arg/res-list
Process an arg/res-list component of the isomaps input.
Isodata-process-arg/res-list-iso-list
Lift isodata-process-arg/res-list-iso to lists.
Isodata-process-res
Process a result specification in the isomap input.
Isodata-fresh-defiso-name-with-*s-suffix
Suffix a name with as many *s as needed to make it a valid name for a new defiso.
Isodata-process-newp-of-new-name
Process the :newp-of-new-name input.
Isodata-process-isomaps-ress
Isodata-process-isomaps-args
Isodata-process-arg/res-list-iso-add-ress
Isodata-process-arg/res-list-iso-add-args
Isodata-process-old
Process the old input.
Isodata-process-undefined
Process the :undefined input.
Isodata-process-arg/res-list-aux
Isodata-isomap-listp
Recognize lists of isomorphic mapping records.
Isodata-fresh-defiso-name-with-*s-suffix-aux