git.iko.soy/Idris-dev
on master help sign in
Pretty printing data declarations
1b6709fEdwin Brady
src/Core/TT.hs+5
compare with master
unifiedsplit
@@ -50,6 +50,11 @@ instance MonadPlus TC where
50discard :: Monad m => m a -> m ()
50discard :: Monad m => m a -> m ()
51discard f = f >> return ()
51discard f = f >> return ()
52
52
53+showSep :: String -> [String] -> String
54+showSep sep [] = ""
55+showSep sep [x] = x
56+showSep sep (x:xs) = x ++ sep ++ showSep sep xs
57+
53-- RAW TERMS ----------------------------------------------------------------
58-- RAW TERMS ----------------------------------------------------------------
54
59
55-- Names are hierarchies of strings, describing scope (so no danger of
60-- 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 #-}
2
3
3module Idris.AbsSyntax where
4module Idris.AbsSyntax where
4
5
@@ -56,7 +57,12 @@ data Command = Quit | Help | Eval PTerm
56data Fixity = Infixl { prec :: Int }
57data Fixity = Infixl { prec :: Int }
57 | Infixr { prec :: Int }
58 | Infixr { prec :: Int }
58 | InfixN { prec :: Int }
59 | 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
60
66
61data FixDecl = Fix Fixity String
67data FixDecl = Fix Fixity String
62 deriving (Show, Eq)
68 deriving (Show, Eq)
@@ -70,12 +76,12 @@ data PDecl' t = PFix Fixity [String] -- fixity declaration
70 | PTy Name t -- type declaration
76 | PTy Name t -- type declaration
71 | PClause t t -- pattern clause
77 | PClause t t -- pattern clause
72 | PData (PData' t) -- data declaration
78 | PData (PData' t) -- data declaration
73− deriving (Show, Functor)
79+ deriving Functor
74
80
75data PData' t = PDatadecl { d_name :: Name,
81data PData' t = PDatadecl { d_name :: Name,
76 d_tcon :: t,
82 d_tcon :: t,
77 d_cons :: [(Name, t)] }
83 d_cons :: [(Name, t)] }
78− deriving (Show, Functor)
84+ deriving Functor
79
85
80-- Handy to get a free function for applying PTerm -> PTerm functions
86-- Handy to get a free function for applying PTerm -> PTerm functions
81-- across a program, by deriving Functor
87-- across a program, by deriving Functor
@@ -97,6 +103,21 @@ data PTerm = PQuote Raw
97instance Show PTerm where
103instance Show PTerm where
98 show tm = showImp False tm
104 show tm = showImp False tm
99
105
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+
100showImp :: Bool -> PTerm -> String
121showImp :: Bool -> PTerm -> String
101showImp impl tm = se 10 tm where
122showImp impl tm = se 10 tm where
102 se p (PQuote r) = "![" ++ show r ++ "]"
123 se p (PQuote r) = "![" ++ show r ++ "]"
src/Main.hs+2−2
@@ -51,10 +51,10 @@ dumpDecls :: [PDecl] -> String
51dumpDecls [] = ""
51dumpDecls [] = ""
52dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
52dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
53
53
54−dumpDecl (PFix f ops) = show f ++ " ==> " ++ show ops
54+dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
55dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
55dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
56dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r
56dumpDecl (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
58
58
59getFile :: Opt -> Maybe String
59getFile :: Opt -> Maybe String
60getFile (Filename str) = Just str
60getFile (Filename str) = Just str