git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3993 from Melvar/standard-shows
385cf27Niklas Larsson
libs/contrib/CFFI/Types.idr+5−5
compare with master
unifiedsplit
@@ -29,11 +29,11 @@ Show CType where
29 show PTR = "PTR"
29 show PTR = "PTR"
30
30
31Show Composite where
31Show Composite where
32− show (T ct) = show ct
32+ showPrec d (T ct) = showPrec d ct
33− show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
33+ showPrec d (ARRAY n t) = showCon d "ARRAY" $ showArg n ++ showArg t
34− show (STRUCT xs) = "STRUCT " ++ show xs
34+ showPrec d (STRUCT xs) = showCon d "STRUCT" $ showArg xs
35− show (UNION xs) = "UNION " ++ show xs
35+ showPrec d (UNION xs) = showCon d "UNION" $ showArg xs
36− show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
36+ showPrec d (PACKEDSTRUCT xs) = showCon d "PACKEDSTRUCT" $ showArg xs
37
37
38||| What Idris type the C type is marshalled to
38||| What Idris type the C type is marshalled to
39translate : CType -> Type
39translate : CType -> Type
libs/contrib/Data/ZZ.idr+2−2
@@ -24,8 +24,8 @@ absZ (Pos n) = n
24absZ (NegS n) = S n
24absZ (NegS n) = S n
25
25
26implementation Show ZZ where
26implementation Show ZZ where
27− show (Pos n) = show n
27+ showPrec d (Pos n) = showPrec d n
28− show (NegS n) = "-" ++ show (S n)
28+ showPrec d (NegS n) = showParens (d >= PrefixMinus) $ "-" ++ showPrec PrefixMinus (S n)
29
29
30negNat : Nat -> ZZ
30negNat : Nat -> ZZ
31negNat Z = Pos Z
31negNat Z = Pos Z
libs/contrib/Text/Literate.idr+4−4
@@ -42,10 +42,10 @@ data Token = CodeBlock String String String
42 | Any String
42 | Any String
43 | CodeLine String String
43 | CodeLine String String
44
44
45−Show (Token) where
45+Show Token where
46− show (CodeBlock l r x) = unwords ["CodeBlock", show (l,r), show x]
46+ showPrec d (CodeBlock l r x) = showCon d "CodeBlock" $ showArg l ++ showArg r ++ showArg x
47− show (Any x) = unwords ["Any", show x]
47+ showPrec d (Any x) = showCon d "Any" $ showArg x
48− show (CodeLine m x) = unwords ["CodeLine", show m, show x]
48+ showPrec d (CodeLine m x) = showCon d "CodeLine" $ showArg m ++ showArg x
49
49
50rawTokens : (delims : List (String, String))
50rawTokens : (delims : List (String, String))
51 -> (markers : List String)
51 -> (markers : List String)
libs/effects/Effect/Logging/Level.idr+9−9
@@ -58,15 +58,15 @@ implementation Cast (LogLevel n) Nat where
58 cast {n} _ = n
58 cast {n} _ = n
59
59
60implementation Show (LogLevel n) where
60implementation Show (LogLevel n) where
61− show OFF = "OFF"
61+ showPrec d OFF = "OFF"
62− show TRACE = "TRACE"
62+ showPrec d TRACE = "TRACE"
63− show DEBUG = "DEBUG"
63+ showPrec d DEBUG = "DEBUG"
64− show INFO = "INFO"
64+ showPrec d INFO = "INFO"
65− show WARN = "WARN"
65+ showPrec d WARN = "WARN"
66− show FATAL = "FATAL"
66+ showPrec d FATAL = "FATAL"
67− show ERROR = "ERROR"
67+ showPrec d ERROR = "ERROR"
68− show ALL = "ALL"
68+ showPrec d ALL = "ALL"
69− show (CUSTOM n) = unwords ["CUSTOM", show n]
69+ showPrec d (CUSTOM n) = showCon d "CUSTOM" $ showArg n
70
70
71implementation Eq (LogLevel n) where
71implementation Eq (LogLevel n) where
72 (==) x y = lvlEq x y
72 (==) x y = lvlEq x y
libs/pruviloj/Pruviloj/Derive/Eliminators.idr+2−2
@@ -130,8 +130,8 @@ getElimTy info ctors =
130data ElimArg = IHArgument TTName | NormalArgument TTName
130data ElimArg = IHArgument TTName | NormalArgument TTName
131
131
132implementation Show ElimArg where
132implementation Show ElimArg where
133− show (IHArgument x) = "IHArgument " ++ show x
133+ showPrec d (IHArgument x) = showCon d "IHArgument" $ showArg x
134− show (NormalArgument x) = "NormalArgument " ++ show x
134+ showPrec d (NormalArgument x) = showCon d "NormalArgument" $ showArg x
135
135
136getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
136getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
137 (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)
137 (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)