• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Evmac-input-print-p
      • Function-definedness
      • Event-macro-input-processing
      • Event-macro-screen-printing
      • Make-event-terse
      • Event-macro-applicability-conditions
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
        • Event-macro-xdoc-constructors-user-level
        • Event-macro-xdoc-constructors-implementation-level
          • Xdoc::evmac-topic-implementation
          • Xdoc::evmac-topic-event-generation
          • Xdoc::evmac-topic-input-processing
          • Xdoc::evmac-topic-library-extensions
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

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