• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • 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
    • 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

• 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))))))))))))