0 | module Text.Show.Pretty
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import Text.PrettyPrint.Bernardy
  5 |
  6 | import public Text.Show.Value
  7 | import public Text.Show.PrettyVal
  8 | import public Text.Show.PrettyVal.Derive
  9 |
 10 | %default total
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          Utilities
 14 | --------------------------------------------------------------------------------
 15 |
 16 | dropTrailingZeros : SnocList Char -> String
 17 | dropTrailingZeros [<]        = "0"
 18 | dropTrailingZeros [<'.']     = "0"
 19 | dropTrailingZeros (i :< '.') = fastPack (i <>> [])
 20 | dropTrailingZeros (i :< '0') = dropTrailingZeros i
 21 | dropTrailingZeros sc         = fastPack (sc <>> [])
 22 |
 23 | roundUp : SnocList Char -> String
 24 | roundUp [<]        = "1"
 25 | roundUp [<'.']     = "1"
 26 | roundUp (i :< '.') = show $ cast {to = Integer} (fastPack (i <>> [])) + 1
 27 | roundUp (i :< '9') = roundUp i
 28 | roundUp (i :< c)   = fastPack (i <>> [chr $ ord c + 1])
 29 |
 30 | ||| Prints a floating point number with at most the given number
 31 | ||| of digits after the dot.
 32 | export
 33 | printDouble : (precision : Nat) -> Double -> String
 34 | printDouble prec v =
 35 |   case forget $ split ('.' ==) (fastUnpack $ show v) of
 36 |     [x,y] =>
 37 |       case splitAt prec y of
 38 |         (pre,[])   => dropTrailingZeros ([<] <>< (x ++ '.' :: pre))
 39 |         (pre,c::_) =>
 40 |           if c <= '4'
 41 |              then dropTrailingZeros ([<] <>< (x ++ '.' :: pre))
 42 |              else roundUp ([<] <>< (x ++ '.' :: pre))
 43 |     _     => show v
 44 |
 45 | -- Don't put parenthesis around constructors in infix chains
 46 | isInfixAtom : Value -> Bool
 47 | isInfixAtom (InfixCons _ _) = False
 48 | isInfixAtom (Neg _)         = False
 49 | isInfixAtom _               = True
 50 |
 51 | isAtom : Value -> Bool
 52 | isAtom (Con _ (_ :: _))  = False
 53 | isAtom v                 = isInfixAtom v
 54 |
 55 | onLineAfter : {opts : _} -> Doc opts -> Doc opts -> Doc opts
 56 | onLineAfter l d = vappend d (indent 2 l)
 57 |
 58 | toDoc : {opts : _} -> Value -> Doc opts
 59 | toDoc val =
 60 |   case val of
 61 |     Con (MkName "") vs => sep $ atoms vs
 62 |     Con (MkName c)  [] => line c
 63 |     Con (MkName c)  vs => prettyCon Open c (atoms vs)
 64 |     InfixCons v1 cvs   => sep (infx v1 cvs)
 65 |     Rec (MkName c) fs  => prettyRecord Open c (fields fs)
 66 |     Lst vs             => list (docs vs)
 67 |     Tuple v1 v2 vs     => tuple (toDoc v1 :: toDoc v2 :: docs vs)
 68 |     Neg v              => line "-" <+> atom v
 69 |     Natural x          => line x
 70 |     Dbl x              => line x
 71 |     Chr x              => line x
 72 |     Str x              => line x
 73 |
 74 |   where
 75 |     atom : Value -> Doc opts
 76 |     atom v = if isAtom v then toDoc v else parens (toDoc v)
 77 |
 78 |     -- the explicit list mappings like `atoms`, `docs`, and
 79 |     -- `fields` are necessary to convince the totality checker.
 80 |     atoms : List Value -> List (Doc opts)
 81 |     atoms []        = []
 82 |     atoms (x :: xs) = atom x :: atoms xs
 83 |
 84 |     infixAtom : Value -> Doc opts
 85 |     infixAtom v = if isInfixAtom v then toDoc v else parens (toDoc v)
 86 |
 87 |     field : (VName,Value) -> Doc opts
 88 |     field (MkName s,v) =
 89 |       let name := line s <++> equals
 90 |           val  := toDoc v
 91 |        in ifMultiline (name <++> val) (val `onLineAfter` name)
 92 |
 93 |     fields : List (VName,Value) -> List (Doc opts)
 94 |     fields []        = []
 95 |     fields (p :: ps) = field p :: fields ps
 96 |
 97 |     docs : List Value -> List (Doc opts)
 98 |     docs []        = []
 99 |     docs (x :: xs) = toDoc x :: docs xs
100 |
101 |     infx : Value -> List (VName,Value) -> List (Doc opts)
102 |     infx v []                  = [infixAtom v]
103 |     infx v ((MkName n,v2)::ps) = (infixAtom v <++> line n) :: infx v2 ps
104 |
105 | public export
106 | dfltOpts : LayoutOpts
107 | dfltOpts = Opts 80
108 |
109 | ||| Pretty print a generic value. Our intention is that the result is
110 | ||| equivalent to the 'Show' instance for the original value, except possibly
111 | ||| easier to understand by a human.
112 | export %inline
113 | valToDoc : {opts : _} -> Value -> Doc opts
114 | valToDoc = toDoc
115 |
116 | ||| Pretty print a generic value. Our intention is that the result is
117 | ||| equivalent to the 'Show' instance for the original value, except possibly
118 | ||| easier to understand by a human.
119 | export %inline
120 | valToStr : Value -> String
121 | valToStr = render dfltOpts . valToDoc
122 |
123 | --------------------------------------------------------------------------------
124 | --          Pretty via Show
125 | --------------------------------------------------------------------------------
126 |
127 | export %inline
128 | reify : Show a => a -> Maybe Value
129 | reify = parseValue . show
130 |
131 | ||| Try to show a value, prettily. If we do not understand the value, then we
132 | ||| just use its standard 'Show' instance.
133 | export
134 | ppDoc : {opts : _} -> Show a => a -> Doc opts
135 | ppDoc a =
136 |   let txt = show a
137 |    in maybe (fromString txt) valToDoc (parseValue txt)
138 |
139 | ||| Convert a generic value into a pretty 'String', if possible.
140 | export %inline
141 | ppShow : Show a => a -> String
142 | ppShow = render dfltOpts . ppDoc
143 |
144 | ||| Pretty print something that may be converted to a list as a list.
145 | ||| Each entry is on a separate line, which means that we don't do clever
146 | ||| pretty printing, and so this works well for large strucutures.
147 | export %inline
148 | ppDocList : {opts : _} -> (Foldable f, Show a) => f a -> Doc opts
149 | ppDocList = list . map ppDoc . toList
150 |
151 | ||| Pretty print something that may be converted to a list as a list.
152 | ||| Each entry is on a separate line, which means that we don't do clever
153 | ||| pretty printing, and so this works well for large strucutures.
154 | export %inline
155 | ppShowList : (Foldable f, Show a) => f a -> String
156 | ppShowList = render dfltOpts . ppDocList
157 |
158 |
159 | ||| Pretty print a generic value to stdout.
160 | export
161 | pPrint : Show a => a -> IO ()
162 | pPrint = putStrLn . ppShow
163 |
164 | ||| Pretty print something that may be converted to a list as a list.
165 | ||| Each entry is on a separate line, which means that we don't do clever
166 | ||| pretty printing, and so this works well for large strucutures.
167 | export
168 | pPrintList : (Foldable f, Show a) => f a -> IO ()
169 | pPrintList = putStrLn . ppShowList
170 |
171 | --------------------------------------------------------------------------------
172 | --          Pretty via PrettyVal
173 | --------------------------------------------------------------------------------
174 |
175 | ||| Render a value in the `PrettyVal` interface to a `Doc`.
176 | ||| The benefit of this function is that `PrettyVal` instances may
177 | ||| be derived automatically using generics.
178 | export
179 | dumpDoc : {opts : _} -> PrettyVal a => a -> Doc opts
180 | dumpDoc = valToDoc . prettyVal
181 |
182 | ||| Render a value in the `PrettyVal` interface to a `String`.
183 | ||| The benefit of this function is that `PrettyVal` instances may
184 | ||| be derived automatically using generics.
185 | export
186 | dumpStr : PrettyVal a => a -> String
187 | dumpStr = render dfltOpts . dumpDoc
188 |
189 | ||| Render a value using the `PrettyVal` interface
190 | ||| and show it to standard out.
191 | export
192 | dumpIO : PrettyVal a => a -> IO ()
193 | dumpIO = putStrLn . dumpStr
194 |
195 | --------------------------------------------------------------------------------
196 | --          Pre-processing
197 | --------------------------------------------------------------------------------
198 |
199 | ||| This type is used to allow pre-processing of values before showing them.
200 | public export
201 | record PreProc a where
202 |   constructor MkPreProc
203 |   preProc : Value -> Value
204 |   val     : a
205 |
206 | export
207 | PrettyVal a => PrettyVal (PreProc a) where
208 |   prettyVal (MkPreProc p v) = p (prettyVal v)
209 |
210 | ||| Hide the given constructors when showing a value.
211 | export
212 | ppHide : (VName -> Bool) -> a -> PreProc a
213 | ppHide p = MkPreProc (hideCon False p)
214 |
215 | ||| Hide the given constructors when showing a value.
216 | ||| In addition, hide values if all of their children were hidden.
217 | export
218 | ppHideNested : (VName -> Bool) -> a -> PreProc a
219 | ppHideNested p = MkPreProc (hideCon True p)
220 |