{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Modal/AS_Modal.der.hs
Copyright   :  (c) T.Mossakowski, W.Herding, C.Maeder, Uni Bremen 2004-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Abstract syntax for modal logic extension of CASL
  Only the added syntax is specified
-}

module Modal.AS_Modal where

import Common.Id
import Common.AS_Annotation

import CASL.AS_Basic_CASL

import Data.Data
-- DrIFT command
{-! global: GetRange !-}

type M_BASIC_SPEC = BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA

type AnModFORM = Annoted (FORMULA M_FORMULA)

data M_BASIC_ITEM = Simple_mod_decl [Annoted SIMPLE_ID] [AnModFORM] Range
                  | Term_mod_decl [Annoted SORT] [AnModFORM] Range
                    deriving (Int -> M_BASIC_ITEM -> ShowS
[M_BASIC_ITEM] -> ShowS
M_BASIC_ITEM -> String
(Int -> M_BASIC_ITEM -> ShowS)
-> (M_BASIC_ITEM -> String)
-> ([M_BASIC_ITEM] -> ShowS)
-> Show M_BASIC_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M_BASIC_ITEM] -> ShowS
$cshowList :: [M_BASIC_ITEM] -> ShowS
show :: M_BASIC_ITEM -> String
$cshow :: M_BASIC_ITEM -> String
showsPrec :: Int -> M_BASIC_ITEM -> ShowS
$cshowsPrec :: Int -> M_BASIC_ITEM -> ShowS
Show, Typeable, Typeable M_BASIC_ITEM
Constr
DataType
Typeable M_BASIC_ITEM =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c M_BASIC_ITEM)
-> (M_BASIC_ITEM -> Constr)
-> (M_BASIC_ITEM -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c M_BASIC_ITEM))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c M_BASIC_ITEM))
-> ((forall b. Data b => b -> b) -> M_BASIC_ITEM -> M_BASIC_ITEM)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r)
-> (forall u. (forall d. Data d => d -> u) -> M_BASIC_ITEM -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> M_BASIC_ITEM -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM)
-> Data M_BASIC_ITEM
M_BASIC_ITEM -> Constr
M_BASIC_ITEM -> DataType
(forall b. Data b => b -> b) -> M_BASIC_ITEM -> M_BASIC_ITEM
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_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) -> M_BASIC_ITEM -> u
forall u. (forall d. Data d => d -> u) -> M_BASIC_ITEM -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_BASIC_ITEM
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_BASIC_ITEM)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c M_BASIC_ITEM)
$cTerm_mod_decl :: Constr
$cSimple_mod_decl :: Constr
$tM_BASIC_ITEM :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
gmapMp :: (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
gmapM :: (forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_BASIC_ITEM -> m M_BASIC_ITEM
gmapQi :: Int -> (forall d. Data d => d -> u) -> M_BASIC_ITEM -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M_BASIC_ITEM -> u
gmapQ :: (forall d. Data d => d -> u) -> M_BASIC_ITEM -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M_BASIC_ITEM -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_BASIC_ITEM -> r
gmapT :: (forall b. Data b => b -> b) -> M_BASIC_ITEM -> M_BASIC_ITEM
$cgmapT :: (forall b. Data b => b -> b) -> M_BASIC_ITEM -> M_BASIC_ITEM
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c M_BASIC_ITEM)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c M_BASIC_ITEM)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c M_BASIC_ITEM)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_BASIC_ITEM)
dataTypeOf :: M_BASIC_ITEM -> DataType
$cdataTypeOf :: M_BASIC_ITEM -> DataType
toConstr :: M_BASIC_ITEM -> Constr
$ctoConstr :: M_BASIC_ITEM -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_BASIC_ITEM
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_BASIC_ITEM
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_BASIC_ITEM -> c M_BASIC_ITEM
$cp1Data :: Typeable M_BASIC_ITEM
Data)

data RIGOR = Rigid | Flexible deriving (Int -> RIGOR -> ShowS
[RIGOR] -> ShowS
RIGOR -> String
(Int -> RIGOR -> ShowS)
-> (RIGOR -> String) -> ([RIGOR] -> ShowS) -> Show RIGOR
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RIGOR] -> ShowS
$cshowList :: [RIGOR] -> ShowS
show :: RIGOR -> String
$cshow :: RIGOR -> String
showsPrec :: Int -> RIGOR -> ShowS
$cshowsPrec :: Int -> RIGOR -> ShowS
Show, Typeable, Typeable RIGOR
Constr
DataType
Typeable RIGOR =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RIGOR -> c RIGOR)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RIGOR)
-> (RIGOR -> Constr)
-> (RIGOR -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RIGOR))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RIGOR))
-> ((forall b. Data b => b -> b) -> RIGOR -> RIGOR)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r)
-> (forall u. (forall d. Data d => d -> u) -> RIGOR -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> RIGOR -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR)
-> Data RIGOR
RIGOR -> Constr
RIGOR -> DataType
(forall b. Data b => b -> b) -> RIGOR -> RIGOR
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RIGOR -> c RIGOR
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RIGOR
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) -> RIGOR -> u
forall u. (forall d. Data d => d -> u) -> RIGOR -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RIGOR
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RIGOR -> c RIGOR
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RIGOR)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RIGOR)
$cFlexible :: Constr
$cRigid :: Constr
$tRIGOR :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
gmapMp :: (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
gmapM :: (forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RIGOR -> m RIGOR
gmapQi :: Int -> (forall d. Data d => d -> u) -> RIGOR -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RIGOR -> u
gmapQ :: (forall d. Data d => d -> u) -> RIGOR -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RIGOR -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RIGOR -> r
gmapT :: (forall b. Data b => b -> b) -> RIGOR -> RIGOR
$cgmapT :: (forall b. Data b => b -> b) -> RIGOR -> RIGOR
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RIGOR)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RIGOR)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RIGOR)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RIGOR)
dataTypeOf :: RIGOR -> DataType
$cdataTypeOf :: RIGOR -> DataType
toConstr :: RIGOR -> Constr
$ctoConstr :: RIGOR -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RIGOR
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RIGOR
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RIGOR -> c RIGOR
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RIGOR -> c RIGOR
$cp1Data :: Typeable RIGOR
Data)

data M_SIG_ITEM =
          Rigid_op_items RIGOR [Annoted (OP_ITEM M_FORMULA)] Range
                 -- pos: op, semi colons
        | Rigid_pred_items RIGOR [Annoted (PRED_ITEM M_FORMULA)] Range
                 -- pos: pred, semi colons
             deriving (Int -> M_SIG_ITEM -> ShowS
[M_SIG_ITEM] -> ShowS
M_SIG_ITEM -> String
(Int -> M_SIG_ITEM -> ShowS)
-> (M_SIG_ITEM -> String)
-> ([M_SIG_ITEM] -> ShowS)
-> Show M_SIG_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M_SIG_ITEM] -> ShowS
$cshowList :: [M_SIG_ITEM] -> ShowS
show :: M_SIG_ITEM -> String
$cshow :: M_SIG_ITEM -> String
showsPrec :: Int -> M_SIG_ITEM -> ShowS
$cshowsPrec :: Int -> M_SIG_ITEM -> ShowS
Show, Typeable, Typeable M_SIG_ITEM
Constr
DataType
Typeable M_SIG_ITEM =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c M_SIG_ITEM)
-> (M_SIG_ITEM -> Constr)
-> (M_SIG_ITEM -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c M_SIG_ITEM))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c M_SIG_ITEM))
-> ((forall b. Data b => b -> b) -> M_SIG_ITEM -> M_SIG_ITEM)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r)
-> (forall u. (forall d. Data d => d -> u) -> M_SIG_ITEM -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> M_SIG_ITEM -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM)
-> Data M_SIG_ITEM
M_SIG_ITEM -> Constr
M_SIG_ITEM -> DataType
(forall b. Data b => b -> b) -> M_SIG_ITEM -> M_SIG_ITEM
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_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) -> M_SIG_ITEM -> u
forall u. (forall d. Data d => d -> u) -> M_SIG_ITEM -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_SIG_ITEM
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_SIG_ITEM)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_SIG_ITEM)
$cRigid_pred_items :: Constr
$cRigid_op_items :: Constr
$tM_SIG_ITEM :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
gmapMp :: (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
gmapM :: (forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_SIG_ITEM -> m M_SIG_ITEM
gmapQi :: Int -> (forall d. Data d => d -> u) -> M_SIG_ITEM -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M_SIG_ITEM -> u
gmapQ :: (forall d. Data d => d -> u) -> M_SIG_ITEM -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M_SIG_ITEM -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_SIG_ITEM -> r
gmapT :: (forall b. Data b => b -> b) -> M_SIG_ITEM -> M_SIG_ITEM
$cgmapT :: (forall b. Data b => b -> b) -> M_SIG_ITEM -> M_SIG_ITEM
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_SIG_ITEM)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_SIG_ITEM)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c M_SIG_ITEM)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_SIG_ITEM)
dataTypeOf :: M_SIG_ITEM -> DataType
$cdataTypeOf :: M_SIG_ITEM -> DataType
toConstr :: M_SIG_ITEM -> Constr
$ctoConstr :: M_SIG_ITEM -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_SIG_ITEM
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_SIG_ITEM
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_SIG_ITEM -> c M_SIG_ITEM
$cp1Data :: Typeable M_SIG_ITEM
Data)

data MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM M_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)
$cTerm_mod :: Constr
$cSimple_mod :: 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)

data M_FORMULA = BoxOrDiamond Bool MODALITY (FORMULA M_FORMULA) Range
               {- The identifier and the term specify the kind of the modality
               pos: "[]" or  "<>", True if Box, False if Diamond -}
             deriving (Int -> M_FORMULA -> ShowS
[M_FORMULA] -> ShowS
M_FORMULA -> String
(Int -> M_FORMULA -> ShowS)
-> (M_FORMULA -> String)
-> ([M_FORMULA] -> ShowS)
-> Show M_FORMULA
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M_FORMULA] -> ShowS
$cshowList :: [M_FORMULA] -> ShowS
show :: M_FORMULA -> String
$cshow :: M_FORMULA -> String
showsPrec :: Int -> M_FORMULA -> ShowS
$cshowsPrec :: Int -> M_FORMULA -> ShowS
Show, M_FORMULA -> M_FORMULA -> Bool
(M_FORMULA -> M_FORMULA -> Bool)
-> (M_FORMULA -> M_FORMULA -> Bool) -> Eq M_FORMULA
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: M_FORMULA -> M_FORMULA -> Bool
$c/= :: M_FORMULA -> M_FORMULA -> Bool
== :: M_FORMULA -> M_FORMULA -> Bool
$c== :: M_FORMULA -> M_FORMULA -> Bool
Eq, Eq M_FORMULA
Eq M_FORMULA =>
(M_FORMULA -> M_FORMULA -> Ordering)
-> (M_FORMULA -> M_FORMULA -> Bool)
-> (M_FORMULA -> M_FORMULA -> Bool)
-> (M_FORMULA -> M_FORMULA -> Bool)
-> (M_FORMULA -> M_FORMULA -> Bool)
-> (M_FORMULA -> M_FORMULA -> M_FORMULA)
-> (M_FORMULA -> M_FORMULA -> M_FORMULA)
-> Ord M_FORMULA
M_FORMULA -> M_FORMULA -> Bool
M_FORMULA -> M_FORMULA -> Ordering
M_FORMULA -> M_FORMULA -> M_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 :: M_FORMULA -> M_FORMULA -> M_FORMULA
$cmin :: M_FORMULA -> M_FORMULA -> M_FORMULA
max :: M_FORMULA -> M_FORMULA -> M_FORMULA
$cmax :: M_FORMULA -> M_FORMULA -> M_FORMULA
>= :: M_FORMULA -> M_FORMULA -> Bool
$c>= :: M_FORMULA -> M_FORMULA -> Bool
> :: M_FORMULA -> M_FORMULA -> Bool
$c> :: M_FORMULA -> M_FORMULA -> Bool
<= :: M_FORMULA -> M_FORMULA -> Bool
$c<= :: M_FORMULA -> M_FORMULA -> Bool
< :: M_FORMULA -> M_FORMULA -> Bool
$c< :: M_FORMULA -> M_FORMULA -> Bool
compare :: M_FORMULA -> M_FORMULA -> Ordering
$ccompare :: M_FORMULA -> M_FORMULA -> Ordering
$cp1Ord :: Eq M_FORMULA
Ord, Typeable, Typeable M_FORMULA
Constr
DataType
Typeable M_FORMULA =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c M_FORMULA)
-> (M_FORMULA -> Constr)
-> (M_FORMULA -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c M_FORMULA))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_FORMULA))
-> ((forall b. Data b => b -> b) -> M_FORMULA -> M_FORMULA)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r)
-> (forall u. (forall d. Data d => d -> u) -> M_FORMULA -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> M_FORMULA -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA)
-> Data M_FORMULA
M_FORMULA -> Constr
M_FORMULA -> DataType
(forall b. Data b => b -> b) -> M_FORMULA -> M_FORMULA
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_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) -> M_FORMULA -> u
forall u. (forall d. Data d => d -> u) -> M_FORMULA -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_FORMULA
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_FORMULA)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_FORMULA)
$cBoxOrDiamond :: Constr
$tM_FORMULA :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
gmapMp :: (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
gmapM :: (forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M_FORMULA -> m M_FORMULA
gmapQi :: Int -> (forall d. Data d => d -> u) -> M_FORMULA -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M_FORMULA -> u
gmapQ :: (forall d. Data d => d -> u) -> M_FORMULA -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M_FORMULA -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> M_FORMULA -> r
gmapT :: (forall b. Data b => b -> b) -> M_FORMULA -> M_FORMULA
$cgmapT :: (forall b. Data b => b -> b) -> M_FORMULA -> M_FORMULA
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_FORMULA)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M_FORMULA)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c M_FORMULA)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M_FORMULA)
dataTypeOf :: M_FORMULA -> DataType
$cdataTypeOf :: M_FORMULA -> DataType
toConstr :: M_FORMULA -> Constr
$ctoConstr :: M_FORMULA -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_FORMULA
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M_FORMULA
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M_FORMULA -> c M_FORMULA
$cp1Data :: Typeable M_FORMULA
Data)

-- Generated by DrIFT, look but don't touch!

instance GetRange M_BASIC_ITEM where
  getRange :: M_BASIC_ITEM -> Range
getRange x :: M_BASIC_ITEM
x = case M_BASIC_ITEM
x of
    Simple_mod_decl _ _ p :: Range
p -> Range
p
    Term_mod_decl _ _ p :: Range
p -> Range
p
  rangeSpan :: M_BASIC_ITEM -> [Pos]
rangeSpan x :: M_BASIC_ITEM
x = case M_BASIC_ITEM
x of
    Simple_mod_decl a :: [Annoted SIMPLE_ID]
a b :: [AnModFORM]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Annoted SIMPLE_ID] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SIMPLE_ID]
a, [AnModFORM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [AnModFORM]
b,
                                         Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Term_mod_decl a :: [Annoted SORT]
a b :: [AnModFORM]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Annoted SORT] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SORT]
a, [AnModFORM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [AnModFORM]
b,
                                       Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

instance GetRange RIGOR where
  getRange :: RIGOR -> Range
getRange = Range -> RIGOR -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: RIGOR -> [Pos]
rangeSpan x :: RIGOR
x = case RIGOR
x of
    Rigid -> []
    Flexible -> []

instance GetRange M_SIG_ITEM where
  getRange :: M_SIG_ITEM -> Range
getRange x :: M_SIG_ITEM
x = case M_SIG_ITEM
x of
    Rigid_op_items _ _ p :: Range
p -> Range
p
    Rigid_pred_items _ _ p :: Range
p -> Range
p
  rangeSpan :: M_SIG_ITEM -> [Pos]
rangeSpan x :: M_SIG_ITEM
x = case M_SIG_ITEM
x of
    Rigid_op_items a :: RIGOR
a b :: [Annoted (OP_ITEM M_FORMULA)]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [RIGOR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RIGOR
a, [Annoted (OP_ITEM M_FORMULA)] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted (OP_ITEM M_FORMULA)]
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Rigid_pred_items a :: RIGOR
a b :: [Annoted (PRED_ITEM M_FORMULA)]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [RIGOR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RIGOR
a, [Annoted (PRED_ITEM M_FORMULA)] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted (PRED_ITEM M_FORMULA)]
b,
                                          Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]

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
    Simple_mod a :: SIMPLE_ID
a -> [[Pos]] -> [Pos]
joinRanges [SIMPLE_ID -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SIMPLE_ID
a]
    Term_mod a :: TERM M_FORMULA
a -> [[Pos]] -> [Pos]
joinRanges [TERM M_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM M_FORMULA
a]

instance GetRange M_FORMULA where
  getRange :: M_FORMULA -> Range
getRange x :: M_FORMULA
x = case M_FORMULA
x of
    BoxOrDiamond _ _ _ p :: Range
p -> Range
p
  rangeSpan :: M_FORMULA -> [Pos]
rangeSpan x :: M_FORMULA
x = case M_FORMULA
x of
    BoxOrDiamond a :: Bool
a b :: MODALITY
b c :: FORMULA M_FORMULA
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [Bool -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Bool
a, MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
b,
                                        FORMULA M_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA M_FORMULA
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]