git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3993 from Melvar/standard-shows

Make a few Show instances parenthesise properly

commit385cf270b56ff065072518468574397282fad435 authorNiklas Larsson <metaniklas@gmail.com> dateTue 15 Aug 2017, 20:24 (9 years ago) parentebd2e6f18a1826
5 files changed+22−22
compare with master
unifiedsplit
libs/contrib/CFFI/Types.idr+5−5 libs/contrib/Data/ZZ.idr+2−2 libs/contrib/Text/Literate.idr+4−4 libs/effects/Effect/Logging/Level.idr+9−9 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2
libs/contrib/CFFI/Types.idr+5−5
@@ -29,11 +29,11 @@ Show CType where
2929 show PTR = "PTR"
3030
3131Show Composite where
32− show (T ct) = show ct
33− show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
34− show (STRUCT xs) = "STRUCT " ++ show xs
35− show (UNION xs) = "UNION " ++ show xs
36− show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
32+ showPrec d (T ct) = showPrec d ct
33+ showPrec d (ARRAY n t) = showCon d "ARRAY" $ showArg n ++ showArg t
34+ showPrec d (STRUCT xs) = showCon d "STRUCT" $ showArg xs
35+ showPrec d (UNION xs) = showCon d "UNION" $ showArg xs
36+ showPrec d (PACKEDSTRUCT xs) = showCon d "PACKEDSTRUCT" $ showArg xs
3737
3838||| What Idris type the C type is marshalled to
3939translate : CType -> Type
libs/contrib/Data/ZZ.idr+2−2
@@ -24,8 +24,8 @@ absZ (Pos n) = n
2424absZ (NegS n) = S n
2525
2626implementation Show ZZ where
27− show (Pos n) = show n
28− show (NegS n) = "-" ++ show (S n)
27+ showPrec d (Pos n) = showPrec d n
28+ showPrec d (NegS n) = showParens (d >= PrefixMinus) $ "-" ++ showPrec PrefixMinus (S n)
2929
3030negNat : Nat -> ZZ
3131negNat Z = Pos Z
libs/contrib/Text/Literate.idr+4−4
@@ -42,10 +42,10 @@ data Token = CodeBlock String String String
4242 | Any String
4343 | CodeLine String String
4444
45−Show (Token) where
46− show (CodeBlock l r x) = unwords ["CodeBlock", show (l,r), show x]
47− show (Any x) = unwords ["Any", show x]
48− show (CodeLine m x) = unwords ["CodeLine", show m, show x]
45+Show Token where
46+ showPrec d (CodeBlock l r x) = showCon d "CodeBlock" $ showArg l ++ showArg r ++ showArg x
47+ showPrec d (Any x) = showCon d "Any" $ showArg x
48+ showPrec d (CodeLine m x) = showCon d "CodeLine" $ showArg m ++ showArg x
4949
5050rawTokens : (delims : List (String, String))
5151 -> (markers : List String)
libs/effects/Effect/Logging/Level.idr+9−9
@@ -58,15 +58,15 @@ implementation Cast (LogLevel n) Nat where
5858 cast {n} _ = n
5959
6060implementation Show (LogLevel n) where
61− show OFF = "OFF"
62− show TRACE = "TRACE"
63− show DEBUG = "DEBUG"
64− show INFO = "INFO"
65− show WARN = "WARN"
66− show FATAL = "FATAL"
67− show ERROR = "ERROR"
68− show ALL = "ALL"
69− show (CUSTOM n) = unwords ["CUSTOM", show n]
61+ showPrec d OFF = "OFF"
62+ showPrec d TRACE = "TRACE"
63+ showPrec d DEBUG = "DEBUG"
64+ showPrec d INFO = "INFO"
65+ showPrec d WARN = "WARN"
66+ showPrec d FATAL = "FATAL"
67+ showPrec d ERROR = "ERROR"
68+ showPrec d ALL = "ALL"
69+ showPrec d (CUSTOM n) = showCon d "CUSTOM" $ showArg n
7070
7171implementation Eq (LogLevel n) where
7272 (==) x y = lvlEq x y
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2
@@ -130,8 +130,8 @@ getElimTy info ctors =
130130data ElimArg = IHArgument TTName | NormalArgument TTName
131131
132132implementation Show ElimArg where
133− show (IHArgument x) = "IHArgument " ++ show x
134− show (NormalArgument x) = "NormalArgument " ++ show x
133+ showPrec d (IHArgument x) = showCon d "IHArgument" $ showArg x
134+ showPrec d (NormalArgument x) = showCon d "NormalArgument" $ showArg x
135135
136136getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
137137 (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)