		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-topic-design-notes

Generate an XDOC topic for the design notes of an event macro.

This utility takes the following arguments:

The event macro's symbol.
A string for the href link with the actual notes, normally of the form res/.../<notes>.pdf, based on the XDOC resource directory.
A list of additional parent topics, besides the macro itself.
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.
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.

Macro: evmac-topic-design-notes

(defmacro xdoc::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
    (cons
     'xdoc::topstring
     (cons
      (cons
       'xdoc::p
       (cons
        '"The design of "
        (cons
         macro-ref
         (cons
          '" is described in "
          (cons
              (cons 'xdoc::a
                    (cons ':href
                          (cons notes-ref '("these notes"))))
              '(", which use "
                    (xdoc::a :href
                             "res/kestrel-design-notes/notation.pdf"
                             "this notation")
                    "."))))))
      (append
       (and
        correspondences
        (cons
         '(xdoc::p
           "The correspondence between
                            the design notes and the user documentation
                            is the following:")
         (cons
          (cons
           'xdoc::ul-fn
           (cons
            'nil
            (cons (cons 'xdoc::evmac-topic-design-notes-make-bullets
                        (cons (cons 'list correspondences)
                              'nil))
                  'nil)))
          'nil)))
       additional-doc)))))
  (cons
   'defxdoc
   (cons
      this-topic
      (cons ':parents
            (cons parents
                  (cons ':short
                        (cons short
                              (cons ':long (cons long 'nil))))))))))

Definitions and Theorems

Function: evmac-topic-design-notes-make-bullets

(defun xdoc::evmac-topic-design-notes-make-bullets (correspondences)
  (declare (xargs :guard (xdoc::tree-listp correspondences)))
  (let ((__function__ 'xdoc::evmac-topic-design-notes-make-bullets))
    (declare (ignorable __function__))
    (cond ((endp correspondences) nil)
          (t (cons (xdoc::li (car correspondences))
                   (xdoc::evmac-topic-design-notes-make-bullets
                        (cdr correspondences)))))))

Theorem: tree-listp-of-evmac-topic-design-notes-make-bullets

(defthm xdoc::tree-listp-of-evmac-topic-design-notes-make-bullets
 (implies
  (and (xdoc::tree-listp correspondences))
  (b*
   ((bullets
     (xdoc::evmac-topic-design-notes-make-bullets correspondences)))
   (xdoc::tree-listp bullets)))
 :rule-classes :rewrite)