; XDOC Documentation System for ACL2
; Copyright (C) 2009-2016 Centaur Technology
;
; Contact:
;   Centaur Technology Formal Verification Group
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
;   http://www.centtech.com/
;
; License: (An MIT/X11-style license)
;
;   Permission is hereby granted, free of charge, to any person obtaining a
;   copy of this software and associated documentation files (the "Software"),
;   to deal in the Software without restriction, including without limitation
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
;   and/or sell copies of the Software, and to permit persons to whom the
;   Software is furnished to do so, subject to the following conditions:
;
;   The above copyright notice and this permission notice shall be included in
;   all copies or substantial portions of the Software.
;
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
;   DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <jared@centtech.com> (but see next comment)

; This book was created by Matt Kaufmann to define function save-rendered,
; essentially using code that was formerly in community book
; books/doc/top.lisp, with original author Jared Davis.

(in-package "XDOC")

(include-book "defxdoc-raw")
(include-book "save")
(include-book "system/doc/render-doc-base" :dir :system)
(include-book "alter")
(include-book "xdoc-error")

(set-state-ok t)
(program)

(defttag :open-output-channel!)

(defconst *acl2-doc-search-separator* "###---###---###---###---###")

; Here is old code that has been replaced so as to speed up printing; see a
; comment about fms! in acl2-doc-print-topic-index below.
#||
(defun acl2-doc-fix-symbol-msg (sym)
  (cond ((eq (intern$ (symbol-name sym) "ACL2") sym)
         (msg "~s0" (symbol-name sym)))
        (t (msg "~s0::~s1" (symbol-package-name sym) (symbol-name sym)))))

(defun acl2-doc-fix-symbol-lst-msg (lst)
  (cond ((endp lst) "")
        ((endp (cdr lst))
         (acl2-doc-fix-symbol-msg (car lst)))
        (t (msg "~@0 ~@1"
                (acl2-doc-fix-symbol-msg (car lst))
                (acl2-doc-fix-symbol-lst-msg (cdr lst))))))
||#

(defun acl2-doc-print-fix-symbol (sym channel state)
  (cond ((eq (intern$ (symbol-name sym) "ACL2") sym)
         (princ$ (symbol-name sym) channel state))
        (t (pprogn (princ$ (symbol-package-name sym) channel state)
                   (princ$ "::" channel state)
                   (princ$ (symbol-name sym) channel state)))))

(defun acl2-doc-print-fix-symbol-lst (lst channel state)
  (cond ((endp lst) state)
        ((endp (cdr lst))
         (acl2-doc-print-fix-symbol (car lst) channel state))
        (t (pprogn 
            (acl2-doc-print-fix-symbol (car lst) channel state)
            (princ$ " " channel state)
            (acl2-doc-print-fix-symbol-lst (cdr lst) channel state)))))

(defun remove-sgr-1 (s i len acc)
  (let ((p (search *sgr-prefix* s :start2 i)))
    (cond
     (p (let ((p2 (search "m" s :start2 (+ 2 p))))
          (assert$
           p2
           (remove-sgr-1 s (1+ p2) len
                         (concatenate 'string
                                      acc
                                      (subseq s i p))))))
     (t (concatenate 'string acc (subseq s i len))))))

(defun remove-sgr (s)

; The acl2-doc search file, acl2-doc-search, needs to avoid having any SGR
; control sequences, so that searches there can match up with searches in the
; acl2-doc buffer, where those markings have been removed.  See comments in the
; definition of sgr-prefix in display.lisp for more on SGR.

  (let ((p (search *sgr-prefix* s :start2 0)))
    (cond ((null p)
           s)
          (t (remove-sgr-1 s p (length s) (subseq s 0 p))))))

(defun acl2-doc-print-topic-index (tuple channel state)

; Warning: Do not set the buffer to read-only here, because this
; function may be called repeatedly for the same buffer, e.g., by
; function acl2-doc-search-buffer.

; The fms! call that is commented out just below is equivalent to the code
; below it, but is much slower.  Replacing that fms! call reduced the time for
; acl2-doc-print-topic-index-lst under save-rendered, when building the full
; ACL2+books manual 7/18/2021, from 52.50 seconds to 2.74 seconds.

; (fms! "~s0~|Topic: ~@1~|Parent list: (~@2)~|~@3~%~s4~|"
;       (list (cons #\0 *acl2-doc-search-separator*)
;             (cons #\1 (acl2-doc-fix-symbol-msg (nth 0 tuple)))
;             (cons #\2 (acl2-doc-fix-symbol-lst-msg (nth 1 tuple)))
;             (cons #\3 (if (equal (length tuple) 4)
;                           (if (eq (nth 0 tuple) 'TOP)
;                               ""
;                             (msg ":DOC source: ~s0~|" (nth 3 tuple)))
;                         ":DOC source: ACL2 Sources~|"))
;             (cons #\4 (nth 2 tuple)))
;       channel state nil)

  (pprogn (newline channel state)
          (princ$ *acl2-doc-search-separator* channel state)
          (newline channel state)
          (princ$ "Topic: " channel state)
          (acl2-doc-print-fix-symbol (nth 0 tuple) channel state)
          (newline channel state)
          (princ$ "Parent list: (" channel state)
          (acl2-doc-print-fix-symbol-lst (nth 1 tuple) channel state)
          (princ$ ")" channel state)
          (newline channel state)
          (if (equal (length tuple) 4)
              (if (eq (nth 0 tuple) 'TOP)
                  state
                (pprogn (princ$ ":DOC source: " channel state)
                        (princ$ (remove-sgr (nth 3 tuple)) channel state)
                        (newline channel state)))
            (pprogn (princ$ ":DOC source: ACL2 Sources" channel state)
                    (newline channel state)))
          (princ$ (remove-sgr (nth 2 tuple)) channel state)
          (newline channel state)))

(defun acl2-doc-print-topic-index-lst (tuple-lst channel state)
  (cond ((endp tuple-lst) state)
        (t (pprogn
            (acl2-doc-print-topic-index (car tuple-lst) channel state)
            (acl2-doc-print-topic-index-lst (cdr tuple-lst) channel state)))))

(defmacro with-acl2-doc-images (form)

; Form evaluates to (mv val state) and we return (value val), except that form
; is evaluated in an environment where documentation will be printed to be
; rendered with images.  We restore the original environment even in the case
; of an error.

; Form should not contain with wadi- variable bound by b* below.  We should
; really use something like check-vars-not-free, but this will do.  ("Wadi" is
; based on the name of this macro.)

  `(b* (((mv - wadi-env-val state)
         (getenv$ "ACL2_DOC_IMAGES" state))
        ((mv - wadi-temp state)
         (acl2::acl2-unwind-protect
          "with-acl2-doc-images"
          (prog2$ (setenv$ "ACL2_DOC_IMAGES" "t")
                  (mv-let (wadi-temp state)
                    ,form
                    (value wadi-temp)))
          (prog2$ (setenv$ "ACL2_DOC_IMAGES" (or wadi-env-val ""))
                  state)
          (prog2$ (setenv$ "ACL2_DOC_IMAGES" (or wadi-env-val "" ""))
                  state))))
     (value wadi-temp)))

(defun save-rendered (outfile
                      header
                      topic-list-name
                      error ; when true, cause an error on xdoc or Markup error
                      write-acl2-doc-search-file
                      state)

; See books/doc/top.lisp for an example call of xdoc::save-rendered.  In
; particular, the constant *rendered-doc-combined-header* defined in that file
; is an example of header, which goes at the top of the generated file; and
; topic-list-name is a symbol, such as acl2::*acl2+books-documentation*.

; Below we bind force-missing-parents-p and maybe-add-top-topic-p both true.
; These could be formal parameters if need be.

; Example of outfile:
;   (acl2::extend-pathname (cbd)
;                           "../system/doc/rendered-doc-combined.lsp"
;                           state))


  (let ((force-missing-parents-p t)
        (maybe-add-top-topic-p t)
        (search-file (if (position acl2::*directory-separator* outfile)
                         (concatenate 'string
                                      (acl2::get-directory-of-file outfile)
                                      acl2::*directory-separator-string*
                                      "acl2-doc-search")
                       "acl2-doc-search")))
    (state-global-let*
     ((current-package "ACL2" set-current-package-state))
     (b* ((- (initialize-xdoc-errors error))
          (state (f-put-global 'broken-links-limit nil state))
          ((mv ? all-topics0 state)
           (all-xdoc-topics state))
          (all-topics
           (time$
            (let* ((all-topics1 (normalize-parents-list ; Should we clean-topics?
                                 all-topics0))
                   (all-topics2 (if maybe-add-top-topic-p
                                    (maybe-add-top-topic all-topics1)
                                  all-topics1))
                   (all-topics3 (if force-missing-parents-p
                                    (force-missing-parents all-topics2)
                                  all-topics2)))
              all-topics3)))
          ((er rendered)
           (time$ (with-acl2-doc-images
                   (render-topics all-topics all-topics state))))
          (rendered (time$ (split-acl2-topics rendered nil nil nil)))
          (- (cw "Writing ~s0~%" outfile))
          ((mv channel state) (open-output-channel! outfile :character state))
          ((unless channel)
           (cw "can't open ~s0 for output." outfile)
           (acl2::silent-error state))
          (state (princ$ header channel state))
          (state (fms! "(in-package \"ACL2\")~|~%(defconst ~x0 '~|"
                       (list (cons #\0 topic-list-name))
                       channel state nil))

; I tried replacing the fms! call below with mostly princ$ calls, but I needed
; a prin1$ call for (at least) the main doc string of each topic (to escape
; characters as necessary, especially double-quote (")).  However, the measured
; time reduction was slight, however; 16.77 seconds reduced to 16.03 seconds.
; The bytes allocated were reduced more noticeably, 12,642,544 down to 1,456;
; however, that's trivial compared to more than 22GB allocated by render-topics
; when saving rendered-doc-combined.lsp.

          (state (time$ (fms! "~x0"
                              (list (cons #\0 rendered))
                              channel state nil)))
          (state (fms! ")" nil channel state nil))
          (state (newline channel state))
          (state (close-output-channel channel state))
          (- (report-xdoc-errors 'save-rendered))
          ((when (not write-acl2-doc-search-file))
           (value '(value-triple :ok)))
          ((mv channel state)
           (open-output-channel! search-file :character state))
          ((unless channel)
           (cw "can't open ~s0 for output." search-file)
           (acl2::silent-error state))
          (state (time$
                  (acl2-doc-print-topic-index-lst rendered channel state)))
          (state (close-output-channel channel state)))
       (value '(value-triple :ok))))))

(defmacro save-rendered-event (outfile
                               header
                               topic-list-name
                               error ; when true, cause an error on xdoc or Markup error
                               &key
                               script-file ; e.g., for building TAGS-acl2-doc
                               script-args
                               timep ; if a surrounding time$ call is desired
                               write-acl2-doc-search-file
                               )
  (let* ((form1 `(save-rendered
                  ,outfile ,header ,topic-list-name ,error
                  ,write-acl2-doc-search-file state))
         (form2 `(prog2$ (let ((script-file ,script-file)
                               (script-args ,script-args))
                           (and script-file
                                (sys-call ; requires active trust tag
                                 script-file script-args)))
                         ,form1))
         (form3 (if timep
                    `(time$ ,form2)
                  form2)))
    `(make-event
      ,form3)))