		Search-engine friendly clone of the ACL2 documentation.

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