-- 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.
type RecordedEvent = (RecordedEventType, Unique)

-- | 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.
data RecordedIndivEvent = 
  ChannelWrite Unique
  | ChannelRead Unique
  | BarrierSyncIndiv Unique
  deriving (Eq, Ord)

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

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

nameEvent :: RecordedEvent -> State (Map.Map Unique String) String
nameEvent (_, c) = getName c

nameIndivEvent :: RecordedIndivEvent -> State (Map.Map Unique String) String
nameIndivEvent (ChannelWrite c) = do c' <- getName c
                                     return $ c' ++ "!"
nameIndivEvent (ChannelRead c) = do c' <- getName c
                                    return $ c' ++ "?"
nameIndivEvent (BarrierSyncIndiv c) = do c' <- getName c
                                         return $ c' ++ "*"

ensureAllNamed :: Map.Map Unique String -> [RecordedEvent] -> Map.Map Unique String
-- Quite hacky:
ensureAllNamed m es = execState (mapM_ nameEvent es) m

ensureAllNamedIndiv :: Map.Map Unique String -> [RecordedIndivEvent] -> Map.Map Unique String
-- Quite hacky:
ensureAllNamedIndiv m es = execState (mapM_ nameIndivEvent es) m


-- The list of integers is for alting
type TraceT = StateT ([Int], TraceStore)

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

type ChannelLabels = Map.Map Unique String

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

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, 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] -> TraceT IO ()
recordEvent e
           = do (x,y) <- get
                case (x, y) of
                  (as, Trace (pid,tvls,Hierarchy es)) ->
                       put (as, Trace (pid, tvls, Hierarchy (foldl (flip addSeqEventH) es e)))
                  _ -> return ()

mergeSubProcessTraces :: [TraceStore] -> TraceT IO ()
mergeSubProcessTraces ts
  = do s <- get
       case s of
         (as, Trace (pid, tvls, Hierarchy es)) ->
           put (as, Trace (pid, tvls, Hierarchy $ addParEventsH ts' es))
           where ts' = [t | Trace (_,_,Hierarchy t) <- ts]
         _ -> return ()


shouldMakeNewSetVCR :: Set.Set ProcessId -> Set.Set (Set.Set ProcessId, RecordedEvent)
  -> 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 (a, TraceStore) IO ()
labelEvent e l
  = labelUnique (getEventUnique e) l

labelUnique :: Unique -> String -> StateT (a, 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 (a, 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