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