		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-implementation-level

Xdoc::evmac-topic-implementation

Generate an XDOC topic for the implementation of an event macro.

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 xdoc::li, and the so-wrapped items are put into an xdoc::ul.

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.

If there are no items, the list is omitted altogether.

This macro also provides a :default-parent option, which is nil by default and is passed to defxdoc+.

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 defxdoc+, to provide additional information about the implementation being documented.

Macro: evmac-topic-implementation

(defmacro xdoc::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)
     (cons
      'xdoc::topstring
      (cons
       '(xdoc::p
         "The implementation functions have arguments and results
                        consistently named as follows
                        (unless otherwise stated, explicitly or implicitly,
                        in the functions):")
       (cons
        (cons 'xdoc::ul
              (xdoc::evmac-topic-implementation-li-wrap items))
        (cons
         '(xdoc::p
           "Implementation functions' arguments and results
                        that are not listed above
                        are described in, or clear from,
                        those functions' documentation.")
         additional)))))))
  (cons
   'defxdoc+
   (cons
    this-topic
    (cons
     ':parents
     (cons
      (cons parent-topic 'nil)
      (cons
       ':short
       (cons
        short
        (append
            (and long (list :long long))
            (cons ':order-subtopics
                  (cons 't
                        (cons ':default-parent
                              (cons default-parent 'nil)))))))))))))

Definitions and Theorems

Function: evmac-topic-implementation-li-wrap

(defun xdoc::evmac-topic-implementation-li-wrap (items)
 (declare (xargs :guard (true-listp items)))
 (let ((__function__ 'xdoc::evmac-topic-implementation-li-wrap))
  (declare (ignorable __function__))
  (cond
   ((endp items) nil)
   (t
    (cons
         (cons 'xdoc::li (cons (car items) 'nil))
         (xdoc::evmac-topic-implementation-li-wrap (cdr items)))))))

Theorem: true-listp-of-evmac-topic-implementation-li-wrap

(defthm xdoc::true-listp-of-evmac-topic-implementation-li-wrap
  (b* ((li-wrapped-items
            (xdoc::evmac-topic-implementation-li-wrap items)))
    (true-listp li-wrapped-items))
  :rule-classes :rewrite)

Function: evmac-topic-implementation-item-input

(defun xdoc::evmac-topic-implementation-item-input (name)
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'xdoc::evmac-topic-implementation-item-input))
    (declare (ignorable __function__))
    (xdoc::&& "@('" name
              "') is the homonymous input to the event macro.")))

Function: evmac-topic-implementation-item-input-untyped/typed

(defun xdoc::evmac-topic-implementation-item-input-untyped/typed
       (name)
 (declare (xargs :guard (stringp name)))
 (let
  ((__function__
        'xdoc::evmac-topic-implementation-item-input-untyped/typed))
  (declare (ignorable __function__))
  (xdoc::&&
   "@('" 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.")))

Function: evmac-topic-implementation-item-fn-doc

(defun xdoc::evmac-topic-implementation-item-fn-doc (name)
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'xdoc::evmac-topic-implementation-item-fn-doc))
   (declare (ignorable __function__))
   (xdoc::&& "@('" name
             "') is the homonymous function symbol "
             "described in the user documentation.")))

Function: evmac-topic-implementation-item-thm-doc

(defun xdoc::evmac-topic-implementation-item-thm-doc (name)
  (declare (xargs :guard (stringp name)))
  (let
     ((__function__ 'xdoc::evmac-topic-implementation-item-thm-doc))
    (declare (ignorable __function__))
    (xdoc::&& "@('" name
              "') is the homonymous theorem symbol "
              "described in the user documentation.")))

Function: evmac-topic-implementation-item-var-doc

(defun xdoc::evmac-topic-implementation-item-var-doc (name)
  (declare (xargs :guard (stringp name)))
  (let
     ((__function__ 'xdoc::evmac-topic-implementation-item-var-doc))
    (declare (ignorable __function__))
    (xdoc::&& "@('" name
              "') is the homonymous variable symbol "
              "described in the user documentation.")))