1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
; 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 <jared@centtech.com>
(in-package "XDOC")
(include-book "std/util/bstar" :dir :system)
(set-state-ok t)
(program)
; fmt-to-str-orig.lisp
;
; This file is merely a bootstrapping hack.
;
; We implement a bare-bones pretty printer, similar to ACL2's fmt-to-string or
; str::pretty. Unlike ACL2's fmt-to-string, we use narrower margins and print
; with downcased symbols.
;
; This function was historically used throughout XDOC in the pretty-printing of
; terms, e.g., to handle things like @(def ...). Today, XDOC's preprocessor
; instead uses str::pretty, which allows us to avoid nasty problems with using
; ACL2's formatting functions to print outside of the loop, e.g., for use with
; the ACL2 Sidekick.
;
; Why do we still need this file, then? Well, macros such as DEFINE and
; DEFAGGREGATE, which are used in the definition of str::pretty, have their own
; documentation-generation functionality. Historically these documentation
; producing routines made use of fmt-to-string. This leads to circular
; dependencies such as fmt-to-str -> str::pretty -> define -> fmt-to-str!
;
; To break this circularity, we keep the original implementation of fmt-to-str,
; renaming it to fmt-to-str-orig. We use the orig version in macros such as
; DEFINE to minimize dependencies and avoid these loops. When these macros
; call fmt-to-str-orig, they're running in the real ACL2 loop, so we don't have
; these outside-the-loop problems. Meanwhile, we avoid the fmt functions in
; the real preprocessor code.
(defun fmt-to-str-orig-aux (string alist base-pkg state)
;; Use ACL2's fancy new string-printing stuff to do pretty-printing
(b* ((hard-right-margin (f-get-global 'acl2::fmt-hard-right-margin state))
(soft-right-margin (f-get-global 'acl2::fmt-soft-right-margin state))
(print-case (f-get-global 'acl2::print-case state))
(pkg (current-package state))
(base-pkg-name (symbol-package-name base-pkg))
((mv er ?val state) (acl2::in-package-fn base-pkg-name state))
((when er)
(er hard? 'fmt-to-str-orig-aux "Error switching to package ~x0" base-pkg-name)
(mv "" state))
(state (set-fmt-hard-right-margin 68 state))
(state (set-fmt-soft-right-margin 62 state))
(state (set-print-case :downcase state))
((mv channel state) (open-output-channel :string :character state))
((mv ?col state) (fmt1 string alist 0 channel state nil))
((mv er1 str state) (get-output-stream-string$ channel state))
((mv er2 ?val state) (acl2::in-package-fn pkg state))
(state (set-fmt-hard-right-margin hard-right-margin state))
(state (set-fmt-soft-right-margin soft-right-margin state))
(state (set-print-case print-case state))
((when er1)
(er hard? 'fmt-to-str-orig-aux "Error with get-output-stream-string$?")
(mv "" state))
((when er2)
(er hard? 'fmt-to-str-orig-aux "Error switching back to package ~x0" pkg)
(mv "" state)))
(mv str state)))
(defun fmt-to-str-orig (x base-pkg state)
;; Basic formatting of sexprs, no encoding or autolinking
(fmt-to-str-orig-aux "~x0" (list (cons #\0 x)) base-pkg state))
|
