• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
        • Soft-future-work
        • Soft-macros
        • Updates-to-workshop-material
        • Soft-implementation
          • Soft-implementation-core
          • Gen-macro2-of-macro
          • Defun-inst-implementation
          • Defthm-inst-implementation
          • Defsoft-implementation
          • Defunvar-implementation
          • Defund-sk2-implementation
          • Defun-sk2-implementation
          • Define-sk2-implementation
          • Defchoose2-implementation
          • Defund2-implementation
          • Defun2-implementation
          • Define2-implementation
        • Soft-notions
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Soft-implementation

Gen-macro2-of-macro

Generate a second-order counterpart of an event macro.

SOFT provides second-order counterparts of a number of event macros. For instance, it provides defun2 as a second-order counterpart of defun. These second-order macros are implemented as simply their first-order counterparts followed by defsoft. Since their implementation has such a simple and regular structure, we capture it in this ``meta'' macro, which you use to generate the second-order macros.

Macro: gen-macro2-of-macro

(defmacro gen-macro2-of-macro (macro)
 (declare (xargs :guard (symbolp macro)))
 (b*
   ((macro2 (str::cat (symbol-name macro) "2"))
    (softmacro2 (intern$ macro2 "SOFT"))
    (acl2macro2 (intern$ macro2 "ACL2"))
    (macro2-string (str::downcase-string (symbol-name softmacro2)))
    (acl2macro2-string (str::cat "acl2::" macro2-string)))
  (cons
   'defsection
   (cons
    (intern$ (str::cat macro2 "-IMPLEMENTATION")
             "SOFT")
    (cons
     ':parents
     (cons
      (cons 'soft-implementation
            (cons softmacro2 'nil))
      (cons
       ':short
       (cons
        (str::cat "Implementation of @(tsee "
                  macro2-string ").")
        (cons
         ':long
         (cons
          (str::cat "@(def " macro2-string
                    ") @(def " acl2macro2-string ")")
          (cons
           (cons
            'defmacro
            (cons
             softmacro2
             (cons
              '(sofun &rest rest)
              (cons
               (cons
                'list
                (cons
                   ''progn
                   (cons (cons 'list*
                               (cons (cons 'quote (cons macro 'nil))
                                     '(sofun rest)))
                         '((list 'defsoft sofun)))))
               'nil))))
           (cons
            (cons
             'defmacro
             (cons
              acl2macro2
              (cons
               '(&rest args)
               (cons
                    (cons 'list*
                          (cons (cons 'quote (cons softmacro2 'nil))
                                '(args)))
                    'nil))))
            'nil))))))))))))