    {-# OPTIONS_GHC -Wunused-imports #-}

    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@
    newtype CallSite = CallSite { CallSite -> ([Char], SrcLoc)
    unCallSite :: (SrcFun, SrcLoc) }

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

    -- * Simple String representations
    -- Note that there are @Agda.Syntax.Common.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 (CallSite ([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 (([Char], SrcLoc) -> [Char]) -> [([Char], SrcLoc)] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (CallSite -> [Char]
    prettyCallSite (CallSite -> [Char])
    -> (([Char], SrcLoc) -> CallSite) -> ([Char], SrcLoc) -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char], SrcLoc) -> CallSite
    CallSite) (CallStack -> [([Char], SrcLoc)]
    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 = (([Char], SrcLoc) -> CallSite)
    -> Maybe ([Char], SrcLoc) -> Maybe CallSite
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], SrcLoc) -> CallSite
    CallSite (Maybe ([Char], SrcLoc) -> Maybe CallSite)
    -> (CallStack -> Maybe ([Char], SrcLoc))
    -> CallStack
    -> Maybe CallSite
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [([Char], SrcLoc)] -> Maybe ([Char], SrcLoc)
    forall a. [a] -> Maybe a
    listToMaybe ([([Char], SrcLoc)] -> Maybe ([Char], SrcLoc))
    -> (CallStack -> [([Char], SrcLoc)])
    -> CallStack
    -> Maybe ([Char], SrcLoc)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [([Char], SrcLoc)]
    getCallStack

    -- | @CallStack@ comprising only the most recent @CallSite@
    truncatedCallStack :: CallStack -> CallStack
    truncatedCallStack :: CallStack -> CallStack
    truncatedCallStack CallStack
    cs = CallStack
    -> (([Char], SrcLoc) -> CallStack)
    -> Maybe ([Char], SrcLoc)
    -> CallStack
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe CallStack
    emptyCallStack ([([Char], SrcLoc)] -> CallStack
    fromCallSiteList ([([Char], SrcLoc)] -> CallStack)
    -> (([Char], SrcLoc) -> [([Char], SrcLoc)])
    -> ([Char], SrcLoc)
    -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Char], SrcLoc) -> [([Char], SrcLoc)]
    forall a. a -> [a]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure) ((CallSite -> ([Char], SrcLoc))
    -> Maybe CallSite -> Maybe ([Char], SrcLoc)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CallSite -> ([Char], SrcLoc)
    unCallSite (Maybe CallSite -> Maybe ([Char], SrcLoc))
    -> Maybe CallSite -> Maybe ([Char], SrcLoc)
    forall a b. (a -> b) -> a -> b
    $ 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 = [([Char], SrcLoc)] -> CallStack
    fromCallSiteList ([([Char], SrcLoc)] -> CallStack)
    -> (CallStack -> [([Char], SrcLoc)]) -> CallStack -> CallStack
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((CallSite -> ([Char], SrcLoc)) -> [CallSite] -> [([Char], SrcLoc)]
    forall a b. (a -> b) -> [a] -> [b]
    map CallSite -> ([Char], SrcLoc)
    unCallSite ([CallSite] -> [([Char], SrcLoc)])
    -> ([([Char], SrcLoc)] -> [CallSite])
    -> [([Char], SrcLoc)]
    -> [([Char], SrcLoc)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [CallSite] -> [CallSite]
    f ([CallSite] -> [CallSite])
    -> ([([Char], SrcLoc)] -> [CallSite])
    -> [([Char], SrcLoc)]
    -> [CallSite]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], SrcLoc) -> CallSite) -> [([Char], SrcLoc)] -> [CallSite]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char], SrcLoc) -> CallSite
    CallSite) ([([Char], SrcLoc)] -> [([Char], SrcLoc)])
    -> (CallStack -> [([Char], SrcLoc)])
    -> CallStack
    -> [([Char], SrcLoc)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CallStack -> [([Char], SrcLoc)]
    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.