{-# LANGUAGE DeriveDataTypeable #-}
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)