		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-implementation-level

Xdoc::evmac-topic-event-generation

Generate an XDOC topic for the event generation that is part of the implementation of an event macro.

An event macro may generate some events only locally; in this case, the :some-local-p argument must be t. An event macro may generate some events both locally and non-locally, where the local variant has proof hints and the non-local variant does not; in this case, the :some-local-nonlocal-p argument must be t. An event macro may generate some events only non-locally; in this case the :some-nonlocal-p argument must be t. These arguments are used to customize the generated :long.

Macro: evmac-topic-event-generation

(defmacro xdoc::evmac-topic-event-generation
          (macro &key some-local-p
                 some-local-nonlocal-p some-nonlocal-p)
 (declare (xargs :guard (and (symbolp macro)
                             (booleanp some-local-p)
                             (booleanp some-local-nonlocal-p)
                             (booleanp some-nonlocal-p))))
 (b*
  ((macro-name (string-downcase (symbol-name macro)))
   (macro-ref (concatenate 'string
                           "@(tsee " macro-name ")"))
   (this-topic (add-suffix macro "-EVENT-GENERATION"))
   (parent-topic (add-suffix macro "-IMPLEMENTATION"))
   (short (concatenate 'string
                       "Event generation performed by "
                       macro-ref "."))
   (para-local-nonlocal?
    (and
     some-local-nonlocal-p
     '((xdoc::p
        "Some events are generated in two slightly different variants:
                 one that is local to the generated "
        (xdoc::seetopic "acl2::encapsulate" "@('encapsulate')")
        ", and one that is exported from the "
        (xdoc::seetopic "acl2::encapsulate" "@('encapsulate')")
        ". Proof hints are in the former but not in the latter,
                 thus keeping the ACL2 history ``clean'';
                 some proof hints may refer to events
                 that are generated only locally to the "
        (xdoc::seetopic "acl2::encapsulate" "@('encapsulate')")
        "."))))
   (para-local?
    (and
     some-local-p
     '((xdoc::p
        "Some events are generated only locally to the generated "
        (xdoc::seetopic "acl2::encapsulate" "@('encapsulate')")
        ". These are auxiliary events
                 needed to introduce the non-local (i.e. exported) events,
                 but whose presence in the ACL2 history is no longer needed
                 once the exported events have been introduced.
                 These only-local events have generated fresh names.
                 In contrast, exported events have names
                 that are user-controlled, directly or indirectly."))))
   (para-nonlocal?
    (and
     some-nonlocal-p
     '((xdoc::p
        "Some events are generated only non-locally to the generated "
        (xdoc::seetopic "acl2::encapsulate" "@('encapsulate')")
        ", i.e. they are exported,
                 without local counterparts."))))
   (long?
        (and (or some-local-nonlocal-p
                 some-local-p some-nonlocal-p)
             (cons 'xdoc::topstring
                   (append para-local-nonlocal?
                           (append para-local? para-nonlocal?))))))
  (cons
   'defxdoc+
   (cons
    this-topic
    (cons
     ':parents
     (cons
      (cons parent-topic 'nil)
      (cons
        ':short
        (cons short
              (append (and long? (list :long long?))
                      '(:order-subtopics t
                                         :default-parent t))))))))))