{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MonoLocalBinds #-}
{- |
Module      :  ./TopHybrid/AS_TopHybrid.der.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  nevrenato@gmail.com
Stability   :  experimental
Portability :  portable

Description :
Abstract syntax for an hybridized logic. Declaration
of the basic specification. Underlying Spec; Declaration
of nominals and modalities, and axioms.
-}

module TopHybrid.AS_TopHybrid where

import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.ToXml

import Logic.Logic

import Unsafe.Coerce

import Data.Data
import Data.Monoid ()

import Text.XML.Light

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

{- Union of the the declaration of nominals/modalities and the
   spec correspondent to the underlying logic -}
data TH_BSPEC s = Bspec { TH_BSPEC s -> [TH_BASIC_ITEM]
bitems :: [TH_BASIC_ITEM], TH_BSPEC s -> s
und :: s }
  deriving (Int -> TH_BSPEC s -> ShowS
[TH_BSPEC s] -> ShowS
TH_BSPEC s -> String
(Int -> TH_BSPEC s -> ShowS)
-> (TH_BSPEC s -> String)
-> ([TH_BSPEC s] -> ShowS)
-> Show (TH_BSPEC s)
forall s. Show s => Int -> TH_BSPEC s -> ShowS
forall s. Show s => [TH_BSPEC s] -> ShowS
forall s. Show s => TH_BSPEC s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TH_BSPEC s] -> ShowS
$cshowList :: forall s. Show s => [TH_BSPEC s] -> ShowS
show :: TH_BSPEC s -> String
$cshow :: forall s. Show s => TH_BSPEC s -> String
showsPrec :: Int -> TH_BSPEC s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> TH_BSPEC s -> ShowS
Show, Typeable, Typeable (TH_BSPEC s)
Constr
DataType
Typeable (TH_BSPEC s) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s))
-> (TH_BSPEC s -> Constr)
-> (TH_BSPEC s -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (TH_BSPEC s)))
-> ((forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r)
-> (forall u. (forall d. Data d => d -> u) -> TH_BSPEC s -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s))
-> Data (TH_BSPEC s)
TH_BSPEC s -> Constr
TH_BSPEC s -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s))
(forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s)
forall s. Data s => Typeable (TH_BSPEC s)
forall s. Data s => TH_BSPEC s -> Constr
forall s. Data s => TH_BSPEC s -> DataType
forall s.
Data s =>
(forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s
forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u
forall s u.
Data s =>
(forall d. Data d => d -> u) -> TH_BSPEC s -> [u]
forall s r r'.
Data s =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
forall s r r'.
Data s =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s)
forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s)
forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s))
forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_BSPEC s))
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) -> TH_BSPEC s -> u
forall u. (forall d. Data d => d -> u) -> TH_BSPEC s -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_BSPEC s))
$cBspec :: Constr
$tTH_BSPEC :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
$cgmapMo :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
gmapMp :: (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
$cgmapMp :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
gmapM :: (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
$cgmapM :: forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u
$cgmapQi :: forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u
gmapQ :: (forall d. Data d => d -> u) -> TH_BSPEC s -> [u]
$cgmapQ :: forall s u.
Data s =>
(forall d. Data d => d -> u) -> TH_BSPEC s -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
$cgmapQr :: forall s r r'.
Data s =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
$cgmapQl :: forall s r r'.
Data s =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r
gmapT :: (forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s
$cgmapT :: forall s.
Data s =>
(forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_BSPEC s))
$cdataCast2 :: forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_BSPEC s))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s))
$cdataCast1 :: forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s))
dataTypeOf :: TH_BSPEC s -> DataType
$cdataTypeOf :: forall s. Data s => TH_BSPEC s -> DataType
toConstr :: TH_BSPEC s -> Constr
$ctoConstr :: forall s. Data s => TH_BSPEC s -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s)
$cgunfold :: forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s)
$cgfoldl :: forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s)
$cp1Data :: forall s. Data s => Typeable (TH_BSPEC s)
Data)

-- Declaration of nominals/modalities
data TH_BASIC_ITEM = Simple_mod_decl [MODALITY]
                   | Simple_nom_decl [NOMINAL]
                     deriving (Int -> TH_BASIC_ITEM -> ShowS
[TH_BASIC_ITEM] -> ShowS
TH_BASIC_ITEM -> String
(Int -> TH_BASIC_ITEM -> ShowS)
-> (TH_BASIC_ITEM -> String)
-> ([TH_BASIC_ITEM] -> ShowS)
-> Show TH_BASIC_ITEM
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TH_BASIC_ITEM] -> ShowS
$cshowList :: [TH_BASIC_ITEM] -> ShowS
show :: TH_BASIC_ITEM -> String
$cshow :: TH_BASIC_ITEM -> String
showsPrec :: Int -> TH_BASIC_ITEM -> ShowS
$cshowsPrec :: Int -> TH_BASIC_ITEM -> ShowS
Show, Typeable, Typeable TH_BASIC_ITEM
Constr
DataType
Typeable TH_BASIC_ITEM =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM)
-> (TH_BASIC_ITEM -> Constr)
-> (TH_BASIC_ITEM -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TH_BASIC_ITEM))
-> ((forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r)
-> (forall u. (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM)
-> Data TH_BASIC_ITEM
TH_BASIC_ITEM -> Constr
TH_BASIC_ITEM -> DataType
(forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TH_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) -> TH_BASIC_ITEM -> u
forall u. (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TH_BASIC_ITEM)
$cSimple_nom_decl :: Constr
$cSimple_mod_decl :: Constr
$tTH_BASIC_ITEM :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
gmapMp :: (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
gmapM :: (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> u
gmapQ :: (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r
gmapT :: (forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM
$cgmapT :: (forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TH_BASIC_ITEM)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TH_BASIC_ITEM)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM)
dataTypeOf :: TH_BASIC_ITEM -> DataType
$cdataTypeOf :: TH_BASIC_ITEM -> DataType
toConstr :: TH_BASIC_ITEM -> Constr
$ctoConstr :: TH_BASIC_ITEM -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM
$cp1Data :: Typeable TH_BASIC_ITEM
Data)

type MODALITY = SIMPLE_ID
type NOMINAL = SIMPLE_ID

{- The strucuture of an hybridized sentence, where f correponds to the
underlying logic -}
data TH_FORMULA f = At NOMINAL (TH_FORMULA f)
                  | Uni NOMINAL (TH_FORMULA f)
                  | Exist NOMINAL (TH_FORMULA f)
                  | Box MODALITY (TH_FORMULA f)
                  | Dia MODALITY (TH_FORMULA f)
                  | UnderLogic f
                  | Conjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Disjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Implication (TH_FORMULA f) (TH_FORMULA f)
                  | BiImplication (TH_FORMULA f) (TH_FORMULA f)
                  | Here NOMINAL
                  | Neg (TH_FORMULA f)
                  | Par (TH_FORMULA f)
                  | TrueA
                  | FalseA
                    deriving (Int -> TH_FORMULA f -> ShowS
[TH_FORMULA f] -> ShowS
TH_FORMULA f -> String
(Int -> TH_FORMULA f -> ShowS)
-> (TH_FORMULA f -> String)
-> ([TH_FORMULA f] -> ShowS)
-> Show (TH_FORMULA f)
forall f. Show f => Int -> TH_FORMULA f -> ShowS
forall f. Show f => [TH_FORMULA f] -> ShowS
forall f. Show f => TH_FORMULA f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TH_FORMULA f] -> ShowS
$cshowList :: forall f. Show f => [TH_FORMULA f] -> ShowS
show :: TH_FORMULA f -> String
$cshow :: forall f. Show f => TH_FORMULA f -> String
showsPrec :: Int -> TH_FORMULA f -> ShowS
$cshowsPrec :: forall f. Show f => Int -> TH_FORMULA f -> ShowS
Show, TH_FORMULA f -> TH_FORMULA f -> Bool
(TH_FORMULA f -> TH_FORMULA f -> Bool)
-> (TH_FORMULA f -> TH_FORMULA f -> Bool) -> Eq (TH_FORMULA f)
forall f. Eq f => TH_FORMULA f -> TH_FORMULA f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c/= :: forall f. Eq f => TH_FORMULA f -> TH_FORMULA f -> Bool
== :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c== :: forall f. Eq f => TH_FORMULA f -> TH_FORMULA f -> Bool
Eq, Eq (TH_FORMULA f)
Eq (TH_FORMULA f) =>
(TH_FORMULA f -> TH_FORMULA f -> Ordering)
-> (TH_FORMULA f -> TH_FORMULA f -> Bool)
-> (TH_FORMULA f -> TH_FORMULA f -> Bool)
-> (TH_FORMULA f -> TH_FORMULA f -> Bool)
-> (TH_FORMULA f -> TH_FORMULA f -> Bool)
-> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> (TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f)
-> Ord (TH_FORMULA f)
TH_FORMULA f -> TH_FORMULA f -> Bool
TH_FORMULA f -> TH_FORMULA f -> Ordering
TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
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
forall f. Ord f => Eq (TH_FORMULA f)
forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Bool
forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Ordering
forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
min :: TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
$cmin :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
max :: TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
$cmax :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
>= :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c>= :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Bool
> :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c> :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Bool
<= :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c<= :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Bool
< :: TH_FORMULA f -> TH_FORMULA f -> Bool
$c< :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Bool
compare :: TH_FORMULA f -> TH_FORMULA f -> Ordering
$ccompare :: forall f. Ord f => TH_FORMULA f -> TH_FORMULA f -> Ordering
$cp1Ord :: forall f. Ord f => Eq (TH_FORMULA f)
Ord, Typeable, Typeable (TH_FORMULA f)
Constr
DataType
Typeable (TH_FORMULA f) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f))
-> (TH_FORMULA f -> Constr)
-> (TH_FORMULA f -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (TH_FORMULA f)))
-> ((forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r)
-> (forall u. (forall d. Data d => d -> u) -> TH_FORMULA f -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TH_FORMULA f -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f))
-> Data (TH_FORMULA f)
TH_FORMULA f -> Constr
TH_FORMULA f -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f))
(forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f)
forall f. Data f => Typeable (TH_FORMULA f)
forall f. Data f => TH_FORMULA f -> Constr
forall f. Data f => TH_FORMULA f -> DataType
forall f.
Data f =>
(forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f
forall f u.
Data f =>
Int -> (forall d. Data d => d -> u) -> TH_FORMULA f -> u
forall f u.
Data f =>
(forall d. Data d => d -> u) -> TH_FORMULA f -> [u]
forall f r r'.
Data f =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
forall f r r'.
Data f =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
forall f (m :: * -> *).
(Data f, Monad m) =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
forall f (m :: * -> *).
(Data f, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
forall f (c :: * -> *).
Data f =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f)
forall f (c :: * -> *).
Data f =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f)
forall f (t :: * -> *) (c :: * -> *).
(Data f, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f))
forall f (t :: * -> * -> *) (c :: * -> *).
(Data f, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_FORMULA f))
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) -> TH_FORMULA f -> u
forall u. (forall d. Data d => d -> u) -> TH_FORMULA f -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_FORMULA f))
$cFalseA :: Constr
$cTrueA :: Constr
$cPar :: Constr
$cNeg :: Constr
$cHere :: Constr
$cBiImplication :: Constr
$cImplication :: Constr
$cDisjunction :: Constr
$cConjunction :: Constr
$cUnderLogic :: Constr
$cDia :: Constr
$cBox :: Constr
$cExist :: Constr
$cUni :: Constr
$cAt :: Constr
$tTH_FORMULA :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
$cgmapMo :: forall f (m :: * -> *).
(Data f, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
gmapMp :: (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
$cgmapMp :: forall f (m :: * -> *).
(Data f, MonadPlus m) =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
gmapM :: (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
$cgmapM :: forall f (m :: * -> *).
(Data f, Monad m) =>
(forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_FORMULA f -> u
$cgmapQi :: forall f u.
Data f =>
Int -> (forall d. Data d => d -> u) -> TH_FORMULA f -> u
gmapQ :: (forall d. Data d => d -> u) -> TH_FORMULA f -> [u]
$cgmapQ :: forall f u.
Data f =>
(forall d. Data d => d -> u) -> TH_FORMULA f -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
$cgmapQr :: forall f r r'.
Data f =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
$cgmapQl :: forall f r r'.
Data f =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r
gmapT :: (forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f
$cgmapT :: forall f.
Data f =>
(forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_FORMULA f))
$cdataCast2 :: forall f (t :: * -> * -> *) (c :: * -> *).
(Data f, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (TH_FORMULA f))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f))
$cdataCast1 :: forall f (t :: * -> *) (c :: * -> *).
(Data f, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f))
dataTypeOf :: TH_FORMULA f -> DataType
$cdataTypeOf :: forall f. Data f => TH_FORMULA f -> DataType
toConstr :: TH_FORMULA f -> Constr
$ctoConstr :: forall f. Data f => TH_FORMULA f -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f)
$cgunfold :: forall f (c :: * -> *).
Data f =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f)
$cgfoldl :: forall f (c :: * -> *).
Data f =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f)
$cp1Data :: forall f. Data f => Typeable (TH_FORMULA f)
Data)

instance ToJson f => ToJson (TH_FORMULA f) where
  asJson :: TH_FORMULA f -> Json
asJson _ = [JPair] -> Json
mkJObj []

instance ToXml f => ToXml (TH_FORMULA f) where
  asXml :: TH_FORMULA f -> Element
asXml _ = String -> () -> Element
forall t. Node t => String -> t -> Element
unode "missing" ()

{- Existential quantification is used, in the Sentences, Spec and Signature
because, we need to hide that these datatypes are polymorphic, or else,
haskell will complain that their types will vary with the same logic. Which
is forbidden in Logic class by using functional dependencies. -}

{- An hybridized formula has the hybrid constructors; the constructors
of the hybridized logic and the logic identifier, so that we can
identify the underlying logic, by only looking to the sentence. -}
data Frm_Wrap = forall l sub bs f s sm si mo sy rw pf .
    (Logic l sub bs f s sm si mo sy rw pf)
    => Frm_Wrap l (TH_FORMULA f)
  deriving Typeable

instance Show Frm_Wrap where
  show :: Frm_Wrap -> String
show (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) = "Frm_Wrap " String -> ShowS
forall a. [a] -> [a] -> [a]
++ l -> String
forall a. Show a => a -> String
show l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TH_FORMULA f -> String
forall a. Show a => a -> String
show TH_FORMULA f
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

instance ToJson Frm_Wrap where
  asJson :: Frm_Wrap -> Json
asJson (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) = [JPair] -> Json
mkJObj [("Frm_Wrap:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ l -> String
forall a. Show a => a -> String
show l
l, TH_FORMULA f -> Json
forall a. ToJson a => a -> Json
asJson TH_FORMULA f
f)]

instance ToXml Frm_Wrap where
  asXml :: Frm_Wrap -> Element
asXml (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) =
    Attr -> Element -> Element
add_attr (String -> String -> Attr
mkAttr "language" (String -> Attr) -> String -> Attr
forall a b. (a -> b) -> a -> b
$ l -> String
forall a. Show a => a -> String
show l
l) (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ String -> Element -> Element
forall t. Node t => String -> t -> Element
unode "Frm_Wrap" (Element -> Element) -> Element -> Element
forall a b. (a -> b) -> a -> b
$ TH_FORMULA f -> Element
forall a. ToXml a => a -> Element
asXml TH_FORMULA f
f

{- An hybridized specification has the basic specification; The declararation
of nominals and modalities, and the axioms; -}
data Spc_Wrap = forall l sub bs sen si smi sign mor symb raw pf .
    (Logic l sub bs sen si smi sign mor symb raw pf)
    => Spc_Wrap l (TH_BSPEC bs) [Annoted Frm_Wrap]
  deriving Typeable

instance Show Spc_Wrap where
  show :: Spc_Wrap -> String
show (Spc_Wrap l :: l
l b :: TH_BSPEC bs
b a :: [Annoted Frm_Wrap]
a) =
    "Spc_Wrap " String -> ShowS
forall a. [a] -> [a] -> [a]
++ l -> String
forall a. Show a => a -> String
show l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TH_BSPEC bs -> String
forall a. Show a => a -> String
show TH_BSPEC bs
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Annoted Frm_Wrap] -> String
forall a. Show a => a -> String
show [Annoted Frm_Wrap]
a

instance Semigroup Spc_Wrap where
  _ <> :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap
<> _ = String -> Spc_Wrap
forall a. HasCallStack => String -> a
error "Not implemented!"

instance Monoid Spc_Wrap where
 mempty :: Spc_Wrap
mempty = String -> Spc_Wrap
forall a. HasCallStack => String -> a
error "Not implemented!"

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

-- Why do we need to compare specifications ?
instance Ord Spc_Wrap where
        compare :: Spc_Wrap -> Spc_Wrap -> Ordering
compare _ _ = Ordering
GT

instance Eq Spc_Wrap where
       == :: Spc_Wrap -> Spc_Wrap -> Bool
(==) _ _ = Bool
False
-- --------------

-- Who do we need to order formulas ?
instance Ord Frm_Wrap where
        compare :: Frm_Wrap -> Frm_Wrap -> Ordering
compare a :: Frm_Wrap
a b :: Frm_Wrap
b = if Frm_Wrap
a Frm_Wrap -> Frm_Wrap -> Bool
forall a. Eq a => a -> a -> Bool
== Frm_Wrap
b then Ordering
EQ else Ordering
GT

{- Need to use unsafe coerce here, as the typechecker as no way to know
that if l == l' then type f == type f'. However, we know. -}
instance Eq Frm_Wrap where
       == :: Frm_Wrap -> Frm_Wrap -> Bool
(==) (Frm_Wrap l :: l
l f :: TH_FORMULA f
f) (Frm_Wrap l' :: l
l' f' :: TH_FORMULA f
f') =
               (l -> String
forall a. Show a => a -> String
show l
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== l -> String
forall a. Show a => a -> String
show l
l') Bool -> Bool -> Bool
&& (TH_FORMULA f -> TH_FORMULA f
forall a b. a -> b
unsafeCoerce TH_FORMULA f
f TH_FORMULA f -> TH_FORMULA f -> Bool
forall a. Eq a => a -> a -> Bool
== TH_FORMULA f
f')

-- Why do we need range ?
instance GetRange Frm_Wrap where
        getRange :: Frm_Wrap -> Range
getRange (Frm_Wrap _ f :: TH_FORMULA f
f) = TH_FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange TH_FORMULA f
f
        rangeSpan :: Frm_Wrap -> [Pos]
rangeSpan (Frm_Wrap _ f :: TH_FORMULA f
f) = TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
f

instance GetRange Spc_Wrap where
        getRange :: Spc_Wrap -> Range
getRange (Spc_Wrap _ s :: TH_BSPEC bs
s _) = TH_BSPEC bs -> Range
forall a. GetRange a => a -> Range
getRange TH_BSPEC bs
s
        rangeSpan :: Spc_Wrap -> [Pos]
rangeSpan (Spc_Wrap _ s :: TH_BSPEC bs
s _) = TH_BSPEC bs -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_BSPEC bs
s

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

instance GetRange s => GetRange (TH_BSPEC s) where
  getRange :: TH_BSPEC s -> Range
getRange = Range -> TH_BSPEC s -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: TH_BSPEC s -> [Pos]
rangeSpan x :: TH_BSPEC s
x = case TH_BSPEC s
x of
    Bspec a :: [TH_BASIC_ITEM]
a b :: s
b -> [[Pos]] -> [Pos]
joinRanges [[TH_BASIC_ITEM] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [TH_BASIC_ITEM]
a, s -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan s
b]

instance GetRange TH_BASIC_ITEM where
  getRange :: TH_BASIC_ITEM -> Range
getRange = Range -> TH_BASIC_ITEM -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: TH_BASIC_ITEM -> [Pos]
rangeSpan x :: TH_BASIC_ITEM
x = case TH_BASIC_ITEM
x of
    Simple_mod_decl a :: [MODALITY]
a -> [[Pos]] -> [Pos]
joinRanges [[MODALITY] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [MODALITY]
a]
    Simple_nom_decl a :: [MODALITY]
a -> [[Pos]] -> [Pos]
joinRanges [[MODALITY] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [MODALITY]
a]

instance GetRange f => GetRange (TH_FORMULA f) where
  getRange :: TH_FORMULA f -> Range
getRange = Range -> TH_FORMULA f -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: TH_FORMULA f -> [Pos]
rangeSpan x :: TH_FORMULA f
x = case TH_FORMULA f
x of
    At a :: MODALITY
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Uni a :: MODALITY
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Exist a :: MODALITY
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Box a :: MODALITY
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Dia a :: MODALITY
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    UnderLogic a :: f
a -> [[Pos]] -> [Pos]
joinRanges [f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan f
a]
    Conjunction a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Disjunction a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Implication a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    BiImplication a :: TH_FORMULA f
a b :: TH_FORMULA f
b -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a, TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
b]
    Here a :: MODALITY
a -> [[Pos]] -> [Pos]
joinRanges [MODALITY -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan MODALITY
a]
    Neg a :: TH_FORMULA f
a -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a]
    Par a :: TH_FORMULA f
a -> [[Pos]] -> [Pos]
joinRanges [TH_FORMULA f -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan TH_FORMULA f
a]
    TrueA -> []
    FalseA -> []

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