xdoc-constructors

(in-package "ACL2")

(defxdoc+ event-macro-xdoc-constructors
  :parents (event-macros composite-constructors)
  :short "Utilities to construct <see topic='@(url xdoc)'>XDOC</see> strings
          to document <see topic='@(url event-macros)'>event macros</see>
          and their implementations.")

(defxdoc+ event-macro-xdoc-constructors-user-level
  :parents (event-macro-xdoc-constructors)
  :short "Utilities to construct <see topic='@(url xdoc)'>XDOC</see> strings
          to document <see topic='@(url event-macros)'>event macros</see>
          at the user level."
  :long (topstring (p "The @('xdoc::evmac-section-...') utilities construct level-3 sections.
     Some are relatively thin wrappers,
     which precede their arguments
     (which must be zero or more pieces of XDOC text)
     with specific level-3 headings.
     Other utilities provide more automation.")
    (p "The @('xdoc::evmac-input-...') utilities construct
     <see topic='@(url xdoc::desc)'>descriptions</see>
     of inputs that are expected to be common to multiple event macros.
     Each such utility includes zero or more parameters
     to customize the description,
     as well as zero or more additional pieces of XDOC text (e.g. paragraphs)
     that are appended after the automatically generated XDOC text."))
  :default-parent t)

(defmacro+ evmac-section-intro
  (&rest content)
  :short "Construct the introduction section
          of the user documentation of an event macro."
  `(section *evmac-section-intro-title* ,@CONTENT))

(defmacro+ evmac-section-form
  (&rest content)
  :short "Construct the general form section
          of the user documentation of an event macro."
  `(section *evmac-section-form-title* ,@CONTENT))

(defmacro+ evmac-section-inputs
  (&rest content)
  :short "Construct the inputs section
          of the user documentation of an event macro."
  `(section *evmac-section-inputs-title* ,@CONTENT))

(defmacro+ evmac-section-appconds
  (macro &rest content)
  (declare (xargs :guard (symbolp macro)))
  :short "Construct the applicability conditions section
          of the user documentation of an event macro."
  :long (topstring (p "Since this documentation is part of the XDOC topic
     whose name is the name of the macro,
     the @('macro-ref') variable is not a link."))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')"))
      (inputs-ref (concatenate 'string
          "`"
          *evmac-section-inputs-title*
          "' section")))
    `(section *evmac-section-appconds-title*
      (p "In order for "
        ,MACRO-REF
        " to apply,
        in addition to the requirements on the inputs
        stated in the "
        ,INPUTS-REF
        ", the following "
        (seetopic "acl2::event-macro-applicability-conditions"
          "applicability conditions")
        " must be proved.
         The proofs are attempted when "
        ,MACRO-REF
        " is called,
        using the hints optionally supplied as the @(':hints') input
        described in the "
        ,INPUTS-REF
        ".")
      ,@CONTENT)))

(defmacro+ evmac-section-generated
  (&rest content)
  :short "Construct the generated events section
          of the user documentation of an event macro."
  `(section *evmac-section-generated-title*
    ,@CONTENT))

(defmacro+ evmac-section-redundancy
  (macro)
  (declare (xargs :guard (symbolp macro)))
  :short "Construct the redundancy section
          of the user documentation of an event macro."
  :long (topstring (p "This assumes an event macro with a @(':print') and @(':show-only') inputs
     with specific meanings.
     This XDOC constructor may be generalized in the future
     to cover event macros that do not have exactly
     those two specific inputs with those specific meanings.")
    (p "Since this documentation is part of the XDOC topic
     whose name is the name of the macro,
     the @('macro-ref') variable is not a link."))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')")))
    `(section *evmac-section-redundancy-title*
      (p (concatenate 'string
          "A call of "
          ,MACRO-REF
          " is redundant if and only if
         it is identical to a previous successful call of "
          ,MACRO-REF
          " whose @(':show-only') input is not @('t'),
         except that the two calls may differ in
         their @(':print') and @(':show-only') inputs.
         These inputs do not affect the generated events,
         and thus they are ignored for the purpose of redundancy."))
      (p (concatenate 'string
          "A call of "
          ,MACRO-REF
          " whose @(':show-only') input is @('t')
         does not generate any event.
         Thus, no successive call may be redundant with such a call.")))))

(defmacro+ evmac-input-hints
  (&key additional)
  :short "Construct a description of the @(':hints') input
          for the user documentation of an event macro."
  (let ((appconds-ref (concatenate 'string
         "`"
         *evmac-section-appconds-title*
         "' section")))
    `(desc "@(':hints') — default @('nil')"
      (p "Hints to prove the applicability conditions.")
      (p "It must be one of the following:")
      (ul (li "A "
          (seetopic "acl2::keyword-value-listp"
            "keyword-value list")
          " @('(appcond1 hints1 appcond2 hints2 ...)'),
         where each @('appcondk') is a keyword
         that identifies one of the applicability conditions
         listed in the "
          ,APPCONDS-REF
          " and each @('hintsk') is a list of hints of the kind
         that may appear just after @(':hints') in a @(tsee defthm).
         The hints @('hintsk') are used
         to prove applicability condition @('appcondk').
         The @('appcond1'), @('appcond2'), ... keywords must be all distinct.
         An @('appcondk') keyword is allowed only if
         the corresponding applicability condition is present,
         as specified in the "
          ,APPCONDS-REF
          ".")
        (li "A list of hints of the kind
         that may appear just after @(':hints') in a @(tsee defthm).
         In this case, these same hints are used
         to prove every applicability condition,."))
      ,@ADDITIONAL)))

(defmacro+ evmac-input-print
  (macro &key additional)
  :short "Construct a description of the @(':print') input
          for the user documentation of an event macro."
  :long (topstring-p "Since this documentation is part of the XDOC topic
    whose name is the name of the macro,
    the @('macro-ref') variable is not a link.")
  (declare (xargs :guard (symbolp macro)))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')")))
    `(desc "@(':print') — default @(':result')"
      (p "Specifies what is printed on the screen
        (see "
        (seetopic "acl2::event-macro-screen-printing"
          "screen printing")
        ").")
      (p "It must be one of the following:")
      (ul (li "@('nil'), to print nothing (not even error output).")
        (li "@(':error'), to print only error output (if any).")
        (li "@(':result'), to print, besides any error output,
         also the "
          (seetopic "acl2::event-macro-results" "results")
          " of "
          ,MACRO-REF
          ".
         This is the default value of the @(':print') input.")
        (li "@(':info'), to print,
         besides any error output and the results,
         also some additional information about
         the internal operations of "
          ,MACRO-REF
          ".")
        (li "@(':all'), to print,
         besides any error output,
         the results,
         and the additional information,
         also ACL2's output in response to all the submitted events."))
      (p "If the call of "
        ,MACRO-REF
        " is redundant,
        an indication to that effect is printed on the screen,
        unless @(':print') is @('nil').")
      ,@ADDITIONAL)))

(defmacro+ evmac-input-show-only
  (macro &key additional)
  :short "Construct a description of the @(':show-only') input
          for the user documentation of an event macro."
  :long (topstring-p "Since this documentation is part of the XDOC topic
    whose name is the name of the macro,
    the @('macro-ref') variable is not a link.")
  (declare (xargs :guard (symbolp macro)))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@('" macro-name "')"))
      (redundancy-ref (concatenate 'string
          "`"
          *evmac-section-redundancy-title*
          "' section")))
    `(desc "@(':show-only') — default @('nil')"
      (p (concatenate 'string
          "Determines whether the event expansion of "
          ,MACRO-REF
          " is submitted to ACL2 or just printed on the screen:"))
      (ul (li "@('nil'), to submit it.")
        (li (concatenate 'string
            "@('t'), to just print it.
          In this case:
          the event expansion is printed even if @(':print') is @('nil')
          (because the user has explicitly asked to show the event expansion);
          the resulting events are not re-printed separately
          (other than their appearance in the printed event expansion)
          even if @(':print') is @(':result') or @(':info') or @(':all');
          no ACL2 output is printed for the event expansion
          even if @(':print') is @(':all')
          (because the event expansion is not submitted).
          If the call of "
            ,MACRO-REF
            " is redundant
          (as defined in the "
            ,REDUNDANCY-REF
            "), the event expansion generated by the existing call
          is printed.")))
      ,@ADDITIONAL)))

(defmacro+ evmac-desc-input-name
  (prefix &key desc auto-desc additional name-rest)
  :short "Construct a description of a @(':...-name') input
          for the user documentation of an event macro."
  :long (topstring (p "This is for an input to determine the name of
     an entity (e.g. a function) generated by the event macro.")
    (p "The @('...') in @(':...-name') is passed as
     the @('prefix') argument of this macro.")
    (p "A description of the entitty whose name is being determined
     is passed as the @('desc') argument of this macro.")
    (p "The @('auto-desc') argument of this macro describes the name used
     when the @(':...-name') input is @(':auto').")
    (p "An XDOC tree of additional text can be passed
     as the @('additional') argument of this macro.")
    (p "The @('name-rest') argument of this macro is
     the name that the generated documentation says that will be used
     as the name of the entity in the rest of the documentation page."))
  (declare (xargs :guard (and (stringp prefix)
        (stringp desc)
        (stringp auto-desc)
        (stringp name-rest))))
  `(desc ,(CONCATENATE 'STRING "@(':" PREFIX "-name') — default @(':auto')")
    (p "Determines the name of " ,DESC ".")
    (p "It must be one of the following:")
    (ul (li "@(':auto'), to use " ,AUTO-DESC ".")
      (li "Any other symbol, to use as the name."))
    ,@(AND ADDITIONAL (LIST ADDITIONAL))
    (p "In the rest of this documentation page,
      let @('"
      ,NAME-REST
      "') be this name.")))

(defmacro+ evmac-desc-input-enable-t/nil
  (prefix &key default desc)
  :short "Construct a description of a @(':...-enable') input
          for the user documentation of an event macro."
  :long (topstring (p "This is for an input to determine the enablement of
     an entity (e.g. a function) generated by the event macro.")
    (p "The @('...') in @(':...-enable') is passed as
     the @('prefix') argument of this macro.")
    (p "The default is passed as the @('default') argument of this macro.")
    (p "The description of the entity is passed as
     the @('desc') argument of this macro."))
  (declare (xargs :guard (and (stringp prefix) (booleanp default) (stringp desc))))
  `(desc ,(CONCATENATE 'STRING "@(':" PREFIX "-enable') — default "
              (IF DEFAULT
                  "@('t')"
                  "@('nil')"))
    (p "Determines whether " ,DESC " is enabled.")
    (p "It must be one of the following:")
    (ul (li "@('t'), to enable.")
      (li "@('nil'), to disable."))))

(defmacro+ evmac-desc-function/lambda/macro
  (&key (subject '"It")
    (1arg 'nil)
    (1res 'nil)
    (stobjs 'nil)
    (guard 'nil)
    (dont-be-or-call 'nil)
    (additional-function 'nil)
    (additional-lambda 'nil)
    (additional-forms '""))
  :short "Construct a common description text for an input that must be
          a function name or a lambda expression or a macro name."
  :long (topstring (p "This text expresses some common requirements
     on this kind of inputs to event macros.")
    (p "This utility provides some customization facilities:")
    (ul (li "The @('subject') parameter must be XDOC text
      that describes the subject of the assertion of the requirements.
      The default is the string @('"It"'),
      which should be appropriate if this text follows
      some preceding text that describes what the input is for.")
      (li "The @('1arg') parameter must be a boolean
      that specifies whether the function or lambda expression
      must be unary (i.e. take one argument) or not.")
      (li "The @('1res') parameter must be a boolean
      that specifies whether the function or lambda expression
      must return a single (i.e. non-@(tsee mv)) result or not.")
      (li "The @('stobjs') parameter must be a boolean
      that specifies whether the function or lambda expression
      can have input or output stobjs.")
      (li "The @('guard') parameter must be one of the following:
      (i) XDOC text that describes the condition under which
      the guards must be verified;
      (ii) @('t'), to indicate that the guards must always be verified;
      (iii) @('nil'), to indicate that there are no requirements
      on the guards being verified.
      The default is @('nil').")
      (li "The @('dont-be-or-call') parameter must be one of the following:
      (i) XDOC text that describes functions that
      the input (if a function) must differ from
      or that the input (if a lambda expression) must not reference;
      (ii) @('nil') (the default), to indicate no such requirements.")
      (li "The @('additional-function') parameter must be one of the following:
      (i) XDOC text that describes additional requirements
      for the function (typically a sentence);
      (ii) @('nil') (the default) for no additional text.")
      (li "The @('additional-lambda') parameter must be one of the following:
      (i) XDOC text that describes additional requirements
      for the lambda expression (typically a sentence);
      (ii) @('nil') (the default) for no additional text.")
      (li "The @('additional-forms') parameter must consist of
      XDOC list items that describe additional possible forms of the input,
      besides the function and lambda expression forms.
      For instance, an additional form could be a keyword @(':auto')
      to infer the function or lambda expression automatically.
      The default is the empty string, i.e. no additional forms."))
    (p "Looking at some uses of this utility should make it clearer.")
    (p "This utility may need to be extended and generalized in the future,
     in particular with more customization facilities."))
  `(&& (p ,SUBJECT " must be one of the following:")
    (ul (li "The name of a "
        ,(IF 1ARG
     "unary "
     "")
        "logic-mode function."
        ,(IF STOBJS
     ""
     '(XDOC::&& " This function must have no input or output "
       (XDOC::SEETOPIC "acl2::stobj" "stobjs") "."))
        ,(IF 1RES
     '(XDOC::&& " This function must return
              a single (i.e. non-"
       (XDOC::SEETOPIC "acl2::mv" "@('mv')") " result.")
     "")
        ,(COND ((EQ GUARD T) " This function must be guard-verified.")
       ((EQ GUARD NIL) "")
       (T
        `(XDOC::&& " If " ,GUARD
          ", then this function must be guard-verified.")))
        ,(IF DONT-BE-OR-CALL
     `(XDOC::&& " This function must be distinct from " ,DONT-BE-OR-CALL ".")
     "")
        ,(IF ADDITIONAL-FUNCTION
     `(XDOC::&& " " ,ADDITIONAL-FUNCTION)
     ""))
      (li "A "
        ,(IF 1ARG
     "unary "
     "")
        "closed lambda expression
       that only references logic-mode functions."
        ,(IF STOBJS
     ""
     '(XDOC::&& " This lambda expression must have no input or output "
       (XDOC::SEETOPIC "acl2::stobj" "stobjs") "."))
        ,(IF 1RES
     '(XDOC::&& " This lambda expression must return
              a single (i.e. non-"
       (XDOC::SEETOPIC "acl2::mv" "@('mv')") " result.")
     "")
        ,(COND
  ((EQ GUARD T)
   `(XDOC::&& " The body of this lambda expression
                 must only call guard-verified functions,
                 except possibly
                 in the @(':logic') subterms of "
     (XDOC::SEETOPIC "acl2::mbe" "@('mbe')") "s or via "
     (XDOC::SEETOPIC "acl2::ec-call" "@('ec-call')") "."))
  ((EQ GUARD NIL) "")
  (T
   `(XDOC::&& " If " ,GUARD ", then the body of this lambda expression
                   must only call guard-verified functions,
                   except possibly
                   in the @(':logic') subterms of "
     (XDOC::SEETOPIC "acl2::mbe" "@('mbe')") "s or via "
     (XDOC::SEETOPIC "acl2::ec-call" "@('ec-call')") ".")))
        " As an abbreviation, the name @('mac') of a macro stands for
       the lambda expression @('(lambda (z1 z2 ...) (mac z1 z2 ...))'),
       where @('z1'), @('z2'), ... are the required parameters of @('mac');
       that is, a macro name abbreviates its eta-expansion
       (considering only the macro's required parameters)."
        ,(IF DONT-BE-OR-CALL
     `(XDOC::&& " This lambda expression must not reference " ,DONT-BE-OR-CALL
       ".")
     "")
        ,(IF ADDITIONAL-LAMBDA
     `(XDOC::&& " " ,ADDITIONAL-LAMBDA)
     ""))
      ,ADDITIONAL-FORMS)))

(defmacro+ evmac-desc-term
  (&key (subject 'nil)
    (free-vars 'nil)
    (1res 'nil)
    (stobjs 'nil)
    (guard 'nil)
    (dont-call 'nil)
    (additional 'nil))
  :short "Construct a common description text for an input that must be a term."
  :long (topstring (p "This text expresses some common requirements
     on this kind of inputs to event macros.")
    (p "This utility provides some customization facilities:")
    (ul (li "The @('subject') parameter must be either @('nil')
      or XDOC text that describes
      the subject of the assertion of the requirements.
      The default is @('nil'), which means that there is no subject,
      and the description starts with "A term that...".
      If not @('nil'), the description starts with
      "<i>subject</i> must be a term...".")
      (li "The @('free-vars') parameter must be one of the following:
      (i) XDOC text that describes the allowed free variables in the term;
      (ii) @('nil') (the default) for no requirements on free variables.")
      (li "The @('1res') parameter must be a boolean
      that specifies whether the term
      must return a single (i.e. non-@(tsee mv)) value or not.")
      (li "The @('stobjs') parameter must be a boolean
      that specifies whether the term
      can have input or output stobjs.")
      (li "The @('guard') parameter must be one of the following:
      (i) XDOC text that describes the condition under which
      the guards must be verified;
      (ii) @('t'), to indicate that the guards must always be verified;
      (iii) @('nil'), to indicate that there are no requirements
      on the guards being verified.
      The default is @('nil').")
      (li "The @('dont-call') parameters must one of the following:
      (i) XDOC text that describes functions that this term must not call;
      (ii) @('nil') (the default),
      to indicate that the term may call any function.")
      (li "The @('additional') parameter must be one of the following:
      (i) XDOC text that describes additional requirements
      for the term (typically a sentence);
      (ii) @('nil') (the default) for no additional text."))
    (p "Looking at some uses of this utility should make it clearer.")
    (p "This utility may need to be extended and generalized in the future,
     in particular with more customization facilities."))
  `(&& ,@(IF SUBJECT
      (LIST SUBJECT " must be a")
      (LIST "A"))
    " term that only references logic-mode functions"
    ,(IF FREE-VARS
     `(XDOC::&& " and that includes no free variables other than " ,FREE-VARS)
     "")
    ,(IF STOBJS
     ""
     '(XDOC::&& ". This term must have no output "
       (XDOC::SEETOPIC "acl2::stobj" "stobjs") "."))
    ,(IF 1RES
     `(XDOC::&& " This term must return
            a single (i.e. non-"
       (XDOC::SEETOPIC "acl2::mv" "@('mv')") " value.")
     "")
    ,(COND
  ((EQ GUARD T)
   `(XDOC::&& " This term
               must only call guard-verified functions,
               except possibly
               in the @(':logic') subterms of "
     (XDOC::SEETOPIC "acl2::mbe" "@('mbe')") "s or via "
     (XDOC::SEETOPIC "acl2::ec-call" "@('ec-call')") "."))
  ((EQ GUARD NIL) "")
  (T
   `(XDOC::&& " If " ,GUARD ", then this term
                 must only call guard-verified functions,
                 except possibly
                 in the @(':logic') subterms of "
     (XDOC::SEETOPIC "acl2::mbe" "@('mbe')") "s or via "
     (XDOC::SEETOPIC "acl2::ec-call" "@('ec-call')") ".")))
    ,(IF DONT-CALL
     `(XDOC::&& " This term must not reference " ,DONT-CALL ".")
     "")
    ,(IF ADDITIONAL
     `(XDOC::&& " " ,ADDITIONAL)
     "")))

(defmacro+ evmac-appcond
  (name main &key design-notes design-notes-appcond presence)
  :short "Construct an applicability condition description
          in the user documentation of an event macro."
  :long (topstring (p "This generates an @(tsee xdoc::desc).")
    (p "The @('name') input must be a string
     that names the applicability condition.")
    (p "The @('main') input must be an XDOC tree
     that contains the main description of the applicability condition,
     consisting of explanatory natural language
     and formal code for the formula(s).")
    (p "The @('design-notes') and @('design-notes-appcond') inputs
     must be either both present or both absent.
     If present, they must be both XDOC trees:
     the first one references the design notes of the event macro
     (which usually includes a link to the design notes);
     the second one provides the name of the applicability condition
     (usually some mathematical notation) used in the design notes.
     If these two inputs are present,
     the generated XDOC includes text
     relating the applicability condition to the design notes.")
    (p "If the @('presence') input is present,
     it must be an XDOC tree.
     In this case,
     the generated XDOC includes text
     explaining that the applicability condition is present
     under the condition described by the @('presence') input."))
  (declare (xargs :guard (stringp name)))
  `(desc ,(CONCATENATE 'STRING "@('" NAME "')")
    ,MAIN
    ,@(AND DESIGN-NOTES DESIGN-NOTES-APPCOND
       `((XDOC::P "This corresponds to " ,DESIGN-NOTES-APPCOND " in the "
          ,DESIGN-NOTES ".")))
    ,@(AND PRESENCE
       `((XDOC::P "This applicability condition is present if and only if "
          ,PRESENCE ".")))))

(defsection evmac-topic-design-notes
  :short "Generate an XDOC topic for the design notes of an event macro."
  :long (topstring (p "This utility takes the following arguments:")
    (ul (li "The event macro's symbol.")
      (li "A string for the @('href') link with the actual notes,
      normally of the form @('res/.../<notes>.pdf'), based on the "
        (seetopic "xdoc::add-resource-directory"
          "XDOC resource directory")
        ".")
      (li "A list of additional parent topics, besides the macro itself.")
      (li "Zero or more XDOC trees (often just strings)
      to put into the bullets that explain the correspondence between
      the symbols in the design notes and the user documentation.
      If this list is empty,
      then no bulletted list is generated,
      and no introductory text for it.")
      (li "Zero or more XDOC trees (often paragraphs)
      that provide some additional explanation
      about how the design notes relate to the event macro
      (e.g. parts of the design notes that are not implemented yet."))
    (@def "xdoc::evmac-topic-design-notes"))
  (define evmac-topic-design-notes-make-bullets
    ((correspondences tree-listp))
    :returns (bullets tree-listp :hyp :guard)
    :parents nil
    (cond ((endp correspondences) nil)
      (t (cons (li (car correspondences))
          (evmac-topic-design-notes-make-bullets (cdr correspondences))))))
  (defmacro evmac-topic-design-notes
    (macro notes-ref
      &key
      additional-parents
      correspondences
      additional-doc)
    (declare (xargs :guard (and (symbolp macro)
          (stringp notes-ref)
          (symbol-listp additional-parents))))
    (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@(tsee " macro-name ")"))
        (this-topic (add-suffix macro "-DESIGN"))
        (parents (cons macro additional-parents))
        (short (concatenate 'string "Design notes for " macro-ref "."))
        (long `(topstring (p "The design of "
              ,MACRO-REF
              " is described in "
              (a :href ,NOTES-REF "these notes")
              ", which use "
              (a :href "res/kestrel-design-notes/notation.pdf"
                "this notation")
              ".")
            ,@(AND CORRESPONDENCES
       `((XDOC::P "The correspondence between
                            the design notes and the user documentation
                            is the following:")
         (XDOC::UL-FN NIL
          (XDOC::EVMAC-TOPIC-DESIGN-NOTES-MAKE-BULLETS
           (LIST ,@CORRESPONDENCES)))))
            ,@ADDITIONAL-DOC)))
      `(defxdoc ,THIS-TOPIC
        :parents ,PARENTS
        :short ,SHORT
        :long ,LONG))))

(defxdoc+ event-macro-xdoc-constructors-implementation-level
  :parents (event-macro-xdoc-constructors)
  :short "Utilities to construct <see topic='@(url xdoc)'>XDOC</see> strings
          to document the implementation of
          <see topic='@(url event-macros)'>event macros</see>."
  :default-parent t)

(defsection evmac-topic-implementation
  :short "Generate an XDOC topic for the implementation of an event macro."
  :long (topstring (p "The topic lists the names used for arguments and results of functions,
     along with brief descriptions of the names.
     This listing consists of bullets in an unordered list.
     The @(':items') argument must be a list of XDOC trees,
     each of which is wrapped into an @(tsee xdoc::li),
     and the so-wrapped items are put into an @(tsee xdoc::ul).")
    (p "We also provide some named constants for certain common items,
     like the @('state') variable.
     We also provide some functions for certain common kinds of items,
     like the user inputs to the event macro.")
    (p "If there are no items, the list is omitted altogether.")
    (p "This macro also provides a @(':default-parent') option,
     which is @('nil') by default and is passed to @(tsee defxdoc+).")
    (p "This macro also provides a @(':additional') option,
     which must be a list of XDOC trees (@('nil') by default),
     which is added at the end of the @(tsee defxdoc+),
     to provide additional information about
     the implementation being documented.")
    (@def "xdoc::evmac-topic-implementation"))
  (define evmac-topic-implementation-li-wrap
    ((items true-listp))
    :parents nil
    :returns (li-wrapped-items true-listp)
    (cond ((endp items) nil)
      (t (cons `(li ,(CAR ITEMS))
          (evmac-topic-implementation-li-wrap (cdr items))))))
  (defmacro evmac-topic-implementation
    (macro &key items default-parent additional)
    (declare (xargs :guard (symbolp macro)))
    (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@(tsee " macro-name ")"))
        (this-topic (add-suffix macro "-IMPLEMENTATION"))
        (parent-topic macro)
        (short (concatenate 'string "Implementation of " macro-ref "."))
        (long (and (or items additional)
            `(topstring (p "The implementation functions have arguments and results
                        consistently named as follows
                        (unless otherwise stated, explicitly or implicitly,
                        in the functions):")
              (ul ,@(XDOC::EVMAC-TOPIC-IMPLEMENTATION-LI-WRAP ITEMS))
              (p "Implementation functions' arguments and results
                        that are not listed above
                        are described in, or clear from,
                        those functions' documentation.")
              ,@ADDITIONAL))))
      `(defxdoc+ ,THIS-TOPIC
        :parents (,PARENT-TOPIC)
        :short ,SHORT
        ,@(AND LONG (LIST :LONG LONG))
        :order-subtopics t
        :default-parent ,DEFAULT-PARENT)))
  (defconst *evmac-topic-implementation-item-state*
    (&& "@('state') is the ACL2 "
      (seetopic "acl2::state" "state")
      "."))
  (defconst *evmac-topic-implementation-item-wrld*
    (&& "@('wrld') is the ACL2 "
      (seetopic "acl2::world" "world")
      "."))
  (defconst *evmac-topic-implementation-item-ctx*
    (&& "@('ctx') is the "
      (seetopic "ctx" "context")
      " used for errors."))
  (defconst *evmac-topic-implementation-item-call*
    "@('call') is the call of the event macro.")
  (defconst *evmac-topic-implementation-item-names-to-avoid*
    "@('names-to-avoid') is a cumulative list of names of generated events,
     used to ensure the absence of name clashes in the generated events.")
  (defconst *evmac-topic-implementation-item-appcond-thm-names*
    "@('appcond-thm-names') is an alist
     from the keywords that identify the applicability conditions
     to the corresponding generated theorem names.")
  (define evmac-topic-implementation-item-input
    ((name stringp))
    :parents nil
    (&& "@('"
      name
      "') is the homonymous input to the event macro."))
  (define evmac-topic-implementation-item-input-untyped/typed
    ((name stringp))
    :parents nil
    (&& "@('"
      name
      "') is the homonymous input to the event macro
               if it has no type;
               otherwise, it is the (possibly different) typed value
               resulting from processing that input."))
  (define evmac-topic-implementation-item-fn-doc
    ((name stringp))
    :parents nil
    (&& "@('"
      name
      "') is the homonymous function symbol "
      "described in the user documentation."))
  (define evmac-topic-implementation-item-thm-doc
    ((name stringp))
    :parents nil
    (&& "@('"
      name
      "') is the homonymous theorem symbol "
      "described in the user documentation."))
  (define evmac-topic-implementation-item-var-doc
    ((name stringp))
    :parents nil
    (&& "@('"
      name
      "') is the homonymous variable symbol "
      "described in the user documentation.")))

(defmacro+ evmac-topic-library-extensions
  (macro)
  :short "Generate an XDOC topic for the library extensions
          that are part of the implementation of an event macro."
  (declare (xargs :guard (symbolp macro)))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@(tsee " macro-name ")"))
      (this-topic (add-suffix macro "-LIBRARY-EXTENSIONS"))
      (parent-topic (add-suffix macro "-IMPLEMENTATION"))
      (short (concatenate 'string
          "Library extensions for "
          macro-ref
          "."))
      (long (topstring-p "These are used by, but more general than, "
          macro-ref
          ". Thus, they should be moved
                 to more general libraries eventually.")))
    `(defxdoc+ ,THIS-TOPIC
      :parents (,PARENT-TOPIC)
      :short ,SHORT
      :long ,LONG
      :order-subtopics t
      :default-parent t)))

(defmacro+ evmac-topic-input-processing
  (macro &rest additional)
  :short "Generate an XDOC topic for the input processing
          that is part of the implementation of an event macro."
  :long (topstring-p "This macro accepts additional pieces of XDOC text,
    which are added at the end of the generated @(':long').")
  (declare (xargs :guard (symbolp macro)))
  (b* ((macro-name (string-downcase (symbol-name macro))) (macro-ref (concatenate 'string "@(tsee " macro-name ")"))
      (this-topic (add-suffix macro "-INPUT-PROCESSING"))
      (parent-topic (add-suffix macro "-IMPLEMENTATION"))
      (short (concatenate 'string
          "Input processing performed by "
          macro-ref
          "."))
      (long `(topstring (p "See "
            (seetopic "acl2::event-macro-input-processing"
              "input processing")
            " for general background.")
          ,@ADDITIONAL)))
    `(defxdoc+ ,THIS-TOPIC
      :parents (,PARENT-TOPIC)
      :short ,SHORT
      :long ,LONG
      :order-subtopics t
      :default-parent t)))

(defmacro+ evmac-topic-event-generation
  (macro &key
    some-local-p
    some-local-nonlocal-p
    some-nonlocal-p)
  :short "Generate an XDOC topic for the event generation
          that is part of the implementation of an event macro."
  :long (topstring-p "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').")
  (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
          '((p "Some events are generated in two slightly different variants:
                 one that is local to the generated "
             (seetopic "acl2::encapsulate" "@('encapsulate')")
             ", and one that is exported from the "
             (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 "
             (seetopic "acl2::encapsulate" "@('encapsulate')")
             "."))))
      (para-local? (and some-local-p
          '((p "Some events are generated only locally to the generated "
             (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
          '((p "Some events are generated only non-locally to the generated "
             (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)
          `(topstring ,@PARA-LOCAL-NONLOCAL?
            ,@PARA-LOCAL?
            ,@PARA-NONLOCAL?))))
    `(defxdoc+ ,THIS-TOPIC
      :parents (,PARENT-TOPIC)
      :short ,SHORT
      ,@(AND LONG? (LIST :LONG LONG?))
      :order-subtopics t
      :default-parent t)))