module CSPM.Compiler.Processes (
Proc(..),
ProcOperator(..),
ProcName(..),
prettyPrintAllRequiredProcesses,
) where
import qualified CSPM.Compiler.Map as M
import qualified CSPM.Compiler.Set as S
import CSPM.Compiler.Events
import CSPM.DataStructures.Names
import CSPM.Evaluator.Values
import Util.PrettyPrint
data ProcName = ProcName {
name :: Name,
arguments :: [[Value]]
}
instance Eq ProcName where
pn1 == pn2 = name pn1 == name pn2 && arguments pn1 == arguments pn2
instance PrettyPrintable ProcName where
prettyPrint (ProcName n args) =
prettyPrint n
<> hcat (map (\as -> parens (list (map prettyPrint as))) args)
instance Show ProcName where
show pn = show (prettyPrint pn)
data ProcOperator =
Chase
| Diamond
| Explicate
| Normalize
| ModelCompress
| StrongBisim
| TauLoopFactor
| WeakBisim
deriving (Eq)
instance PrettyPrintable ProcOperator where
prettyPrint Chase = text "chase"
prettyPrint Diamond = text "diamond"
prettyPrint Explicate = text "explicate"
prettyPrint Normalize = text "normal"
prettyPrint ModelCompress = text "model_compress"
prettyPrint StrongBisim = text "sbisim"
prettyPrint TauLoopFactor = text "tau_loop_factor"
prettyPrint WeakBisim = text "wbisim"
instance Show ProcOperator where
show p = show (prettyPrint p)
data Proc =
PAlphaParallel [(S.Set Event, Proc)]
| PException Proc (S.Set Event) Proc
| PExternalChoice [Proc]
| PGenParallel (S.Set Event) [Proc]
| PHide Proc (S.Set Event)
| PInternalChoice [Proc]
| PInterrupt Proc Proc
| PInterleave [Proc]
| PLinkParallel Proc (M.Map Event Event) Proc
| POperator ProcOperator Proc
| PPrefix Event Proc
| PRename (M.Relation Event Event) Proc
| PSequentialComp Proc Proc
| PSlidingChoice Proc Proc
| PProcCall ProcName Proc
instance PrettyPrintable Proc where
prettyPrint (PAlphaParallel aps) =
text "||" <+> braces (list (map (\ (a,p) ->
parens (prettyPrint a <> char ',' <+> prettyPrint p)) aps))
prettyPrint (PException p1 a p2) =
prettyPrint p1 <+> text "[|" <> prettyPrint a <> text "|>"
<+> prettyPrint p2
prettyPrint (PExternalChoice ps) =
sep (punctuateFront (text "[] ") (map prettyPrint ps))
prettyPrint (PGenParallel a ps) =
text "||" <+> brackets (prettyPrint a)
<+> braces (list (map prettyPrint ps))
prettyPrint (PHide p a) =
prettyPrint p <+> char '\\' <+> prettyPrint a
prettyPrint (PInternalChoice ps) =
sep (punctuateFront (text "|~| ") (map prettyPrint ps))
prettyPrint (PInterleave ps) =
sep (punctuateFront (text "||| ") (map prettyPrint ps))
prettyPrint (PLinkParallel p1 evm p2) =
prettyPrint p1 <+> text "[" <>
list (map (\(evLeft, evRight) -> prettyPrint evLeft <+> text "<-"
<+> prettyPrint evRight) evm)
<> text "]" <+> prettyPrint p2
prettyPrint (POperator op p) =
prettyPrint op <> parens (prettyPrint p)
prettyPrint (PPrefix e p) =
prettyPrint e <+> text "->" <+> prettyPrint p
prettyPrint (PRename evm p) =
prettyPrint p <> text "[["
<> list (map (\ (evOld, evNew) ->
prettyPrint evOld <+> text "<-"
<+> prettyPrint evNew) evm)
<> text "]]"
prettyPrint (PSequentialComp p1 p2) =
prettyPrint p1 <+> text "->" <+> prettyPrint p2
prettyPrint (PSlidingChoice p1 p2) =
prettyPrint p1 <+> text "|>" <+> prettyPrint p2
prettyPrint (PProcCall n _) = prettyPrint n
instance Show Proc where
show p = show (prettyPrint p)
splitProcIntoComponents :: Proc -> (Proc, [(ProcName, Proc)])
splitProcIntoComponents p =
let
explored pns n = n `elem` (map fst pns)
exploreAll :: [(ProcName, Proc)] -> [Proc] -> [(ProcName, Proc)]
exploreAll pns [] = pns
exploreAll pns (p:ps) = exploreAll (explore pns p) ps
explore :: [(ProcName, Proc)] -> Proc -> [(ProcName, Proc)]
explore pns (PAlphaParallel aps) = exploreAll pns ps
where ps = map snd aps
explore pns (PException p1 _ p2) = exploreAll pns [p1, p2]
explore pns (PExternalChoice ps) = exploreAll pns ps
explore pns (PGenParallel _ ps) = exploreAll pns ps
explore pns (PHide p _) = explore pns p
explore pns (PInternalChoice ps) = exploreAll pns ps
explore pns (PInterrupt p1 p2) = exploreAll pns [p1, p2]
explore pns (PInterleave ps) = exploreAll pns ps
explore pns (PLinkParallel p1 _ p2) = exploreAll pns [p1, p2]
explore pns (POperator _ p) = explore pns p
explore pns (PPrefix _ p) = explore pns p
explore pns (PRename _ p) = explore pns p
explore pns (PSequentialComp p1 p2) = exploreAll pns [p1, p2]
explore pns (PSlidingChoice p1 p2) = exploreAll pns [p1, p2]
explore pns (PProcCall n p) =
if explored pns n then pns
else explore ((n, p):pns) p
in (p, explore [] p)
prettyPrintAllRequiredProcesses :: Proc -> Doc
prettyPrintAllRequiredProcesses p =
let
(pInit, namedPs) = splitProcIntoComponents p
ppNamedProc (n,p) =
hang (prettyPrint n <+> char '=') tabWidth (prettyPrint p)
in
vcat (punctuate (char '\n') ((map ppNamedProc namedPs)++[prettyPrint pInit]))