8c64e9c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Got pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!

8c64e9cDominic Mulligan15 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -67,7 +67,7 @@ Executable idris

68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

69 containers, process, transformers, filepath, directory,

70− binary, bytestring, epic>=0.9.3

70+ binary, bytestring, epic>=0.9.3, pretty

72 Extensions: MultiParamTypeClasses, FunctionalDependencies,

73 FlexibleInstances, TemplateHaskell

src/Core/Elaborate.hs+6−1

@@ -21,6 +21,8 @@ import Data.Char

21import Data.List

22import Debug.Trace

24+import Util.Pretty

25+

24-- I don't really want this here, but it's useful for the test shell

26-- I don't really want this here, but it's useful for the test shell

25data Command = Theorem Name Raw

27data Command = Theorem Name Raw

26 | Eval Raw

28 | Eval Raw

@@ -29,7 +31,10 @@ data Command = Theorem Name Raw

29 | Tac (Elab ())

31 | Tac (Elab ())

31data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

33data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

32− deriving Show

34+

35+instance Pretty aux => Pretty (ElabState aux) where

36+ pretty (ES (pState, aux) str _) = text "test"

37+

33type Elab' aux a = StateT (ElabState aux) TC a

38type Elab' aux a = StateT (ElabState aux) TC a

34type Elab a = Elab' () a

39type Elab a = Elab' () a

src/Core/ProofShell.hs+4−2

@@ -11,6 +11,8 @@ import Core.Elaborate

11import Control.Monad.State

12import System.Console.Haskeline

14+import Util.Pretty

15+

14data ShellState = ShellState

16data ShellState = ShellState

15 { ctxt :: Context,

17 { ctxt :: Context,

16 prf :: Maybe ProofState,

18 prf :: Maybe ProofState,

@@ -50,13 +52,13 @@ processCommand (Tac e) state

50 (pterm ps')

52 (pterm ps')

51 (ptype ps')

53 (ptype ps')

52 (context ps') }, resp)

54 (context ps') }, resp)

53− err -> (state, show err)

55+ err -> (state, show . render . pretty $ err)

54 | otherwise = (state, "No proof in progress")

56 | otherwise = (state, "No proof in progress")

56runShell :: ShellState -> InputT IO ShellState

58runShell :: ShellState -> InputT IO ShellState

57runShell st = do (prompt, parser) <-

59runShell st = do (prompt, parser) <-

58 maybe (return ("TT# ", parseCommand))

60 maybe (return ("TT# ", parseCommand))

59− (\st -> do outputStrLn (show st)

61+ (\st -> do outputStrLn . render . pretty $ st

60 return (show (thname st) ++ "# ", parseTactic))

62 return (show (thname st) ++ "# ", parseTactic))

61 (prf st)

63 (prf st)

62 x <- getInputLine prompt

64 x <- getInputLine prompt

src/Core/ProofState.hs+42−1

@@ -13,10 +13,12 @@ import Core.TT

13import Core.Unify

15import Control.Monad.State

16−import Control.Applicative

16+import Control.Applicative hiding (empty)

17import Data.List

18import Debug.Trace

20+import Util.Pretty

21+

20data ProofState = PS { thname :: Name,

22data ProofState = PS { thname :: Name,

21 holes :: [Name], -- holes still to be solved

23 holes :: [Name], -- holes still to be solved

22 nextname :: Int, -- name supply

24 nextname :: Int, -- name supply

@@ -94,6 +96,45 @@ instance Show ProofState where

94 " =?= " ++ showEnv ps v

96 " =?= " ++ showEnv ps v

95 showG ps b = showEnv ps (binderTy b)

97 showG ps b = showEnv ps (binderTy b)

99+instance Pretty ProofState where

100+ pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =

101+ if size nm > breakingSize then

102+ pretty nm <> colon $$ nest nestingSize (text " no more goals.")

103+ else

104+ pretty nm <> colon <+> text " no more goals."

105+ pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =

106+ let OK g = goal (Just h) tm in

107+ let wkEnv = premises g in

108+ text "Other goals" <+> colon <+> pretty hs $$

109+ prettyPs wkEnv (reverse wkEnv) $$

110+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$

111+ pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

112+ where

113+ prettyGoal ps (Guess t v) =

114+ if size v > breakingSize then

115+ prettyEnv ps t <+> text "=?=" $$

116+ nest nestingSize (prettyEnv ps v)

117+ else

118+ prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

119+ prettyGoal ps b = prettyEnv ps $ binderTy b

120+

121+ prettyPs env [] = empty

122+ prettyPs env ((n, Let t v):bs) =

123+ nest nestingSize (pretty n <+> colon <+>

124+ if size v > breakingSize then

125+ prettyEnv env t <+> text "=" $$

126+ nest nestingSize (prettyEnv env v) $$

127+ nest nestingSize (prettyPs env bs)

128+ else

129+ prettyEnv env t <+> text "=" <+> prettyEnv env v $$

130+ nest nestingSize (prettyPs env bs))

131+ prettyPs env ((n, b):bs) =

132+ if size (binderTy b) > breakingSize then

133+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)

134+ else

135+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$

136+ nest nestingSize (prettyPs env bs))

137+

97same Nothing n = True

138same Nothing n = True

98same (Just x) n = x == n

139same (Just x) n = x == n

140

src/Core/TT.hs+142−1

@@ -1,4 +1,4 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, FlexibleInstances #-}

3module Core.TT where

@@ -36,6 +36,9 @@ data FC = FC { fc_fname :: String,

36deriving instance Binary FC

37!-}

39+instance Sized FC where

40+ size (FC f l) = 1 + length f

41+

39instance Show FC where

42instance Show FC where

40 show (FC f l) = f ++ ":" ++ show l

43 show (FC f l) = f ++ ":" ++ show l

@@ -50,6 +53,17 @@ data Err = Msg String

50 | At FC Err

53 | At FC Err

51 deriving Eq

54 deriving Eq

56+instance Sized Err where

57+ size (Msg msg) = length msg

58+ size (CantUnify left right err score) = size left + size right + size err

59+ size (NoSuchVariable name) = size name

60+ size (NotInjective l c r) = size l + size c + size r

61+ size (CantResolve trm) = size trm

62+ size (IncompleteTerm trm) = size trm

63+ size UniverseError = 1

64+ size ProgramLineComment = 1

65+ size (At fc err) = size fc + size err

66+

53score :: Err -> Int

67score :: Err -> Int

54score (CantUnify _ _ m s) = s + score m

68score (CantUnify _ _ m s) = s + score m

55score (CantResolve _) = 20

69score (CantResolve _) = 20

@@ -62,10 +76,30 @@ instance Show Err where

62 ++ show e ++ " " ++ show i

76 ++ show e ++ " " ++ show i

63 show _ = "Error"

77 show _ = "Error"

79+instance Pretty Err where

80+ pretty (Msg m) = text m

81+ pretty (CantUnify l r e i) =

82+ if size l + size r > breakingSize then

83+ text "Cannot unify" <+> colon $$

84+ nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

85+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

86+ else

87+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

88+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

89+ pretty _ = text "Error"

90+

65data TC a = OK a

91data TC a = OK a

66 | Error Err

92 | Error Err

67 deriving (Eq, Functor)

93 deriving (Eq, Functor)

95+instance Pretty a => Pretty (TC a) where

96+ pretty (OK ok) = pretty ok

97+ pretty (Error err) =

98+ if size err > breakingSize then

99+ text "Error" <+> colon $$ (nest nestingSize $ pretty err)

100+ else

101+ text "Error" <+> colon <+> pretty err

102+

69instance Show a => Show (TC a) where

103instance Show a => Show (TC a) where

70 show (OK x) = show x

104 show (OK x) = show x

71 show (Error str) = "Error: " ++ show str

105 show (Error str) = "Error: " ++ show str

@@ -120,6 +154,16 @@ data Name = UN String

120deriving instance Binary Name

154deriving instance Binary Name

121!-}

155!-}

122

156

157+instance Sized Name where

158+ size (UN n) = 1

159+ size (NS n els) = 1 + length els

160+ size (MN i n) = 1

161+

162+instance Pretty Name where

163+ pretty (UN n) = text n

164+ pretty (NS n s) = pretty n

165+ pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace

166+

123instance Show Name where

167instance Show Name where

124 show (UN n) = n

168 show (UN n) = n

125 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

169 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n

@@ -192,6 +236,23 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

192deriving instance Binary Const

236deriving instance Binary Const

193!-}

237!-}

194

238

239+instance Sized Const where

240+ size _ = 1

241+

242+instance Pretty Const where

243+ pretty (I i) = text . show $ i

244+ pretty (BI i) = text . show $ i

245+ pretty (Fl f) = text . show $ f

246+ pretty (Ch c) = text . show $ c

247+ pretty (Str s) = text s

248+ pretty IType = text "Int"

249+ pretty BIType = text "BigInt"

250+ pretty FlType = text "Float"

251+ pretty ChType = text "Char"

252+ pretty StrType = text "String"

253+ pretty PtrType = text "Ptr"

254+ pretty Forgot = text "Forgot"

255+

195data Raw = Var Name

256data Raw = Var Name

196 | RBind Name (Binder Raw) Raw

257 | RBind Name (Binder Raw) Raw

197 | RApp Raw Raw

258 | RApp Raw Raw

@@ -229,6 +290,17 @@ data Binder b = Lam { binderTy :: b }

229deriving instance Binary Binder

290deriving instance Binary Binder

230!-}

291!-}

231

292

293+instance Sized a => Sized (Binder a) where

294+ size (Lam ty) = 1 + size ty

295+ size (Pi ty) = 1 + size ty

296+ size (Let ty val) = 1 + size ty + size val

297+ size (NLet ty val) = 1 + size ty + size val

298+ size (Hole ty) = 1 + size ty

299+ size (GHole ty) = 1 + size ty

300+ size (Guess ty val) = 1 + size ty + size val

301+ size (PVar ty) = 1 + size ty

302+ size (PVTy ty) = 1 + size ty

303+

232fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

304fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

233fmapMB f (Let t v) = liftM2 Let (f t) (f v)

305fmapMB f (Let t v) = liftM2 Let (f t) (f v)

234fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

306fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

@@ -270,6 +342,9 @@ data UExp = UVar Int -- universe variable

270 | UVal Int -- explicit universe level

342 | UVal Int -- explicit universe level

271 deriving (Eq, Ord)

343 deriving (Eq, Ord)

272

344

345+instance Sized UExp where

346+ size _ = 1

347+

273-- We assume that universe levels have been checked, so anything external

348-- We assume that universe levels have been checked, so anything external

274-- can just have the same universe variable and we won't get any new

349-- can just have the same universe variable and we won't get any new

275-- cycles.

350-- cycles.

@@ -300,6 +375,12 @@ data NameType = Bound | Ref | DCon Int Int | TCon Int Int

300deriving instance Binary NameType

375deriving instance Binary NameType

301!-}

376!-}

302

377

378+instance Sized NameType where

379+ size _ = 1

380+

381+instance Pretty NameType where

382+ pretty = text . show

383+

303instance Eq NameType where

384instance Eq NameType where

304 Bound == Bound = True

385 Bound == Bound = True

305 Ref == Ref = True

386 Ref == Ref = True

@@ -319,6 +400,18 @@ data TT n = P NameType n (TT n) -- embed type

319deriving instance Binary TT

400deriving instance Binary TT

320!-}

401!-}

321

402

403+instance Sized a => Sized (TT a) where

404+ size (P name n trm) = 1 + size name + size n + size trm

405+ size (V v) = 1

406+ size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy

407+ size (App l r) = 1 + size l + size r

408+ size (Constant c) = size c

409+ size Erased = 1

410+ size (Set u) = 1 + size u

411+

412+instance Pretty a => Pretty (TT a) where

413+ pretty

414+

322type EnvTT n = [(n, Binder (TT n))]

415type EnvTT n = [(n, Binder (TT n))]

323

416

324data Datatype n = Data { d_typename :: n,

417data Datatype n = Data { d_typename :: n,

@@ -507,6 +600,54 @@ instance Show Const where

507showEnv env t = showEnv' env t False

600showEnv env t = showEnv' env t False

508showEnvDbg env t = showEnv' env t True

601showEnvDbg env t = showEnv' env t True

509

602

603+prettyEnv env t = prettyEnv' env t False

604+ where

605+ prettyEnv' env t dbg = prettySe 10 env t dbg

606+

607+ bracket outer inner p

608+ | inner > outer = lparen <> p <> rparen

609+ | otherwise = p

610+

611+ prettySe p env (P nt n t) debug =

612+ pretty n <+>

613+ if debug then

614+ lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack

615+ else

616+ empty

617+ prettySe p env (V i) debug

618+ | i < length env =

619+ if debug then

620+ text . show . fst $ env!!i

621+ else

622+ lbrack <+> text (show i) <+> rbrack

623+ | otherwise = text "unbound" <+> text (show i) <+> text "!"

624+ prettySe p env (Bind n b@(Pi t) sc) debug

625+ | noOccurrence n sc && not debug =

626+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

627+ prettySe p env (Bind n b sc) debug =

628+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

629+ prettySe p env (App f a) debug =

630+ bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

631+ prettySe p env (Constant c) debug = pretty c

632+ prettySe p env Erased debug = text "[_]"

633+ prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)

634+

635+ prettySb env n (Lam t) = prettyB env "λ" "=>" n t

636+ prettySb env n (Hole t) = prettyB env "?defer" "." n t

637+ prettySb env n (Pi t) = prettyB env "(" ") ->" n t

638+ prettySb env n (PVar t) = prettyB env "pat" "." n t

639+ prettySb env n (PVTy t) = prettyB env "pty" "." n t

640+ prettySb env n (Let t v) = prettyBv env "let" "in" n t v

641+ prettySb env n (Guess t v) = prettyBv env "??" "in" n t v

642+

643+ prettyB env op sc n t debug =

644+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc

645+

646+ prettyBv env op sc n t v debug =

647+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>

648+ prettySe 10 env v debug <> text sc

649+

650+

510showEnv' env t dbg = se 10 env t where

651showEnv' env t dbg = se 10 env t where

511 se p env (P nt n t) = show n

652 se p env (P nt n t) = show n

512 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

653 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

src/Idris/AbsSyntax.hs+37−3

@@ -5,7 +5,7 @@ module Idris.AbsSyntax where

6import Core.TT

7import Core.Evaluate

8−import Core.Elaborate

8+import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

11import System.Console.Haskeline

@@ -576,6 +576,26 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

576deriving instance Binary PTactic'

577!-}

578

579+instance Sized a => Sized (PTactic' a) where

580+ size (Intro nms) = 1 + size nms

581+ size Intros = 1

582+ size (Focus nm) = 1 + size nm

583+ size (Refine nm bs) = 1 + size nm + length bs

584+ size (Rewrite t) = 1 + size t

585+ size (LetTac nm t) = 1 + size nm + size t

586+ size (Exact t) = 1 + size t

587+ size Compute = 1

588+ size Trivial = 1

589+ size Solve = 1

590+ size Attack = 1

591+ size ProofState = 1

592+ size ProofTerm = 1

593+ size Undo = 1

594+ size (Try l r) = 1 + size l + size r

595+ size (TSeq l r) = 1 + size l + size r

596+ size Qed = 1

597+ size Abandon = 1

598+

579type PTactic = PTactic' PTerm

599type PTactic = PTactic' PTerm

580

600

581data PDo' t = DoExp FC t

601data PDo' t = DoExp FC t

@@ -588,6 +608,13 @@ data PDo' t = DoExp FC t

588deriving instance Binary PDo'

608deriving instance Binary PDo'

589!-}

609!-}

590

610

611+instance Sized a => Sized (PDo' a) where

612+ size (DoExp fc t) = 1 + size fc + size t

613+ size (DoBind fc nm t) = 1 + size fc + size nm + size t

614+ size (DoBindP fc l r) = 1 + size fc + size l + size r

615+ size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

616+ size (DoLetP fc l r) = 1 + size fc + size l + size r

617+

591type PDo = PDo' PTerm

618type PDo = PDo' PTerm

592

619

593-- The priority gives a hint as to elaboration order. Best to elaborate

620-- The priority gives a hint as to elaboration order. Best to elaborate

@@ -605,6 +632,13 @@ data PArg' t = PImp { priority :: Int,

605 getScript :: t,

632 getScript :: t,

606 getTm :: t }

633 getTm :: t }

607 deriving (Show, Eq, Functor)

634 deriving (Show, Eq, Functor)

635+

636+instance Sized a => Sized (PArg' a) where

637+ size (PImp p l nm trm) = 1 + size nm + size trm

638+ size (PExp p l trm) = 1 + size trm

639+ size (PConstraint p l trm) = 1 + size trm

640+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm

641+

608{-!

642{-!

609deriving instance Binary PArg'

643deriving instance Binary PArg'

610!-}

644!-}

@@ -886,7 +920,7 @@ instance Sized PTerm where

886 size (PQuote rawTerm) = size rawTerm

920 size (PQuote rawTerm) = size rawTerm

887 size (PRef fc name) = size name

921 size (PRef fc name) = size name

888 size (PLam name ty bdy) = 1 + size ty + size bdy

922 size (PLam name ty bdy) = 1 + size ty + size bdy

889− size (PPi name ty bdy) = 1 + size ty + size bdy

923+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy

890 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy

924 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy

891 size (PTyped trm ty) = 1 + size trm + size ty

925 size (PTyped trm ty) = 1 + size trm + size ty

892 size (PApp fc name args) = 1 + size args

926 size (PApp fc name args) = 1 + size args

@@ -897,7 +931,7 @@ instance Sized PTerm where

897 size (PResolveTC fc) = 1

931 size (PResolveTC fc) = 1

898 size (PEq fc left right) = 1 + size left + size right

932 size (PEq fc left right) = 1 + size left + size right

899 size (PPair fc left right) = 1 + size left + size right

933 size (PPair fc left right) = 1 + size left + size right

900− size (PDPair fs left right) = 1 + size left + size right

934+ size (PDPair fs left ty right) = 1 + size left + size ty + size right

901 size (PAlternative alts) = 1 + size alts

935 size (PAlternative alts) = 1 + size alts

902 size (PHidden hidden) = size hidden

936 size (PHidden hidden) = size hidden

903 size PSet = 1

937 size PSet = 1

src/Idris/Prover.hs+8−1

@@ -17,6 +17,8 @@ import Idris.DataOpts

17import System.Console.Haskeline

18import Control.Monad.State

20+import Util.Pretty

21+

20prover :: Bool -> Name -> Idris ()

22prover :: Bool -> Name -> Idris ()

21prover lit x =

23prover lit x =

22 do ctxt <- getContext

24 do ctxt <- getContext

@@ -55,7 +57,11 @@ elabStep st e = do case runStateT e st of

55 OK (a, st') -> return (a, st')

57 OK (a, st') -> return (a, st')

56 Error a -> do i <- get

58 Error a -> do i <- get

57 fail (pshow i a)

59 fail (pshow i a)

58−

60+

61+dumpState :: IState -> ProofState -> IO ()

62+dumpState _ pst = putStrLn . render . pretty $ pst

63+

64+{-

59dumpState :: IState -> ProofState -> IO ()

65dumpState :: IState -> ProofState -> IO ()

60dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

66dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"

61dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)

67dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)

@@ -80,6 +86,7 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)

81 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

87 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v

82 showG b = tshow (binderTy b)

88 showG b = tshow (binderTy b)

89+-}

84lifte :: ElabState [PDecl] -> ElabD a -> Idris a

91lifte :: ElabState [PDecl] -> ElabD a -> Idris a

85lifte st e = do (v, _) <- elabStep st e

92lifte st e = do (v, _) <- elabStep st e

src/Util/Pretty.hs+16−1

@@ -1,10 +1,12 @@

1module Util.Pretty (

2 module Text.PrettyPrint.HughesPJ,

3+ Sized(..), breakingSize, nestingSize,

3− Sized(..), Pretty(..)

4+ Pretty(..)

4) where

5) where

6import Text.PrettyPrint.HughesPJ

7import Text.PrettyPrint.HughesPJ

9+-- A rough notion of size for pretty printing various types.

8class Sized a where

10class Sized a where

9 size :: a -> Int

11 size :: a -> Int

@@ -14,5 +16,18 @@ instance (Sized a, Sized b) => Sized (a, b) where

14instance Sized a => Sized [a] where

16instance Sized a => Sized [a] where

15 size = sum . map size

17 size = sum . map size

19+-- The maximum size before we break on to another line.

20+breakingSize :: Int

21+breakingSize = 5

22+

23+nestingSize :: Int

24+nestingSize = 2

25+

17class Pretty a where

26class Pretty a where

18 pretty :: a -> Doc

27 pretty :: a -> Doc

28+

29+instance Pretty () where

30+ pretty () = text "()"

31+

32+instance Pretty a => Pretty [a] where

33+ pretty l = foldr (<+>) empty $ map pretty l