{-# 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]