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