		Search-engine friendly clone of the ACL2 documentation.

Deftutorial-implementation

Deftutorial-gen-defpage

Generate the macro to define a (non-top) page of the tutorial.

Signature
(deftutorial-gen-defpage tut-name) → events
Arguments: tut-name — Guard (symbolp tut-name).
Returns: events — Type (pseudo-event-form-listp events).

The generated macro stores information about these pages into the table. The information consists of a pair in the table, whose key is the keyword :pages and whose value is a list of (information about) pages, in reverse order of introduction (i.e. new pages are consed). Each element of the list is a list (name title text1 text2 ...) obtained from the arguments of the macro.

Definitions and Theorems

Function: deftutorial-gen-defpage

(defun deftutorial-gen-defpage (tut-name)
 (declare (xargs :guard (symbolp tut-name)))
 (let ((__function__ 'deftutorial-gen-defpage))
  (declare (ignorable __function__))
  (b* ((defpage (packn-pos (list 'def- tut-name '-page)
                           tut-name))
       (defpage-fn (add-suffix defpage "-FN"))
       (tut-table (add-suffix tut-name "-TABLE")))
   (cons
    (cons
     'defun
     (cons
      defpage-fn
      (cons
       '(page-name page-title page-text wrld)
       (cons
        (cons
         'b*
         (cons
          (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
            (cons
             'page-name
             (cons
              (cons
                'packn-pos
                (cons (cons 'list
                            (cons (cons 'quote (cons tut-name 'nil))
                                  '('- page-name)))
                      (cons (cons 'quote (cons tut-name 'nil))
                            'nil)))
              'nil))
            '((page (list* page-name page-title page-text))
              (new-pages (cons page pages)))))
          (cons
           (cons
            'cons
            (cons
             ''table
             (cons
              (cons
               'cons
               (cons
                   (cons 'quote (cons tut-table 'nil))
                   '((cons ':pages
                           (cons (cons 'quote (cons new-pages 'nil))
                                 'nil)))))
              'nil)))
           'nil)))
        'nil))))
    (cons
     (cons
      'defmacro
      (cons
       defpage
       (cons
        '(page-name page-title &rest page-text)
        (cons
         (cons
          'cons
          (cons
           ''make-event
           (cons
            (cons
             'cons
             (cons
              (cons
               'cons
               (cons
                (cons 'quote (cons defpage-fn 'nil))
                '((cons
                     (cons 'quote (cons page-name 'nil))
                     (cons (cons 'quote (cons page-title 'nil))
                           (cons (cons 'quote (cons page-text 'nil))
                                 '((w state))))))))
              '('nil)))
            'nil)))
         'nil))))
     'nil)))))

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

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