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))