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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.CallStack

Synopsis

- data CallStack
- 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
- prettySrcLoc :: SrcLoc -> String
- prettyCallStack :: CallStack -> String
- callStack :: HasCallStack => CallStack
- withCallerCallStack :: HasCallStack => (CallStack -> b) -> b
- prettyCallSite :: CallSite -> String
- headCallSite :: CallStack -> Maybe CallSite
- withCurrentCallStack :: HasCallStack => (CallStack -> b) -> b
- withNBackCallStack :: HasCallStack => Word -> (CallStack -> b) -> b
- type SrcLocPackage = String
- type SrcLocModule = String
- type SrcFun = String
- type SrcLocFile = String
- type SrcLocLine = Int
- type SrcLocCol = Int
- newtype CallSite = CallSite {
  - unCallSite :: (SrcFun, SrcLoc)
  }
- type CallSiteFilter = CallSite -> Bool
- filterCallStack :: CallSiteFilter -> CallStack -> CallStack
- overCallSites :: ([CallSite] -> [CallSite]) -> CallStack -> CallStack
- popnCallStack :: Word -> CallStack -> CallStack
- truncatedCallStack :: CallStack -> CallStack

# 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>:... in interactive:Ghci...

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

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 Word32 Source # icod_ :: CallStack -> S Word32 Source # value :: Word32 -> R CallStack Source #
NFData CallStack | Since: deepseq-1.4.2.0
Instance details Defined in Control.DeepSeq Methods rnf :: CallStack -> () 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.Internal.IsList

Associated Types

type Item CallStack |
Instance details Defined in GHC.Internal.IsList type Item CallStack = (String, SrcLoc)

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.Internal.Show Methods showsPrec :: Int -> CallStack -> ShowS Source # show :: CallStack -> String Source # showList :: [CallStack] -> ShowS Source #
type Item CallStack |
Instance details Defined in GHC.Internal.IsList type Item CallStack = (String, SrcLoc)

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

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 Word32 Source # icod_ :: SrcLoc -> S Word32 Source # value :: Word32 -> R SrcLoc Source #
NFData SrcLoc | Since: deepseq-1.4.2.0
Instance details Defined in Control.DeepSeq Methods rnf :: SrcLoc -> () Source #
Generic SrcLoc |

Instance details

Defined in GHC.Internal.Generics

Associated Types

type Rep SrcLoc | Since: base-4.15.0.0

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 Source #

to :: Rep SrcLoc x -> SrcLoc Source #

Show SrcLoc | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.Show Methods showsPrec :: Int -> SrcLoc -> ShowS Source # show :: SrcLoc -> String Source # showList :: [SrcLoc] -> ShowS Source #
Eq SrcLoc | Since: base-4.9.0.0
Instance details Defined in GHC.Internal.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.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)))))

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

prettySrcLoc :: SrcLoc -> String Source #

Pretty print a `SrcLoc`.

Since: ghc-internal-4.9.0.0

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.

callStack :: HasCallStack => CallStack Source #

Return the current `CallStack`.

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

Since: base-4.9.0.0

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 #

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

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`

newtype CallSite Source #

Type of an entry in a `CallStack`

Constructors

CallSite |

Fields

- unCallSite :: (SrcFun, SrcLoc)

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

type CallSiteFilter = CallSite -> Bool Source #

Type of a filter for `CallSite`

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`