0 | module Prelude.Show
  1 |
  2 | import Builtin
  3 | import Prelude.Basics
  4 | import Prelude.EqOrd
  5 | import Prelude.Num
  6 | import Prelude.Types
  7 |
  8 | %default total
  9 |
 10 | ----------
 11 | -- SHOW --
 12 | ----------
 13 |
 14 | ||| The precedence of an Idris operator or syntactic context.
 15 | public export
 16 | data Prec = Open | Equal | Dollar | Backtick | User Nat | PrefixMinus | App
 17 |
 18 | ||| Gives the constructor index of the Prec as a helper for writing
 19 | ||| implementations.
 20 | public export
 21 | precCon : Prec -> Integer
 22 | precCon Open        = 0
 23 | precCon Equal       = 1
 24 | precCon Dollar      = 2
 25 | precCon Backtick    = 3
 26 | precCon (User n)    = 4
 27 | precCon PrefixMinus = 5
 28 | precCon App         = 6
 29 |
 30 | export
 31 | Eq Prec where
 32 |   (==) (User m) (User n) = m == n
 33 |   (==) x        y        = precCon x == precCon y
 34 |
 35 | export
 36 | Ord Prec where
 37 |   compare (User m) (User n) = compare m n
 38 |   compare x        y        = compare (precCon x) (precCon y)
 39 |
 40 | ||| Things that have a canonical `String` representation.
 41 | ||| A minimal implementation includes either `show` or `showPrec`.
 42 | public export
 43 | interface Show ty where
 44 |   constructor MkShow
 45 |   ||| Convert a value to its `String` representation.
 46 |   ||| @ x the value to convert
 47 |   total
 48 |   show : (x : ty) -> String
 49 |   show x = showPrec Open x
 50 |
 51 |   ||| Convert a value to its `String` representation in a certain precedence
 52 |   ||| context.
 53 |   |||
 54 |   ||| A value should produce parentheses around itself if and only if the given
 55 |   ||| precedence context is greater than or equal to the precedence of the
 56 |   ||| outermost operation represented in the produced `String`.  *This is
 57 |   ||| different from Haskell*, which requires it to be strictly greater.  `Open`
 58 |   ||| should thus always produce *no* outermost parens, `App` should always
 59 |   ||| produce outermost parens except on atomic values and those that provide
 60 |   ||| their own bracketing, like `Pair` and `List`.
 61 |   ||| @ d the precedence context.
 62 |   ||| @ x the value to convert
 63 |   total
 64 |   showPrec : (d : Prec) -> (x : ty) -> String
 65 |   showPrec _ x = show x
 66 |
 67 | ||| Surround a `String` with parentheses depending on a condition.
 68 | ||| @ b whether to add parentheses
 69 | public export
 70 | showParens : (b : Bool) -> String -> String
 71 | showParens False s = s
 72 | showParens True  s = "(" ++ s ++ ")"
 73 |
 74 | ||| A helper for the common case of showing a non-infix constructor with at
 75 | ||| least one argument, for use with `showArg`.
 76 | |||
 77 | ||| Apply `showCon` to the precedence context, the constructor name, and the
 78 | ||| args shown with `showArg` and concatenated.  Example:
 79 | ||| ```idris example
 80 | ||| data Ann a = MkAnn String a
 81 | |||
 82 | ||| Show a => Show (Ann a) where
 83 | |||   showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
 84 | ||| ```
 85 | public export
 86 | showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
 87 | showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs)
 88 |
 89 | ||| A helper for the common case of showing a non-infix constructor with at
 90 | ||| least one argument, for use with `showCon`.
 91 | |||
 92 | ||| This adds a space to the front so the results can be directly concatenated.
 93 | ||| See `showCon` for details and an example.
 94 | public export %tcinline
 95 | showArg : Show a => (x : a) -> String
 96 | showArg x = " " ++ showPrec App x
 97 |
 98 | firstCharIs : (Char -> Bool) -> String -> Bool
 99 | firstCharIs p "" = False
100 | firstCharIs p str = p (assert_total (prim__strHead str))
101 |
102 | primNumShow : (a -> String) -> Prec -> a -> String
103 | primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
104 |
105 | export
106 | Show Int where
107 |   showPrec = primNumShow prim__cast_IntString
108 |
109 | export
110 | Show Integer where
111 |   showPrec = primNumShow prim__cast_IntegerString
112 |
113 | export
114 | Show Bits8 where
115 |   showPrec = primNumShow prim__cast_Bits8String
116 |
117 | export
118 | Show Bits16 where
119 |   showPrec = primNumShow prim__cast_Bits16String
120 |
121 | export
122 | Show Bits32 where
123 |   showPrec = primNumShow prim__cast_Bits32String
124 |
125 | export
126 | Show Bits64 where
127 |   showPrec = primNumShow prim__cast_Bits64String
128 |
129 | export
130 | Show Int8 where
131 |   showPrec = primNumShow prim__cast_Int8String
132 |
133 | export
134 | Show Int16 where
135 |   showPrec = primNumShow prim__cast_Int16String
136 |
137 | export
138 | Show Int32 where
139 |   showPrec = primNumShow prim__cast_Int32String
140 |
141 | export
142 | Show Int64 where
143 |   showPrec = primNumShow prim__cast_Int64String
144 |
145 | export
146 | Show Double where
147 |   showPrec = primNumShow prim__cast_DoubleString
148 |
149 | protectEsc : (Char -> Bool) -> String -> String -> String
150 | protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s
151 |
152 | showLitChar : Char -> String -> String
153 | showLitChar '\a'   = ("\\a" ++)
154 | showLitChar '\b'   = ("\\b" ++)
155 | showLitChar '\f'   = ("\\f" ++)
156 | showLitChar '\n'   = ("\\n" ++)
157 | showLitChar '\r'   = ("\\r" ++)
158 | showLitChar '\t'   = ("\\t" ++)
159 | showLitChar '\v'   = ("\\v" ++)
160 | showLitChar '\SO'  = protectEsc (== 'H') "\\SO"
161 | showLitChar '\DEL' = ("\\DEL" ++)
162 | showLitChar '\\'   = ("\\\\" ++)
163 | showLitChar c
164 |     = case getAt (fromInteger (prim__cast_CharInteger c)) asciiTab of
165 |            Just k => strCons '\\' . (k ++)
166 |            Nothing => if (c > '\DEL')
167 |                          then strCons '\\' . protectEsc isDigit (show (prim__cast_CharInt c))
168 |                          else strCons c
169 |   where
170 |     asciiTab : List String
171 |     asciiTab
172 |         = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
173 |            "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",
174 |            "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
175 |            "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]
176 |
177 | showLitString : List Char -> String -> String
178 | showLitString []        = id
179 | showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
180 | showLitString (c  ::cs) = (showLitChar c) . showLitString cs
181 |
182 | export
183 | Show Char where
184 |   show '\'' = "'\\''"
185 |   show c    = strCons '\'' (showLitChar c "'")
186 |
187 | export
188 | Show String where
189 |   show cs = strCons '"' (showLitString (unpack cs) "\"")
190 |
191 | export
192 | Show Nat where
193 |   show n = show (the Integer (natToInteger n))
194 |
195 | export
196 | Show Bool where
197 |   show True = "True"
198 |   show False = "False"
199 |
200 | export
201 | Show Void where
202 |   show v impossible
203 |
204 | export
205 | Show () where
206 |   show () = "()"
207 |
208 | export
209 | (Show a, Show b) => Show (a, b) where
210 |   show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
211 |
212 | export
213 | (Show a, {y : a} -> Show (p y)) => Show (DPair a p) where
214 |     show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
215 |
216 | export
217 | Show a => Show (List a) where
218 |   show xs = "[" ++ show' "" xs ++ "]"
219 |     where
220 |       show' : String -> List a -> String
221 |       show' acc []        = acc
222 |       show' acc [x]       = acc ++ show x
223 |       show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
224 |
225 | export
226 | Show a => Show (Maybe a) where
227 |   showPrec d Nothing  = "Nothing"
228 |   showPrec d (Just x) = showCon d "Just" (showArg x)
229 |
230 | export
231 | (Show a, Show b) => Show (Either a b) where
232 |   showPrec d (Left x)  = showCon d "Left" $ showArg x
233 |   showPrec d (Right x) = showCon d "Right" $ showArg x
234 |
235 | export
236 | Show Ordering where
237 |   show LT = "LT"
238 |   show EQ = "EQ"
239 |   show GT = "GT"
240 |