3dff1b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2305 from Melvar/showprec

Add showPrec to Show

commit3dff1b5fc70209a419d42592d607960480fd5dcd authorDavid Christiansen <david@davidchristiansen.dk> dateSat 23 May 2015, 16:15 (11 years ago) parent22c8cda 1fec4fa

8 files changed+316−204

compare with master

unifiedsplit

CHANGELOG+6 libs/base/Data/Complex.idr+3−1 libs/base/Language/Reflection/Utils.idr+113−97 libs/contrib/Data/Heap.idr+2−2 libs/prelude/Prelude.idr+1−100 libs/prelude/Prelude/Show.idr+187 libs/prelude/prelude.ipkg+1−1 test/quasiquote001/expected+3−3

CHANGELOG+6

@@ -1,3 +1,9 @@

1+New in 0.9.19:

2+--------------

3+* The Show class has been moved into Prelude.Show and augmented with the method

4+ showPrec, which allows correct parenthesization of showed terms. This comes

5+ with the type Prec of precedences and a few helper functions.

17New in 0.9.18:

28--------------

39* GHC 7.10 compatibility

libs/base/Data/Complex.idr+3−1

@@ -22,7 +22,9 @@ instance Eq a => Eq (Complex a) where

2222 (==) a b = realPart a == realPart b && imagPart a == imagPart b

2323

2424instance Show a => Show (Complex a) where

25− show (r:+i) = "("++show r++":+"++show i++")"

25+ showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i

26+ where plus_i : Prec

27+ plus_i = User 6

2628

2729

2830

libs/base/Language/Reflection/Utils.idr+113−97

@@ -64,23 +64,23 @@ binderTy (PVTy t) = t

6464

6565mutual

6666 instance Show SpecialName where

67− show (WhereN i n1 n2) = "(WhereN " ++ show i ++ " " ++

68− show n1 ++ " " ++ show n2 ++ ")"

69− show (WithN i n) = "(WithN " ++ show i ++ " " ++ show n ++ ")"

70− show (InstanceN i ss) = "(InstanceN " ++ show i ++ " " ++ show ss ++ ")"

71− show (ParentN n s) = "(ParentN " ++ show n ++ " " ++ show s ++ ")"

72− show (MethodN n) = "(MethodN " ++ show n ++ ")"

73− show (CaseN n) = "(CaseN " ++ show n ++ ")"

74− show (ElimN n) = "(ElimN " ++ show n ++ ")"

75− show (InstanceCtorN n) = "(InstanceCtorN " ++ show n ++ ")"

76− show (MetaN parent meta) = "(MetaN " ++ show parent ++ " " ++ show meta ++ ")"

67+ showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++

68+ showArg n1 ++ showArg n2

69+ showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n

70+ showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss

71+ showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s

72+ showPrec d (MethodN n) = showCon d "MethodN" $ showArg n

73+ showPrec d (CaseN n) = showCon d "CaseN" $ showArg n

74+ showPrec d (ElimN n) = showCon d "ElimN" $ showArg n

75+ showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n

76+ showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta

7777

7878 instance Show TTName where

79− show (UN str) = "(UN " ++ show str ++ ")"

80− show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"

81− show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"

82− show (SN sn) = "(SN " ++ assert_total (show sn) ++ ")"

83− show NErased = "NErased"

79+ showPrec d (UN str) = showCon d "UN" $ showArg str

80+ showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns

81+ showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str

82+ showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)

83+ showPrec d NErased = "NErased"

8484

8585mutual

8686 instance Eq TTName where

@@ -104,28 +104,44 @@ mutual

104104 _ == _ = False

105105

106106instance Show TTUExp where

107− show (UVar i) = "(UVar " ++ show i ++ ")"

108− show (UVal i) = "(UVal " ++ show i ++ ")"

107+ showPrec d (UVar i) = showCon d "UVar" $ showArg i

108+ showPrec d (UVal i) = showCon d "UVal" $ showArg i

109109

110110instance Eq TTUExp where

111111 (UVar i) == (UVar j) = i == j

112112 (UVal i) == (UVal j) = i == j

113113 x == y = False

114114

115+instance Show NativeTy where

116+ show IT8 = "IT8"

117+ show IT16 = "IT16"

118+ show IT32 = "IT32"

119+ show IT64 = "IT64"

120+

121+instance Show IntTy where

122+ showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t

123+ showPrec d ITNative = "ITNative"

124+ showPrec d ITBig = "ITBig"

125+ showPrec d ITChar = "ITChar"

126+

127+instance Show ArithTy where

128+ showPrec d (ATInt t) = showCon d "ATInt" $ showArg t

129+ showPrec d ATFloat = "ATFloat"

130+

115131instance Show Const where

116− show (I i) = "(I " ++ show i ++ ")"

117− show (BI n) = "(BI " ++ show n ++ ")"

118− show (Fl f) = "(Fl " ++ show f ++ ")"

119− show (Ch c) = "(Ch " ++ show c ++ ")"

120− show (Str str) = "(Str " ++ show str ++ ")"

121− show (B8 b) = "(B8 ...)"

122− show (B16 b) = "(B16 ...)"

123− show (B32 b) = "(B32 ...)"

124− show (B64 b) = "(B64 ...)"

125− show (AType x) = "(AType ...)"

126− show StrType = "StrType"

127− show VoidType = "VoidType"

128− show Forgot = "Forgot"

132+ showPrec d (I i) = showCon d "I" $ showArg i

133+ showPrec d (BI n) = showCon d "BI" $ showArg n

134+ showPrec d (Fl f) = showCon d "Fl" $ showArg f

135+ showPrec d (Ch c) = showCon d "Ch" $ showArg c

136+ showPrec d (Str str) = showCon d "Str" $ showArg str

137+ showPrec d (B8 b) = showCon d "B8" $ showArg b

138+ showPrec d (B16 b) = showCon d "B16" $ showArg b

139+ showPrec d (B32 b) = showCon d "B32" $ showArg b

140+ showPrec d (B64 b) = showCon d "B64" $ showArg b

141+ showPrec d (AType x) = showCon d "AType" $ showArg x

142+ showPrec d StrType = "StrType"

143+ showPrec d VoidType = "VoidType"

144+ showPrec d Forgot = "Forgot"

129145

130146instance Eq NativeTy where

131147 IT8 == IT8 = True

@@ -164,10 +180,10 @@ instance Eq Const where

164180

165181

166182instance Show NameType where

167− show Bound = "Bound"

168− show Ref = "Ref"

169− show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"

170− show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"

183+ showPrec d Bound = "Bound"

184+ showPrec d Ref = "Ref"

185+ showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar

186+ showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar

171187

172188instance Eq NameType where

173189 Bound == Bound = True

@@ -177,15 +193,15 @@ instance Eq NameType where

177193 x == y = False

178194

179195instance (Show a) => Show (Binder a) where

180− show (Lam t) = "(Lam " ++ show t ++ ")"

181− show (Pi t _) = "(Pi " ++ show t ++ ")"

182− show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"

183− show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"

184− show (Hole t) = "(Hole " ++ show t ++ ")"

185− show (GHole t) = "(GHole " ++ show t ++ ")"

186− show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"

187− show (PVar t) = "(PVar " ++ show t ++ ")"

188− show (PVTy t) = "(PVTy " ++ show t ++ ")"

196+ showPrec d (Lam t) = showCon d "Lam" $ showArg t

197+ showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2

198+ showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2

199+ showPrec d (NLet t1 t2) = showCon d "NLet" $ showArg t1 ++ showArg t2

200+ showPrec d (Hole t) = showCon d "Hole" $ showArg t

201+ showPrec d (GHole t) = showCon d "GHole" $ showArg t

202+ showPrec d (Guess t1 t2) = showCon d "Guess" $ showArg t1 ++ showArg t2

203+ showPrec d (PVar t) = showCon d "PVar" $ showArg t

204+ showPrec d (PVTy t) = showCon d "PVTy" $ showArg t

189205

190206instance (Eq a) => Eq (Binder a) where

191207 (Lam t) == (Lam t') = t == t'

@@ -200,17 +216,17 @@ instance (Eq a) => Eq (Binder a) where

200216 x == y = False

201217

202218instance Show TT where

203− show = my_show

204− where %assert_total my_show : TT -> String

205− my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"

206− my_show (V i) = "(V " ++ show i ++ ")"

207− my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"

208− my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"

209− my_show (TConst c) = "(TConst " ++ show c ++ ")"

210− my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"

211− my_show Erased = "Erased"

212− my_show Impossible = "Impossible"

213− my_show (TType u) = "(TType " ++ show u ++ ")"

219+ showPrec = my_show

220+ where %assert_total my_show : Prec -> TT -> String

221+ my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t

222+ my_show d (V i) = showCon d "V" $ showArg i

223+ my_show d (Bind n b t) = showCon d "Bind" $ showArg n ++ showArg b ++ showArg t

224+ my_show d (App t1 t2) = showCon d "App" $ showArg t1 ++ showArg t2

225+ my_show d (TConst c) = showCon d "TConst" $ showArg c

226+ my_show d (Proj tm i) = showCon d "Proj" $ showArg tm ++ showArg i

227+ my_show d Erased = "Erased"

228+ my_show d Impossible = "Impossible"

229+ my_show d (TType u) = showCon d "TType" $ showArg u

214230

215231instance Eq TT where

216232 a == b = equalp a b

@@ -251,53 +267,53 @@ forget tm = fe [] tm

251267 fe env Impossible = Nothing

252268

253269instance Show Raw where

254− show r = my_show r

255− where %assert_total my_show : Raw -> String

256− my_show (Var n) = "(Var " ++ show n ++ ")"

257− my_show (RBind n b tm) = "(RBind " ++ show n ++ " " ++ show b ++ " " ++ my_show tm ++ ")"

258− my_show (RApp tm tm') = "(RApp " ++ my_show tm ++ " " ++ my_show tm' ++ ")"

259− my_show RType = "RType"

260− my_show (RForce tm) = "(RForce " ++ my_show tm ++ ")"

261− my_show (RConstant c) = "(RConstant " ++ show c ++ ")"

270+ showPrec = my_show

271+ where %assert_total my_show : Prec -> Raw -> String

272+ my_show d (Var n) = showCon d "Var" $ showArg n

273+ my_show d (RBind n b tm) = showCon d "RBind" $ showArg n ++ showArg b ++ " " ++ my_show App tm

274+ my_show d (RApp tm tm') = showCon d "RApp" $ " " ++ my_show App tm ++ " " ++ my_show App tm'

275+ my_show d RType = "RType"

276+ my_show d (RForce tm) = showCon d "RForce" $ " " ++ my_show App tm

277+ my_show d (RConstant c) = showCon d "RConstant" $ showArg c

262278

263279instance Show SourceLocation where

264− show (FileLoc filename line col) = "FileLoc \"" ++ filename ++ "\" " ++ show line ++ " " ++ show col

280+ showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col

265281

266282instance Show Err where

267− show (Msg x) = "Msg \"" ++ x ++ "\""

268− show (InternalMsg x) = "InternalMsg \"" ++ x ++ "\""

269− show (CantUnify x tm tm' err xs y) = "CantUnify " ++ show x ++

270− " ( " ++ show tm ++ ") (" ++ show tm' ++ ") (" ++ show err ++ ") " ++

271− show xs ++ " " ++ show y

272− show (InfiniteUnify n tm xs) = "InfiniteUnify " ++ show n ++ show tm ++ show xs

273− show (CantConvert tm tm' xs) = "CantConvert " ++ show tm ++ show tm' ++ show xs

274− show (CantSolveGoal tm ctxt) = "CantSolveGoal " ++ show tm ++ " " ++ show ctxt

275− show (UnifyScope n n' tm xs) = "UnifyScope " ++ show n ++ " " ++ show n' ++ " " ++ show tm ++ " " ++ show xs

276− show (CantInferType x) = "CantInferType " ++ show x

277− show (NonFunctionType tm tm') = "NonFunctionType " ++ show tm ++ show tm'

278− show (NotEquality tm tm') = "NotEquality " ++ show tm ++ " " ++ show tm'

279− show (TooManyArguments n) = "TooManyArguments " ++ show n

280− show (CantIntroduce tm) = "CantIntroduce " ++ show tm

281− show (NoSuchVariable n) = "NoSuchVariable " ++ show n

282− show (WithFnType tm) = "WithFnType " ++ show tm

283− show (CantMatch tm) = "CantMatch " ++ show tm

284− show (NoTypeDecl n) = "NoTypeDecl " ++ show n

285− show (NotInjective tm tm' x) = "NotInjective " ++ show tm ++ " " ++ show tm'

286− show (CantResolve tm) = "CantResolve " ++ show tm

287− show (InvalidTCArg n tm) = "InvalidTCName " ++ show n ++ " (" ++ show tm ++ ")"

288− show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

289− show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

290− show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

291− show UniverseError = "UniverseError"

292− show ProgramLineComment = "ProgramLineComment"

293− show (Inaccessible n) = "Inaccessible " ++ show n

294− show (UnknownImplicit n f) = "UnknownImplicit " ++ show n ++ " " ++ show f

295− show (NonCollapsiblePostulate n) = "NonCollapsiblePostulate " ++ show n

296− show (AlreadyDefined n) = "AlreadyDefined " ++ show n

297− show (ProofSearchFail err) = "ProofSearchFail " ++ show err

298− show (NoRewriting tm) = "NoRewriting " ++ show tm

299− show (ProviderError x) = "ProviderError \"" ++ show x ++ "\""

300− show (LoadingFailed x err) = "LoadingFailed " ++ show x ++ " (" ++ show err ++ ")"

283+ showPrec d (Msg x) = showCon d "Msg" $ showArg x

284+ showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x

285+ showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++

286+ showArg tm ++ showArg tm' ++ showArg err ++

287+ showArg xs ++ showArg y

288+ showPrec d (InfiniteUnify n tm xs) = showCon d "InfiniteUnify" $ showArg n ++ showArg tm ++ showArg xs

289+ showPrec d (CantConvert tm tm' xs) = showCon d "CantConvert" $ showArg tm ++ showArg tm' ++ showArg xs

290+ showPrec d (CantSolveGoal tm ctxt) = showCon d "CantSolveGoal" $ showArg tm ++ showArg ctxt

291+ showPrec d (UnifyScope n n' tm xs) = showCon d "UnifyScope" $ showArg n ++ showArg n' ++ showArg tm ++ showArg xs

292+ showPrec d (CantInferType x) = showCon d "CantInferType" $ showArg x

293+ showPrec d (NonFunctionType tm tm') = showCon d "NonFunctionType" $ showArg tm ++ showArg tm'

294+ showPrec d (NotEquality tm tm') = showCon d "NotEquality" $ showArg tm ++ showArg tm'

295+ showPrec d (TooManyArguments n) = showCon d "TooManyArguments" $ showArg n

296+ showPrec d (CantIntroduce tm) = showCon d "CantIntroduce" $ showArg tm

297+ showPrec d (NoSuchVariable n) = showCon d "NoSuchVariable" $ showArg n

298+ showPrec d (WithFnType tm) = showCon d "WithFnType" $ showArg tm

299+ showPrec d (CantMatch tm) = showCon d "CantMatch" $ showArg tm

300+ showPrec d (NoTypeDecl n) = showCon d "NoTypeDecl" $ showArg n

301+ showPrec d (NotInjective tm tm' x) = showCon d "NotInjective" $ showArg tm ++ showArg tm'

302+ showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm

303+ showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm

304+ showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

305+ showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

306+ showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm

307+ showPrec d UniverseError = "UniverseError"

308+ showPrec d ProgramLineComment = "ProgramLineComment"

309+ showPrec d (Inaccessible n) = showCon d "Inaccessible" $ showArg n

310+ showPrec d (UnknownImplicit n f) = showCon d "UnknownImplicit" $ showArg n ++ showArg f

311+ showPrec d (NonCollapsiblePostulate n) = showCon d "NonCollapsiblePostulate" $ showArg n

312+ showPrec d (AlreadyDefined n) = showCon d "AlreadyDefined" $ showArg n

313+ showPrec d (ProofSearchFail err) = showCon d "ProofSearchFail" $ showArg err

314+ showPrec d (NoRewriting tm) = showCon d "NoRewriting" $ showArg tm

315+ showPrec d (ProviderError x) = showCon d "ProviderError" $ showArg x

316+ showPrec d (LoadingFailed x err) = showCon d "LoadingFailed" $ showArg x ++ showArg err

301317

302318-------------------------

303319-- Idiom brackets for Raw

libs/contrib/Data/Heap.idr+2−2

@@ -114,8 +114,8 @@ sort = Heap.toList . Heap.fromList

114114--------------------------------------------------------------------------------

115115

116116instance Show a => Show (MaxiphobicHeap a) where

117− show Empty = "Empty"

118− show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"

117+ showPrec d Empty = "Empty"

118+ showPrec d (Node s l e r) = showCon d "Node" $ " _" ++ showArg l ++ showArg e ++ showArg r

119119

120120instance Eq a => Eq (MaxiphobicHeap a) where

121121 Empty == Empty = True

libs/prelude/Prelude.idr+1−100

@@ -24,6 +24,7 @@ import public Prelude.Uninhabited

2424import public Prelude.Pairs

2525import public Prelude.Stream

2626import public Prelude.Providers

27+import public Prelude.Show

2728import public Decidable.Equality

2829import public Language.Reflection

2930import public Language.Reflection.Errors

@@ -37,106 +38,6 @@ decAsBool (Yes _) = True

3738decAsBool (No _) = False

3839

3940

40−-- Show and instances

41−

42−class Show a where

43− partial show : a -> String

44−

45−instance Show Int where

46− show = prim__toStrInt

47−

48−instance Show Integer where

49− show = prim__toStrBigInt

50−

51−instance Show Float where

52− show = prim__floatToStr

53−

54−

55−firstCharIs : (Char -> Bool) -> String -> Bool

56−firstCharIs p s with (strM s)

57− firstCharIs p "" | StrNil = False

58− firstCharIs p (strCons c cs) | StrCons c cs = p c

59−

60−protectEsc : (Char -> Bool) -> String -> String -> String

61−protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s

62−

63−showLitChar : Char -> String -> String

64−showLitChar '\a' = ("\\a" ++)

65−showLitChar '\b' = ("\\b" ++)

66−showLitChar '\f' = ("\\f" ++)

67−showLitChar '\n' = ("\\n" ++)

68−showLitChar '\r' = ("\\r" ++)

69−showLitChar '\t' = ("\\t" ++)

70−showLitChar '\v' = ("\\v" ++)

71−showLitChar '\SO' = protectEsc (== 'H') "\\SO"

72−showLitChar '\DEL' = ("\\DEL" ++)

73−showLitChar '\\' = ("\\\\" ++)

74−showLitChar c = case getAt (cast (cast {to=Int} c)) asciiTab of

75− Just k => strCons '\\' . (k ++)

76− Nothing => if (c > '\DEL')

77− then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))

78− else strCons c

79− where asciiTab : List String

80− asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",

81− "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",

82− "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",

83− "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]

84−

85− getAt : Nat -> List String -> Maybe String

86− getAt Z (x :: xs) = Just x

87− getAt (S k) (x :: xs) = getAt k xs

88− getAt _ [] = Nothing

89−

90−showLitString : List Char -> String -> String

91−showLitString [] = id

92−showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs

93−showLitString (c ::cs) = showLitChar c . showLitString cs

94−

95−instance Show Char where

96− show '\'' = "'\\''"

97− show c = strCons '\'' (showLitChar c "'")

98−

99−instance Show String where

100− show cs = strCons '"' (showLitString (cast cs) "\"")

101−

102−instance Show Nat where

103− show n = show (the Integer (cast n))

104−

105−instance Show Bool where

106− show True = "True"

107− show False = "False"

108−

109−instance Show () where

110− show () = "()"

111−

112−instance Show Bits8 where

113− show b = b8ToString b

114−

115−instance Show Bits16 where

116− show b = b16ToString b

117−

118−instance Show Bits32 where

119− show b = b32ToString b

120−

121−instance Show Bits64 where

122− show b = b64ToString b

123−

124−instance (Show a, Show b) => Show (a, b) where

125− show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

126−

127−instance Show a => Show (List a) where

128− show xs = "[" ++ show' "" xs ++ "]" where

129− show' acc [] = acc

130− show' acc [x] = acc ++ show x

131− show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

132−

133−instance Show a => Show (Maybe a) where

134− show Nothing = "Nothing"

135− show (Just x) = "Just " ++ show x

136−

137−instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

138− show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

139−

14041---- Functor instances

14142

14243instance Functor PrimIO where

libs/prelude/Prelude/Show.idrnew file+187

@@ -0,0 +1,187 @@

1+module Prelude.Show

3+import Builtins

5+import Prelude.Basics

6+import Prelude.Bits

7+import Prelude.Bool

8+import Prelude.Cast

9+import Prelude.Chars

10+import Prelude.Classes

11+import Prelude.List

12+import Prelude.Maybe

13+import Prelude.Nat

14+import Prelude.Strings

15+

16+%default total

17+

18+||| The precedence of an Idris operator or syntactic context.

20+

21+||| Gives the constructor index of the Prec as a helper for writing instances.

22+precCon : Prec -> Integer

23+precCon Open = 0

24+precCon Eq = 1

25+precCon Dollar = 2

26+precCon Backtick = 3

27+precCon (User n) = 4

28+precCon PrefixMinus = 5

29+precCon App = 6

30+

31+instance Eq Prec where

32+ (==) (User m) (User n) = m == n

33+ (==) x y = precCon x == precCon y

34+

35+instance Ord Prec where

36+ compare (User m) (User n) = compare m n

37+ compare x y = compare (precCon x) (precCon y)

38+

39+||| Things that have a canonical `String` representation.

40+class Show a where

41+ ||| Convert a value to its `String` representation.

42+ |||

43+ ||| @ a the value to convert

44+ partial

45+ show : (x : a) -> String

46+ show = showPrec Open

47+

48+ ||| Convert a value to its `String` representation in a certain precedence

49+ ||| context.

50+ |||

51+ ||| A value should produce parentheses around itself if and only if the given

52+ ||| precedence context is greater than or equal to the precedence of the

53+ ||| outermost operation represented in the produced `String`. *This is

54+ ||| different from Haskell*, which requires it to be strictly greater. `Open`

55+ ||| should thus always produce *no* outermost parens, `App` should always

56+ ||| produce outermost parens except on atomic values and those that provide

57+ ||| their own bracketing, like `Pair` and `List`.

58+ |||

59+ ||| @ d the precedence context.

60+ ||| @ a the value to convert

61+ partial

62+ showPrec : (d : Prec) -> (x : a) -> String

63+ showPrec _ = show

64+

65+||| Surround a `String` with parentheses depending on a condition.

66+|||

67+||| @ b whether to add parentheses

68+showParens : (b : Bool) -> String -> String

69+showParens False s = s

70+showParens True s = "(" ++ s ++ ")"

71+

72+||| A helper for the common case of showing a non-infix constructor with at

73+||| least one argument, for use with `showArg`.

74+|||

75+||| Apply `showCon` to the precedence context, the constructor name, and the

76+||| args shown with `showArg` and concatenated. Example:

77+||| ```

78+||| data Ann a = MkAnn String a

79+|||

80+||| instance Show a => Show (Ann a) where

81+||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x

82+||| ```

83+showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String

84+showCon d conName shownArgs = showParens (d >= App) $ conName ++ shownArgs

85+

86+||| A helper for the common case of showing a non-infix constructor with at

87+||| least one argument, for use with `showCon`.

88+|||

89+||| This adds a space to the front so the results can be directly

90+||| concatenated. See `showCon` for details and an example.

91+showArg : Show a => (x : a) -> String

92+showArg x = " " ++ showPrec App x

93+

94+instance Show Int where

95+ show = prim__toStrInt

96+

97+instance Show Integer where

98+ show = prim__toStrBigInt

99+

100+instance Show Double where

101+ show = prim__floatToStr

102+

103+firstCharIs : (Char -> Bool) -> String -> Bool

104+firstCharIs p s with (strM s)

105+ firstCharIs p "" | StrNil = False

106+ firstCharIs p (strCons c cs) | StrCons c cs = p c

107+

108+protectEsc : (Char -> Bool) -> String -> String -> String

109+protectEsc p f s = f ++ (if firstCharIs p s then "\\&" else "") ++ s

110+

111+showLitChar : Char -> String -> String

112+showLitChar '\a' = ("\\a" ++)

113+showLitChar '\b' = ("\\b" ++)

114+showLitChar '\f' = ("\\f" ++)

115+showLitChar '\n' = ("\\n" ++)

116+showLitChar '\r' = ("\\r" ++)

117+showLitChar '\t' = ("\\t" ++)

118+showLitChar '\v' = ("\\v" ++)

119+showLitChar '\SO' = protectEsc (== 'H') "\\SO"

120+showLitChar '\DEL' = ("\\DEL" ++)

121+showLitChar '\\' = ("\\\\" ++)

122+showLitChar c = case getAt (cast (cast {to=Int} c)) asciiTab of

123+ Just k => strCons '\\' . (k ++)

124+ Nothing => if (c > '\DEL')

125+ then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))

126+ else strCons c

127+ where asciiTab : List String

128+ asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",

129+ "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",

130+ "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",

131+ "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]

132+

133+ getAt : Nat -> List String -> Maybe String

134+ getAt Z (x :: xs) = Just x

135+ getAt (S k) (x :: xs) = getAt k xs

136+ getAt _ [] = Nothing

137+

138+showLitString : List Char -> String -> String

139+showLitString [] = id

140+showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs

141+showLitString (c ::cs) = showLitChar c . showLitString cs

142+

143+instance Show Char where

144+ show '\'' = "'\\''"

145+ show c = strCons '\'' (showLitChar c "'")

146+

147+instance Show String where

148+ show cs = strCons '"' (showLitString (cast cs) "\"")

149+

150+instance Show Nat where

151+ show n = show (the Integer (cast n))

152+

153+instance Show Bool where

154+ show True = "True"

155+ show False = "False"

156+

157+instance Show () where

158+ show () = "()"

159+

160+instance Show Bits8 where

161+ show b = b8ToString b

162+

163+instance Show Bits16 where

164+ show b = b16ToString b

165+

166+instance Show Bits32 where

167+ show b = b32ToString b

168+

169+instance Show Bits64 where

170+ show b = b64ToString b

171+

172+instance (Show a, Show b) => Show (a, b) where

173+ show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

174+

175+instance Show a => Show (List a) where

176+ show xs = "[" ++ show' "" xs ++ "]" where

177+ show' acc [] = acc

178+ show' acc [x] = acc ++ show x

179+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

180+

181+instance Show a => Show (Maybe a) where

182+ showPrec d Nothing = "Nothing"

183+ showPrec d (Just x) = showCon d "Just" $ showArg x

184+

185+instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

186+ show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

187+

libs/prelude/prelude.ipkg+1−1

@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO,

66 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

77 Prelude.Classes, Prelude.Nat, Prelude.List,

88 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

9− Prelude.Strings, Prelude.Chars, Prelude.Functor,

9+ Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

1111 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

1212

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−(App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1))))))

1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))

22--------------

3−(App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27)))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))

44--------------

5−(App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1))) (Bind (UN "a") (Pi (V 1)) (Bind (UN "b") (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24))))

5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))