git.iko.soy/Idris-dev
on master help sign in
Pretty printer for PTerm
2050102Edwin Brady
src/Idris/AbsSyntax.hs+46−1
compare with master
unifiedsplit
@@ -7,6 +7,7 @@ import Core.Evaluate
7
7
8import Control.Monad.State
8import Control.Monad.State
9import Data.List
9import Data.List
10+import Data.Char
10
11
11data IOption = Logging
12data IOption = Logging
12 deriving (Show, Eq)
13 deriving (Show, Eq)
@@ -92,7 +93,51 @@ data PTerm = PQuote Raw
92 | PHidden PTerm -- irrelevant or hidden pattern
93 | PHidden PTerm -- irrelevant or hidden pattern
93 | PSet
94 | PSet
94 | Placeholder
95 | Placeholder
95− deriving Show
96+
97+instance Show PTerm where
98+ show tm = showImp False tm
99+
100+showImp :: Bool -> PTerm -> String
101+showImp impl tm = se 10 tm where
102+ se p (PQuote r) = "![" ++ show r ++ "]"
103+ se p (PRef n) = show n
104+ se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
105+ se p (PPi Exp n ty sc)
106+ | n `elem` allNamesIn sc = bracket p 2 $
107+ "(" ++ show n ++ " : " ++ se 10 ty ++
108+ ") -> " ++ se 10 sc
109+ | otherwise = bracket p 2 $ se 10 ty ++ " -> " ++ se 10 sc
110+ se p (PPi Imp n ty sc)
111+ | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++
112+ "} -> " ++ se 10 sc
113+ | otherwise = se 10 sc
114+ se p (PApp (PRef op@(UN [f:_])) _ [l, r])
115+ | not impl && not (isAlpha f)
116+ = bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 1 r
117+ se p (PApp f imps args)
118+ = bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")
119+ ++ concatMap seArg args
120+ se p (PHidden tm) = "." ++ se 0 tm
121+ se p PSet = "Set"
122+ se p Placeholder = "_"
123+
124+ seArg arg = " " ++ se 0 arg
125+ siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
126+
127+ bracket outer inner str | inner > outer = "(" ++ str ++ ")"
128+ | otherwise = str
129+
130+allNamesIn :: PTerm -> [Name]
131+allNamesIn tm = nub $ ni [] tm
132+ where
133+ ni env (PRef n)
134+ | not (n `elem` env) = [n]
135+ ni env (PApp f is es) = ni env f ++ concatMap (ni env) (map snd is) ++
136+ concatMap (ni env) es
137+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
138+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
139+ ni env (PHidden tm) = ni env tm
140+ ni env _ = []
96
141
97namesIn :: IState -> PTerm -> [Name]
142namesIn :: IState -> PTerm -> [Name]
98namesIn ist tm = nub $ ni [] tm
143namesIn ist tm = nub $ ni [] tm
src/Main.hs+2−2
@@ -52,8 +52,8 @@ dumpDecls [] = ""
52dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
52dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
53
53
54dumpDecl (PFix f ops) = show f ++ " ==> " ++ show ops
54dumpDecl (PFix f ops) = show f ++ " ==> " ++ show ops
55−dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ show t
55+dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
56−dumpDecl (PClause l r) = "pat " ++ show l ++ " = " ++ show r
56+dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r
57dumpDecl (PData d) = "data " ++ show d
57dumpDecl (PData d) = "data " ++ show d
58
58
59getFile :: Opt -> Maybe String
59getFile :: Opt -> Maybe String