@@ -7,6 +7,7 @@ import Core.Evaluate
77
88import Control.Monad.State
99import Data.List
10+import Data.Char
1011
1112data IOption = Logging
1213 deriving (Show, Eq)
@@ -92,7 +93,51 @@ data PTerm = PQuote Raw
9293 | PHidden PTerm -- irrelevant or hidden pattern
9394 | PSet
9495 | 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 _ = []
96141
97142namesIn :: IState -> PTerm -> [Name]
98143namesIn ist tm = nub $ ni [] tm