• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Define-sk
      • Defines
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
        • Deftutorial-implementation
          • Deftutorial-gen-deftopics
          • Deftutorial-gen-defpage
          • Deftutorial-gen-deftop
          • Deftutorial-gen-section
          • Deftutorial-fn
          • Deftutorial-definition
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Support
      • Defthm-signed-byte-p
      • Defthm-unsigned-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deftutorial-implementation

Deftutorial-gen-deftopics

Generate the macro to define the XDOC topics of the tutorial.

Signature

(deftutorial-gen-deftopics tut-name tut-title) → events

Arguments

tut-name — Guard (symbolp tut-name).

tut-title — Guard (stringp tut-title).

Returns

events — Type (pseudo-event-form-listp events).

The generated macro retrieves from the table the information about top and non-top pages, and creates defxdoc forms for each of them. The (non-top) pages are reversed, so they are in the order of introduction (this is not necessary, but this way we keep the ACL2 history more consistent). We extend the long string of each page with the appropriate links to other pages; we use empty boxes to create a line of separation just before those links.

Definitions and Theorems

Function: deftutorial-gen-deftopics

(defun deftutorial-gen-deftopics (tut-name tut-title)
 (declare (xargs :guard (and (symbolp tut-name)
                             (stringp tut-title))))
 (let ((__function__ 'deftutorial-gen-deftopics))
  (declare (ignorable __function__))
  (b* ((deftopics (packn-pos (list 'def- tut-name '-topics)
                             tut-name))
       (deftopics-fn (add-suffix deftopics "-FN"))
       (deftopics-loop (add-suffix deftopics "-LOOP"))
       (tut-table (add-suffix tut-name "-TABLE")))
   (cons
    (cons
     'defun
     (cons
      deftopics-loop
      (cons
       '(pages previous-name previous-title)
       (cons
        (cons
         'b*
         (cons
          (cons
           '((when (endp pages)) nil)
           (cons
            '(page (car pages))
            (cons
             '(page-name (car page))
             (cons
              '(page-title (cadr page))
              (cons
               '(page-text (cddr page))
               (cons
                '(previous-link?
                  (and
                   previous-name
                   (cons
                    'xdoc::p
                    (cons
                      '"<b>Previous:</b> "
                      (cons (cons 'xdoc::seetopic
                                  (cons (symbol-name previous-name)
                                        (cons previous-title 'nil)))
                            'nil)))))
                (cons
                 '((mv next-name next-title)
                   (if (consp (cdr pages))
                       (mv (car (cadr pages))
                           (cadr (cadr pages)))
                     (mv nil nil)))
                 (cons
                  '(next-link?
                    (and
                     (consp (cdr pages))
                     (cons
                      'xdoc::p
                      (cons
                          '"<b>Next:</b> "
                          (cons (cons 'xdoc::seetopic
                                      (cons (symbol-name next-name)
                                            (cons next-title 'nil)))
                                'nil)))))
                  (cons
                   (cons
                    'topic
                    (cons
                     (cons
                      'cons
                      (cons
                       ''defxdoc
                       (cons
                        (cons
                         'cons
                         (cons
                          'page-name
                          (cons
                           (cons
                            'cons
                            (cons
                             '':parents
                             (cons
                              (cons
                               'cons
                               (cons
                                (cons
                                 'cons
                                 (cons
                                  (cons 'quote (cons tut-name 'nil))
                                  '('nil)))
                                (cons
                                 (cons
                                  'cons
                                  (cons
                                   '':short
                                   (cons
                                    (cons
                                     'cons
                                     (cons
                                      (cons
                                       'concatenate
                                       (cons
                                        ''string
                                        (cons
                                           tut-title
                                           '(": " page-title "."))))
                                      '((cons
                                         ':long
                                         (cons
                                          (cons
                                           'xdoc::topstring
                                           (append
                                            page-text
                                            (cons
                                             '(xdoc::box)
                                             (append
                                              (and
                                               previous-link?
                                               (list
                                                    previous-link?))
                                              (and
                                               next-link?
                                               (list
                                                    next-link?))))))
                                          'nil)))))
                                    'nil)))
                                 'nil)))
                              'nil)))
                           'nil)))
                        'nil)))
                     'nil))
                   (cons
                    (cons
                     'topics
                     (cons
                          (cons deftopics-loop
                                '((cdr pages) page-name page-title))
                          'nil))
                    'nil))))))))))
          '((cons topic topics))))
        'nil))))
    (cons
     (cons
      'defun
      (cons
       deftopics-fn
       (cons
        '(wrld)
        (cons
         (cons
          'b*
          (cons
           (cons
            (cons
             'top
             (cons
              (cons
               'cdr
               (cons
                (cons
                 'assoc-eq
                 (cons
                  ':top
                  (cons
                     (cons 'table-alist
                           (cons (cons 'quote (cons tut-table 'nil))
                                 '(wrld)))
                     'nil)))
                'nil))
              'nil))
            (cons
             (cons
              'pages
              (cons
               (cons
                'cdr
                (cons
                 (cons
                  'assoc-eq
                  (cons
                   ':pages
                   (cons
                     (cons 'table-alist
                           (cons (cons 'quote (cons tut-table 'nil))
                                 '(wrld)))
                     'nil)))
                 'nil))
               'nil))
             (cons
              '(pages (reverse pages))
              (cons
               '(top-parents (car top))
               (cons
                '(top-text (cdr top))
                (cons
                 '(start-link?
                   (and
                    (consp pages)
                    (cons
                     'xdoc::p
                     (cons
                      '"<b>Start:</b> "
                      (cons
                        (cons 'xdoc::seetopic
                              (cons (symbol-name (car (car pages)))
                                    (cons (cadr (car pages)) 'nil)))
                        'nil)))))
                 (cons
                  (cons
                   'top-topic
                   (cons
                    (cons
                     'cons
                     (cons
                      ''defxdoc
                      (cons
                       (cons
                        'cons
                        (cons
                         (cons 'quote (cons tut-name 'nil))
                         (cons
                          (cons
                           'cons
                           (cons
                            '':parents
                            (cons
                             (cons
                              'cons
                              (cons
                               'top-parents
                               (cons
                                (cons
                                 'cons
                                 (cons
                                  '':short
                                  (cons
                                   (cons
                                    'cons
                                    (cons
                                     (cons
                                      'concatenate
                                      (cons
                                           ''string
                                           (cons tut-title '("."))))
                                     '((cons
                                        ':long
                                        (cons
                                         (cons
                                          'xdoc::topstring
                                          (append
                                           top-text
                                           (cons
                                            '(xdoc::box)
                                            (and
                                              start-link?
                                              (list start-link?)))))
                                         'nil)))))
                                   'nil)))
                                'nil)))
                             'nil)))
                          'nil)))
                       'nil)))
                    'nil))
                  (cons
                   (cons
                        'topics
                        (cons (cons deftopics-loop '(pages nil nil))
                              'nil))
                   'nil))))))))
           '((cons 'progn (cons top-topic topics)))))
         'nil))))
     (cons
      (cons
       'defmacro
       (cons
        deftopics
        (cons
         'nil
         (cons
          (cons
           'cons
           (cons
            ''make-event
            (cons
             (cons
              'cons
              (cons
                  (cons 'cons
                        (cons (cons 'quote (cons deftopics-fn 'nil))
                              '('((w state)))))
                  '('nil)))
             'nil)))
          'nil))))
      'nil))))))

Theorem: pseudo-event-form-listp-of-deftutorial-gen-deftopics

(defthm pseudo-event-form-listp-of-deftutorial-gen-deftopics
  (b* ((events (deftutorial-gen-deftopics tut-name tut-title)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)