Filtering...

process-book-readme

books/misc/process-book-readme
other
(in-package "ACL2")
other
(program)
other
(set-state-ok t)
next-newlinefunction
(defun next-newline
  (str pos len)
  (cond ((int= pos len) len)
    ((eql (char str pos) #\
) pos)
    (t (next-newline str (1+ pos) len))))
break-string-into-lines-recfunction
(defun break-string-into-lines-rec
  (str pos len acc)
  (cond ((int= pos len) (reverse acc))
    ((eql (char str pos) #\
) (break-string-into-lines-rec str (1+ pos) len acc))
    (t (let ((new-pos (next-newline str pos len)))
        (break-string-into-lines-rec str
          new-pos
          len
          (cons (subseq str pos new-pos) acc))))))
find-whitespace-stringfunction
(defun find-whitespace-string
  (string-list)
  (cond ((endp string-list) nil)
    ((let* ((str (car string-list)) (len (length str)))
       (or (member-char-stringp #\  str (1- len))
         (member-char-stringp #\	 str (1- len)))) (car string-list))
    (t (find-whitespace-string (cdr string-list)))))
break-string-into-linesfunction
(defun break-string-into-lines
  (str msg ctx state)
  (let* ((lines (break-string-into-lines-rec str 0 (length str) nil)) (bad-line (find-whitespace-string lines)))
    (cond (bad-line (er soft
          ctx
          "Found ~@0 line with whitespace:~%~x1~|"
          msg
          bad-line))
      (t (value lines)))))
process-book-readme-fnfunction
(defun process-book-readme-fn
  (readme-filename state)
  (declare (xargs :guard (stringp readme-filename)))
  (let ((ctx 'process-book-readme))
    (mv-let (channel state)
      (open-input-channel readme-filename :object state)
      (cond ((null channel) (er soft
            ctx
            "Unable to open file ~x0 for input."
            readme-filename))
        (t (mv-let (eofp alist state)
            (read-object channel state)
            (pprogn (close-input-channel channel state)
              (cond (eofp (er soft
                    ctx
                    "No form could be read from input file ~x0."
                    readme-filename))
                ((not (and (true-list-listp alist) (alistp (strip-cdrs alist)))) (er soft
                    ctx
                    "The form read from a book's Readme.lsp file should be ~
                       an list of true lists each with at least two elements, ~
                       but ~X01 is not."
                    alist
                    (abbrev-evisc-tuple state)))
                (t (let* ((files-entry (assoc-eq :files alist)) (title-entry (assoc-eq :title alist))
                      (author/s-entry (assoc-eq :author/s alist))
                      (keywords-entry (assoc-eq :keywords alist))
                      (abstract-entry (assoc-eq :abstract alist))
                      (perm-entry (assoc-eq :permission alist))
                      (files (and (true-listp files-entry)
                          (eql (length files-entry) 2)
                          (stringp (cadr files-entry))
                          (cadr files-entry)))
                      (title (and (true-listp title-entry)
                          (eql (length title-entry) 2)
                          (stringp (cadr title-entry))
                          (cadr title-entry)))
                      (author/s (and (string-listp (cdr author/s-entry))
                          (cdr author/s-entry)))
                      (keywords (and (string-listp (cdr keywords-entry))
                          (cdr keywords-entry)))
                      (abstract (and (true-listp abstract-entry)
                          (eql (length abstract-entry) 2)
                          (stringp (cadr abstract-entry))
                          (cadr abstract-entry)))
                      (perm (and (true-listp perm-entry)
                          (eql (length perm-entry) 2)
                          (stringp (cadr perm-entry))
                          (cadr perm-entry))))
                    (cond ((not (and files title author/s keywords abstract perm)) (er soft
                          ctx
                          "No valid field for ~x0 in Readme.lsp alist."
                          (cond ((not files) :files)
                            ((not title) :title)
                            ((not author/s) :author/s)
                            ((not keywords) :keywords)
                            ((not abstract) :abstract)
                            (t :permission))))
                      (t (pprogn (fms "File ~s0 PASSES the check.~|"
                            (list (cons #\0 readme-filename))
                            (standard-co state)
                            state
                            nil)
                          (value :invisible))))))))))))))
process-book-readmemacro
(defmacro process-book-readme
  (&key dir)
  (declare (xargs :guard (or (null dir) (stringp dir))))
  `(process-book-readme-fn (concatenate 'string
      (let ((dir ,DIR))
        (cond (dir (cond ((eql (char dir (1- (length dir))) *directory-separator*) dir)
              (t (concatenate 'string dir *directory-separator-string*))))
          (t (cbd))))
      "Readme.lsp")
    state))