-----------------------------------------------------------------------------
-- |
-- Module      :  CSPM.FiringRules.Rules
-- Copyright   :  (c) Fontaine 2010 - 2011
-- License     :  BSD3
-- 
-- Maintainer  :  fontaine@cs.uni-duesseldorf.de
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- This modules defines data types for (CSP) proof trees.
-- A proof trees show that a particular transition is valid
-- with respect to the firing rules semantics.
--
-- (For more info on the firing rule semantics 
-- see: The Theory and Practice of Concurrency A.W. Roscoe 1999.)
-- 
-- We use three separate data types for tau rules, tick rules and regular rules.
--
-- There is a one-to-one correspondence between each constructor of the data types
-- 'RuleTau', 'RuleTick', 'RuleEvent' and one fireing rule.
--
-- A list of the implemented firing rules (as pdf) is available via the package maintainer or
-- the web page.
--
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleContexts, StandaloneDeriving, UndecidableInstances #-}
module CSPM.FiringRules.Rules where

import CSPM.CoreLanguage

-- | A sum-type for tau, tick and regular proof trees.
data Rule i
  = TauRule (RuleTau i)
  | TickRule (RuleTick i)
  | EventRule (RuleEvent i)

-- | Is this a proof tree for a tau-transition
isTauRule :: Rule i -> Bool
isTauRule (TauRule {}) = True
isTauRule _ = False

-- | Representation of tau proof trees.
data RuleTau i
  = Hidden (EventSet i) (RuleEvent i)
  | HideTau (EventSet i) (RuleTau i)
  | SeqTau (RuleTau i) (Process i)
  | SeqTick (RuleTick i) (Process i)
  | InternalChoiceL (Process i) (Process i)
  | InternalChoiceR (Process i) (Process i)
  | ChaosStop (EventSet i)
  | TimeoutOccurs (Process i) (Process i)
  | TimeoutTauR (RuleTau i) (Process i)
  | ExtChoiceTauL (RuleTau i) (Process i)
  | ExtChoiceTauR (Process i) (RuleTau i)
  | InterleaveTauL (RuleTau i) (Process i)
  | InterleaveTauR (Process i) (RuleTau i)
  | InterleaveTickL (RuleTick i) (Process i)
  | InterleaveTickR (Process i) (RuleTick i)
  | ShareTauL (EventSet i) (RuleTau i) (Process i)
  | ShareTauR (EventSet i) (Process i) (RuleTau i)
  | ShareTickL (EventSet i) (RuleTick i) (Process i)
  | ShareTickR (EventSet i) (Process i) (RuleTick i)
  | AParallelTauL (EventSet i) (EventSet i) (RuleTau i) (Process i)
  | AParallelTauR (EventSet i) (EventSet i) (Process i) (RuleTau i)
  | AParallelTickL (EventSet i) (EventSet i) (RuleTick i) (Process i)
  | AParallelTickR (EventSet i) (EventSet i) (Process i) (RuleTick i)
  | InterruptTauL (RuleTau i) (Process i)
  | InterruptTauR (Process i) (RuleTau i)
  | TauRepAParallel [Either (EventSet i,Process i) (EventSet i,RuleTau i)]
  | RenamingTau (RenamingRelation i) (RuleTau i)
  | LinkLinked (RenamingRelation i) (RuleEvent i) (RuleEvent i)
  | LinkTauL (RenamingRelation i) (RuleTau i) (Process i)
  | LinkTauR (RenamingRelation i) (Process i) (RuleTau i)
  | LinkTickL (RenamingRelation i) (RuleTick i) (Process i)
  | LinkTickR (RenamingRelation i)  (Process i) (RuleTick i)
  | TraceSwitchOn (Process i) -- pseudo-tau for debugging

-- | Representation of tick proof trees.
data RuleTick i
  = SkipTick
  | HiddenTick (EventSet i) (RuleTick i)
  | InterruptTick (RuleTick i) (Process i)
  | TimeoutTick (RuleTick i) (Process i)
  | ShareOmega (EventSet i)
  | AParallelOmega (EventSet i) (EventSet i)
  | RepAParallelOmega [EventSet i]
  | InterleaveOmega
  | ExtChoiceTickL (RuleTick i) (Process i)
  | ExtChoiceTickR (Process i) (RuleTick i)
  | RenamingTick (RenamingRelation i) (RuleTick i)
  | LinkParallelTick (RenamingRelation i)

-- | Representation of regular proof trees (i.e. non-tau and non-tick transitions)
data RuleEvent i
  = HPrefix (Event i) (Prefix i)
  | ExtChoiceL (RuleEvent i) (Process i)
  | ExtChoiceR (Process i) (RuleEvent i)
  | InterleaveL (RuleEvent i) (Process i)
  | InterleaveR (Process i) (RuleEvent i)
  | SeqNormal (RuleEvent i) (Process i)
  | NotHidden (EventSet i) (RuleEvent i)
  | NotShareL (EventSet i) (RuleEvent i) (Process i)
  | NotShareR (EventSet i) (Process i) (RuleEvent i)
  | Shared (EventSet i) (RuleEvent i) (RuleEvent i)
  | AParallelL (EventSet i) (EventSet i) (RuleEvent i) (Process i)
  | AParallelR (EventSet i) (EventSet i) (Process i) (RuleEvent i)
  | AParallelBoth (EventSet i) (EventSet i) (RuleEvent i) (RuleEvent i)
  | RepAParallelEvent [EventRepAPart i]
  | NoInterrupt (RuleEvent i) (Process i)
  | InterruptOccurs (Process i) (RuleEvent i)
  | TimeoutNo (RuleEvent i) (Process i)
  | Rename (RenamingRelation i) (Event i) (RuleEvent i)
-- todo make special cases for Rename injective and rename relational
  | RenameNotInDomain (RenamingRelation i) (RuleEvent i)
  | ChaosEvent (EventSet i) (Event i)
  | LinkEventL (RenamingRelation i) (RuleEvent i) (Process i)
  | LinkEventR (RenamingRelation i) (Process i) (RuleEvent i)
  | NoException (EventSet i) (RuleEvent i)  (Process i)
  | ExceptionOccurs (EventSet i) (Process i) (RuleEvent i)

type EventRepAPart i
  = Either (EventSet i, Process i) (EventSet i, RuleEvent i)

{-
Not sure about this.
Maybe this moves somewhere else or should be implemented differently.
This somehow complicated by the use of type-families 
-}
deriving instance
  (Show (Event i), Show (Prefix i), Show (Process i), Show (ExtProcess i)
  ,Show (EventSet i), Show (RenamingRelation i))
  => Show (RuleEvent i)
deriving instance
  (Eq (Event i), Eq (Prefix i), Eq (Process i), Eq (ExtProcess i), Eq (EventSet i)
  ,Eq (RenamingRelation i) )
  => Eq (RuleEvent i)
deriving instance
  (Ord (Event i), Ord (Prefix i), Ord (Process i), Ord (ExtProcess i), Ord (EventSet i)
  ,Ord (RenamingRelation i) )
  => Ord (RuleEvent i)


deriving instance
  (Show (Process i), Show (EventSet i), Show (Prefix i), Show (ExtProcess i)
  ,Show (RenamingRelation i))
  => Show (RuleTick i)
deriving instance
  (Eq (Process i), Eq (EventSet i), Eq (Prefix i), Eq (ExtProcess i)
  ,Eq (RenamingRelation i))
  => Eq (RuleTick i)
deriving instance
  (Ord (Process i), Ord (EventSet i), Ord (Prefix i), Ord (ExtProcess i)
  ,Ord (RenamingRelation i))
   => Ord (RuleTick i)


deriving instance
  (Show (RuleEvent i), Show (RuleTick i), Show (Process i)
  ,Show (EventSet i), Show (RenamingRelation i))
  => Show (RuleTau i)
deriving instance
  (Eq (RuleEvent i), Eq (RuleTick i), Eq (Process i)
  ,Eq (EventSet i), Eq (RenamingRelation i))
  => Eq (RuleTau i)
deriving instance
  (Ord (RuleEvent i), Ord (RuleTick i), Ord (Process i), Ord (EventSet i)
  ,Ord (ExtProcess i), Ord (Prefix i), Ord (Event i),Ord (RenamingRelation i) )
  => Ord (RuleTau i)

deriving instance
  (Show (RuleEvent i), Show (RuleTick i), Show (RuleTau i))
  => Show (Rule i)

deriving instance
  (Eq (RuleEvent i), Eq (RuleTick i), Eq (RuleTau i))
  => Eq (Rule i)