{-# OPTIONS -fglasgow-exts #-}

{-
 - Copyright (c) 2008,  Jochem Berndsen
 - All rights reserved.
 - 
 - Redistribution and use in source and binary forms, with or without
 - modification, are permitted provided that the following conditions
 - are met:
 - 
 -   1. Redistributions of source code must retain the above copyright
 -      notice, this list of conditions and the following disclaimer.
 -   2. 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.
 -   3. Neither the name of the author 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 HOLDER 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 FOUNDATION 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.Hasim.Process
-- Copyright   : (c) Jochem Berndsen 2008
-- License     : BSD3
--
-- Maintainer  : jochem@functor.nl
-- Stability   : experimental
-- Portability : unportable
--
-- This module takes care of defining processes and their actions.

-- We need GHC extensions due to GADTs, existentials,
-- multiparameter type classes and functional dependencies.

module Control.Hasim.Process (
    Proc(..),

    Acceptor,
    Process(..),
    PrimAction(..),
    Action(Prim),
    Atom(..),
    Runnable(..),
    runnable2process,
    toRunnable,
    AcceptResult(..)

) where

-- Internal imports
import Control.Hasim.Types

-- External imports
import Control.Monad.State
import Control.Monad.Trans
import Data.IORef

-- | A @Proc st pkt@ is a process that potentially accepts packets of type 
-- @pkt@ while maintaining state @st@.
data Proc pkt st = Proc { acceptor :: IORef [(Acceptor pkt st, Maybe Runnable)]
                          -- ^ The list of acceptors with the continuations
                          -- after the WithAcceptor.
   
                        , wakeup :: IORef (Maybe Runnable)
                          -- ^ The current wakeup function, if any. 

                        , action :: IORef (Maybe Runnable)
                          -- ^ The starting action. Loses its relevance
                          -- after startup of the simulation.
   
                        , identifier :: Id
                          -- ^ The identifier of this process. Must be unique
                          -- or hell will ensue. Guaranteed to be unique by
                          -- the creator of the process.
   
                        , name :: String
                          -- ^ The name of the process. Determined by the user,
                          -- may be any string. Used for displaying information
                          -- to the user.
                        
                        , currentState :: IORef st
                          -- ^ The state of the process.
                        }

-- | An acceptor of a @pkt@ is an 'AcceptResult', which is either
--   * @Refuse@ if the packet is to be delivered at a later time, or
--   never, of course
--   * @Parallel act@ if a current computation should not be suspended,
--   but the state should be changed.
--   * @Interrupt act@ if the current computation should be suspended.
type Acceptor pkt st = pkt -> AcceptResult pkt st

-- | The type of result of the 'Acceptor'
data AcceptResult pkt st = Refuse
                         | Parallel (st -> st)
                         | Interrupt (Action pkt st ())

-- Useful instance for debugging
instance Show (Proc pkt st) where
    show p = "Proc<" ++ name p ++ ">"

instance Eq (Proc pkt st) where
    p == p' = identifier p == identifier p'
    p /= p' = identifier p /= identifier p'

-- We need this if we want to store Proc's in a Map or Set
instance Ord (Proc pkt st) where
    p `compare` p' = identifier p `compare` identifier p'
    p <= p' = identifier p <= identifier p'
    p < p' = identifier p < identifier p'
    p > p' = identifier p > identifier p'
    p >= p' = identifier p >= identifier p'

-- Useful instance for debugging
instance Show Process where
    show (Process p) = "Process<" ++ name p ++ ">"

instance Eq Process where
    (Process p) == (Process p') = identifier p == identifier p'
    (Process p) /= (Process p') = identifier p /= identifier p'

-- We need this if we want to store Processes in a Map or Set
instance Ord Process where
    (Process p) `compare` (Process p') = identifier p `compare` identifier p'
    (Process p) <= (Process p') = identifier p <= identifier p'
    (Process p) < (Process p') = identifier p < identifier p'
    (Process p) > (Process p') = identifier p > identifier p'
    (Process p) >= (Process p') = identifier p >= identifier p'
  
-- | Existential type for a 'Proc'. A 'Process' is a @Proc pkt@
-- for some @pkt@.
data Process = forall pkt st. Process (Proc pkt st)

-- | GADT for the primitive actions. These are the primitives
-- Hasim supports. 
--
-- A @PrimAction pkt st a@ is a primitive action where
--   * @pkt@ is the packet type the associated 'Proc' supports.
--   * @st@ is the state of the associated 'Proc'.
--   * @a@ is the return type of the PrimAction.
--   (this is why we need a GADT; the return type
--   varies for each primitive action).
data PrimAction :: * -> * -> * -> * where
    -- Returning a value. Used to implement @return@ in the 'Action'
    -- monad.
    Ret :: a -> PrimAction pkt st a

    -- Wait for a nonnegative time period. The parameter is the
    -- _absolute time_ until we wait.
    Wait :: Time -> PrimAction pkt st ()

    -- Send a packet to a process, with a maximum time.
    -- Returns whether the sending succeeded. Initiates a watch of the
    -- target process.
    Send :: snd -> Proc snd st2 -> Time -> PrimAction pkt st Bool

    -- Removes the watch of a certain target process. Used to implement
    -- the timeout of a send.
    Unwatch :: Proc rcv st2 -> PrimAction pkt st ()

    -- Perform an action with a certain new acceptor. The new acceptor
    -- and the current continuation are pushed onto the acceptor stack.
    WithAcceptor :: Acceptor pkt st -> Action pkt st () -> PrimAction pkt st ()

    -- Pop the top acceptor + continuation from the acceptor stack.
    PopAcceptor :: PrimAction pkt st ()

    -- Perform an arbitrary I/O operation. The result from the I/O
    -- operation is returned.
    PerformIO :: IO a -> PrimAction pkt st a

    -- Return the current time.
    ObserveTime :: PrimAction pkt st Time

    -- Inspect the state of the process.
    GetState :: PrimAction pkt st st

    -- Set the new state of the process.
    PutState :: st -> PrimAction pkt st ()

    -- Remove us from the DES.
    WaitForever :: PrimAction pkt st ()


-- Useful instance for debugging.
instance Show (PrimAction pkt st a) where
    show (Ret _) = "Ret<_>"
    show (Wait time) = "Wait<" ++ show time ++ ">"
    show (Send _ proc maxtime) =
        "Send<_," ++ show proc ++ "," ++ show maxtime ++ ">"
    show (WithAcceptor _ _) = "WithAcceptor<_,_>"
    show (Unwatch proc) = "Unwatch<" ++ show proc ++ ">"
    show (PopAcceptor) = "PopAcceptor"
    show (PerformIO _) = "PerformIO<_>"
    show (ObserveTime) = "ObserveTime"
    show (GetState) = "GetState"
    show (PutState _) = "PutState<_>"
    show WaitForever = "WaitForever"

-- | The @Action@ GADT. This is a GADT with three
-- parameters; an @Action pkt st a@ is a action where
--   * pkt denotes the packet type of incoming packets
--   * st denotes the state that can be modified
--     and inspected
--   * a denotes the result value of the @Action@
data Action :: * -> * -> * -> * where
    -- Perform a primitive action.
    Prim :: PrimAction pkt st a -> Action pkt st a
    
    -- Monadic sequencing of actions.
    (:>>=) :: Action pkt st a -> (a -> Action pkt st b) -> Action pkt st b

-- The Monad instance for the @Action@ GADT.
instance Monad (Action pkt st) where
    return = Prim . Ret
    (>>=) = (:>>=)

-- The MonadIO instance for the @Action@ GADT.
instance MonadIO (Action pkt st) where
    liftIO = Prim . PerformIO

-- The MonadState instance for the @Action@ GADT.
instance MonadState st (Action pkt st) where
    put = Prim . PutState
    get = Prim $ GetState
    

-- | Existential type for the 'PrimAction' type.
data Atom = forall a st pkt. Atom (PrimAction pkt st a)

-- | A 'Runnable' is an action that can be run. A 'Runnable' has
-- three parameters:
--   * The first is the process to which this 'Runnable' belongs.
--   * The second is a primitive action to be run.
--   * The third is Maybe a continuation.
data Runnable = forall a pkt st. 
    Run (Proc pkt st) (PrimAction pkt st a) (Maybe (a -> Runnable))    

-- | Finds the 'Process' (existential type) belonging to a 'Runnable'.
runnable2process :: Runnable -> Process
runnable2process (Run proc _ _) = Process proc


-- Helper functions

atom :: Action pkt st a -> Bool
atom (Prim _) = True
atom _ = False

unprim :: Action pkt st a -> PrimAction pkt st a
unprim (Prim x) = x
unprim _ = error "PrimAction.unprim : error : not an atom"

unleft :: Action pkt st a -> Action pkt st a
unleft ((m :>>= k) :>>= l) = m :>>= (\x -> (k x :>>= l))
unleft x = x

-- | Converts a process with an action to a 'Runnable'. 
toRunnable :: Proc pkt st -> Action pkt st () -> Runnable
-- We need to find the first atomic action. 
-- Distinct two cases; the first is if this action is a
-- composed one; in that case it is the leftmost action if
-- that is a primitive; or retry with the 'unleft' function.
-- This function makes the :>>= constructors go "more to the right",
-- hence we eventually terminate.
toRunnable proc a@(m :>>= f) 
    | atom m = Run proc (unprim m) (Just (\x -> toRunnable proc (f x)))
    | otherwise = toRunnable proc (unleft a)
-- The second case is if this action is primitive. This case is trivial.
toRunnable proc (Prim x) = Run proc x Nothing