{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Hybrid/AS_Hybrid.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 hybrid logic extension of CASL
Only the added syntax is specified
-}

module Hybrid.AS_Hybrid where

import Common.Id
import Common.AS_Annotation

import CASL.AS_Basic_CASL

import Data.Data

-- DrIFT command
{-! global: GetRange !-}

type H_BASIC_SPEC = BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA

type AnHybFORM = Annoted (FORMULA H_FORMULA)

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

data MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM H_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 NOMINAL = Simple_nom SIMPLE_ID
        deriving (Int -> NOMINAL -> ShowS
[NOMINAL] -> ShowS
NOMINAL -> String
(Int -> NOMINAL -> ShowS)
-> (NOMINAL -> String) -> ([NOMINAL] -> ShowS) -> Show NOMINAL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NOMINAL] -> ShowS
$cshowList :: [NOMINAL] -> ShowS
show :: NOMINAL -> String
$cshow :: NOMINAL -> String
showsPrec :: Int -> NOMINAL -> ShowS
$cshowsPrec :: Int -> NOMINAL -> ShowS
Show, NOMINAL -> NOMINAL -> Bool
(NOMINAL -> NOMINAL -> Bool)
-> (NOMINAL -> NOMINAL -> Bool) -> Eq NOMINAL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NOMINAL -> NOMINAL -> Bool
$c/= :: NOMINAL -> NOMINAL -> Bool
== :: NOMINAL -> NOMINAL -> Bool
$c== :: NOMINAL -> NOMINAL -> Bool
Eq, Eq NOMINAL
Eq NOMINAL =>
(NOMINAL -> NOMINAL -> Ordering)
-> (NOMINAL -> NOMINAL -> Bool)
-> (NOMINAL -> NOMINAL -> Bool)
-> (NOMINAL -> NOMINAL -> Bool)
-> (NOMINAL -> NOMINAL -> Bool)
-> (NOMINAL -> NOMINAL -> NOMINAL)
-> (NOMINAL -> NOMINAL -> NOMINAL)
-> Ord NOMINAL
NOMINAL -> NOMINAL -> Bool
NOMINAL -> NOMINAL -> Ordering
NOMINAL -> NOMINAL -> NOMINAL
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 :: NOMINAL -> NOMINAL -> NOMINAL
$cmin :: NOMINAL -> NOMINAL -> NOMINAL
max :: NOMINAL -> NOMINAL -> NOMINAL
$cmax :: NOMINAL -> NOMINAL -> NOMINAL
>= :: NOMINAL -> NOMINAL -> Bool
$c>= :: NOMINAL -> NOMINAL -> Bool
> :: NOMINAL -> NOMINAL -> Bool
$c> :: NOMINAL -> NOMINAL -> Bool
<= :: NOMINAL -> NOMINAL -> Bool
$c<= :: NOMINAL -> NOMINAL -> Bool
< :: NOMINAL -> NOMINAL -> Bool
$c< :: NOMINAL -> NOMINAL -> Bool
compare :: NOMINAL -> NOMINAL -> Ordering
$ccompare :: NOMINAL -> NOMINAL -> Ordering
$cp1Ord :: Eq NOMINAL
Ord, Typeable, Typeable NOMINAL
Constr
DataType
Typeable NOMINAL =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> NOMINAL -> c NOMINAL)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NOMINAL)
-> (NOMINAL -> Constr)
-> (NOMINAL -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NOMINAL))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NOMINAL))
-> ((forall b. Data b => b -> b) -> NOMINAL -> NOMINAL)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NOMINAL -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NOMINAL -> r)
-> (forall u. (forall d. Data d => d -> u) -> NOMINAL -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> NOMINAL -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL)
-> Data NOMINAL
NOMINAL -> Constr
NOMINAL -> DataType
(forall b. Data b => b -> b) -> NOMINAL -> NOMINAL
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NOMINAL -> c NOMINAL
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NOMINAL
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) -> NOMINAL -> u
forall u. (forall d. Data d => d -> u) -> NOMINAL -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NOMINAL
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NOMINAL -> c NOMINAL
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NOMINAL)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NOMINAL)
$cSimple_nom :: Constr
$tNOMINAL :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
gmapMp :: (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
gmapM :: (forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NOMINAL -> m NOMINAL
gmapQi :: Int -> (forall d. Data d => d -> u) -> NOMINAL -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NOMINAL -> u
gmapQ :: (forall d. Data d => d -> u) -> NOMINAL -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NOMINAL -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NOMINAL -> r
gmapT :: (forall b. Data b => b -> b) -> NOMINAL -> NOMINAL
$cgmapT :: (forall b. Data b => b -> b) -> NOMINAL -> NOMINAL
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NOMINAL)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NOMINAL)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NOMINAL)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NOMINAL)
dataTypeOf :: NOMINAL -> DataType
$cdataTypeOf :: NOMINAL -> DataType
toConstr :: NOMINAL -> Constr
$ctoConstr :: NOMINAL -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NOMINAL
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NOMINAL
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NOMINAL -> c NOMINAL
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NOMINAL -> c NOMINAL
$cp1Data :: Typeable NOMINAL
Data)

data H_FORMULA = At NOMINAL (FORMULA H_FORMULA) Range
                | BoxOrDiamond Bool MODALITY (FORMULA H_FORMULA) Range
                | Here NOMINAL Range
                | Univ NOMINAL (FORMULA H_FORMULA) Range
                | Exist NOMINAL (FORMULA H_FORMULA) Range
             deriving (Int -> H_FORMULA -> ShowS
[H_FORMULA] -> ShowS
H_FORMULA -> String
(Int -> H_FORMULA -> ShowS)
-> (H_FORMULA -> String)
-> ([H_FORMULA] -> ShowS)
-> Show H_FORMULA
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [H_FORMULA] -> ShowS
$cshowList :: [H_FORMULA] -> ShowS
show :: H_FORMULA -> String
$cshow :: H_FORMULA -> String
showsPrec :: Int -> H_FORMULA -> ShowS
$cshowsPrec :: Int -> H_FORMULA -> ShowS
Show, H_FORMULA -> H_FORMULA -> Bool
(H_FORMULA -> H_FORMULA -> Bool)
-> (H_FORMULA -> H_FORMULA -> Bool) -> Eq H_FORMULA
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: H_FORMULA -> H_FORMULA -> Bool
$c/= :: H_FORMULA -> H_FORMULA -> Bool
== :: H_FORMULA -> H_FORMULA -> Bool
$c== :: H_FORMULA -> H_FORMULA -> Bool
Eq, Eq H_FORMULA
Eq H_FORMULA =>
(H_FORMULA -> H_FORMULA -> Ordering)
-> (H_FORMULA -> H_FORMULA -> Bool)
-> (H_FORMULA -> H_FORMULA -> Bool)
-> (H_FORMULA -> H_FORMULA -> Bool)
-> (H_FORMULA -> H_FORMULA -> Bool)
-> (H_FORMULA -> H_FORMULA -> H_FORMULA)
-> (H_FORMULA -> H_FORMULA -> H_FORMULA)
-> Ord H_FORMULA
H_FORMULA -> H_FORMULA -> Bool
H_FORMULA -> H_FORMULA -> Ordering
H_FORMULA -> H_FORMULA -> H_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 :: H_FORMULA -> H_FORMULA -> H_FORMULA
$cmin :: H_FORMULA -> H_FORMULA -> H_FORMULA
max :: H_FORMULA -> H_FORMULA -> H_FORMULA
$cmax :: H_FORMULA -> H_FORMULA -> H_FORMULA
>= :: H_FORMULA -> H_FORMULA -> Bool
$c>= :: H_FORMULA -> H_FORMULA -> Bool
> :: H_FORMULA -> H_FORMULA -> Bool
$c> :: H_FORMULA -> H_FORMULA -> Bool
<= :: H_FORMULA -> H_FORMULA -> Bool
$c<= :: H_FORMULA -> H_FORMULA -> Bool
< :: H_FORMULA -> H_FORMULA -> Bool
$c< :: H_FORMULA -> H_FORMULA -> Bool
compare :: H_FORMULA -> H_FORMULA -> Ordering
$ccompare :: H_FORMULA -> H_FORMULA -> Ordering
$cp1Ord :: Eq H_FORMULA
Ord, Typeable, Typeable H_FORMULA
Constr
DataType
Typeable H_FORMULA =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c H_FORMULA)
-> (H_FORMULA -> Constr)
-> (H_FORMULA -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c H_FORMULA))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_FORMULA))
-> ((forall b. Data b => b -> b) -> H_FORMULA -> H_FORMULA)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r)
-> (forall u. (forall d. Data d => d -> u) -> H_FORMULA -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> H_FORMULA -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA)
-> Data H_FORMULA
H_FORMULA -> Constr
H_FORMULA -> DataType
(forall b. Data b => b -> b) -> H_FORMULA -> H_FORMULA
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c H_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) -> H_FORMULA -> u
forall u. (forall d. Data d => d -> u) -> H_FORMULA -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c H_FORMULA
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c H_FORMULA)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_FORMULA)
$cExist :: Constr
$cUniv :: Constr
$cHere :: Constr
$cBoxOrDiamond :: Constr
$cAt :: Constr
$tH_FORMULA :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
gmapMp :: (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
gmapM :: (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
gmapQi :: Int -> (forall d. Data d => d -> u) -> H_FORMULA -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> H_FORMULA -> u
gmapQ :: (forall d. Data d => d -> u) -> H_FORMULA -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> H_FORMULA -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r
gmapT :: (forall b. Data b => b -> b) -> H_FORMULA -> H_FORMULA
$cgmapT :: (forall b. Data b => b -> b) -> H_FORMULA -> H_FORMULA
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_FORMULA)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_FORMULA)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c H_FORMULA)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c H_FORMULA)
dataTypeOf :: H_FORMULA -> DataType
$cdataTypeOf :: H_FORMULA -> DataType
toConstr :: H_FORMULA -> Constr
$ctoConstr :: H_FORMULA -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c H_FORMULA
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c H_FORMULA
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA
$cp1Data :: Typeable H_FORMULA
Data)

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

instance GetRange H_BASIC_ITEM where
  getRange :: H_BASIC_ITEM -> Range
getRange x :: H_BASIC_ITEM
x = case H_BASIC_ITEM
x of
    Simple_mod_decl _ _ p :: Range
p -> Range
p
    Term_mod_decl _ _ p :: Range
p -> Range
p
    Simple_nom_decl _ _ p :: Range
p -> Range
p
  rangeSpan :: H_BASIC_ITEM -> [Pos]
rangeSpan x :: H_BASIC_ITEM
x = case H_BASIC_ITEM
x of
    Simple_mod_decl a :: [Annoted SIMPLE_ID]
a b :: [AnHybFORM]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Annoted SIMPLE_ID] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SIMPLE_ID]
a, [AnHybFORM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [AnHybFORM]
b,
                                         Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Term_mod_decl a :: [Annoted SORT]
a b :: [AnHybFORM]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Annoted SORT] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SORT]
a, [AnHybFORM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [AnHybFORM]
b,
                                       Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Simple_nom_decl a :: [Annoted SIMPLE_ID]
a b :: [AnHybFORM]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [[Annoted SIMPLE_ID] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted SIMPLE_ID]
a, [AnHybFORM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [AnHybFORM]
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 H_SIG_ITEM where
  getRange :: H_SIG_ITEM -> Range
getRange x :: H_SIG_ITEM
x = case H_SIG_ITEM
x of
    Rigid_op_items _ _ p :: Range
p -> Range
p
    Rigid_pred_items _ _ p :: Range
p -> Range
p
  rangeSpan :: H_SIG_ITEM -> [Pos]
rangeSpan x :: H_SIG_ITEM
x = case H_SIG_ITEM
x of
    Rigid_op_items a :: RIGOR
a b :: [Annoted (OP_ITEM H_FORMULA)]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [RIGOR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RIGOR
a, [Annoted (OP_ITEM H_FORMULA)] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted (OP_ITEM H_FORMULA)]
b,
                                        Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Rigid_pred_items a :: RIGOR
a b :: [Annoted (PRED_ITEM H_FORMULA)]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [RIGOR -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan RIGOR
a, [Annoted (PRED_ITEM H_FORMULA)] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted (PRED_ITEM H_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 H_FORMULA
a -> [[Pos]] -> [Pos]
joinRanges [TERM H_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TERM H_FORMULA
a]

instance GetRange NOMINAL where
  getRange :: NOMINAL -> Range
getRange = Range -> NOMINAL -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: NOMINAL -> [Pos]
rangeSpan x :: NOMINAL
x = case NOMINAL
x of
    Simple_nom a :: SIMPLE_ID
a -> [[Pos]] -> [Pos]
joinRanges [SIMPLE_ID -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SIMPLE_ID
a]

instance GetRange H_FORMULA where
  getRange :: H_FORMULA -> Range
getRange x :: H_FORMULA
x = case H_FORMULA
x of
    At _ _ p :: Range
p -> Range
p
    BoxOrDiamond _ _ _ p :: Range
p -> Range
p
    Here _ p :: Range
p -> Range
p
    Univ _ _ p :: Range
p -> Range
p
    Exist _ _ p :: Range
p -> Range
p
  rangeSpan :: H_FORMULA -> [Pos]
rangeSpan x :: H_FORMULA
x = case H_FORMULA
x of
    At a :: NOMINAL
a b :: FORMULA H_FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [NOMINAL -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan NOMINAL
a, FORMULA H_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA H_FORMULA
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    BoxOrDiamond a :: Bool
a b :: MODALITY
b c :: FORMULA H_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 H_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA H_FORMULA
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    Here a :: NOMINAL
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [NOMINAL -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan NOMINAL
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    Univ a :: NOMINAL
a b :: FORMULA H_FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [NOMINAL -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan NOMINAL
a, FORMULA H_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA H_FORMULA
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Exist a :: NOMINAL
a b :: FORMULA H_FORMULA
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [NOMINAL -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan NOMINAL
a, FORMULA H_FORMULA -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FORMULA H_FORMULA
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]