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