module Control.Concurrent.CHPSpec.Monad
(
CHP, MonadCHP(..), liftIO_CHP, liftIO_CHP', foreverP, specify, Process, process, subProcess,
onPoisonTrap, onPoisonRethrow, throwPoison, Poisonable(..), poisonAll,
skip, stop
) where
import Control.Applicative ((<$>))
import Control.Arrow
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Foldable as F (toList)
import Data.Function (on)
import Data.List (intercalate, nubBy)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Traversable as T
import qualified Text.PrettyPrint.HughesPJ as PP
import Control.Concurrent.CHPSpec.Base
import Control.Concurrent.CHPSpec.CSP
import Control.Concurrent.CHPSpec.LazySmallCheck
import Control.Concurrent.CHPSpec.Print
import Control.Concurrent.CHPSpec.Process
import Control.Concurrent.CHPSpec.Spec
foreverP :: CHP a -> CHP b
foreverP = stopSpecT . liftM (Repeat . snd) . finSpecT
skip :: CHP ()
skip = return ()
stop :: CHP a
stop = stopSpecT $ return Stop
fromMaybeStr :: String -> Maybe String -> String
fromMaybeStr def m = case m of
Just str | not (null str) -> str
_ -> def
iter :: (Eq events, Ord k) => (Map.Map k events -> spec -> events) -> (Map.Map k (spec, events)) -> (Map.Map k (spec, events))
iter f m = let m' = Map.map ((id &&& f (Map.map snd m)) . fst) m
in if Map.map snd m == Map.map snd m'
then m'
else iter f m'
specify :: Bool -> CHP () -> IO String
specify showIO main
= specify' showIO <$> execStateT (finSpecT $ process "main" main) emptyCHPState
where
emptyCHPState = CHPState Map.empty Set.empty Map.empty [] 1 1
specify' :: Bool -> CHPState -> String
specify' showIO st = render specs ++ declMain
where
render :: Map.Map String [SpecItem' String String] -> String
render = PP.render . PP.vcat . (map pprintForwardDecl allChans ++) . map (pprintProc eventMap) . Map.toList
declMain :: String
declMain = "\nmain = main_1 " ++ (if showIO then "" else
"\\ {" ++ intercalate "," (map getName $ Set.toList $ chpIOEvents st) ++ "}"
) ++ "\n"
where
getName = fromJust . flip Map.lookup events
pulledProcesses :: Map.Map (Integer, String) [SpecItem]
pulledProcesses =
collapseMapMap (\s n -> (n, s ++ "_" ++ show n))
(Map.unionWith Map.union oldProcs pulledProcs)
where
rawProcesses :: Map.Map String (Map.Map Integer Spec)
rawProcesses = Map.map (Map.map (fst . snd)) $ chpProcessMap st
rep :: Spec -> State (Integer, Map.Map String (Map.Map Integer Spec)) Integer
rep x = do (!n, m) <- get
put (succ n, insertMapMap "repeated" n (x ++ [Call n]) m)
return n
oldProcs, pulledProcs :: Map.Map String (Map.Map Integer Spec)
(oldProcs, (_, pulledProcs))
= runState (T.mapM (T.mapM $ T.mapM $ pullUpRepeatM rep) rawProcesses)
(chpNextProcess st, Map.empty)
specs :: Map.Map String [SpecItem' String String]
specs = Map.mapKeys snd $ Map.map (fmap (subSpec showProc showComm) . pruneSpec) pulledProcesses
where
showProc :: ProcessId -> String
showProc p = fromMaybeStr ("p_" ++ show p) $ Map.lookup p procs
showComm :: CommId -> String
showComm (Left c) = fromMaybeStr ("c_" ++ show c) $ Map.lookup c events
showComm (Right (c, d, x)) = showComm (Left c) ++ (if d == DirInput
then "?" else "!") ++ "x_" ++ show x
procs = Map.fromList $ Map.keys pulledProcesses
allChans = nubBy ((==) `on` baseName) $ F.toList $ foldr Set.union Set.empty $ Map.elems eventMap
events = chpEventMap st
eventMap = Map.map snd $ iter (findAllComms baseName) $ Map.map (flip (,) Set.empty) $ specs
baseName = takeWhile (`notElem` "?!.")
liftIO_CHP' :: Serial a => String -> IO a -> CHP a
liftIO_CHP' label _ = CHPSpecT $ \k ->
do (vals, complete) <- fuzz k
unless complete $
liftIO $ putStrLn "Incomplete fuzzing of IO computation"
nonces <- replicateM (length vals) newEvent
let firstLabel = "IO_" ++ label ++ show (head nonces)
zipWithM_ labelEvent nonces (map (firstLabel++) suffixes)
modify $ \st -> st { chpIOEvents = Set.union
(Set.fromList nonces) (chpIOEvents st) }
return (error "liftIO return", \s -> [Alt $ zipWith (\n f -> Sync (Left n) : snd f s) nonces vals])
where
suffixes = map (:[]) ['A'..'Z'] ++ map show [(0::Integer)..]
liftIO_CHP :: Serial a => IO a -> CHP a
liftIO_CHP = liftIO_CHP' ""