1b6709f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pretty printing data declarations

commit1b6709fcb57a86abbacceec28838fed5c57a38c4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 7 Oct 2011, 01:36 (15 years ago) parent2050102

3 files changed+32−6

compare with master

unifiedsplit

src/Core/TT.hs+5 src/Idris/AbsSyntax.hs+25−4 src/Main.hs+2−2

src/Core/TT.hs+5

@@ -50,6 +50,11 @@ instance MonadPlus TC where

5050discard :: Monad m => m a -> m ()

5151discard f = f >> return ()

5252

53+showSep :: String -> [String] -> String

54+showSep sep [] = ""

55+showSep sep [x] = x

56+showSep sep (x:xs) = x ++ sep ++ showSep sep xs

57+

5358-- RAW TERMS ----------------------------------------------------------------

5459

5560-- Names are hierarchies of strings, describing scope (so no danger of

src/Idris/AbsSyntax.hs+25−4

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

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

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

2+ TypeSynonymInstances #-}

34module Idris.AbsSyntax where

@@ -56,7 +57,12 @@ data Command = Quit | Help | Eval PTerm

5657data Fixity = Infixl { prec :: Int }

5758 | Infixr { prec :: Int }

5859 | InfixN { prec :: Int }

59− deriving (Show, Eq)

60+ deriving Eq

61+

62+instance Show Fixity where

63+ show (Infixl i) = "infixl " ++ show i

64+ show (Infixr i) = "infixr " ++ show i

65+ show (InfixN i) = "infix " ++ show i

6066

6167data FixDecl = Fix Fixity String

6268 deriving (Show, Eq)

@@ -70,12 +76,12 @@ data PDecl' t = PFix Fixity [String] -- fixity declaration

7076 | PTy Name t -- type declaration

7177 | PClause t t -- pattern clause

7278 | PData (PData' t) -- data declaration

73− deriving (Show, Functor)

79+ deriving Functor

7480

7581data PData' t = PDatadecl { d_name :: Name,

7682 d_tcon :: t,

7783 d_cons :: [(Name, t)] }

78− deriving (Show, Functor)

84+ deriving Functor

7985

8086-- Handy to get a free function for applying PTerm -> PTerm functions

8187-- across a program, by deriving Functor

@@ -97,6 +103,21 @@ data PTerm = PQuote Raw

97103instance Show PTerm where

98104 show tm = showImp False tm

99105

106+instance Show PDecl where

107+ show (PFix f ops) = show f ++ " " ++ showSep ", " ops

108+ show (PTy n ty) = show n ++ " : " ++ show ty

109+ show (PClause l r) = show l ++ " = " ++ show r

110+ show (PData d) = show d

111+

112+instance Show PData where

113+ show d = showDImp False d

114+

115+showDImp :: Bool -> PData -> String

116+showDImp impl (PDatadecl n ty cons)

117+ = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

118+ ++ showSep "\n\t| "

119+ (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)

120+

100121showImp :: Bool -> PTerm -> String

101122showImp impl tm = se 10 tm where

102123 se p (PQuote r) = "![" ++ show r ++ "]"

src/Main.hs+2−2

@@ -51,10 +51,10 @@ dumpDecls :: [PDecl] -> String

5151dumpDecls [] = ""

5252dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

5353

54−dumpDecl (PFix f ops) = show f ++ " ==> " ++ show ops

54+dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops

5555dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

5656dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r

57−dumpDecl (PData d) = "data " ++ show d

57+dumpDecl (PData d) = "data " ++ showDImp True d

5858

5959getFile :: Opt -> Maybe String

6060getFile (Filename str) = Just str