module Agda.Utils.Trace where
import Control.Monad
import Data.Monoid
import Data.Generics (Typeable, Data)
type Trace = CurrentCall
type SiblingCall = ChildCall
data CurrentCall a
= Current a (ParentCall a) [SiblingCall a] [ChildCall a]
| TopLevel [ChildCall a]
deriving (Typeable, Data)
data ParentCall a
= Parent a (ParentCall a) [SiblingCall a]
| NoParent
deriving (Typeable, Data)
data ChildCall a = Child a [ChildCall a]
deriving (Typeable, Data)
newCall :: a -> Trace a -> Trace a
newCall c (TopLevel cs) = Current c NoParent cs []
newCall c (Current c' p ss cs) = Current c (Parent c' p ss) cs []
updateCall :: a -> Trace a -> Trace a
updateCall c (TopLevel _) = error $ "updateCall: no a in progress"
updateCall c (Current _ p ss cs) = case p of
NoParent -> TopLevel $ Child c cs : ss
Parent c' p' ss' -> Current c' p' ss' $ Child c cs : ss
matchCall :: (call -> Maybe a) -> Trace call -> Maybe a
matchCall f tr = case matchTrace f' tr of
[] -> Nothing
x : _ -> Just x
where
f' (Child c _) = maybe [] (:[]) $ f c
matchCalls :: (call -> Maybe a) -> Trace call -> [a]
matchCalls f = matchTrace f'
where
f' (Child c _) = maybe [] (:[]) $ f c
matchTrace :: Monoid m => (ChildCall call -> m) -> Trace call -> m
matchTrace f (TopLevel _) = mempty
matchTrace f t@(Current c _ _ cs) =
f (Child c cs) `mappend` matchTrace f (updateCall c t)