{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./ExtModal/AS_ExtModal.der.hs Copyright : DFKI GmbH 2009 License : GPLv2 or higher, see LICENSE.txt Maintainer : codruta.liliana@gmail.com Stability : experimental Portability : portable -} module ExtModal.AS_ExtModal where import Common.Id import Common.AS_Annotation import CASL.AS_Basic_CASL import Data.Data -- DrIFT command {-! global: GetRange !-} type EM_BASIC_SPEC = BASIC_SPEC EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA data FrameForm = FrameForm { FrameForm -> [VAR_DECL] frameVars :: [VAR_DECL] , FrameForm -> [Annoted (FORMULA EM_FORMULA)] frameForms :: [Annoted (FORMULA EM_FORMULA)] , FrameForm -> Range frameFormRange :: Range } deriving (Int -> FrameForm -> ShowS [FrameForm] -> ShowS FrameForm -> String (Int -> FrameForm -> ShowS) -> (FrameForm -> String) -> ([FrameForm] -> ShowS) -> Show FrameForm forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [FrameForm] -> ShowS $cshowList :: [FrameForm] -> ShowS show :: FrameForm -> String $cshow :: FrameForm -> String showsPrec :: Int -> FrameForm -> ShowS $cshowsPrec :: Int -> FrameForm -> ShowS Show, FrameForm -> FrameForm -> Bool (FrameForm -> FrameForm -> Bool) -> (FrameForm -> FrameForm -> Bool) -> Eq FrameForm forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: FrameForm -> FrameForm -> Bool $c/= :: FrameForm -> FrameForm -> Bool == :: FrameForm -> FrameForm -> Bool $c== :: FrameForm -> FrameForm -> Bool Eq, Eq FrameForm Eq FrameForm => (FrameForm -> FrameForm -> Ordering) -> (FrameForm -> FrameForm -> Bool) -> (FrameForm -> FrameForm -> Bool) -> (FrameForm -> FrameForm -> Bool) -> (FrameForm -> FrameForm -> Bool) -> (FrameForm -> FrameForm -> FrameForm) -> (FrameForm -> FrameForm -> FrameForm) -> Ord FrameForm FrameForm -> FrameForm -> Bool FrameForm -> FrameForm -> Ordering FrameForm -> FrameForm -> FrameForm forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: FrameForm -> FrameForm -> FrameForm $cmin :: FrameForm -> FrameForm -> FrameForm max :: FrameForm -> FrameForm -> FrameForm $cmax :: FrameForm -> FrameForm -> FrameForm >= :: FrameForm -> FrameForm -> Bool $c>= :: FrameForm -> FrameForm -> Bool > :: FrameForm -> FrameForm -> Bool $c> :: FrameForm -> FrameForm -> Bool <= :: FrameForm -> FrameForm -> Bool $c<= :: FrameForm -> FrameForm -> Bool < :: FrameForm -> FrameForm -> Bool $c< :: FrameForm -> FrameForm -> Bool compare :: FrameForm -> FrameForm -> Ordering $ccompare :: FrameForm -> FrameForm -> Ordering $cp1Ord :: Eq FrameForm Ord, Typeable, Typeable FrameForm Constr DataType Typeable FrameForm => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FrameForm -> c FrameForm) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FrameForm) -> (FrameForm -> Constr) -> (FrameForm -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FrameForm)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FrameForm)) -> ((forall b. Data b => b -> b) -> FrameForm -> FrameForm) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r) -> (forall u. (forall d. Data d => d -> u) -> FrameForm -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> FrameForm -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm) -> Data FrameForm FrameForm -> Constr FrameForm -> DataType (forall b. Data b => b -> b) -> FrameForm -> FrameForm (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FrameForm -> c FrameForm (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FrameForm forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> FrameForm -> u forall u. (forall d. Data d => d -> u) -> FrameForm -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FrameForm forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FrameForm -> c FrameForm forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FrameForm) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FrameForm) $cFrameForm :: Constr $tFrameForm :: DataType gmapMo :: (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm gmapMp :: (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm gmapM :: (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FrameForm -> m FrameForm gmapQi :: Int -> (forall d. Data d => d -> u) -> FrameForm -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FrameForm -> u gmapQ :: (forall d. Data d => d -> u) -> FrameForm -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> FrameForm -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FrameForm -> r gmapT :: (forall b. Data b => b -> b) -> FrameForm -> FrameForm $cgmapT :: (forall b. Data b => b -> b) -> FrameForm -> FrameForm dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FrameForm) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FrameForm) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FrameForm) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FrameForm) dataTypeOf :: FrameForm -> DataType $cdataTypeOf :: FrameForm -> DataType toConstr :: FrameForm -> Constr $ctoConstr :: FrameForm -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FrameForm $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FrameForm gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FrameForm -> c FrameForm $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FrameForm -> c FrameForm $cp1Data :: Typeable FrameForm Data) data ModDefn = ModDefn Bool Bool [Annoted Id] [Annoted FrameForm] Range -- Booleans: time (True) or not and term (True) or simple modality deriving (Int -> ModDefn -> ShowS [ModDefn] -> ShowS ModDefn -> String (Int -> ModDefn -> ShowS) -> (ModDefn -> String) -> ([ModDefn] -> ShowS) -> Show ModDefn forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [ModDefn] -> ShowS $cshowList :: [ModDefn] -> ShowS show :: ModDefn -> String $cshow :: ModDefn -> String showsPrec :: Int -> ModDefn -> ShowS $cshowsPrec :: Int -> ModDefn -> ShowS Show, ModDefn -> ModDefn -> Bool (ModDefn -> ModDefn -> Bool) -> (ModDefn -> ModDefn -> Bool) -> Eq ModDefn forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ModDefn -> ModDefn -> Bool $c/= :: ModDefn -> ModDefn -> Bool == :: ModDefn -> ModDefn -> Bool $c== :: ModDefn -> ModDefn -> Bool Eq, Eq ModDefn Eq ModDefn => (ModDefn -> ModDefn -> Ordering) -> (ModDefn -> ModDefn -> Bool) -> (ModDefn -> ModDefn -> Bool) -> (ModDefn -> ModDefn -> Bool) -> (ModDefn -> ModDefn -> Bool) -> (ModDefn -> ModDefn -> ModDefn) -> (ModDefn -> ModDefn -> ModDefn) -> Ord ModDefn ModDefn -> ModDefn -> Bool ModDefn -> ModDefn -> Ordering ModDefn -> ModDefn -> ModDefn forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: ModDefn -> ModDefn -> ModDefn $cmin :: ModDefn -> ModDefn -> ModDefn max :: ModDefn -> ModDefn -> ModDefn $cmax :: ModDefn -> ModDefn -> ModDefn >= :: ModDefn -> ModDefn -> Bool $c>= :: ModDefn -> ModDefn -> Bool > :: ModDefn -> ModDefn -> Bool $c> :: ModDefn -> ModDefn -> Bool <= :: ModDefn -> ModDefn -> Bool $c<= :: ModDefn -> ModDefn -> Bool < :: ModDefn -> ModDefn -> Bool $c< :: ModDefn -> ModDefn -> Bool compare :: ModDefn -> ModDefn -> Ordering $ccompare :: ModDefn -> ModDefn -> Ordering $cp1Ord :: Eq ModDefn Ord, Typeable, Typeable ModDefn Constr DataType Typeable ModDefn => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModDefn -> c ModDefn) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModDefn) -> (ModDefn -> Constr) -> (ModDefn -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModDefn)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModDefn)) -> ((forall b. Data b => b -> b) -> ModDefn -> ModDefn) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r) -> (forall u. (forall d. Data d => d -> u) -> ModDefn -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> ModDefn -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn) -> Data ModDefn ModDefn -> Constr ModDefn -> DataType (forall b. Data b => b -> b) -> ModDefn -> ModDefn (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModDefn -> c ModDefn (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModDefn forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> ModDefn -> u forall u. (forall d. Data d => d -> u) -> ModDefn -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModDefn forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModDefn -> c ModDefn forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModDefn) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModDefn) $cModDefn :: Constr $tModDefn :: DataType gmapMo :: (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn gmapMp :: (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn gmapM :: (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModDefn -> m ModDefn gmapQi :: Int -> (forall d. Data d => d -> u) -> ModDefn -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ModDefn -> u gmapQ :: (forall d. Data d => d -> u) -> ModDefn -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> ModDefn -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModDefn -> r gmapT :: (forall b. Data b => b -> b) -> ModDefn -> ModDefn $cgmapT :: (forall b. Data b => b -> b) -> ModDefn -> ModDefn dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModDefn) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModDefn) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ModDefn) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModDefn) dataTypeOf :: ModDefn -> DataType $cdataTypeOf :: ModDefn -> DataType toConstr :: ModDefn -> Constr $ctoConstr :: ModDefn -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModDefn $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModDefn gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModDefn -> c ModDefn $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModDefn -> c ModDefn $cp1Data :: Typeable ModDefn Data) data EM_BASIC_ITEM = ModItem ModDefn | Nominal_decl [Annoted SIMPLE_ID] Range deriving (Int -> EM_BASIC_ITEM -> ShowS [EM_BASIC_ITEM] -> ShowS EM_BASIC_ITEM -> String (Int -> EM_BASIC_ITEM -> ShowS) -> (EM_BASIC_ITEM -> String) -> ([EM_BASIC_ITEM] -> ShowS) -> Show EM_BASIC_ITEM forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [EM_BASIC_ITEM] -> ShowS $cshowList :: [EM_BASIC_ITEM] -> ShowS show :: EM_BASIC_ITEM -> String $cshow :: EM_BASIC_ITEM -> String showsPrec :: Int -> EM_BASIC_ITEM -> ShowS $cshowsPrec :: Int -> EM_BASIC_ITEM -> ShowS Show, Typeable, Typeable EM_BASIC_ITEM Constr DataType Typeable EM_BASIC_ITEM => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM) -> (EM_BASIC_ITEM -> Constr) -> (EM_BASIC_ITEM -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_BASIC_ITEM)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_BASIC_ITEM)) -> ((forall b. Data b => b -> b) -> EM_BASIC_ITEM -> EM_BASIC_ITEM) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r) -> (forall u. (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM) -> Data EM_BASIC_ITEM EM_BASIC_ITEM -> Constr EM_BASIC_ITEM -> DataType (forall b. Data b => b -> b) -> EM_BASIC_ITEM -> EM_BASIC_ITEM (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> u forall u. (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_BASIC_ITEM) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_BASIC_ITEM) $cNominal_decl :: Constr $cModItem :: Constr $tEM_BASIC_ITEM :: DataType gmapMo :: (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM gmapMp :: (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM gmapM :: (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_BASIC_ITEM -> m EM_BASIC_ITEM gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> u gmapQ :: (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EM_BASIC_ITEM -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_BASIC_ITEM -> r gmapT :: (forall b. Data b => b -> b) -> EM_BASIC_ITEM -> EM_BASIC_ITEM $cgmapT :: (forall b. Data b => b -> b) -> EM_BASIC_ITEM -> EM_BASIC_ITEM dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_BASIC_ITEM) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_BASIC_ITEM) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EM_BASIC_ITEM) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_BASIC_ITEM) dataTypeOf :: EM_BASIC_ITEM -> DataType $cdataTypeOf :: EM_BASIC_ITEM -> DataType toConstr :: EM_BASIC_ITEM -> Constr $ctoConstr :: EM_BASIC_ITEM -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_BASIC_ITEM gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_BASIC_ITEM -> c EM_BASIC_ITEM $cp1Data :: Typeable EM_BASIC_ITEM Data) data ModOp = Composition | Intersection | Union | OrElse deriving (ModOp -> ModOp -> Bool (ModOp -> ModOp -> Bool) -> (ModOp -> ModOp -> Bool) -> Eq ModOp forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ModOp -> ModOp -> Bool $c/= :: ModOp -> ModOp -> Bool == :: ModOp -> ModOp -> Bool $c== :: ModOp -> ModOp -> Bool Eq, Eq ModOp Eq ModOp => (ModOp -> ModOp -> Ordering) -> (ModOp -> ModOp -> Bool) -> (ModOp -> ModOp -> Bool) -> (ModOp -> ModOp -> Bool) -> (ModOp -> ModOp -> Bool) -> (ModOp -> ModOp -> ModOp) -> (ModOp -> ModOp -> ModOp) -> Ord ModOp ModOp -> ModOp -> Bool ModOp -> ModOp -> Ordering ModOp -> ModOp -> ModOp forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: ModOp -> ModOp -> ModOp $cmin :: ModOp -> ModOp -> ModOp max :: ModOp -> ModOp -> ModOp $cmax :: ModOp -> ModOp -> ModOp >= :: ModOp -> ModOp -> Bool $c>= :: ModOp -> ModOp -> Bool > :: ModOp -> ModOp -> Bool $c> :: ModOp -> ModOp -> Bool <= :: ModOp -> ModOp -> Bool $c<= :: ModOp -> ModOp -> Bool < :: ModOp -> ModOp -> Bool $c< :: ModOp -> ModOp -> Bool compare :: ModOp -> ModOp -> Ordering $ccompare :: ModOp -> ModOp -> Ordering $cp1Ord :: Eq ModOp Ord, Typeable, Typeable ModOp Constr DataType Typeable ModOp => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModOp -> c ModOp) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModOp) -> (ModOp -> Constr) -> (ModOp -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModOp)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModOp)) -> ((forall b. Data b => b -> b) -> ModOp -> ModOp) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r) -> (forall u. (forall d. Data d => d -> u) -> ModOp -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> ModOp -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp) -> Data ModOp ModOp -> Constr ModOp -> DataType (forall b. Data b => b -> b) -> ModOp -> ModOp (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModOp -> c ModOp (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModOp forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> ModOp -> u forall u. (forall d. Data d => d -> u) -> ModOp -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModOp forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModOp -> c ModOp forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModOp) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModOp) $cOrElse :: Constr $cUnion :: Constr $cIntersection :: Constr $cComposition :: Constr $tModOp :: DataType gmapMo :: (forall d. Data d => d -> m d) -> ModOp -> m ModOp $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp gmapMp :: (forall d. Data d => d -> m d) -> ModOp -> m ModOp $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp gmapM :: (forall d. Data d => d -> m d) -> ModOp -> m ModOp $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> ModOp -> m ModOp gmapQi :: Int -> (forall d. Data d => d -> u) -> ModOp -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ModOp -> u gmapQ :: (forall d. Data d => d -> u) -> ModOp -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> ModOp -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModOp -> r gmapT :: (forall b. Data b => b -> b) -> ModOp -> ModOp $cgmapT :: (forall b. Data b => b -> b) -> ModOp -> ModOp dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModOp) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModOp) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ModOp) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModOp) dataTypeOf :: ModOp -> DataType $cdataTypeOf :: ModOp -> DataType toConstr :: ModOp -> Constr $ctoConstr :: ModOp -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModOp $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModOp gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModOp -> c ModOp $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModOp -> c ModOp $cp1Data :: Typeable ModOp Data) {- Union corresponds to alternative and intersection to parallel composition. The symbols used (like for logical "and" and "or") may be confusing! Guarded alternatives joined with "orElse" may be used to simulate consecutive cases. -} instance Show ModOp where show :: ModOp -> String show o :: ModOp o = case ModOp o of Composition -> ";" Intersection -> "&" Union -> "|" OrElse -> "orElse" data MODALITY = SimpleMod SIMPLE_ID | TermMod (TERM EM_FORMULA) | ModOp ModOp MODALITY MODALITY | TransClos MODALITY | Guard (FORMULA EM_FORMULA) deriving (Int -> MODALITY -> ShowS [MODALITY] -> ShowS MODALITY -> String (Int -> MODALITY -> ShowS) -> (MODALITY -> String) -> ([MODALITY] -> ShowS) -> Show MODALITY forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [MODALITY] -> ShowS $cshowList :: [MODALITY] -> ShowS show :: MODALITY -> String $cshow :: MODALITY -> String showsPrec :: Int -> MODALITY -> ShowS $cshowsPrec :: Int -> MODALITY -> ShowS Show, MODALITY -> MODALITY -> Bool (MODALITY -> MODALITY -> Bool) -> (MODALITY -> MODALITY -> Bool) -> Eq MODALITY forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: MODALITY -> MODALITY -> Bool $c/= :: MODALITY -> MODALITY -> Bool == :: MODALITY -> MODALITY -> Bool $c== :: MODALITY -> MODALITY -> Bool Eq, Eq MODALITY Eq MODALITY => (MODALITY -> MODALITY -> Ordering) -> (MODALITY -> MODALITY -> Bool) -> (MODALITY -> MODALITY -> Bool) -> (MODALITY -> MODALITY -> Bool) -> (MODALITY -> MODALITY -> Bool) -> (MODALITY -> MODALITY -> MODALITY) -> (MODALITY -> MODALITY -> MODALITY) -> Ord MODALITY MODALITY -> MODALITY -> Bool MODALITY -> MODALITY -> Ordering MODALITY -> MODALITY -> MODALITY forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: MODALITY -> MODALITY -> MODALITY $cmin :: MODALITY -> MODALITY -> MODALITY max :: MODALITY -> MODALITY -> MODALITY $cmax :: MODALITY -> MODALITY -> MODALITY >= :: MODALITY -> MODALITY -> Bool $c>= :: MODALITY -> MODALITY -> Bool > :: MODALITY -> MODALITY -> Bool $c> :: MODALITY -> MODALITY -> Bool <= :: MODALITY -> MODALITY -> Bool $c<= :: MODALITY -> MODALITY -> Bool < :: MODALITY -> MODALITY -> Bool $c< :: MODALITY -> MODALITY -> Bool compare :: MODALITY -> MODALITY -> Ordering $ccompare :: MODALITY -> MODALITY -> Ordering $cp1Ord :: Eq MODALITY Ord, Typeable, Typeable MODALITY Constr DataType Typeable MODALITY => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY) -> (MODALITY -> Constr) -> (MODALITY -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MODALITY)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODALITY)) -> ((forall b. Data b => b -> b) -> MODALITY -> MODALITY) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r) -> (forall u. (forall d. Data d => d -> u) -> MODALITY -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> MODALITY -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY) -> Data MODALITY MODALITY -> Constr MODALITY -> DataType (forall b. Data b => b -> b) -> MODALITY -> MODALITY (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> MODALITY -> u forall u. (forall d. Data d => d -> u) -> MODALITY -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MODALITY) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODALITY) $cGuard :: Constr $cTransClos :: Constr $cModOp :: Constr $cTermMod :: Constr $cSimpleMod :: Constr $tMODALITY :: DataType gmapMo :: (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY gmapMp :: (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY gmapM :: (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> MODALITY -> m MODALITY gmapQi :: Int -> (forall d. Data d => d -> u) -> MODALITY -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> MODALITY -> u gmapQ :: (forall d. Data d => d -> u) -> MODALITY -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> MODALITY -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODALITY -> r gmapT :: (forall b. Data b => b -> b) -> MODALITY -> MODALITY $cgmapT :: (forall b. Data b => b -> b) -> MODALITY -> MODALITY dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODALITY) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODALITY) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c MODALITY) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MODALITY) dataTypeOf :: MODALITY -> DataType $cdataTypeOf :: MODALITY -> DataType toConstr :: MODALITY -> Constr $ctoConstr :: MODALITY -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODALITY gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODALITY -> c MODALITY $cp1Data :: Typeable MODALITY Data) -- True booleans for rigid items, False for flexible ones data EM_SIG_ITEM = Rigid_op_items Bool [Annoted (OP_ITEM EM_FORMULA)] Range -- pos: op, semi colons | Rigid_pred_items Bool [Annoted (PRED_ITEM EM_FORMULA)] Range -- pos: pred, semi colons deriving (Int -> EM_SIG_ITEM -> ShowS [EM_SIG_ITEM] -> ShowS EM_SIG_ITEM -> String (Int -> EM_SIG_ITEM -> ShowS) -> (EM_SIG_ITEM -> String) -> ([EM_SIG_ITEM] -> ShowS) -> Show EM_SIG_ITEM forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [EM_SIG_ITEM] -> ShowS $cshowList :: [EM_SIG_ITEM] -> ShowS show :: EM_SIG_ITEM -> String $cshow :: EM_SIG_ITEM -> String showsPrec :: Int -> EM_SIG_ITEM -> ShowS $cshowsPrec :: Int -> EM_SIG_ITEM -> ShowS Show, Typeable, Typeable EM_SIG_ITEM Constr DataType Typeable EM_SIG_ITEM => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM) -> (EM_SIG_ITEM -> Constr) -> (EM_SIG_ITEM -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_SIG_ITEM)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_SIG_ITEM)) -> ((forall b. Data b => b -> b) -> EM_SIG_ITEM -> EM_SIG_ITEM) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r) -> (forall u. (forall d. Data d => d -> u) -> EM_SIG_ITEM -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> EM_SIG_ITEM -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM) -> Data EM_SIG_ITEM EM_SIG_ITEM -> Constr EM_SIG_ITEM -> DataType (forall b. Data b => b -> b) -> EM_SIG_ITEM -> EM_SIG_ITEM (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> EM_SIG_ITEM -> u forall u. (forall d. Data d => d -> u) -> EM_SIG_ITEM -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_SIG_ITEM) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_SIG_ITEM) $cRigid_pred_items :: Constr $cRigid_op_items :: Constr $tEM_SIG_ITEM :: DataType gmapMo :: (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM gmapMp :: (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM gmapM :: (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_SIG_ITEM -> m EM_SIG_ITEM gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_SIG_ITEM -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EM_SIG_ITEM -> u gmapQ :: (forall d. Data d => d -> u) -> EM_SIG_ITEM -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EM_SIG_ITEM -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_SIG_ITEM -> r gmapT :: (forall b. Data b => b -> b) -> EM_SIG_ITEM -> EM_SIG_ITEM $cgmapT :: (forall b. Data b => b -> b) -> EM_SIG_ITEM -> EM_SIG_ITEM dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_SIG_ITEM) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_SIG_ITEM) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EM_SIG_ITEM) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_SIG_ITEM) dataTypeOf :: EM_SIG_ITEM -> DataType $cdataTypeOf :: EM_SIG_ITEM -> DataType toConstr :: EM_SIG_ITEM -> Constr $ctoConstr :: EM_SIG_ITEM -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_SIG_ITEM gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_SIG_ITEM -> c EM_SIG_ITEM $cp1Data :: Typeable EM_SIG_ITEM Data) {- Note, that a diamond formula "<m> f" stand for "<m>1 f" or "<m> >=1 f" Generally "<m>n f" or "<m> >=n f" (n positive) means, that there are at least n successor worlds (wrt m) in which f holds. (This is called grading.) "<m> <=n f" is rarely used (there are at most n successor worlds that fulfill f) By definition "[m]n f" is "not <m>n not f" and thus means: f holds in all successor worlds except in at most n-1 successor worlds. A notation like "[m]<n f" or "[m]<=0 f" would be illegal (only <= or >= with positive n is allowed), thus here "[m]n f" stands for "[m]>=n f" and "[m]<=n f" for "not <m> <=n not f" Another interpretation of "[m]n f" is that any subset with n successor worlds contains at least one successor world fulfilling f. "<m> <=n f" seems to be identical "[m]>=n+1 not f" (at most n successor worlds fulfill f) By duality: [m]<=n f <=> not <m> <=n not f <=> not [m]>=n+1 f <=> <m> >=n+1 not f and: "<m> <=n f" <=> [m]>=n+1 not f <=> not <m> >=n+1 f thus: <m> >=n f <=> not <m> <=n-1 f <=> [m]<=n-1 not f and: [m]>=n f <=> not [m] <=n-1 f There are exactly n successor worlds can be expressed as: <m> >=n f /\ <m> <=n f or: <m> >=n f /\ not <m> >=n+1 f or: [m]>=n+1 not f /\ [m]<=n-1 not f Also box formulas using n (> 1) are rarely used! -} data BoxOp = Box | Diamond | EBox deriving (Int -> BoxOp -> ShowS [BoxOp] -> ShowS BoxOp -> String (Int -> BoxOp -> ShowS) -> (BoxOp -> String) -> ([BoxOp] -> ShowS) -> Show BoxOp forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [BoxOp] -> ShowS $cshowList :: [BoxOp] -> ShowS show :: BoxOp -> String $cshow :: BoxOp -> String showsPrec :: Int -> BoxOp -> ShowS $cshowsPrec :: Int -> BoxOp -> ShowS Show, BoxOp -> BoxOp -> Bool (BoxOp -> BoxOp -> Bool) -> (BoxOp -> BoxOp -> Bool) -> Eq BoxOp forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: BoxOp -> BoxOp -> Bool $c/= :: BoxOp -> BoxOp -> Bool == :: BoxOp -> BoxOp -> Bool $c== :: BoxOp -> BoxOp -> Bool Eq, Eq BoxOp Eq BoxOp => (BoxOp -> BoxOp -> Ordering) -> (BoxOp -> BoxOp -> Bool) -> (BoxOp -> BoxOp -> Bool) -> (BoxOp -> BoxOp -> Bool) -> (BoxOp -> BoxOp -> Bool) -> (BoxOp -> BoxOp -> BoxOp) -> (BoxOp -> BoxOp -> BoxOp) -> Ord BoxOp BoxOp -> BoxOp -> Bool BoxOp -> BoxOp -> Ordering BoxOp -> BoxOp -> BoxOp forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: BoxOp -> BoxOp -> BoxOp $cmin :: BoxOp -> BoxOp -> BoxOp max :: BoxOp -> BoxOp -> BoxOp $cmax :: BoxOp -> BoxOp -> BoxOp >= :: BoxOp -> BoxOp -> Bool $c>= :: BoxOp -> BoxOp -> Bool > :: BoxOp -> BoxOp -> Bool $c> :: BoxOp -> BoxOp -> Bool <= :: BoxOp -> BoxOp -> Bool $c<= :: BoxOp -> BoxOp -> Bool < :: BoxOp -> BoxOp -> Bool $c< :: BoxOp -> BoxOp -> Bool compare :: BoxOp -> BoxOp -> Ordering $ccompare :: BoxOp -> BoxOp -> Ordering $cp1Ord :: Eq BoxOp Ord, Typeable, Typeable BoxOp Constr DataType Typeable BoxOp => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOp -> c BoxOp) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOp) -> (BoxOp -> Constr) -> (BoxOp -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoxOp)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOp)) -> ((forall b. Data b => b -> b) -> BoxOp -> BoxOp) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r) -> (forall u. (forall d. Data d => d -> u) -> BoxOp -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> BoxOp -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp) -> Data BoxOp BoxOp -> Constr BoxOp -> DataType (forall b. Data b => b -> b) -> BoxOp -> BoxOp (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOp -> c BoxOp (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOp forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> BoxOp -> u forall u. (forall d. Data d => d -> u) -> BoxOp -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOp forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOp -> c BoxOp forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoxOp) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOp) $cEBox :: Constr $cDiamond :: Constr $cBox :: Constr $tBoxOp :: DataType gmapMo :: (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp gmapMp :: (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp gmapM :: (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> BoxOp -> m BoxOp gmapQi :: Int -> (forall d. Data d => d -> u) -> BoxOp -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BoxOp -> u gmapQ :: (forall d. Data d => d -> u) -> BoxOp -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> BoxOp -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOp -> r gmapT :: (forall b. Data b => b -> b) -> BoxOp -> BoxOp $cgmapT :: (forall b. Data b => b -> b) -> BoxOp -> BoxOp dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOp) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOp) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c BoxOp) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BoxOp) dataTypeOf :: BoxOp -> DataType $cdataTypeOf :: BoxOp -> DataType toConstr :: BoxOp -> Constr $ctoConstr :: BoxOp -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOp $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOp gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOp -> c BoxOp $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOp -> c BoxOp $cp1Data :: Typeable BoxOp Data) {- the EBox is a short cut for a box and a diamond asserting that a next world exists and that the formula holds in all of them. -} data FormPrefix = BoxOrDiamond BoxOp MODALITY Bool Int {- The first identifier and the term specify the kind of the modality pos: "[]", "<>" or "<[]>" The second identifier is used for grading: pos: "<=" or ">=", False if Leq (less than/equal), True if Geq (greater than/equal), positive integers -} | Hybrid Bool SIMPLE_ID {- True if @, False if Here pos: "@", "Here" -} | PathQuantification Bool -- pos: "A", "E", True if Universal (A), False if Existential (E) | NextY Bool -- pos: "X", "Y", True if Next (X), False if Yesterday (Y) | StateQuantification Bool Bool {- The time direction (past vs future) and quantification type must be given, as follows: (True, True) if (Future, Universal), i.e. Generally (G); (True, False) if (Future, Existential), i.e. Eventually (F); (False, True) if (Past, Universal), i.e. Hitherto (H); (False, False) if (Past, Existential), i.e. Previously (P); pos: "G", "H", "F", "P" -} | FixedPoint Bool VAR -- pos: "mu", "nu", True if "mu", False if "nu" deriving (Int -> FormPrefix -> ShowS [FormPrefix] -> ShowS FormPrefix -> String (Int -> FormPrefix -> ShowS) -> (FormPrefix -> String) -> ([FormPrefix] -> ShowS) -> Show FormPrefix forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [FormPrefix] -> ShowS $cshowList :: [FormPrefix] -> ShowS show :: FormPrefix -> String $cshow :: FormPrefix -> String showsPrec :: Int -> FormPrefix -> ShowS $cshowsPrec :: Int -> FormPrefix -> ShowS Show, FormPrefix -> FormPrefix -> Bool (FormPrefix -> FormPrefix -> Bool) -> (FormPrefix -> FormPrefix -> Bool) -> Eq FormPrefix forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: FormPrefix -> FormPrefix -> Bool $c/= :: FormPrefix -> FormPrefix -> Bool == :: FormPrefix -> FormPrefix -> Bool $c== :: FormPrefix -> FormPrefix -> Bool Eq, Eq FormPrefix Eq FormPrefix => (FormPrefix -> FormPrefix -> Ordering) -> (FormPrefix -> FormPrefix -> Bool) -> (FormPrefix -> FormPrefix -> Bool) -> (FormPrefix -> FormPrefix -> Bool) -> (FormPrefix -> FormPrefix -> Bool) -> (FormPrefix -> FormPrefix -> FormPrefix) -> (FormPrefix -> FormPrefix -> FormPrefix) -> Ord FormPrefix FormPrefix -> FormPrefix -> Bool FormPrefix -> FormPrefix -> Ordering FormPrefix -> FormPrefix -> FormPrefix forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: FormPrefix -> FormPrefix -> FormPrefix $cmin :: FormPrefix -> FormPrefix -> FormPrefix max :: FormPrefix -> FormPrefix -> FormPrefix $cmax :: FormPrefix -> FormPrefix -> FormPrefix >= :: FormPrefix -> FormPrefix -> Bool $c>= :: FormPrefix -> FormPrefix -> Bool > :: FormPrefix -> FormPrefix -> Bool $c> :: FormPrefix -> FormPrefix -> Bool <= :: FormPrefix -> FormPrefix -> Bool $c<= :: FormPrefix -> FormPrefix -> Bool < :: FormPrefix -> FormPrefix -> Bool $c< :: FormPrefix -> FormPrefix -> Bool compare :: FormPrefix -> FormPrefix -> Ordering $ccompare :: FormPrefix -> FormPrefix -> Ordering $cp1Ord :: Eq FormPrefix Ord, Typeable, Typeable FormPrefix Constr DataType Typeable FormPrefix => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormPrefix -> c FormPrefix) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormPrefix) -> (FormPrefix -> Constr) -> (FormPrefix -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormPrefix)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormPrefix)) -> ((forall b. Data b => b -> b) -> FormPrefix -> FormPrefix) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r) -> (forall u. (forall d. Data d => d -> u) -> FormPrefix -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> FormPrefix -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix) -> Data FormPrefix FormPrefix -> Constr FormPrefix -> DataType (forall b. Data b => b -> b) -> FormPrefix -> FormPrefix (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormPrefix -> c FormPrefix (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormPrefix forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> FormPrefix -> u forall u. (forall d. Data d => d -> u) -> FormPrefix -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormPrefix forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormPrefix -> c FormPrefix forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormPrefix) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormPrefix) $cFixedPoint :: Constr $cStateQuantification :: Constr $cNextY :: Constr $cPathQuantification :: Constr $cHybrid :: Constr $cBoxOrDiamond :: Constr $tFormPrefix :: DataType gmapMo :: (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix gmapMp :: (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix gmapM :: (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> FormPrefix -> m FormPrefix gmapQi :: Int -> (forall d. Data d => d -> u) -> FormPrefix -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FormPrefix -> u gmapQ :: (forall d. Data d => d -> u) -> FormPrefix -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> FormPrefix -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormPrefix -> r gmapT :: (forall b. Data b => b -> b) -> FormPrefix -> FormPrefix $cgmapT :: (forall b. Data b => b -> b) -> FormPrefix -> FormPrefix dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormPrefix) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormPrefix) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FormPrefix) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormPrefix) dataTypeOf :: FormPrefix -> DataType $cdataTypeOf :: FormPrefix -> DataType toConstr :: FormPrefix -> Constr $ctoConstr :: FormPrefix -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormPrefix $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormPrefix gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormPrefix -> c FormPrefix $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormPrefix -> c FormPrefix $cp1Data :: Typeable FormPrefix Data) data EM_FORMULA = PrefixForm FormPrefix (FORMULA EM_FORMULA) Range | UntilSince Bool (FORMULA EM_FORMULA) (FORMULA EM_FORMULA) Range -- pos: "Until", "Since", True if Until, False if Since | ModForm ModDefn deriving (Int -> EM_FORMULA -> ShowS [EM_FORMULA] -> ShowS EM_FORMULA -> String (Int -> EM_FORMULA -> ShowS) -> (EM_FORMULA -> String) -> ([EM_FORMULA] -> ShowS) -> Show EM_FORMULA forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [EM_FORMULA] -> ShowS $cshowList :: [EM_FORMULA] -> ShowS show :: EM_FORMULA -> String $cshow :: EM_FORMULA -> String showsPrec :: Int -> EM_FORMULA -> ShowS $cshowsPrec :: Int -> EM_FORMULA -> ShowS Show, EM_FORMULA -> EM_FORMULA -> Bool (EM_FORMULA -> EM_FORMULA -> Bool) -> (EM_FORMULA -> EM_FORMULA -> Bool) -> Eq EM_FORMULA forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: EM_FORMULA -> EM_FORMULA -> Bool $c/= :: EM_FORMULA -> EM_FORMULA -> Bool == :: EM_FORMULA -> EM_FORMULA -> Bool $c== :: EM_FORMULA -> EM_FORMULA -> Bool Eq, Eq EM_FORMULA Eq EM_FORMULA => (EM_FORMULA -> EM_FORMULA -> Ordering) -> (EM_FORMULA -> EM_FORMULA -> Bool) -> (EM_FORMULA -> EM_FORMULA -> Bool) -> (EM_FORMULA -> EM_FORMULA -> Bool) -> (EM_FORMULA -> EM_FORMULA -> Bool) -> (EM_FORMULA -> EM_FORMULA -> EM_FORMULA) -> (EM_FORMULA -> EM_FORMULA -> EM_FORMULA) -> Ord EM_FORMULA EM_FORMULA -> EM_FORMULA -> Bool EM_FORMULA -> EM_FORMULA -> Ordering EM_FORMULA -> EM_FORMULA -> EM_FORMULA forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA $cmin :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA max :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA $cmax :: EM_FORMULA -> EM_FORMULA -> EM_FORMULA >= :: EM_FORMULA -> EM_FORMULA -> Bool $c>= :: EM_FORMULA -> EM_FORMULA -> Bool > :: EM_FORMULA -> EM_FORMULA -> Bool $c> :: EM_FORMULA -> EM_FORMULA -> Bool <= :: EM_FORMULA -> EM_FORMULA -> Bool $c<= :: EM_FORMULA -> EM_FORMULA -> Bool < :: EM_FORMULA -> EM_FORMULA -> Bool $c< :: EM_FORMULA -> EM_FORMULA -> Bool compare :: EM_FORMULA -> EM_FORMULA -> Ordering $ccompare :: EM_FORMULA -> EM_FORMULA -> Ordering $cp1Ord :: Eq EM_FORMULA Ord, Typeable, Typeable EM_FORMULA Constr DataType Typeable EM_FORMULA => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA) -> (EM_FORMULA -> Constr) -> (EM_FORMULA -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_FORMULA)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_FORMULA)) -> ((forall b. Data b => b -> b) -> EM_FORMULA -> EM_FORMULA) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r) -> (forall u. (forall d. Data d => d -> u) -> EM_FORMULA -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> EM_FORMULA -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA) -> Data EM_FORMULA EM_FORMULA -> Constr EM_FORMULA -> DataType (forall b. Data b => b -> b) -> EM_FORMULA -> EM_FORMULA (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> EM_FORMULA -> u forall u. (forall d. Data d => d -> u) -> EM_FORMULA -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_FORMULA) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_FORMULA) $cModForm :: Constr $cUntilSince :: Constr $cPrefixForm :: Constr $tEM_FORMULA :: DataType gmapMo :: (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA gmapMp :: (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA gmapM :: (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> EM_FORMULA -> m EM_FORMULA gmapQi :: Int -> (forall d. Data d => d -> u) -> EM_FORMULA -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EM_FORMULA -> u gmapQ :: (forall d. Data d => d -> u) -> EM_FORMULA -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EM_FORMULA -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EM_FORMULA -> r gmapT :: (forall b. Data b => b -> b) -> EM_FORMULA -> EM_FORMULA $cgmapT :: (forall b. Data b => b -> b) -> EM_FORMULA -> EM_FORMULA dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_FORMULA) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EM_FORMULA) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EM_FORMULA) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EM_FORMULA) dataTypeOf :: EM_FORMULA -> DataType $cdataTypeOf :: EM_FORMULA -> DataType toConstr :: EM_FORMULA -> Constr $ctoConstr :: EM_FORMULA -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EM_FORMULA gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EM_FORMULA -> c EM_FORMULA $cp1Data :: Typeable EM_FORMULA Data) -- Generated by DrIFT, look but don't touch! instance GetRange FrameForm where getRange :: FrameForm -> Range getRange x :: FrameForm x = case FrameForm x of FrameForm _ _ p :: Range p -> Range p rangeSpan :: FrameForm -> [Pos] rangeSpan x :: FrameForm x = case FrameForm x of FrameForm a :: [VAR_DECL] a b :: [Annoted (FORMULA EM_FORMULA)] b c :: Range c -> [[Pos]] -> [Pos] joinRanges [[VAR_DECL] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [VAR_DECL] a, [Annoted (FORMULA EM_FORMULA)] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted (FORMULA EM_FORMULA)] b, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range c] instance GetRange ModDefn where getRange :: ModDefn -> Range getRange x :: ModDefn x = case ModDefn x of ModDefn _ _ _ _ p :: Range p -> Range p rangeSpan :: ModDefn -> [Pos] rangeSpan x :: ModDefn x = case ModDefn x of ModDefn a :: Bool a b :: Bool b c :: [Annoted Id] c d :: [Annoted FrameForm] d e :: Range e -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool b, [Annoted Id] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted Id] c, [Annoted FrameForm] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted FrameForm] d, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range e] instance GetRange EM_BASIC_ITEM where getRange :: EM_BASIC_ITEM -> Range getRange x :: EM_BASIC_ITEM x = case EM_BASIC_ITEM x of ModItem _ -> Range nullRange Nominal_decl _ p :: Range p -> Range p rangeSpan :: EM_BASIC_ITEM -> [Pos] rangeSpan x :: EM_BASIC_ITEM x = case EM_BASIC_ITEM x of ModItem a :: ModDefn a -> [[Pos]] -> [Pos] joinRanges [ModDefn -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan ModDefn a] Nominal_decl a :: [Annoted SIMPLE_ID] a b :: Range b -> [[Pos]] -> [Pos] joinRanges [[Annoted SIMPLE_ID] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted SIMPLE_ID] a, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range b] instance GetRange ModOp where getRange :: ModOp -> Range getRange = Range -> ModOp -> Range forall a b. a -> b -> a const Range nullRange rangeSpan :: ModOp -> [Pos] rangeSpan x :: ModOp x = case ModOp x of Composition -> [] Intersection -> [] Union -> [] OrElse -> [] instance GetRange MODALITY where getRange :: MODALITY -> Range getRange = Range -> MODALITY -> Range forall a b. a -> b -> a const Range nullRange rangeSpan :: MODALITY -> [Pos] rangeSpan x :: MODALITY x = case MODALITY x of SimpleMod a :: SIMPLE_ID a -> [[Pos]] -> [Pos] joinRanges [SIMPLE_ID -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan SIMPLE_ID a] TermMod a :: TERM EM_FORMULA a -> [[Pos]] -> [Pos] joinRanges [TERM EM_FORMULA -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan TERM EM_FORMULA a] ModOp a :: ModOp a b :: MODALITY b c :: MODALITY c -> [[Pos]] -> [Pos] joinRanges [ModOp -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan ModOp a, MODALITY -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan MODALITY b, MODALITY -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan MODALITY c] TransClos a :: MODALITY a -> [[Pos]] -> [Pos] joinRanges [MODALITY -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan MODALITY a] Guard a :: FORMULA EM_FORMULA a -> [[Pos]] -> [Pos] joinRanges [FORMULA EM_FORMULA -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan FORMULA EM_FORMULA a] instance GetRange EM_SIG_ITEM where getRange :: EM_SIG_ITEM -> Range getRange x :: EM_SIG_ITEM x = case EM_SIG_ITEM x of Rigid_op_items _ _ p :: Range p -> Range p Rigid_pred_items _ _ p :: Range p -> Range p rangeSpan :: EM_SIG_ITEM -> [Pos] rangeSpan x :: EM_SIG_ITEM x = case EM_SIG_ITEM x of Rigid_op_items a :: Bool a b :: [Annoted (OP_ITEM EM_FORMULA)] b c :: Range c -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, [Annoted (OP_ITEM EM_FORMULA)] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted (OP_ITEM EM_FORMULA)] b, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range c] Rigid_pred_items a :: Bool a b :: [Annoted (PRED_ITEM EM_FORMULA)] b c :: Range c -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, [Annoted (PRED_ITEM EM_FORMULA)] -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan [Annoted (PRED_ITEM EM_FORMULA)] b, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range c] instance GetRange BoxOp where getRange :: BoxOp -> Range getRange = Range -> BoxOp -> Range forall a b. a -> b -> a const Range nullRange rangeSpan :: BoxOp -> [Pos] rangeSpan x :: BoxOp x = case BoxOp x of Box -> [] Diamond -> [] EBox -> [] instance GetRange FormPrefix where getRange :: FormPrefix -> Range getRange = Range -> FormPrefix -> Range forall a b. a -> b -> a const Range nullRange rangeSpan :: FormPrefix -> [Pos] rangeSpan x :: FormPrefix x = case FormPrefix x of BoxOrDiamond a :: BoxOp a b :: MODALITY b c :: Bool c d :: Int d -> [[Pos]] -> [Pos] joinRanges [BoxOp -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan BoxOp a, MODALITY -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan MODALITY b, Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool c, Int -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Int d] Hybrid a :: Bool a b :: SIMPLE_ID b -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, SIMPLE_ID -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan SIMPLE_ID b] PathQuantification a :: Bool a -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a] NextY a :: Bool a -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a] StateQuantification a :: Bool a b :: Bool b -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool b] FixedPoint a :: Bool a b :: SIMPLE_ID b -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, SIMPLE_ID -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan SIMPLE_ID b] instance GetRange EM_FORMULA where getRange :: EM_FORMULA -> Range getRange x :: EM_FORMULA x = case EM_FORMULA x of PrefixForm _ _ p :: Range p -> Range p UntilSince _ _ _ p :: Range p -> Range p ModForm _ -> Range nullRange rangeSpan :: EM_FORMULA -> [Pos] rangeSpan x :: EM_FORMULA x = case EM_FORMULA x of PrefixForm a :: FormPrefix a b :: FORMULA EM_FORMULA b c :: Range c -> [[Pos]] -> [Pos] joinRanges [FormPrefix -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan FormPrefix a, FORMULA EM_FORMULA -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan FORMULA EM_FORMULA b, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range c] UntilSince a :: Bool a b :: FORMULA EM_FORMULA b c :: FORMULA EM_FORMULA c d :: Range d -> [[Pos]] -> [Pos] joinRanges [Bool -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Bool a, FORMULA EM_FORMULA -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan FORMULA EM_FORMULA b, FORMULA EM_FORMULA -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan FORMULA EM_FORMULA c, Range -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan Range d] ModForm a :: ModDefn a -> [[Pos]] -> [Pos] joinRanges [ModDefn -> [Pos] forall a. GetRange a => a -> [Pos] rangeSpan ModDefn a]