Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.CallStack

Synopsis

Documentation

data CallStack #

Instances

Instances details
IsList CallStack 
Instance details

Defined in GHC.Exts

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 -> ()

Pretty CallStack Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

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 #

type Item CallStack 
Instance details

Defined in GHC.Exts

type Item CallStack = (String, SrcLoc)

data SrcLoc #

Constructors

SrcLoc 

Fields

Instances

Instances details
Eq SrcLoc 
Instance details

Defined in GHC.Stack.Types

Methods

(==) :: SrcLoc -> SrcLoc -> Bool

(/=) :: SrcLoc -> SrcLoc -> Bool

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 -> ()

Pretty SrcLoc Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

Pretty CallSite Source # 
Instance details

Defined in Agda.Utils.CallStack.Pretty

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 #

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

type HasCallStack = ?callStack :: CallStack #

prettySrcLoc :: SrcLoc -> String #

type CallSiteFilter = CallSite -> Bool Source #

Type of a filter for CallSite

type CallSite = (SrcFun, SrcLoc) Source #

Type of an entry in a CallStack

type SrcLocCol = Int Source #

Type of a column of a SrcLoc

type SrcLocLine = Int Source #

Type of a line number of a SrcLoc

type SrcLocFile = String Source #

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

type SrcFun = String Source #

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

type SrcLocModule = String Source #

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

type SrcLocPackage = String Source #

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

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

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.

headCallSite :: CallStack -> Maybe CallSite Source #

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

truncatedCallStack :: CallStack -> CallStack Source #

CallStack comprising only the most recent CallSite

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

Transform a CallStack by transforming its list of CallSite

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

Transform a CallStack by filtering each CallSite

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

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