Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Utils.CallStack

Synopsis

type HasCallStack = ?callStack :: CallStack
data CallStack
type SrcLocPackage = String
type SrcLocModule = String
type SrcFun = String
type SrcLocFile = String
type SrcLocLine = Int
type SrcLocCol = Int
type CallSite = (SrcFun, SrcLoc)
type CallSiteFilter = CallSite -> Bool
data SrcLoc = SrcLoc {
- srcLocPackage :: [Char]
- srcLocModule :: [Char]
- srcLocFile :: [Char]
- srcLocStartLine :: Int
- srcLocStartCol :: Int
- srcLocEndLine :: Int
- srcLocEndCol :: Int
}
withCallerCallStack :: HasCallStack => (CallStack -> b) -> b
prettyCallSite :: CallSite -> String
headCallSite :: CallStack -> Maybe CallSite
withCurrentCallStack :: HasCallStack => (CallStack -> b) -> b
prettyCallStack :: CallStack -> String
prettySrcLoc :: SrcLoc -> String
filterCallStack :: CallSiteFilter -> CallStack -> CallStack
overCallSites :: ([CallSite] -> [CallSite]) -> CallStack -> CallStack
popnCallStack :: Word -> CallStack -> CallStack
truncatedCallStack :: CallStack -> CallStack
withNBackCallStack :: HasCallStack => Word -> (CallStack -> b) -> b
callStack :: HasCallStack => CallStack
fromCallSiteList :: [([Char], SrcLoc)] -> CallStack
getCallStack :: CallStack -> [([Char], SrcLoc)]

Documentation

type HasCallStack = ?callStack :: CallStack #

data CallStack #

Instances

Instances details

Pretty CallStack Source #
Instance details Defined in Agda.Utils.CallStack.Pretty Methods pretty :: CallStack -> Doc Source # prettyPrec :: Int -> CallStack -> Doc Source # prettyList :: [CallStack] -> Doc Source #
EmbPrj CallStack Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: CallStack -> S Int32 Source # icod_ :: CallStack -> S Int32 Source # value :: Int32 -> R CallStack Source #
IsList CallStack
Instance details Defined in GHC.IsList Associated Types type Item CallStack # Methods fromList :: [Item CallStack] -> CallStack # fromListN :: Int -> [Item CallStack] -> CallStack # toList :: CallStack -> [Item CallStack] #
Show CallStack
Instance details Defined in GHC.Show Methods showsPrec :: Int -> CallStack -> ShowS show :: CallStack -> String showList :: [CallStack] -> ShowS
NFData CallStack
Instance details Defined in Control.DeepSeq Methods rnf :: CallStack -> ()
type Item CallStack
Instance details Defined in GHC.IsList type Item CallStack = (String, SrcLoc)

type SrcLocPackage = String Source #

Type of the package name of a SrcLoc | e.g. `Agda-2.…`

type SrcLocModule = String Source #

Type of the module name of a SrcLoc | e.g. Foo

type SrcFun = String Source #

Type of the name of a function in a CallSite | e.g. proveEverything

type SrcLocFile = String Source #

Type of a filename of a SrcLoc | e.g. `srcfullAgdaUtilsFoo.hs`

type SrcLocLine = Int Source #

Type of a line number of a SrcLoc

type SrcLocCol = Int Source #

Type of a column of a SrcLoc

type CallSite = (SrcFun, SrcLoc) Source #

Type of an entry in a CallStack

type CallSiteFilter = CallSite -> Bool Source #

Type of a filter for CallSite

data SrcLoc #

Constructors

SrcLoc
Fields srcLocPackage :: [Char] srcLocModule :: [Char] srcLocFile :: [Char] srcLocStartLine :: Int srcLocStartCol :: Int srcLocEndLine :: Int srcLocEndCol :: Int

Instances

Instances details

Pretty CallSite Source #
Instance details Defined in Agda.Utils.CallStack.Pretty Methods pretty :: CallSite -> Doc Source # prettyPrec :: Int -> CallSite -> Doc Source # prettyList :: [CallSite] -> Doc Source #
Pretty SrcLoc Source #
Instance details Defined in Agda.Utils.CallStack.Pretty Methods pretty :: SrcLoc -> Doc Source # prettyPrec :: Int -> SrcLoc -> Doc Source # prettyList :: [SrcLoc] -> Doc Source #
EmbPrj SrcLoc Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SrcLoc -> S Int32 Source # icod_ :: SrcLoc -> S Int32 Source # value :: Int32 -> R SrcLoc Source #
Generic SrcLoc
Instance details Defined in GHC.Generics Associated Types type Rep SrcLoc :: Type -> Type Methods from :: SrcLoc -> Rep SrcLoc x to :: Rep SrcLoc x -> SrcLoc
Show SrcLoc
Instance details Defined in GHC.Show Methods showsPrec :: Int -> SrcLoc -> ShowS show :: SrcLoc -> String showList :: [SrcLoc] -> ShowS
NFData SrcLoc
Instance details Defined in Control.DeepSeq Methods rnf :: SrcLoc -> ()
Eq SrcLoc
Instance details Defined in GHC.Stack.Types Methods (==) :: SrcLoc -> SrcLoc -> Bool (/=) :: SrcLoc -> SrcLoc -> Bool
type Rep SrcLoc
Instance details Defined in GHC.Generics type Rep SrcLoc = D1 ('MetaData "SrcLoc" "GHC.Stack.Types" "base" 'False) (C1 ('MetaCons "SrcLoc" 'PrefixI 'True) ((S1 ('MetaSel ('Just "srcLocPackage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Char]) :: (S1 ('MetaSel ('Just "srcLocModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Char]) :: S1 ('MetaSel ('Just "srcLocFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Char]))) :: ((S1 ('MetaSel ('Just "srcLocStartLine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "srcLocStartCol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "srcLocEndLine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "srcLocEndCol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))))

withCallerCallStack :: HasCallStack => (CallStack -> b) -> b Source #

prettyCallSite :: CallSite -> String Source #

The same as the un-exported internal function in GHC.Exceptions (prettyCallStackLines) Prints like: doFoo, called at foo.hs:190:24 in main:Main

headCallSite :: CallStack -> Maybe CallSite Source #

Get the most recent CallSite in a CallStack, if there is one.

withCurrentCallStack :: HasCallStack => (CallStack -> b) -> b Source #

prettyCallStack :: CallStack -> String Source #

Pretty-print a CallStack. This has a few differences from GHC.Stack.prettyCallStackLines. We omit the "CallStack (from GetCallStack)" header line for brevity. If there is only one entry (which is common, due to the manual nature of the HasCallStack constraint), shows the entry on one line. If there are multiple, then the following lines are indented.

prettySrcLoc :: SrcLoc -> String #

filterCallStack :: CallSiteFilter -> CallStack -> CallStack Source #

Transform a CallStack by filtering each CallSite

overCallSites :: ([CallSite] -> [CallSite]) -> CallStack -> CallStack Source #

Transform a CallStack by transforming its list of CallSite

popnCallStack :: Word -> CallStack -> CallStack Source #

Pops n entries off a CallStack using popCallStack. Note that frozen callstacks are unaffected.

truncatedCallStack :: CallStack -> CallStack Source #

CallStack comprising only the most recent CallSite

withNBackCallStack :: HasCallStack => Word -> (CallStack -> b) -> b Source #

callStack :: HasCallStack => CallStack #

fromCallSiteList :: [([Char], SrcLoc)] -> CallStack #

getCallStack :: CallStack -> [([Char], SrcLoc)] #