    module Agda.Utils.CallStack.Base (
      -- * Simple type aliases
        SrcLocPackage
      , SrcLocModule
      , SrcFun
      , SrcLocFile
      , SrcLocLine
      , SrcLocCol
      , CallSite
      , CallSiteFilter

      -- * String-based "pretty" representations
      , prettySrcLoc
      , prettyCallSite
      , prettyCallStack

      -- * Generic utilities over CallStack and CallSite
      , filterCallStack
      , headCallSite
      , overCallSites
      , popnCallStack
      , truncatedCallStack
      , withCallerCallStack
      , withCurrentCallStack
      , withNBackCallStack

      -- * Re-exported stuff
      , CallStack
      , callStack
      , fromCallSiteList
      , getCallStack
      , HasCallStack
      , SrcLoc(..)
      )
      where

    import Data.List ( intercalate )
    import Data.Maybe ( listToMaybe )
    import GHC.Stack
      ( callStack
      , CallStack
      , emptyCallStack
      , fromCallSiteList
      , getCallStack
      , HasCallStack
      , popCallStack
      , prettySrcLoc
      , SrcLoc(..)
      )

    -- * Type aliases

    -- | Type of the package name of a @SrcLoc@
    -- | e.g. `Agda-2.…`
    type SrcLocPackage = String

    -- | Type of the module name of a @SrcLoc@
    -- | e.g. `Agda.Utils.Foo`
    type SrcLocModule = String

    -- | Type of the name of a function in a @CallSite@
    -- | e.g. `proveEverything`
    type SrcFun = String

    -- | Type of a filename of a @SrcLoc@
    -- | e.g. `src/full/Agda/Utils/Foo.hs`
    type SrcLocFile = String

    -- | Type of a line number of a @SrcLoc@
    type SrcLocLine = Int

    -- | Type of a column of a @SrcLoc@
    type SrcLocCol = Int

    -- | Type of an entry in  a @CallStack@
    type CallSite = (SrcFun, SrcLoc)

    -- | Type of a filter for @CallSite@
    type CallSiteFilter = CallSite -> Bool

    -- * Simple String representations
    -- Note that there are @Agda.Utils.Pretty@ instances defined in @Agda.Utils.CallStack.Pretty@

    -- | The same as the un-exported internal function in @GHC.Exceptions (prettyCallStackLines)@
    --  Prints like: @doFoo, called at foo.hs:190:24 in main:Main@
    prettyCallSite :: CallSite -> String
    prettyCallSite :: CallSite -> [Char]
    prettyCallSite ([Char]
    fun, SrcLoc
    loc) = [Char]
    fun [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", called at " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ SrcLoc -> [Char]
    prettySrcLoc SrcLoc
    loc

    -- | 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.
    prettyCallStack :: CallStack -> String
    prettyCallStack :: CallStack -> [Char]
    prettyCallStack CallStack
    cs = case (CallSite -> [Char]) -> [CallSite] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map CallSite -> [Char]
    prettyCallSite (CallStack -> [CallSite]
    getCallStack CallStack
    cs) of
      []                  -> [Char]
    "(empty CallStack)"
      [Char]
    firstLoc : [[Char]]
    restLocs -> [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([Char]
    firstLoc [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : (([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++) [[Char]]
    restLocs))

    -- * Generic utilities over CallStack and CallSite

    -- | Get the most recent @CallSite@ in a @CallStack@, if there is one.
    headCallSite :: CallStack -> Maybe CallSite
    headCallSite :: CallStack -> Maybe CallSite
    headCallSite = [CallSite] -> Maybe CallSite
    forall a. [a] -> Maybe a
    listToMaybe ([CallSite] -> Maybe CallSite)
    -> (CallStack -> [CallSite]) -> CallStack -> Maybe CallSite
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [CallSite]
    getCallStack

    -- | @CallStack@ comprising only the most recent @CallSite@
    truncatedCallStack :: CallStack -> CallStack
    truncatedCallStack :: CallStack -> CallStack
    truncatedCallStack CallStack
    cs = CallStack -> (CallSite -> CallStack) -> Maybe CallSite -> CallStack
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe CallStack
    emptyCallStack ([CallSite] -> CallStack
    fromCallSiteList ([CallSite] -> CallStack)
    -> (CallSite -> [CallSite]) -> CallSite -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallSite -> [CallSite]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure) (CallStack -> Maybe CallSite
    headCallSite CallStack
    cs)

    -- | Transform a @CallStack@ by transforming its list of @CallSite@
    overCallSites :: ([CallSite] -> [CallSite]) -> CallStack -> CallStack
    overCallSites :: ([CallSite] -> [CallSite]) -> CallStack -> CallStack
    overCallSites [CallSite] -> [CallSite]
    f = [CallSite] -> CallStack
    fromCallSiteList ([CallSite] -> CallStack)
    -> (CallStack -> [CallSite]) -> CallStack -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [CallSite] -> [CallSite]
    f ([CallSite] -> [CallSite])
    -> (CallStack -> [CallSite]) -> CallStack -> [CallSite]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [CallSite]
    getCallStack

    -- | Transform a @CallStack@ by filtering each @CallSite@
    filterCallStack :: CallSiteFilter -> CallStack -> CallStack
    filterCallStack :: CallSiteFilter -> CallStack -> CallStack
    filterCallStack = ([CallSite] -> [CallSite]) -> CallStack -> CallStack
    overCallSites (([CallSite] -> [CallSite]) -> CallStack -> CallStack)
    -> (CallSiteFilter -> [CallSite] -> [CallSite])
    -> CallSiteFilter
    -> CallStack
    -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallSiteFilter -> [CallSite] -> [CallSite]
    forall a. (a -> Bool) -> [a] -> [a]
    filter

    -- | Pops n entries off a @CallStack@ using @popCallStack@.
    -- Note that frozen callstacks are unaffected.
    popnCallStack :: Word -> CallStack -> CallStack
    popnCallStack :: Word -> CallStack -> CallStack
    popnCallStack Word
    0 = CallStack -> CallStack
    forall a. a -> a
    id
    popnCallStack Word
    n = (Word -> CallStack -> CallStack
    popnCallStack (Word
    n Word -> Word -> Word
    forall a. Num a => a -> a -> a
    - Word
    1)) (CallStack -> CallStack)
    -> (CallStack -> CallStack) -> CallStack -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> CallStack
    popCallStack

    withNBackCallStack :: HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack :: forall b. HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack Word
    n CallStack -> b
    f = CallStack -> b
    f (Word -> CallStack -> CallStack
    popnCallStack Word
    n CallStack
    from)
      where
        -- This very line (always dropped):
        here :: CallStack
    here = CallStack
    HasCallStack => CallStack
    callStack
        -- The invoker (n = 0):
        from :: CallStack
    from = CallStack -> CallStack
    popCallStack CallStack
    here

    withCurrentCallStack :: HasCallStack => (CallStack -> b) -> b
    withCurrentCallStack :: forall b. HasCallStack => (CallStack -> b) -> b
    withCurrentCallStack = Word -> (CallStack -> b) -> b
    forall b. HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack Word
    0
      -- 0 => this line in this utility function.
      -- 1 => the invocation of this utility function.

    withCallerCallStack :: HasCallStack => (CallStack -> b) -> b
    withCallerCallStack :: forall b. HasCallStack => (CallStack -> b) -> b
    withCallerCallStack = Word -> (CallStack -> b) -> b
    forall b. HasCallStack => Word -> (CallStack -> b) -> b
    withNBackCallStack Word
    1
      -- 0 => this line in this utility function.
      -- 1 => our caller.
      -- 2 => their caller.