Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.CallStack

Synopsis

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

# Documentation

data CallStack Source #

`CallStack`s are a lightweight method of obtaining a partial call-stack at any point in the program.

A function can request its call-site with the `HasCallStack` constraint. For example, we can define

    putStrLnWithCallStack :: HasCallStack => String -> IO ()

as a variant of `putStrLn` that will get its call-site and print it, along with the string given as argument. We can access the call-stack inside `putStrLnWithCallStack` with `callStack`.

    putStrLnWithCallStack :: HasCallStack => String -> IO ()
    putStrLnWithCallStack msg = do
      putStrLn msg
      putStrLn (prettyCallStack callStack)

Thus, if we call `putStrLnWithCallStack` we will get a formatted call-stack alongside our string.

    >>> putStrLnWithCallStack "hello"
    hello
    CallStack (from HasCallStack):
      putStrLnWithCallStack, called at <interactive>:2:1 in interactive:Ghci1

GHC solves `HasCallStack` constraints in three steps:

1. If there is a `CallStack` in scope -- i.e. the enclosing function has a `HasCallStack` constraint -- GHC will append the new call-site to the existing `CallStack`.
2. If there is no `CallStack` in scope -- e.g. in the GHCi session above -- and the enclosing definition does not have an explicit type signature, GHC will infer a `HasCallStack` constraint for the enclosing definition (subject to the monomorphism restriction).
3. If there is no `CallStack` in scope and the enclosing definition has an explicit type signature, GHC will solve the `HasCallStack` constraint for the singleton `CallStack` containing just the current call-site.

`CallStack`s do not interact with the RTS and do not require compilation with `-prof`. On the other hand, as they are built up explicitly via the `HasCallStack` constraints, they will generally not contain as much information as the simulated call-stacks maintained by the RTS.

A `CallStack` is a `[(String, SrcLoc)]`. The `String` is the name of function that was called, the `SrcLoc` is the call-site. The list is ordered with the most recently called function at the head.

NOTE: The intrepid user may notice that `HasCallStack` is just an alias for an implicit parameter `?callStack :: CallStack`. This is an implementation detail and should not be considered part of the `CallStack` API, we may decide to change the implementation in the future.

Since: base-4.8.1.0

#### Instances

Instances details

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 #
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 #
IsList CallStack | Be aware that 'fromList . toList = id' only for unfrozen `CallStack`s, since `toList` removes frozenness information. Since: base-4.9.0.0
Instance details Defined in GHC.Exts Associated Types type Item CallStack Source # Methods fromList :: [Item CallStack] -> CallStack Source # fromListN :: Int -> [Item CallStack] -> CallStack Source # toList :: CallStack -> [Item CallStack] Source #
Show CallStack | Since: base-4.9.0.0
Instance details Defined in GHC.Show Methods showsPrec :: Int -> CallStack -> ShowS Source # show :: CallStack -> String Source # showList :: [CallStack] -> ShowS Source #
NFData CallStack | Since: deepseq-1.4.2.0
Instance details Defined in Control.DeepSeq Methods rnf :: CallStack -> () Source #
type Item CallStack |
Instance details Defined in GHC.Exts type Item CallStack = (String, SrcLoc)

callStack :: HasCallStack => CallStack Source #

Return the current `CallStack`.

Does *not* include the call-site of `callStack`.

Since: base-4.9.0.0

prettySrcLoc :: SrcLoc -> String Source #

Pretty print a `SrcLoc`.

Since: base-4.9.0.0

data SrcLoc Source #

A single location in the source code.

Since: base-4.8.1.0

Constructors

SrcLoc |

Fields

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

#### Instances

Instances details

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 #
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 #
Generic SrcLoc |
Instance details Defined in GHC.Generics Associated Types type Rep SrcLoc :: Type -> Type Source # Methods from :: SrcLoc -> Rep SrcLoc x Source # to :: Rep SrcLoc x -> SrcLoc Source #
Show SrcLoc | Since: base-4.9.0.0
Instance details Defined in GHC.Show Methods showsPrec :: Int -> SrcLoc -> ShowS Source # show :: SrcLoc -> String Source # showList :: [SrcLoc] -> ShowS Source #
NFData SrcLoc | Since: deepseq-1.4.2.0
Instance details Defined in Control.DeepSeq Methods rnf :: SrcLoc -> () Source #
Eq SrcLoc | Since: base-4.9.0.0
Instance details Defined in GHC.Stack.Types Methods (==) :: SrcLoc -> SrcLoc -> Bool Source # (/=) :: SrcLoc -> SrcLoc -> Bool Source #
type Rep SrcLoc | Since: base-4.15.0.0

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

type HasCallStack = ?callStack :: CallStack Source #

Request a CallStack.

NOTE: The implicit parameter `?callStack :: CallStack` is an implementation detail and should not be considered part of the `CallStack` API, we may decide to change the implementation in the future.

Since: base-4.9.0.0

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

Extract a list of call-sites from the `CallStack`.

The list is ordered by most recent call.

Since: base-4.8.1.0

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

Convert a list of call-sites to a `CallStack`.

Since: base-4.9.0.0

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.

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

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

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