-- Communicating Haskell Processes.
-- Copyright (c) 2008, University of Kent.
-- All rights reserved.
-- 
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are
-- met:
--
--  * Redistributions of source code must retain the above copyright
--    notice, this list of conditions and the following disclaimer.
--  * Redistributions in binary form must reproduce the above copyright
--    notice, this list of conditions and the following disclaimer in the
--    documentation and/or other materials provided with the distribution.
--  * Neither the name of the University of Kent nor the names of its
--    contributors may be used to endorse or promote products derived from
--    this software without specific prior written permission.
--
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
-- IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
-- THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
-- PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
-- CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
-- EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
-- PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
-- PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
-- LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
-- NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

module Control.Concurrent.CHP.Traces.Base where

import Control.Concurrent.STM
import Control.Monad.State
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Unique

import Control.Concurrent.CHP.Event
import Control.Concurrent.CHP.ProcessId

-- | A globally recorded event, found in CSP and VCR traces.  Either a
-- channel communication (with a unique identifier of the channel) or a
-- barrier synchronisation (with a unique identifier of the barrier).  The
-- identifiers are per channel\/barrier, not per event.  Currently,
-- channels and barriers can never have the same Unique as each other, but
-- do not rely on this behaviour.
--
-- The type became parameterised in version 1.3.0.
type RecordedEvent u = (RecordedEventType, u)

-- | An individual record of an event, found in nested traces.  Either a
-- channel write or read, or a barrier synchronisation, each with a unique
-- identifier for the barrier\/channel.  The event will be recorded by
-- everyone involved, and a ChannelWrite will have the same channel
-- identifier as the corresponding channel-read.  The identifiers are per
-- channel\/barrier, not per event.  Currently, channels and barriers can
-- never have the same Unique as each other, but do not rely on this
-- behaviour.
--
-- ClockSyncIndiv was added in version 1.2.0.
--
-- The type became parameterised, and the Show and Read instances were added in version 1.3.0.
data RecordedIndivEvent u = 
  ChannelWrite u Integer
  | ChannelRead u Integer
  | BarrierSyncIndiv u Integer
  | ClockSyncIndiv u Integer String
  deriving (Eq, Ord, Read, Show)

-- | Added in version 1.3.0.
recordedIndivEventLabel :: RecordedIndivEvent u -> u
recordedIndivEventLabel (ChannelWrite x _) = x
recordedIndivEventLabel (ChannelRead x _) = x
recordedIndivEventLabel (BarrierSyncIndiv x _) = x
recordedIndivEventLabel (ClockSyncIndiv x _ _) = x

-- | Added in version 1.3.0.
recordedIndivEventSeq :: RecordedIndivEvent u -> Integer
recordedIndivEventSeq (ChannelWrite _ n) = n
recordedIndivEventSeq (ChannelRead _ n) = n
recordedIndivEventSeq (BarrierSyncIndiv _ n) = n
recordedIndivEventSeq (ClockSyncIndiv _ n _) = n

indivRec :: (u -> Integer -> RecordedIndivEvent u)
            -> u -> (u -> Integer) -> (RecordedIndivEvent u)
indivRec r u f = r u (f u)

indivRecJust :: (u -> Integer -> RecordedIndivEvent u)
                -> u -> (u -> Integer) -> Maybe (RecordedIndivEvent u)
indivRecJust r u f = Just $ indivRec r u f

type RecEvents = ([RecordedEvent Unique], [RecordedIndivEvent Unique])

getName :: Ord u => String -> u -> State (Map.Map u String) String
getName prefix u
          = do m <- get
               case Map.lookup u m of
                 Just x -> return x
                 Nothing -> let x = prefix ++ show (Map.size m) in
                            do put $ Map.insert u x m
                               return x

nameEvent :: Ord u => RecordedEvent u -> State (Map.Map u String) String
nameEvent (t, c) = liftM (++ suffix) $ getName prefix c
  where
    (prefix, suffix) = case t of
      ChannelComm -> ("_c","")
      BarrierSync -> ("_b","")
      ClockSync st -> ("_t", ':' : st)

nameEvent' :: Ord u => RecordedEvent u -> State (Map.Map u String) (RecordedEvent String)
nameEvent' (t, c) = do c' <- getName prefix c
                       return (t, c' ++ suffix)
  where
    (prefix, suffix) = case t of
      ChannelComm -> ("_c","")
      BarrierSync -> ("_b","")
      ClockSync st -> ("_t", ':' : st)


nameIndivEvent :: Ord u => RecordedIndivEvent u -> State (Map.Map u String) String
nameIndivEvent (ChannelWrite c n) = do c' <- getName "_c" c
                                       return $ c' ++ "![" ++ show n ++ "]"
nameIndivEvent (ChannelRead c n) = do c' <- getName "_c" c
                                      return $ c' ++ "?[" ++ show n ++ "]"
nameIndivEvent (BarrierSyncIndiv c n) = do c' <- getName "_b" c
                                           return $ c' ++ "[" ++ show n ++ "]"
nameIndivEvent (ClockSyncIndiv c n t) = do c' <- getName "_t" c
                                           return $ c' ++ ":" ++ t
                                             ++ "[" ++ show n ++ "]"

nameIndivEvent' :: Ord u => RecordedIndivEvent u -> State (Map.Map u String) (RecordedIndivEvent String)
nameIndivEvent' (ChannelWrite c n) = do c' <- getName "_c" c
                                        return $ ChannelWrite c' n
nameIndivEvent' (ChannelRead c n) = do c' <- getName "_c" c
                                       return $ ChannelRead c' n
nameIndivEvent' (BarrierSyncIndiv c n) = do c' <- getName "_b" c
                                            return $ BarrierSyncIndiv c' n
nameIndivEvent' (ClockSyncIndiv c n t) = do c' <- getName "_t" c
                                            return $ ClockSyncIndiv c' n t


type TraceT = StateT TraceStore

data TraceStore =
  NoTrace
  | Trace (ProcessId, TVar (ChannelLabels Unique), SubTraceStore)

mapSubTrace :: (SubTraceStore -> SubTraceStore) -> TraceStore -> TraceStore
mapSubTrace _ NoTrace = NoTrace
mapSubTrace f (Trace (pid, tv, s)) = Trace (pid, tv, f s)

type ChannelLabels u = Map.Map u String

data SubTraceStore =
  Hierarchy (Structured (RecordedIndivEvent Unique))
  | CSPTraceRev (TVar [(Int, [RecordedEvent Unique])])
  | VCRTraceRev (TVar [Set.Set (Set.Set ProcessId, RecordedEvent Unique)])

data Ord a => Structured a =
  StrEvent a
  | Par [Structured a]
  | RevSeq [(Int, [Structured a])]
  deriving (Eq, Ord)

-- | Records an event where you were the last person to engage in the event
recordEventLast :: [(RecordedEvent Unique, Set.Set ProcessId)] -> TraceStore -> STM ()
recordEventLast news y
           =    case y of
                  Trace (_,_,CSPTraceRev tv) ->
                    do t <- readTVar tv
                       writeTVar tv $! foldl (flip addRLE) t (map fst news)
                  Trace (pid, _, VCRTraceRev tv) -> do
                    t <- readTVar tv
                    let pidSet = (foldl Set.union (Set.singleton pid) $ map snd news)
                        news' = map (\(a,b) -> (b,a)) news
                        t' = case t of
                                -- Trace previously empty:
                               [] -> [Set.fromList news']
                               (z:zs) | shouldMakeNewSetVCR pidSet z
                                         -> Set.fromList news' : t
                                      | otherwise
                                          -> foldl (flip Set.insert) z news' : zs
                    writeTVar tv $! t'
                  _ -> return ()

-- | Records an event where you were one of the people involved
recordEvent :: [RecordedIndivEvent Unique] -> TraceT IO ()
recordEvent e = modify $ mapSubTrace $ \(Hierarchy es) ->
                  Hierarchy (addParEventsH (map StrEvent e) es)

mergeSubProcessTraces :: [TraceStore] -> TraceT IO ()
mergeSubProcessTraces ts
  = modify $ mapSubTrace $ \(Hierarchy es) -> Hierarchy (addParEventsH ts' es)
  where
    ts' = [t | Trace (_,_,Hierarchy t) <- ts]

shouldMakeNewSetVCR :: Set.Set ProcessId -> Set.Set (Set.Set ProcessId, RecordedEvent Unique)
  -> Bool
shouldMakeNewSetVCR newIds existingSet
  = exists existingSet $ \(bigP,_) -> exists bigP $ \p -> exists newIds $ \q ->
      p `pidLessThanOrEqual` q
  where
    -- Like the any function (flipped), but for sets:
    exists :: Ord a => Set.Set a -> (a -> Bool) -> Bool
    exists s f = not . Set.null $ Set.filter f s


compress :: (Eq a, Ord a) => Structured a -> Structured a
compress (RevSeq ((1,s):(n,s'):ss))
  | n == 1 && (s `isPrefixOf` s') = compress $ RevSeq $ (2,s):(1,drop (length s) s'):ss
  | s == s' = compress $ RevSeq $ (n+1,s'):ss
compress x = x


addParEventsH :: (Eq a, Ord a) => [Structured a] -> Structured a -> Structured a
addParEventsH es t = let n = es in case t of
  StrEvent _ -> RevSeq [(1, [Par n, t])]
  Par _ -> RevSeq [(1, [Par n, t])]
  RevSeq ((1,s):ss) -> compress $ RevSeq $ (1,Par n : s) : ss
  RevSeq ss -> compress $ RevSeq $ (1, [Par n]):ss

addSeqEventH :: (Eq a, Ord a) => a -> Structured a -> Structured a
addSeqEventH e (StrEvent e') = RevSeq [(1,[StrEvent e, StrEvent e'])]
addSeqEventH e (Par p) = RevSeq [(1,[StrEvent e, Par p])]
addSeqEventH e (RevSeq ((1,s):ss))
  | (StrEvent e) `notElem` s = compress $ RevSeq $ (1,StrEvent e:s):ss
addSeqEventH e (RevSeq ss) = compress $ RevSeq $ (1,[StrEvent e]):ss


addRLE :: Eq a => a -> [(Int,[a])] -> [(Int,[a])]
-- Single event in most recent list:
addRLE x ((n,[e]):nes)
  -- If we have the same event, bump up the count:
  | x == e = (n+1,[e]):nes
-- Only one list thus far
addRLE x allEs@[(1,es)]
  -- If we are the same as the most recent event, break it off and aggregate:
  | x == head es = [(2, [x]), (1, tail es)]
  -- If we're already in that list, start a new one:
  | x `elem` es = (1,[x]):allEs
  -- Otherwise join the queue!
  | otherwise = [(1,x:es)]
-- Most recent list has count of 1
addRLE x allEs@((1,es):(n,es'):nes)
  -- If adding us to the most recent list forms an identical list to the one
  -- before that, aggregate
  | x == head es' && es == tail es' = (n+1,es'):nes
  -- If we're already in that list, start a new one:
  | x `elem` es = (1,[x]):allEs
  -- Otherwise, join the most recent list
  | otherwise = (1,x:es):(n,es'):nes
-- If no special cases hold, start a new list:
addRLE x nes = (1,[x]):nes


labelEvent :: Event -> String -> StateT TraceStore IO ()
labelEvent e l
  = labelUnique (getEventUnique e) l

labelUnique :: Unique -> String -> StateT TraceStore IO ()
labelUnique u l
  = do t <- get
       case t of
         NoTrace -> return ()
         Trace (_,tvls,_) -> add tvls
  where
    add :: TVar (Map.Map Unique String) -> StateT TraceStore IO ()
    add tv = liftIO $ atomically $ do
      m <- readTVar tv
      writeTVar tv $ Map.insert u l m


blankTraces :: TraceStore -> Int -> IO [TraceStore]
blankTraces NoTrace n = return $ replicate n NoTrace
blankTraces (Trace (pid, tvls, subT)) n =
  return [Trace (newId, tvls, newSubT) | newId <- newIds]
  where
    newIds :: [ProcessId]
    newIds = let ProcessId parts = pid in
      [ProcessId $ parts ++ [ParSeq i 0] | i <- [0 .. (n - 1)]]

    newSubT :: SubTraceStore
    newSubT = case subT of
      Hierarchy {} -> Hierarchy $ RevSeq []
      _ -> subT