• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
        • Isodata
        • Simplify-defun
        • 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
            • Xdoc::desc-apt-input-thm-name
            • Xdoc::desc-apt-input-thm-enable
            • Xdoc::desc-apt-input-verify-guards
            • Xdoc::apt-design-notes-ref
            • Xdoc::desc-apt-input-wrapper-to-old-name
            • Xdoc::desc-apt-input-old-to-wrapper-name
            • Xdoc::desc-apt-input-wrapper-to-old-enable
            • Xdoc::desc-apt-input-wrapper-name
            • Xdoc::desc-apt-input-old-to-wrapper-enable
            • Xdoc::desc-apt-input-old-to-new-name
            • Xdoc::desc-apt-input-old-if-new-name
            • Xdoc::desc-apt-input-new-to-old-name
            • Xdoc::desc-apt-input-wrapper-enable
            • Xdoc::desc-apt-input-old-to-new-enable
            • Xdoc::desc-apt-input-old-if-new-enable
            • Xdoc::desc-apt-input-new-to-old-enable
            • Xdoc::desc-apt-input-new-name
            • Xdoc::desc-apt-input-untranslate
            • Xdoc::desc-apt-input-old
            • Xdoc::desc-apt-input-new-enable
            • Xdoc::desc-apt-input-wrapper
          • Input-processors
          • 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
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Xdoc::apt-constructors

Xdoc::desc-apt-input-thm-name

Build a description of the :thm-name input for the user documentation of an APT transformation.

The wrapper? parameter of this macro has the value :never when the transformation never generates a wrapper; it has the value :optional when the transformation includes a :wrapper input that determines whether the wrapper is generated or not (i.e. the wrapper is optional); it has the value :always when the transformation always generates the wrapper.

The theorem relates the old function to the new function when there is no wrapper function, while it relates the old function to the wrapper function where there is a wrapper function. Thus, the description is tailored based on the wrapper? parameter.

Macro: desc-apt-input-thm-name

(defmacro xdoc::desc-apt-input-thm-name (wrapper? &rest additional)
 (declare
    (xargs :guard (member-eq wrapper? '(:never :optional :always))))
 (b*
  ((new/wrapper-ref
    (case wrapper?
     (:never "@('new')")
     (:optional
      "@('new') (if the @(':wrapper') input is @('nil')) or
                      @('wrapper') (if the @(':wrapper') input is @('t'))")
     (:always "@('wrapper')")))
   (thm-name
    (case wrapper?
     (:never "@('old-to-new')")
     (:optional
      "@('old-to-new')
                      (if the @(':wrapper') input is @('nil')) or
                      @('old-to-wrapper')
                      (if the @(':wrapper') input is @('t'))")
     (:always "@('old-to-wrapper')"))))
  (cons
   'xdoc::desc
   (cons
    '"@('thm-name') — default @(':auto')"
    (cons
     (cons
      'xdoc::p
      (cons
       '"Determines the name of the theorem that relates @('old') to "
       (cons new/wrapper-ref '(":"))))
     (cons
      (cons
       'xdoc::ul
       (cons
        (cons
         'xdoc::li
         (cons
          '"@(':auto'), to use the "
          (cons
           '(xdoc::seetopic "acl2::paired-names" "paired name")
           (cons
            '" obtained by "
            (cons
             '(xdoc::seetopic "acl2::make-paired-name" "pairing")
             (cons
              '" the name of @('old') and the name of "
              (cons
               new/wrapper-ref
               (cons
                   '", putting the result into the same package as "
                   (cons new/wrapper-ref '("."))))))))))
        '((xdoc::li
           "Any other symbol
         (that is not in the main Lisp package and that is not a keyword),
         to use as the name of the theorem."))))
      (cons
         (cons 'xdoc::p
               (cons '"In the rest of this documentation page, let "
                     (cons thm-name '(" be this theorem."))))
         additional)))))))