; XDOC Documentation System for ACL2 ; Copyright (C) 2009-2015 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 ; autolink.lisp -- automatically insert links into pretty-printed s-expressions (in-package "XDOC") (include-book "fmt-to-str") (include-book "names") (local (include-book "misc/assert" :dir :system)) (set-state-ok t) (program) ; Convention: X is a string we are traversing, N is our current position in the ; string, and XL is the length of the string. The imagined guard is: ; ; (declare (xargs :guard (and (stringp x) ; (natp n) ; (natp xl) ; (= xl (length x)) ; (<= n xl)))) ; ; We could do a lot of this in logic mode, but there doesn't seem to be much ; point to that. (defun error-context (x n xl) ;; ==> STRING ;; Tries to show what text is near an error. (declare (type string x)) (b* ((min (nfix (- n 40))) (max (min (+ n 20) xl))) (subseq x min max))) (defun skip-past-ws (x n xl) ;; ==> N-PRIME (declare (type string x)) (cond ((eql xl n) n) ((member (char x n) '(#\Space #\Tab #\Newline #\Page)) (skip-past-ws x (+ 1 n) xl)) (t n))) ; What a pain. We have to implement a symbol parser. (defun parse-symbol-name-part (x n xl bar-escape-p ; have we read an opening bar? slash-escape-p ; have we just read a backslash? some-chars-p ; have we read any chars at all yet? nice-error-msg-p ; do we care about nice error msgs? acc) ;; ==> (MV ERROR NAME N-PRIME) (declare (type string x)) ; This tries to read just one part of a symbol name (i.e., the package part, ; or the name part.) (b* (((when (= xl n)) ;; End of string? Error if we were escaped, or if we have not actually ;; read some characters yet. Otherwise, it was okay. (b* ((result (str::rchars-to-string acc)) ((when (or bar-escape-p slash-escape-p (not some-chars-p))) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": unexpected end of string while reading symbol. " "Characters read so far: " result) "Symbol Parse Error") result n))) (mv nil result n))) (n+1 (+ n 1)) (char (char x n)) ((when slash-escape-p) ;; Slash escape is on, so just add next char verbatim and turn off ;; slash escape. (parse-symbol-name-part x n+1 xl bar-escape-p nil t nice-error-msg-p (cons char acc))) ((when (eql char #\|)) ;; Bar just toggles bar-escaped-ness. (parse-symbol-name-part x n+1 xl (not bar-escape-p) nil t nice-error-msg-p acc)) ((when (eql char #\\)) ;; Slash starts a slash-escape. (parse-symbol-name-part x n+1 xl bar-escape-p t t nice-error-msg-p acc)) ((when bar-escape-p) ;; Bar-escape is on and not a special char. Read verbatim through it's ;; turned off. (parse-symbol-name-part x n+1 xl t nil t nice-error-msg-p (cons char acc))) ((when (member char '(#\Space #\( #\) #\Newline #\Tab #\Page #\: #\, #\' #\`))) ;; Whitespace, paren, colon, comma, quote, backquote, outside of a bar ;; escape; end of symbol. We can stop as long as we've actually read ;; some characters. (if some-chars-p (mv nil (str::rchars-to-string acc) n) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": expected to read some part of a symbol, but found " (implode (list char)) ".") "Symbol Parse Error") "" n))) ((when (or (and (char<= #\a char) (char<= char #\z)))) ;; lowercase letters outside of bar escape get capitalized (parse-symbol-name-part x n+1 xl nil nil t nice-error-msg-p (cons (acl2::char-upcase char) acc)))) ;; Otherwise add the char verbatim (parse-symbol-name-part x n+1 xl nil nil t nice-error-msg-p (cons char acc)))) (defun parse-symbol (x n xl base-pkg ; default package to intern into kpa ; (known-package-alist state) nice-error-msg-p) ;; ==> (MV ERROR SYMBOL N-PRIME) (declare (type string x)) ; This extends parse-symbol-name-part to read both parts. We support keywords, ; etc. This is definitely not going to handle everything in Common Lisp, but ; whatever. (b* (((when (= xl n)) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": end of string while trying to parse a symbol.") "Symbol Parse Error") nil n)) (char (char x n)) ((when (eql char #\:)) ;; Starts with a colon. Maybe it's keyword symbol? (b* (((mv error name n) (parse-symbol-name-part x (+ n 1) xl nil nil nil nice-error-msg-p nil))) (if error (mv error nil n) (mv nil (intern-in-package-of-symbol name :keyword) n)))) ;; Could start with a package name, or with the symbol name (for symbols ;; in the base pkg). Either way, we need to read a symbol name part. ((mv error part1 n) (parse-symbol-name-part x n xl nil nil nil nice-error-msg-p nil)) ((when error) (mv error nil n)) ((when (and (< (+ n 1) xl) (eql (char x n) #\:) (eql (char x (+ n 1)) #\:))) ;; Found "::" after the first part, so it's a package name. (b* (((unless (assoc-equal part1 kpa)) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": not a known package: " part1 ".") "Symbol Parse Error") nil n)) ((mv error part2 n) (parse-symbol-name-part x (+ n 2) xl nil nil nil nice-error-msg-p nil)) ((when error) (mv error nil n)) ;; Things look pretty good here. One weird thing we will try to ;; detect is if there are extra colons, e.g., foo::bar::baz should ;; be disallowed. We really want a whitespace or paren or quote ;; or something ((when (and (< n xl) (eql (char x n) #\:))) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": Three layers of colons in symbol name?") "Symbol Parse Error") nil n))) (mv nil (intern$ part2 part1) n))) ;; Didn't find a :: after part1. ((when (and (< n xl) (eql (char x n) #\:))) (mv (if nice-error-msg-p (str::cat "Near " (error-context x n xl) ": Lone colon after symbol name?") "Symbol Parse Error") nil n))) ;; We seem to have an okay package name, but no ::, so put it into the base ;; package. (mv nil (intern-in-package-of-symbol part1 base-pkg) n))) (encapsulate () (logic) ;; since otherwise local stuff gets skipped (local (defun test (x expect-errmsg expect-result expect-n-prime) (declare (xargs :mode :program)) (b* ((known-pkgs (pairlis$ '("KEYWORD" "ACL2" "XDOC") nil)) ((mv errmsg result n-prime) (parse-symbol x 0 (length x) 'acl2::foo known-pkgs t))) (cw "Errmsg: Found ~x0, expected ~x1~%" errmsg expect-errmsg) (cw "Result: Found ~x0, expected ~x1~%" result expect-result) (cw "N-prime: Found ~x0, expected ~x1~%" n-prime expect-n-prime) (and (or (iff errmsg expect-errmsg) (cw "Errmsg failed!~%")) (or expect-errmsg (equal result expect-result) (cw "Result failed!~%")) (or expect-errmsg (equal n-prime expect-n-prime) (cw "N-Prime failed!~%")))))) (local (progn ;; Things that should work (assert! (test "foo" nil 'acl2::foo 3)) (assert! (test "bar" nil 'acl2::bar 3)) (assert! (test "acl2::bar)" nil 'acl2::bar 9)) (assert! (test "xdoc::bar)" nil 'xdoc::bar 9)) (assert! (test "xdoc::|foo|)" nil 'xdoc::|foo| 11)) (assert! (test "xdoc::bar12 " nil 'xdoc::bar12 11)) (assert! (test ":foo)" nil :foo 4)) (assert! (test ":|foo|)" nil :|foo| 6)) (assert! (test ":||" nil :|| 3)) (assert! (test "acl2::bar|:|)" nil 'acl2::bar|:| 12)) ;; Things that should fail (assert! (test ":" t nil nil)) ;; lone colon, not ok (assert! (test "||:" t nil nil)) ;; ending colon, not ok (assert! (test "::|foo|)" t nil nil)) ;; starting colons w/o pkgname, not ok (assert! (test "acl2:::bar)" t nil nil)) ;; three colons, not ok (assert! (test "acl2::bar:" t nil nil)) ;; extra colon, not ok ;; Uh... bug? feature? (assert! (test "123" nil 'acl2::|123| 3))))) (defun autolink-and-encode (x n xl topics base-pkg kpa acc) ;; ==> ACC ; Main routine for autolinking and HTML encoding s-expressions. X typically ; has a pretty-printed S-expression that we want to turn into an XDOC ; segment. TOPICS is a fast alist whose keys are the known topic names, for ; fast lookups of whether a symbol is a topic. ; ; We walk over the string and look for symbols following open-parens; this ; limitation is meant to reduce the amount of symbol parsing we have to do and ; should be good enough to insert links to function calls. Whenever we find a ; symbol that is a documented topic, we insert a link to it. We also HTML ; encode the string in the process. (b* (((when (int= n xl)) acc) (char1 (char x n)) ((when (eql char1 #\<)) ;; --> "<" in reverse (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa (list* #\; #\t #\l #\& acc))) ((when (eql char1 #\>)) ;; --> ">" in reverse (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa (list* #\; #\t #\g #\& acc))) ((when (eql char1 #\&)) ;; --> "&" in reverse (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa (list* #\; #\p #\m #\a #\& acc))) ((when (eql char1 #\")) ;; --> """ in reverse (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa (list* #\; #\t #\o #\u #\q #\& acc))) ((unless (eql char1 #\()) ;; Anything else except an open paren, we aren't going to do anything ;; special with. This way we don't have to call parse-symbol most of ;; the time. (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa (cons char1 acc))) (acc (cons char1 acc)) ((mv err symbol n-prime) (parse-symbol x (+ 1 n) xl base-pkg kpa nil)) ((when err) ;; Failed to parse a valid symbol after it, so that's fine, maybe we hit ;; a quoted thing like '((1 . 2)) or whatever. Just keep going. (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa acc)) (look (hons-get symbol topics)) ((unless look) ;; Nope, not a documented topic, so that's fine, just leave the paren ;; there and keep on encoding things without inserting a link. (autolink-and-encode x (+ 1 n) xl topics base-pkg kpa acc)) ;; Finally, the interesting case. We just found something like ;; "(append". We want to convert this into, e.g., ;; (append ;; and then keep going with our encoding. (acc ;; (list* #\> #\" acc)) ;; Subtle: normally the "xl" argument should be the length of the string ;; here, but we only want to encode the part of the name that we read. ;; So, use the new N-PRIME returned by the symbol parser for the XL part ;; to stop early. (acc (simple-html-encode-str x (+ 1 n) n-prime acc)) (acc ;; (list* #\> #\e #\e #\s #\/ #\< acc))) ;; Finally recur... (autolink-and-encode x n-prime xl topics base-pkg kpa acc))) (encapsulate () (logic) (local (defun test (str expect) (declare (xargs :mode :program)) (b* ((topics '(acl2::f g h foo bar baz + - xdoc::top1 xdoc::top2)) ;; just for testing (alist (make-fast-alist (pairlis$ topics nil))) (known-pkgs (pairlis$ '("ACL2" "KEYWORD" "XDOC") nil)) (acc (autolink-and-encode str 0 (length str) alist 'acl2::foo known-pkgs nil)) (- (fast-alist-free alist)) (result (str::rchars-to-string acc))) (or (equal result expect) (cw "Result: ~x0~%" result) (cw "Expected: ~x0~%" expect))))) (local (progn (assert! (test "foo" ;; --> "foo")) (assert! (test "foo & bar" ;; --> "foo & bar")) (assert! (test "foo & bar " ;; --> "foo & bar <baz>")) (assert! (test "(foo (+ 1 2))" ;; note that foo doesn't get processed: xdoc::foo is among the topics, but ;; since the base-pkg is acl2, the foo here is acl2::foo. "(foo (+ 1 2))")) (assert! (test "(xdoc::foo (f 1 2))" ;; --> "(xdoc::foo (f 1 2))"))))) (defun xml-ppr-obj-aux (x ; object to pretty-print topics-fal ; fast alist binding all xdoc topic names to [irrelevant] base-pkg ; base package to print from state acc) (b* ((kpa (known-package-alist state)) (str (fmt-to-str x base-pkg)) (acc (autolink-and-encode str 0 (length str) topics-fal base-pkg kpa acc))) acc)) (defun xml-ppr-obj-fn (x topics-fal base-pkg state) (str::rchars-to-string (xml-ppr-obj-aux x topics-fal base-pkg state nil))) (defmacro xml-ppr-obj (x &key (state 'state) (topics-fal 'nil) (base-pkg ''acl2::foo)) `(b* ((acc (xml-ppr-obj-aux ,x ,topics-fal ,base-pkg ,state nil)) (ret (str::rchars-to-string acc))) ret)) (local (progn (assert! (equal (xml-ppr-obj '(f 1 2) :topics-fal (make-fast-alist '((f . nil)))) "(xdoc::f 1 2)")) (assert! (equal (xml-ppr-obj '(f 1 2) :topics-fal (make-fast-alist '((f . nil))) :base-pkg 'xdoc::foo) "(f 1 2)"))))