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

Agda.Utils.CallStack

Synopsis

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 #

NFData CallStack 
Instance details

Defined in Control.DeepSeq

Methods

rnf :: CallStack -> ()

IsList CallStack 
Instance details

Defined in GHC.Internal.IsList

Associated Types

type Item CallStack 
Instance details

Defined in GHC.Internal.IsList

type Item CallStack = (String, SrcLoc)

Methods

fromList :: [Item CallStack] -> CallStack #

fromListN :: Int -> [Item CallStack] -> CallStack #

toList :: CallStack -> [Item CallStack] #

Show CallStack 
Instance details

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> CallStack -> ShowS

show :: CallStack -> String

showList :: [CallStack] -> ShowS

type Item CallStack 
Instance details

Defined in GHC.Internal.IsList

type Item CallStack = (String, SrcLoc)

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.

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

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)] #

data SrcLoc #

Constructors

SrcLoc 

Fields

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 #

NFData SrcLoc 
Instance details

Defined in Control.DeepSeq

Methods

rnf :: SrcLoc -> ()

Generic SrcLoc 
Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep SrcLoc 
Instance details

Defined in GHC.Internal.Generics

type Rep SrcLoc = D1 ('MetaData "SrcLoc" "GHC.Internal.Stack.Types" "ghc-internal" '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)))))

Methods

from :: SrcLoc -> Rep SrcLoc x

to :: Rep SrcLoc x -> SrcLoc

Show SrcLoc 
Instance details

Defined in GHC.Internal.Show

Methods

showsPrec :: Int -> SrcLoc -> ShowS

show :: SrcLoc -> String

showList :: [SrcLoc] -> ShowS

Eq SrcLoc 
Instance details

Defined in GHC.Internal.Stack.Types

Methods

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

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

type Rep SrcLoc 
Instance details

Defined in GHC.Internal.Generics

type Rep SrcLoc = D1 ('MetaData "SrcLoc" "GHC.Internal.Stack.Types" "ghc-internal" '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)))))