deftutorial

(in-package "ACL2")

(evmac-topic-implementation deftutorial
  :default-parent t)

(define deftutorial-gen-deftop
  ((tut-name symbolp))
  :returns (events pseudo-event-form-listp)
  :short "Generate the macro to define the top page of the tutorial."
  :long (topstring-p "The generated macro stores information about the top page into the table.
    The information consists of a pair in the table,
    whose key is the keyword @(':top')
    and whose value is a list @('(parents text1 text2 ...)')
    obtained from the arguments of the macro.")
  (b* ((deftop (packn-pos (list 'def- tut-name '-top) tut-name)) (deftop-fn (add-suffix deftop "-FN"))
      (tut-table (add-suffix tut-name "-TABLE")))
    `((defun ,DEFTOP-FN
       (top-parents top-text)
       (b* ((top (cons top-parents top-text)))
         `(table ,',TUT-TABLE :top ',TOP))) (defmacro ,DEFTOP
        (top-parents &rest top-text)
        `(make-event (,',DEFTOP-FN ',TOP-PARENTS ',TOP-TEXT))))))

(define deftutorial-gen-defpage
  ((tut-name symbolp))
  :returns (events pseudo-event-form-listp)
  :short "Generate the macro to define a (non-top) page of the tutorial."
  :long (topstring-p "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 @(tsee cons)ed).
    Each element of the list is a list @('(name title text1 text2 ...)')
    obtained from the arguments of the macro.")
  (b* ((defpage (packn-pos (list 'def- tut-name '-page) tut-name)) (defpage-fn (add-suffix defpage "-FN"))
      (tut-table (add-suffix tut-name "-TABLE")))
    `((defun ,DEFPAGE-FN
       (page-name page-title page-text wrld)
       (b* ((pages (cdr (assoc-eq :pages (table-alist ',TUT-TABLE wrld)))) (page-name (packn-pos (list ',TUT-NAME '- page-name) ',TUT-NAME))
           (page (list* page-name page-title page-text))
           (new-pages (cons page pages)))
         `(table ,',TUT-TABLE :pages ',NEW-PAGES))) (defmacro ,DEFPAGE
        (page-name page-title &rest page-text)
        `(make-event (,',DEFPAGE-FN ',PAGE-NAME
            ',PAGE-TITLE
            ',PAGE-TEXT
            (w state)))))))

(define deftutorial-gen-deftopics
  ((tut-name symbolp) (tut-title stringp))
  :returns (events pseudo-event-form-listp)
  :short "Generate the macro to define the XDOC topics of the tutorial."
  :long (topstring-p "The generated macro retrieves from the table
    the information about top and non-top pages,
    and creates @(tsee 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.")
  (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")))
    `((defun ,DEFTOPICS-LOOP
       (pages previous-name previous-title)
       (b* (((when (endp pages)) nil) (page (car pages))
           (page-name (car page))
           (page-title (cadr page))
           (page-text (cddr page))
           (previous-link? (and previous-name
               `(p "<b>Previous:</b> "
                 (seetopic ,(SYMBOL-NAME PREVIOUS-NAME)
                   ,PREVIOUS-TITLE))))
           ((mv next-name next-title) (if (consp (cdr pages))
               (mv (car (cadr pages)) (cadr (cadr pages)))
               (mv nil nil)))
           (next-link? (and (consp (cdr pages))
               `(p "<b>Next:</b> "
                 (seetopic ,(SYMBOL-NAME NEXT-NAME) ,NEXT-TITLE))))
           (topic `(defxdoc ,PAGE-NAME
               :parents (,',TUT-NAME)
               :short ,(CONCATENATE 'STRING ,TUT-TITLE ": " PAGE-TITLE ".")
               :long (topstring ,@PAGE-TEXT
                 (box)
                 ,@(AND PREVIOUS-LINK? (LIST PREVIOUS-LINK?))
                 ,@(AND NEXT-LINK? (LIST NEXT-LINK?)))))
           (topics (,DEFTOPICS-LOOP (cdr pages) page-name page-title)))
         (cons topic topics))) (defun ,DEFTOPICS-FN
        (wrld)
        (b* ((top (cdr (assoc-eq :top (table-alist ',TUT-TABLE wrld)))) (pages (cdr (assoc-eq :pages (table-alist ',TUT-TABLE wrld))))
            (pages (reverse pages))
            (top-parents (car top))
            (top-text (cdr top))
            (start-link? (and (consp pages)
                `(p "<b>Start:</b> "
                  (seetopic ,(SYMBOL-NAME (CAR (CAR PAGES)))
                    ,(CADR (CAR PAGES))))))
            (top-topic `(defxdoc ,',TUT-NAME
                :parents ,TOP-PARENTS
                :short ,(CONCATENATE 'STRING ,TUT-TITLE ".")
                :long (topstring ,@TOP-TEXT
                  (box)
                  ,@(AND START-LINK? (LIST START-LINK?)))))
            (topics (,DEFTOPICS-LOOP pages nil nil)))
          `(progn ,TOP-TOPIC ,@TOPICS)))
      (defmacro ,DEFTOPICS
        nil
        `(make-event (,',DEFTOPICS-FN (w state)))))))

(define deftutorial-gen-section
  ((tut-name symbolp))
  :returns (event pseudo-event-formp)
  :short "Generate the macro to define a section in a tutorial page."
  :long (topstring-p "We use a level-5 heading to keep it relatively small.")
  (b* ((tut-section (add-suffix tut-name "-SECTION")))
    `(defmacro ,TUT-SECTION (title) `(h5 ,TITLE))))

(define deftutorial-fn
  ((tut-name symbolp) (tut-title stringp))
  :returns (event pseudo-event-formp)
  :short "Generate all the macros to build the tutorial."
  `(progn ,@(DEFTUTORIAL-GEN-DEFTOP TUT-NAME)
    ,@(DEFTUTORIAL-GEN-DEFPAGE TUT-NAME)
    ,@(DEFTUTORIAL-GEN-DEFTOPICS TUT-NAME TUT-TITLE)
    ,(DEFTUTORIAL-GEN-SECTION TUT-NAME)))

(defsection deftutorial-definition
  :short "Definition of the @(tsee deftutorial) macro."
  (defmacro deftutorial
    (tut-name tut-title)
    (declare (xargs :guard (and (symbolp tut-name) (stringp tut-title))))
    `(make-event (deftutorial-fn ',TUT-NAME ,TUT-TITLE))))