0 | module Text.PrettyPrint.Bernardy.Interface
  1 |
  2 | import Data.List1
  3 | import Data.Vect
  4 | import Data.SortedMap
  5 | import Data.SortedSet
  6 | import Text.PrettyPrint.Bernardy.Combinators
  7 | import Text.PrettyPrint.Bernardy.Core
  8 |
  9 | %default total
 10 |
 11 | public export
 12 | interface Pretty a where
 13 |     constructor MkPretty
 14 |     prettyPrec : {opts : _} -> Prec -> a -> Doc opts
 15 |
 16 | ||| Alias for `prettyPrec Open`
 17 | public export %inline
 18 | pretty : Pretty a => {opts : _} -> a -> Doc opts
 19 | pretty = prettyPrec Open
 20 |
 21 | ||| Alias for `prettyPrec App`
 22 | public export %inline
 23 | prettyArg : Pretty a => {opts : _} -> a -> Doc opts
 24 | prettyArg = prettyPrec App
 25 |
 26 | onLineAfter : {opts : _} -> Doc opts -> Doc opts -> Doc opts
 27 | onLineAfter l d = vappend d (indent 2 l)
 28 |
 29 | -- multilineCon :
 30 | --      {opts : _}
 31 | --   -> (con, firstArg : Doc opts)
 32 | --   -> (args : List (Doc opts))
 33 | --   -> Doc opts
 34 | -- multilineCon con fa as = foldl vcat fa as `onLineAfter` con
 35 |
 36 | ||| Utility for pretty printing Idris data types.
 37 | |||
 38 | ||| Constructor name and arguments are layed out on a single line
 39 | ||| if and only if they fit the page width
 40 | ||| and all pretty printed arguments use only a single line. If
 41 | ||| one of these conditions does not hold, the list of arguments is
 42 | ||| indented by two spaces and layed out vertically after the constructor
 43 | ||| name.
 44 | |||
 45 | ||| ```idris example
 46 | ||| prettyCon "Just" [prettyArg v]
 47 | ||| ```
 48 | export
 49 | prettyCon : {opts : _} -> Prec -> String -> List (Doc opts) -> Doc opts
 50 | prettyCon p c []   = line c
 51 | prettyCon p c args =
 52 |   let con := line c
 53 |    in parenthesise (p >= App) $
 54 |         ifMultiline (hsep $ con :: args) (vsep args `onLineAfter` con)
 55 |
 56 |
 57 | ||| Utility for pretty printing Idris record fields.
 58 | |||
 59 | ||| Field name and value are separated by an equals sign (`=`) and
 60 | ||| layed out on a single line if and only if they fit the page width
 61 | ||| and the pretty printed values is itself on a single line. If
 62 | ||| one of these conditions does not hold, the value is placed on
 63 | ||| the next line and indented by two spaces.
 64 | export
 65 | prettyField : Pretty a => {opts : _} -> String -> a -> Doc opts
 66 | prettyField s v =
 67 |   let name := line s <++> equals
 68 |       val  := pretty v
 69 |    in ifMultiline (name <++> val) (val `onLineAfter` name)
 70 |
 71 | ||| Utility for pretty printing Idris data types with named arguments.
 72 | |||
 73 | ||| This uses record syntax for printing the argument list, but is not
 74 | ||| limited to single-constructor data types.
 75 | |||
 76 | ||| Constructor name and arguments are layed out on a single line
 77 | ||| if and only if they fit the page width
 78 | ||| and all pretty printed arguments use only a single line. If
 79 | ||| one of these conditions does not hold, the list of arguments is
 80 | ||| indented by two spaces and layed out vertically after the constructor
 81 | ||| name.
 82 | |||
 83 | ||| ```idris example
 84 | ||| prettyCon "Just" [prettyArg v]
 85 | ||| ```
 86 | |||
 87 | ||| Note: Use `prettyField` to pair an argument with its field name.
 88 | export
 89 | prettyRecord : {opts : _} -> Prec -> String -> List (Doc opts) -> Doc opts
 90 | prettyRecord p c []   = line c
 91 | prettyRecord p c args =
 92 |   let con  := line c
 93 |       flds := fields args
 94 |    in parenthesise (p >= App) $
 95 |         ifMultiline (con <++> flds) (flds `onLineAfter` con)
 96 |
 97 | --------------------------------------------------------------------------------
 98 | --          Implementations
 99 | --------------------------------------------------------------------------------
100 |
101 | public export %inline
102 | Pretty Char where
103 |   prettyPrec _ = line . show
104 |
105 | public export %inline
106 | Pretty String where
107 |   prettyPrec _ = text . show
108 |
109 | public export %inline
110 | Pretty Bits8 where
111 |   prettyPrec _ = line . show
112 |
113 | public export %inline
114 | Pretty Bits16 where
115 |   prettyPrec _ = line . show
116 |
117 | public export %inline
118 | Pretty Bits32 where
119 |   prettyPrec _ = line . show
120 |
121 | public export %inline
122 | Pretty Bits64 where
123 |   prettyPrec _ = line . show
124 |
125 | public export %inline
126 | Pretty Int8 where
127 |   prettyPrec _ = line . show
128 |
129 | public export %inline
130 | Pretty Int16 where
131 |   prettyPrec _ = line . show
132 |
133 | public export %inline
134 | Pretty Int32 where
135 |   prettyPrec _ = line . show
136 |
137 | public export %inline
138 | Pretty Int64 where
139 |   prettyPrec _ = line . show
140 |
141 | public export %inline
142 | Pretty Integer where
143 |   prettyPrec _ = line . show
144 |
145 | public export %inline
146 | Pretty Double where
147 |   prettyPrec _ = line . show
148 |
149 | public export %inline
150 | Pretty () where
151 |   prettyPrec _ () = line "()"
152 |
153 | public export %inline
154 | Pretty Bool where
155 |   prettyPrec _ True  = "True"
156 |   prettyPrec _ False = "False"
157 |
158 | public export %inline
159 | Pretty Ordering where
160 |   prettyPrec _ LT = "LT"
161 |   prettyPrec _ EQ = "EQ"
162 |   prettyPrec _ GT = "GT"
163 |
164 | public export %inline
165 | Pretty Nat where
166 |   prettyPrec _ = line . show
167 |
168 | public export %inline
169 | Pretty Int where
170 |   prettyPrec _ = line . show
171 |
172 | public export
173 | Pretty a => Pretty (Maybe a) where
174 |   prettyPrec p Nothing  = line "Nothing"
175 |   prettyPrec p (Just x) = prettyCon p "Just" [prettyArg x]
176 |
177 | public export
178 | Pretty a => Pretty b => Pretty (Either a b) where
179 |   prettyPrec p (Left x)  = prettyCon p "Left" [prettyArg x]
180 |   prettyPrec p (Right x) = prettyCon p "Right" [prettyArg x]
181 |
182 | public export %inline
183 | Pretty a => Pretty (List a) where
184 |   prettyPrec _ = list . map pretty
185 |
186 | public export %inline
187 | Pretty a => Pretty (List1 a) where
188 |   prettyPrec p vs = prettyPrec p (toList vs)
189 |
190 | public export %inline
191 | Pretty a => Pretty (SnocList a) where
192 |   prettyPrec _ = snocList . map pretty . (<>> [])
193 |
194 | public export
195 | Pretty a => Pretty b => Pretty (a,b) where
196 |   prettyPrec _ (x,y) = tuple [pretty x, pretty y]
197 |
198 | public export
199 | Pretty a => Pretty (Vect n a) where
200 |   prettyPrec p vs = prettyPrec p (toList vs)
201 |
202 | public export
203 | Pretty k => Pretty v => Pretty (SortedMap k v) where
204 |   prettyPrec p m = prettyCon p "fromList" [prettyArg $ SortedMap.toList m]
205 |
206 | public export
207 | Pretty k => Pretty (SortedSet k) where
208 |   prettyPrec p m = prettyCon p "fromList" [prettyArg $ Prelude.toList m]
209 |
210 | -- Universal interpolation through `Pretty`
211 |
212 | export %defaulthint
213 | ThroughPretty : Pretty a => (layout : LayoutOpts) => Interpolation a
214 | ThroughPretty = TP where [TP] Interpolation a where interpolate = render layout . pretty
215 |