-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Definition of a FDR-compatible CSP core-language.
--   
--   This package contains an interface for a CSP core-language. It defines
--   processes, events, event sets, a EDSL for process operations like
--   parallel or interleaving. This interface can be used to implement a
--   FDR-2.83 compatible CSPM animator. We use this interface in our tool
--   to connect the functional CSPM-sub-language with core CSP
--   functionality.
@package CSPM-CoreLanguage
@version 0.1.0.1


-- | This modules defines the event-related part of an interface between
--   the CSPM-CoreLanguage and the underlying implementation. The
--   underlying implementation has to instantiate the type-families
--   <a>Event</a>, <a>EventSet</a> and <a>RenamingRelation</a> and the
--   class <a>BE</a> (<a>BE</a>== base event).
--   
--   For full CSPM-support (channels with multiple fields, event closure
--   sets etc.) CSPM.CoreLanguage.Field is also needed.
module CSPM.CoreLanguage.Event

-- | Sigma is the set of all events that appear in a system.
type Sigma i = EventSet i

-- | The first argument of all function in <a>BE</a> is a
--   phantom-type-argument, i.e. applications pass _|_ and implementations
--   must not use this value.
class BE i
eventEq :: (BE i) => i -> Event i -> Event i -> Bool
member :: (BE i) => i -> Event i -> EventSet i -> Bool
intersection :: (BE i) => i -> EventSet i -> EventSet i -> EventSet i
difference :: (BE i) => i -> EventSet i -> EventSet i -> EventSet i
union :: (BE i) => i -> EventSet i -> EventSet i -> EventSet i
null :: (BE i) => i -> EventSet i -> Bool
singleton :: (BE i) => i -> Event i -> EventSet i
insert :: (BE i) => i -> Event i -> EventSet i -> EventSet i
delete :: (BE i) => i -> Event i -> EventSet i -> EventSet i
eventSetToList :: (BE i) => i -> EventSet i -> [Event i]
allEvents :: (BE i) => i -> EventSet i
isInRenaming :: (BE i) => i -> RenamingRelation i -> Event i -> Event i -> Bool
imageRenaming :: (BE i) => i -> RenamingRelation i -> Event i -> [Event i]
preImageRenaming :: (BE i) => i -> RenamingRelation i -> Event i -> [Event i]
isInRenamingDomain :: (BE i) => i -> Event i -> RenamingRelation i -> Bool
isInRenamingRange :: (BE i) => i -> Event i -> RenamingRelation i -> Bool
getRenamingDomain :: (BE i) => i -> RenamingRelation i -> [Event i]
getRenamingRange :: (BE i) => i -> RenamingRelation i -> [Event i]
renamingFromList :: (BE i) => i -> [(Event i, Event i)] -> RenamingRelation i
renamingToList :: (BE i) => i -> RenamingRelation i -> [(Event i, Event i)]
singleEventToClosureSet :: (BE i) => i -> Event i -> EventSet i

-- | A wrapper for tick-events, tau-events and events from Sigma.
data TTE i
TickEvent :: TTE i
TauEvent :: TTE i
SEvent :: (Event i) -> TTE i
class ShowEvent i
showEvent :: (ShowEvent i) => i -> String
class ShowTTE i
showTTE :: (ShowTTE i) => i -> String


-- | This modules defines a FDR-compatible CSP core language. The core
--   language deals with CSP related constructs like processes and events,
--   but abstracts, e.g. from the underlying functional programming
--   language.
--   
--   The implementation of the underlying language must provide instances
--   for the type families <a>Prefix</a> and <a>ExtProcess</a> and class
--   <a>BL</a>.
module CSPM.CoreLanguage.Process

-- | A prefix expression.

-- | A proccess that has not yet been switched on.
class (BE i) => BL i
prefixNext :: (BL i) => Prefix i -> Event i -> Maybe (Process i)
switchOn :: (BL i) => ExtProcess i -> Process i

-- | A data type for CSPM processes. For efficency, replicated alphabetized
--   parallel has an explicit constructor. Other replicated operations get
--   translated on the fly. For constructing processes one should rather
--   uses the wrappers from CSPM.CoreLanguage.ProcessWrappers.
data Process i
Prefix :: (Prefix i) -> Process i
ExternalChoice :: (Process i) -> (Process i) -> Process i
InternalChoice :: (Process i) -> (Process i) -> Process i
Interleave :: (Process i) -> (Process i) -> Process i
Interrupt :: (Process i) -> (Process i) -> Process i
Timeout :: (Process i) -> (Process i) -> Process i
Sharing :: (Process i) -> (EventSet i) -> (Process i) -> Process i
AParallel :: (EventSet i) -> (EventSet i) -> (Process i) -> (Process i) -> Process i
RepAParallel :: [(EventSet i, Process i)] -> Process i
Seq :: (Process i) -> (Process i) -> Process i
Hide :: (EventSet i) -> (Process i) -> Process i
Stop :: Process i
Skip :: Process i
Omega :: Process i
Chaos :: (EventSet i) -> Process i

-- | Just for debugging.
AProcess :: Int -> Process i
SwitchedOff :: (ExtProcess i) -> Process i
Renaming :: (RenamingRelation i) -> (Process i) -> Process i
LinkParallel :: (RenamingRelation i) -> (Process i) -> (Process i) -> Process i
isOmega :: Process i -> Bool


-- | Wrappers for the constructors of data type <a>Process</a> and some
--   rewriting rules for replicated operations.
--   
--   This can also be used an EDSL for CSP.
module CSPM.CoreLanguage.ProcessWrapper
prefix :: Prefix i -> Process i
externalChoice :: Process i -> Process i -> Process i
internalChoice :: Process i -> Process i -> Process i
interleave :: Process i -> Process i -> Process i
interrupt :: Process i -> Process i -> Process i
timeout :: Process i -> Process i -> Process i
sharing :: Process i -> EventSet i -> Process i -> Process i
aparallel :: EventSet i -> EventSet i -> Process i -> Process i -> Process i
seq :: Process i -> Process i -> Process i
hide :: EventSet i -> Process i -> Process i
stop :: Process i
skip :: Process i
switchedOff :: ExtProcess i -> Process i
renaming :: RenamingRelation i -> Process i -> Process i
linkParallel :: RenamingRelation i -> Process i -> Process i -> Process i
repSeq :: [Process i] -> Process i
repInternalChoice :: [Process i] -> Process i
repExternalChoice :: [Process i] -> Process i
repInterleave :: [Process i] -> Process i
repAParallel :: [(EventSet i, Process i)] -> Process i
repSharing :: EventSet i -> [Process i] -> Process i
repLinkParallel :: RenamingRelation i -> [Process i] -> Process i
chaos :: EventSet i -> Process i


-- | This modules extends <a>BE</a> for languages that also support
--   multi-field-events and event-closure sets.
module CSPM.CoreLanguage.Field
class (BL i) => BF i
fieldEq :: (BF i) => i -> Field i -> Field i -> Bool
member :: (BF i) => i -> Field i -> FieldSet i -> Bool
intersection :: (BF i) => i -> FieldSet i -> FieldSet i -> FieldSet i
difference :: (BF i) => i -> FieldSet i -> FieldSet i -> FieldSet i
union :: (BF i) => i -> FieldSet i -> FieldSet i -> FieldSet i
null :: (BF i) => i -> FieldSet i -> Bool
singleton :: (BF i) => i -> Field i -> FieldSet i
insert :: (BF i) => i -> Field i -> FieldSet i -> FieldSet i
delete :: (BF i) => i -> Field i -> FieldSet i -> FieldSet i
fieldSetToList :: (BF i) => i -> FieldSet i -> [Field i]
fieldSetFromList :: (BF i) => i -> [Field i] -> FieldSet i
joinFields :: (BF i) => i -> [Field i] -> Event i
splitFields :: (BF i) => i -> Event i -> [Field i]
channelLen :: (BF i) => i -> Field i -> Int
closureStateInit :: (BF i) => i -> EventSet i -> ClosureState i
closureStateNext :: (BF i) => i -> ClosureState i -> Field i -> ClosureState i
closureRestore :: (BF i) => i -> ClosureState i -> EventSet i
viewClosureState :: (BF i) => i -> ClosureState i -> ClosureView
viewClosureFields :: (BF i) => i -> ClosureState i -> FieldSet i
seenPrefixInClosure :: (BF i) => i -> ClosureState i -> Bool
prefixStateInit :: (BF i) => i -> Prefix i -> PrefixState i
prefixStateNext :: (BF i) => i -> PrefixState i -> Field i -> Maybe (PrefixState i)
prefixStateFinalize :: (BF i) => i -> PrefixState i -> Maybe (Prefix i)
viewPrefixState :: (BF i) => i -> PrefixState i -> PrefixFieldView i
data ClosureView
InClosure :: ClosureView
NotInClosure :: ClosureView
MaybeInClosure :: ClosureView
data PrefixFieldView i
FieldOut :: (Field i) -> PrefixFieldView i
FieldIn :: PrefixFieldView i
FieldGuard :: (FieldSet i) -> PrefixFieldView i
instance Show ClosureView
instance Eq ClosureView
instance Ord ClosureView


-- | Just re-exports.
module CSPM.CoreLanguage