• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • 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
            • Transformation-table
              • Remove-irrelevant-inputs-from-transformation-call
              • Record-transformation-call-event
              • Previous-transformation-expansion
            • 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
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Utilities

Transformation-table

APT transformation table.

This table records, for each successful call to an APT transformation, the encapsulate generated by the call. This is used to support redundancy checks for transformations.

Only transformation calls whose :show-only input is (perhaps by default) nil are recorded into the table by the transformations, because calls whose :show-only input is t do not affect the world. The :show-only input, if present, is removed prior to storing a call in the table and prior to comparing a call with the keys in the table.

Since the :print input to transformations only affects screen output, it is similarly removed from a call prior to storing a call in the table and prior to comparing a call with the keys in the table.

The information associated with each call in the table may be extended beyond the encapsulate in the future.

Subtopics

Remove-irrelevant-inputs-from-transformation-call
Remove from a call to a transformation the :print and :show-only inputs, if present.
Record-transformation-call-event
Create an event form to record a transformation call into the transformation table.
Previous-transformation-expansion
Retrieve the encapsulate previously generated by this transformation call, if any.