module Agda.Utils.CallStack.Pretty
(
) where
import Agda.Utils.CallStack.Base
( CallSite
, CallStack
, SrcLoc(..)
, getCallStack
)
import Agda.Utils.Pretty
( (<+>), ($+$), (<>)
, pshow, text
, colon, comma
, nest, parens
, hcat, hsep, vcat
, Pretty(pretty)
)
instance Pretty SrcLoc where
pretty :: SrcLoc -> Doc
pretty SrcLoc {Int
[Char]
srcLocEndCol :: SrcLoc -> Int
srcLocEndLine :: SrcLoc -> Int
srcLocFile :: SrcLoc -> [Char]
srcLocModule :: SrcLoc -> [Char]
srcLocPackage :: SrcLoc -> [Char]
srcLocStartCol :: SrcLoc -> Int
srcLocStartLine :: SrcLoc -> Int
srcLocEndCol :: Int
srcLocEndLine :: Int
srcLocStartCol :: Int
srcLocStartLine :: Int
srcLocFile :: [Char]
srcLocModule :: [Char]
srcLocPackage :: [Char]
..} = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [Doc
physicalLoc, Doc
"in", Doc
logicalLoc]
where
physicalLoc :: Doc
physicalLoc = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [[Char] -> Doc
text [Char]
srcLocFile, Doc
colon, forall a. Show a => a -> Doc
pshow Int
srcLocStartLine, Doc
colon, forall a. Show a => a -> Doc
pshow Int
srcLocStartCol]
logicalLoc :: Doc
logicalLoc = forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [[Char] -> Doc
text [Char]
srcLocPackage, Doc
colon, [Char] -> Doc
text [Char]
srcLocModule]
instance Pretty CallSite where
pretty :: CallSite -> Doc
pretty ([Char]
fun, SrcLoc
loc) = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [[Char] -> Doc
text [Char]
fun forall a. Semigroup a => a -> a -> a
<> Doc
comma, Doc
"called at", forall a. Pretty a => a -> Doc
pretty SrcLoc
loc]
instance Pretty CallStack where
pretty :: CallStack -> Doc
pretty CallStack
cs = case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> Doc
pretty (CallStack -> [CallSite]
getCallStack CallStack
cs) of
[] -> Doc -> Doc
parens Doc
"empty CallStack"
Doc
firstLoc : [Doc]
restLocs -> Doc
firstLoc Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2 (forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [Doc]
restLocs)