{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./ExtModal/Sublogic.hs
Description :  Sublogics for ExtModal logic
Copyright   :  (c) DFKI 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

Sublogics for ExtModal Logic
-}

module ExtModal.Sublogic where

import CASL.AS_Basic_CASL
import CASL.Sublogic

import Common.AS_Annotation

import Data.Data
import Data.Function
import Data.List
import qualified Data.Set as Set

import ExtModal.AS_ExtModal
import ExtModal.ExtModalSign

data Frequency = None | One | Many
  deriving (Int -> Frequency -> ShowS
[Frequency] -> ShowS
Frequency -> String
(Int -> Frequency -> ShowS)
-> (Frequency -> String)
-> ([Frequency] -> ShowS)
-> Show Frequency
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Frequency] -> ShowS
$cshowList :: [Frequency] -> ShowS
show :: Frequency -> String
$cshow :: Frequency -> String
showsPrec :: Int -> Frequency -> ShowS
$cshowsPrec :: Int -> Frequency -> ShowS
Show, Frequency -> Frequency -> Bool
(Frequency -> Frequency -> Bool)
-> (Frequency -> Frequency -> Bool) -> Eq Frequency
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Frequency -> Frequency -> Bool
$c/= :: Frequency -> Frequency -> Bool
== :: Frequency -> Frequency -> Bool
$c== :: Frequency -> Frequency -> Bool
Eq, Eq Frequency
Eq Frequency =>
(Frequency -> Frequency -> Ordering)
-> (Frequency -> Frequency -> Bool)
-> (Frequency -> Frequency -> Bool)
-> (Frequency -> Frequency -> Bool)
-> (Frequency -> Frequency -> Bool)
-> (Frequency -> Frequency -> Frequency)
-> (Frequency -> Frequency -> Frequency)
-> Ord Frequency
Frequency -> Frequency -> Bool
Frequency -> Frequency -> Ordering
Frequency -> Frequency -> Frequency
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 :: Frequency -> Frequency -> Frequency
$cmin :: Frequency -> Frequency -> Frequency
max :: Frequency -> Frequency -> Frequency
$cmax :: Frequency -> Frequency -> Frequency
>= :: Frequency -> Frequency -> Bool
$c>= :: Frequency -> Frequency -> Bool
> :: Frequency -> Frequency -> Bool
$c> :: Frequency -> Frequency -> Bool
<= :: Frequency -> Frequency -> Bool
$c<= :: Frequency -> Frequency -> Bool
< :: Frequency -> Frequency -> Bool
$c< :: Frequency -> Frequency -> Bool
compare :: Frequency -> Frequency -> Ordering
$ccompare :: Frequency -> Frequency -> Ordering
$cp1Ord :: Eq Frequency
Ord, Int -> Frequency
Frequency -> Int
Frequency -> [Frequency]
Frequency -> Frequency
Frequency -> Frequency -> [Frequency]
Frequency -> Frequency -> Frequency -> [Frequency]
(Frequency -> Frequency)
-> (Frequency -> Frequency)
-> (Int -> Frequency)
-> (Frequency -> Int)
-> (Frequency -> [Frequency])
-> (Frequency -> Frequency -> [Frequency])
-> (Frequency -> Frequency -> [Frequency])
-> (Frequency -> Frequency -> Frequency -> [Frequency])
-> Enum Frequency
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Frequency -> Frequency -> Frequency -> [Frequency]
$cenumFromThenTo :: Frequency -> Frequency -> Frequency -> [Frequency]
enumFromTo :: Frequency -> Frequency -> [Frequency]
$cenumFromTo :: Frequency -> Frequency -> [Frequency]
enumFromThen :: Frequency -> Frequency -> [Frequency]
$cenumFromThen :: Frequency -> Frequency -> [Frequency]
enumFrom :: Frequency -> [Frequency]
$cenumFrom :: Frequency -> [Frequency]
fromEnum :: Frequency -> Int
$cfromEnum :: Frequency -> Int
toEnum :: Int -> Frequency
$ctoEnum :: Int -> Frequency
pred :: Frequency -> Frequency
$cpred :: Frequency -> Frequency
succ :: Frequency -> Frequency
$csucc :: Frequency -> Frequency
Enum, Typeable, Typeable Frequency
Constr
DataType
Typeable Frequency =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Frequency -> c Frequency)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Frequency)
-> (Frequency -> Constr)
-> (Frequency -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Frequency))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Frequency))
-> ((forall b. Data b => b -> b) -> Frequency -> Frequency)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Frequency -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Frequency -> r)
-> (forall u. (forall d. Data d => d -> u) -> Frequency -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Frequency -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Frequency -> m Frequency)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Frequency -> m Frequency)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Frequency -> m Frequency)
-> Data Frequency
Frequency -> Constr
Frequency -> DataType
(forall b. Data b => b -> b) -> Frequency -> Frequency
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Frequency -> c Frequency
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Frequency
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) -> Frequency -> u
forall u. (forall d. Data d => d -> u) -> Frequency -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Frequency -> m Frequency
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Frequency -> m Frequency
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Frequency
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Frequency -> c Frequency
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Frequency)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Frequency)
$cMany :: Constr
$cOne :: Constr
$cNone :: Constr
$tFrequency :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Frequency -> m Frequency
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Frequency -> m Frequency
gmapMp :: (forall d. Data d => d -> m d) -> Frequency -> m Frequency
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Frequency -> m Frequency
gmapM :: (forall d. Data d => d -> m d) -> Frequency -> m Frequency
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Frequency -> m Frequency
gmapQi :: Int -> (forall d. Data d => d -> u) -> Frequency -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Frequency -> u
gmapQ :: (forall d. Data d => d -> u) -> Frequency -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Frequency -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Frequency -> r
gmapT :: (forall b. Data b => b -> b) -> Frequency -> Frequency
$cgmapT :: (forall b. Data b => b -> b) -> Frequency -> Frequency
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Frequency)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Frequency)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Frequency)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Frequency)
dataTypeOf :: Frequency -> DataType
$cdataTypeOf :: Frequency -> DataType
toConstr :: Frequency -> Constr
$ctoConstr :: Frequency -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Frequency
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Frequency
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Frequency -> c Frequency
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Frequency -> c Frequency
$cp1Data :: Typeable Frequency
Data)

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

maxSublogic :: Sublogic
maxSublogic :: Sublogic
maxSublogic = Sublogic :: Frequency
-> Bool -> Bool -> Bool -> Frequency -> Bool -> Bool -> Sublogic
Sublogic
    { hasModalities :: Frequency
hasModalities = Frequency
Many
    , hasTermMods :: Bool
hasTermMods = Bool
True
    , hasTransClos :: Bool
hasTransClos = Bool
True
    , hasNominals :: Bool
hasNominals = Bool
True
    , hasTimeMods :: Frequency
hasTimeMods = Frequency
Many
    , hasFixPoints :: Bool
hasFixPoints = Bool
True
    , hasFrameAxioms :: Bool
hasFrameAxioms = Bool
True
    }

botSublogic :: Sublogic
botSublogic :: Sublogic
botSublogic = Sublogic :: Frequency
-> Bool -> Bool -> Bool -> Frequency -> Bool -> Bool -> Sublogic
Sublogic
    { hasModalities :: Frequency
hasModalities = Frequency
None
    , hasTermMods :: Bool
hasTermMods = Bool
False
    , hasTransClos :: Bool
hasTransClos = Bool
False
    , hasNominals :: Bool
hasNominals = Bool
False
    , hasTimeMods :: Frequency
hasTimeMods = Frequency
None
    , hasFixPoints :: Bool
hasFixPoints = Bool
False
    , hasFrameAxioms :: Bool
hasFrameAxioms = Bool
False
    }

-- | the sublogic that can be translated to FOL
foleml :: Sublogic
foleml :: Sublogic
foleml = Sublogic
maxSublogic
  { hasTimeMods :: Frequency
hasTimeMods = Frequency
None
  , hasFixPoints :: Bool
hasFixPoints = Bool
False
  , hasTransClos :: Bool
hasTransClos = Bool
False
  , hasFrameAxioms :: Bool
hasFrameAxioms = Bool
False
  }

joinSublogic :: Sublogic -> Sublogic -> Sublogic
joinSublogic :: Sublogic -> Sublogic -> Sublogic
joinSublogic a :: Sublogic
a b :: Sublogic
b =
  let onMax :: (Sublogic -> c) -> c
onMax f :: Sublogic -> c
f = (c -> c -> c) -> (Sublogic -> c) -> Sublogic -> Sublogic -> c
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on c -> c -> c
forall a. Ord a => a -> a -> a
max Sublogic -> c
f Sublogic
a Sublogic
b
      termM :: Bool
termM = (Sublogic -> Bool) -> Bool
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Bool
hasTermMods
      timeM :: Frequency
timeM = (Sublogic -> Frequency) -> Frequency
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Frequency
hasTimeMods
  in Sublogic :: Frequency
-> Bool -> Bool -> Bool -> Frequency -> Bool -> Bool -> Sublogic
Sublogic
    { hasModalities :: Frequency
hasModalities = Bool -> Frequency -> Frequency
minMod Bool
termM Frequency
timeM
        Frequency -> Frequency -> Frequency
forall a. Ord a => a -> a -> a
`max` (Sublogic -> Frequency) -> Frequency
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Frequency
hasModalities
    , hasTermMods :: Bool
hasTermMods = Bool
termM
    , hasTransClos :: Bool
hasTransClos = (Sublogic -> Bool) -> Bool
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Bool
hasTransClos
    , hasNominals :: Bool
hasNominals = (Sublogic -> Bool) -> Bool
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Bool
hasNominals
    , hasTimeMods :: Frequency
hasTimeMods = Frequency
timeM
    , hasFixPoints :: Bool
hasFixPoints = (Sublogic -> Bool) -> Bool
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Bool
hasFixPoints
    , hasFrameAxioms :: Bool
hasFrameAxioms = (Sublogic -> Bool) -> Bool
forall c. Ord c => (Sublogic -> c) -> c
onMax Sublogic -> Bool
hasFrameAxioms
    }

instance Lattice Sublogic where
  cjoin :: Sublogic -> Sublogic -> Sublogic
cjoin = Sublogic -> Sublogic -> Sublogic
joinSublogic
  ctop :: Sublogic
ctop = Sublogic
maxSublogic
  bot :: Sublogic
bot = Sublogic
botSublogic

joinSublogics :: [Sublogic] -> Sublogic
joinSublogics :: [Sublogic] -> Sublogic
joinSublogics = (Sublogic -> Sublogic -> Sublogic)
-> Sublogic -> [Sublogic] -> Sublogic
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sublogic -> Sublogic -> Sublogic
joinSublogic Sublogic
botSublogic

type ExtModalSL = CASL_SL Sublogic

minSublogicOfForm :: FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm :: FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm = (EM_FORMULA -> ExtModalSL) -> FORMULA EM_FORMULA -> ExtModalSL
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_sentence EM_FORMULA -> ExtModalSL
minSublogicOfEM

minSublogicOfTerm :: TERM EM_FORMULA -> ExtModalSL
minSublogicOfTerm :: TERM EM_FORMULA -> ExtModalSL
minSublogicOfTerm = (EM_FORMULA -> ExtModalSL) -> TERM EM_FORMULA -> ExtModalSL
forall a f. Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
sl_term EM_FORMULA -> ExtModalSL
minSublogicOfEM

minSublogicOfMod :: MODALITY -> ExtModalSL
minSublogicOfMod :: MODALITY -> ExtModalSL
minSublogicOfMod m :: MODALITY
m = case MODALITY
m of
    SimpleMod _ -> ExtModalSL
forall a. Lattice a => CASL_SL a
bottom
    TermMod t :: TERM EM_FORMULA
t -> TERM EM_FORMULA -> ExtModalSL
minSublogicOfTerm TERM EM_FORMULA
t
    ModOp _ m1 :: MODALITY
m1 m2 :: MODALITY
m2 -> (ExtModalSL -> ExtModalSL -> ExtModalSL)
-> (MODALITY -> ExtModalSL) -> MODALITY -> MODALITY -> ExtModalSL
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on ExtModalSL -> ExtModalSL -> ExtModalSL
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max MODALITY -> ExtModalSL
minSublogicOfMod MODALITY
m1 MODALITY
m2
    TransClos c :: MODALITY
c -> (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (\ s :: Sublogic
s -> Sublogic
s {hasTransClos :: Bool
hasTransClos = Bool
True})
      (MODALITY -> ExtModalSL
minSublogicOfMod MODALITY
c)
    Guard f :: FORMULA EM_FORMULA
f -> FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm FORMULA EM_FORMULA
f

minSublogicOfPrefix :: FormPrefix -> ExtModalSL
minSublogicOfPrefix :: FormPrefix -> ExtModalSL
minSublogicOfPrefix fp :: FormPrefix
fp = case FormPrefix
fp of
    BoxOrDiamond _ m :: MODALITY
m _ _ -> MODALITY -> ExtModalSL
minSublogicOfMod MODALITY
m
    Hybrid _ _ -> Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkBot Sublogic
botSublogic {hasNominals :: Bool
hasNominals = Bool
True}
    FixedPoint _ _ -> Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkBot Sublogic
botSublogic {hasFixPoints :: Bool
hasFixPoints = Bool
True}
    _ -> (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (Bool -> [()] -> Sublogic -> Sublogic
forall a. Bool -> [a] -> Sublogic -> Sublogic
setTimeMods Bool
True [()]) ExtModalSL
forall a. Lattice a => CASL_SL a
bottom

minSublogicOfEM :: EM_FORMULA -> ExtModalSL
minSublogicOfEM :: EM_FORMULA -> ExtModalSL
minSublogicOfEM ef :: EM_FORMULA
ef = case EM_FORMULA
ef of
    PrefixForm pf :: FormPrefix
pf f :: FORMULA EM_FORMULA
f _ -> ExtModalSL -> ExtModalSL -> ExtModalSL
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max (FormPrefix -> ExtModalSL
minSublogicOfPrefix FormPrefix
pf)
        (FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm FORMULA EM_FORMULA
f)
    UntilSince _ f1 :: FORMULA EM_FORMULA
f1 f2 :: FORMULA EM_FORMULA
f2 _ -> (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (Bool -> [()] -> Sublogic -> Sublogic
forall a. Bool -> [a] -> Sublogic -> Sublogic
setTimeMods Bool
True [()])
      (ExtModalSL -> ExtModalSL) -> ExtModalSL -> ExtModalSL
forall a b. (a -> b) -> a -> b
$ (ExtModalSL -> ExtModalSL -> ExtModalSL)
-> (FORMULA EM_FORMULA -> ExtModalSL)
-> FORMULA EM_FORMULA
-> FORMULA EM_FORMULA
-> ExtModalSL
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on ExtModalSL -> ExtModalSL -> ExtModalSL
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm FORMULA EM_FORMULA
f1 FORMULA EM_FORMULA
f2
    ModForm md :: ModDefn
md -> ModDefn -> ExtModalSL
minSublogicOfModDefn ModDefn
md

minSublogicOfModDefn :: ModDefn -> ExtModalSL
minSublogicOfModDefn :: ModDefn -> ExtModalSL
minSublogicOfModDefn (ModDefn time :: Bool
time term :: Bool
term il :: [Annoted Id]
il fl :: [Annoted FrameForm]
fl _) =
    (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (\ s :: Sublogic
s -> Sublogic
s {hasFrameAxioms :: Bool
hasFrameAxioms = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Annoted FrameForm] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted FrameForm]
fl})
    (ExtModalSL -> ExtModalSL)
-> ([Annoted (FORMULA EM_FORMULA)] -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)]
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature ([Annoted Id] -> Sublogic -> Sublogic
forall a. [a] -> Sublogic -> Sublogic
setModalities [Annoted Id]
il)
    (ExtModalSL -> ExtModalSL)
-> ([Annoted (FORMULA EM_FORMULA)] -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)]
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (Bool -> Sublogic -> Sublogic
setTermMods Bool
term)
    (ExtModalSL -> ExtModalSL)
-> ([Annoted (FORMULA EM_FORMULA)] -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)]
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sublogic -> Sublogic) -> ExtModalSL -> ExtModalSL
forall a. (a -> a) -> CASL_SL a -> CASL_SL a
updExtFeature (Bool -> [Annoted Id] -> Sublogic -> Sublogic
forall a. Bool -> [a] -> Sublogic -> Sublogic
setTimeMods Bool
time [Annoted Id]
il)
    (ExtModalSL -> ExtModalSL)
-> ([Annoted (FORMULA EM_FORMULA)] -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)]
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExtModalSL] -> ExtModalSL
forall a. Lattice a => [CASL_SL a] -> CASL_SL a
comp_list ([ExtModalSL] -> ExtModalSL)
-> ([Annoted (FORMULA EM_FORMULA)] -> [ExtModalSL])
-> [Annoted (FORMULA EM_FORMULA)]
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annoted (FORMULA EM_FORMULA) -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)] -> [ExtModalSL]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA EM_FORMULA -> ExtModalSL
minSublogicOfForm (FORMULA EM_FORMULA -> ExtModalSL)
-> (Annoted (FORMULA EM_FORMULA) -> FORMULA EM_FORMULA)
-> Annoted (FORMULA EM_FORMULA)
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (FORMULA EM_FORMULA) -> FORMULA EM_FORMULA
forall a. Annoted a -> a
item)
          ([Annoted (FORMULA EM_FORMULA)] -> ExtModalSL)
-> [Annoted (FORMULA EM_FORMULA)] -> ExtModalSL
forall a b. (a -> b) -> a -> b
$ (Annoted FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> [Annoted FrameForm] -> [Annoted (FORMULA EM_FORMULA)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FrameForm -> [Annoted (FORMULA EM_FORMULA)]
frameForms (FrameForm -> [Annoted (FORMULA EM_FORMULA)])
-> (Annoted FrameForm -> FrameForm)
-> Annoted FrameForm
-> [Annoted (FORMULA EM_FORMULA)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted FrameForm -> FrameForm
forall a. Annoted a -> a
item) [Annoted FrameForm]
fl

minSublogicEMSign :: EModalSign -> ExtModalSL
minSublogicEMSign :: EModalSign -> ExtModalSL
minSublogicEMSign s :: EModalSign
s = Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkBot Sublogic
botSublogic
  { hasTermMods :: Bool
hasTermMods = Bool -> Bool
not (Bool -> Bool) -> (Set Id -> Bool) -> Set Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> Bool
forall a. Set a -> Bool
Set.null (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
termMods EModalSign
s
  , hasTimeMods :: Frequency
hasTimeMods = case Set Id -> Int
forall a. Set a -> Int
Set.size (Set Id -> Int) -> Set Id -> Int
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
timeMods EModalSign
s of
      0 -> Frequency
None
      1 -> Frequency
One
      _ -> Frequency
Many
  , hasNominals :: Bool
hasNominals = Bool -> Bool
not (Bool -> Bool) -> (Set Id -> Bool) -> Set Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Id -> Bool
forall a. Set a -> Bool
Set.null (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
nominals EModalSign
s
  , hasModalities :: Frequency
hasModalities = case Set Id -> Int
forall a. Set a -> Int
Set.size (Set Id -> Int) -> Set Id -> Int
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
s of
      0 -> Frequency
None
      1 -> Frequency
One
      _ -> Frequency
Many
  }

minSublogicEMBasic :: EM_BASIC_ITEM -> ExtModalSL
minSublogicEMBasic :: EM_BASIC_ITEM -> ExtModalSL
minSublogicEMBasic bi :: EM_BASIC_ITEM
bi = case EM_BASIC_ITEM
bi of
  ModItem md :: ModDefn
md -> ModDefn -> ExtModalSL
minSublogicOfModDefn ModDefn
md
  Nominal_decl l :: [Annoted SIMPLE_ID]
l _ -> Sublogic -> ExtModalSL
forall a. a -> CASL_SL a
mkBot Sublogic
botSublogic { hasNominals :: Bool
hasNominals = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Annoted SIMPLE_ID] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SIMPLE_ID]
l }

minSLExtSigItem :: EM_SIG_ITEM -> [ExtModalSL]
minSLExtSigItem :: EM_SIG_ITEM -> [ExtModalSL]
minSLExtSigItem si :: EM_SIG_ITEM
si = case EM_SIG_ITEM
si of
  Rigid_op_items _ os :: [Annoted (OP_ITEM EM_FORMULA)]
os _ -> (Annoted (OP_ITEM EM_FORMULA) -> ExtModalSL)
-> [Annoted (OP_ITEM EM_FORMULA)] -> [ExtModalSL]
forall a b. (a -> b) -> [a] -> [b]
map ((EM_FORMULA -> ExtModalSL) -> OP_ITEM EM_FORMULA -> ExtModalSL
forall a f. Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
sl_op_item EM_FORMULA -> ExtModalSL
minSublogicOfEM (OP_ITEM EM_FORMULA -> ExtModalSL)
-> (Annoted (OP_ITEM EM_FORMULA) -> OP_ITEM EM_FORMULA)
-> Annoted (OP_ITEM EM_FORMULA)
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (OP_ITEM EM_FORMULA) -> OP_ITEM EM_FORMULA
forall a. Annoted a -> a
item) [Annoted (OP_ITEM EM_FORMULA)]
os
  Rigid_pred_items _ ps :: [Annoted (PRED_ITEM EM_FORMULA)]
ps _ -> (Annoted (PRED_ITEM EM_FORMULA) -> ExtModalSL)
-> [Annoted (PRED_ITEM EM_FORMULA)] -> [ExtModalSL]
forall a b. (a -> b) -> [a] -> [b]
map ((EM_FORMULA -> ExtModalSL) -> PRED_ITEM EM_FORMULA -> ExtModalSL
forall a f.
Lattice a =>
(f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
sl_pred_item EM_FORMULA -> ExtModalSL
minSublogicOfEM (PRED_ITEM EM_FORMULA -> ExtModalSL)
-> (Annoted (PRED_ITEM EM_FORMULA) -> PRED_ITEM EM_FORMULA)
-> Annoted (PRED_ITEM EM_FORMULA)
-> ExtModalSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted (PRED_ITEM EM_FORMULA) -> PRED_ITEM EM_FORMULA
forall a. Annoted a -> a
item) [Annoted (PRED_ITEM EM_FORMULA)]
ps

setModalities :: [a] -> Sublogic -> Sublogic
setModalities :: [a] -> Sublogic -> Sublogic
setModalities il :: [a]
il s :: Sublogic
s = case [a]
il of
    [_] -> Sublogic
s {hasModalities :: Frequency
hasModalities = Frequency -> Frequency -> Frequency
forall a. Ord a => a -> a -> a
max Frequency
One (Sublogic -> Frequency
hasModalities Sublogic
s)}
    _ -> Sublogic
s {hasModalities :: Frequency
hasModalities = Frequency
Many}

setTermMods :: Bool -> Sublogic -> Sublogic
setTermMods :: Bool -> Sublogic -> Sublogic
setTermMods b :: Bool
b s :: Sublogic
s = if Bool
b then Sublogic
s {hasTermMods :: Bool
hasTermMods = Bool
True} else Sublogic
s

setTimeMods :: Bool -> [a] -> Sublogic -> Sublogic
setTimeMods :: Bool -> [a] -> Sublogic -> Sublogic
setTimeMods b :: Bool
b il :: [a]
il s :: Sublogic
s = if Bool
b then case [a]
il of
    [_] -> Sublogic
s {hasTimeMods :: Frequency
hasTimeMods = Frequency -> Frequency -> Frequency
forall a. Ord a => a -> a -> a
max Frequency
One (Sublogic -> Frequency
hasTimeMods Sublogic
s)}
    _ -> Sublogic
s {hasTimeMods :: Frequency
hasTimeMods = Frequency
Many}
    else Sublogic
s

minMod :: Bool -> Frequency -> Frequency
minMod :: Bool -> Frequency -> Frequency
minMod h_term :: Bool
h_term h_time :: Frequency
h_time = if Bool
h_term Bool -> Bool -> Bool
&& Frequency
h_time Frequency -> Frequency -> Bool
forall a. Eq a => a -> a -> Bool
== Frequency
None then Frequency
One
  else Frequency
h_time

sublogicsDim :: [[Sublogic]]
sublogicsDim :: [[Sublogic]]
sublogicsDim = let
  t :: Bool
t = Bool
True
  b :: Sublogic
b = Sublogic
forall l. Lattice l => l
bot
  f :: [Frequency]
f = [Frequency
One, Frequency
Many]
  in [ [ Sublogic
b { hasModalities :: Frequency
hasModalities = Frequency
h } | Frequency
h <- [Frequency]
f]
     , [ Sublogic
b { hasTermMods :: Bool
hasTermMods = Bool
t }]
     , [ Sublogic
b { hasTransClos :: Bool
hasTransClos = Bool
t }]
     , [ Sublogic
b { hasNominals :: Bool
hasNominals = Bool
t }]
     , [ Sublogic
b { hasModalities :: Frequency
hasModalities = Frequency
h } | Frequency
h <- [Frequency]
f]
     , [ Sublogic
b { hasFixPoints :: Bool
hasFixPoints = Bool
t }]
     , [ Sublogic
b { hasFrameAxioms :: Bool
hasFrameAxioms = Bool
t }] ]

sublogName :: Sublogic -> String
sublogName :: Sublogic -> String
sublogName s :: Sublogic
s = (if Sublogic -> Frequency
hasModalities Sublogic
s Frequency -> Frequency -> Bool
forall a. Eq a => a -> a -> Bool
== Frequency
Many then "Many" else "One")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Sublogic -> Bool
hasTermMods Sublogic
s then "Dyn" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Sublogic -> Bool
hasNominals Sublogic
s then "Hybr" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Sublogic -> Frequency
hasTimeMods Sublogic
s Frequency -> Frequency -> Bool
forall a. Eq a => a -> a -> Bool
== Frequency
Many then "Time"
       else if Sublogic -> Frequency
hasTimeMods Sublogic
s Frequency -> Frequency -> Bool
forall a. Eq a => a -> a -> Bool
== Frequency
One then "SingleTime" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Sublogic -> Bool
hasFixPoints Sublogic
s then "Fix" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Sublogic -> Bool
hasFrameAxioms Sublogic
s then "Frames" else "")
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Sublogic -> Bool
hasTransClos Sublogic
s then "*" else ""

parseSublog :: String -> (Sublogic, String)
parseSublog :: String -> (Sublogic, String)
parseSublog s0 :: String
s0 = let
  (m :: Frequency
m, s1 :: String
s1) = case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Many" String
s0 of
    Nothing -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "One" String
s0 of
      Nothing -> (Frequency
None, String
s0)
      Just r :: String
r -> (Frequency
One, String
r)
    Just r :: String
r -> (Frequency
Many, String
r)
  (tm :: Bool
tm, s2 :: String
s2) = String -> String -> (Bool, String)
parseBool "Dyn" String
s1
  (n :: Bool
n, s3 :: String
s3) = String -> String -> (Bool, String)
parseBool "Hybr" String
s2
  (ti :: Frequency
ti, s4 :: String
s4) = case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Time" String
s3 of
    Just r :: String
r -> (Frequency
Many, String
r)
    Nothing -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SingleTime" String
s3 of
      Nothing -> (Frequency
None, String
s3)
      Just r :: String
r -> (Frequency
One, String
r)
  (fi :: Bool
fi, s5 :: String
s5) = String -> String -> (Bool, String)
parseBool "Fix" String
s4
  (fr :: Bool
fr, s6 :: String
s6) = String -> String -> (Bool, String)
parseBool "Frames" String
s5
  (tr :: Bool
tr, s7 :: String
s7) = String -> String -> (Bool, String)
parseBool "*" String
s6
  in (Sublogic :: Frequency
-> Bool -> Bool -> Bool -> Frequency -> Bool -> Bool -> Sublogic
Sublogic
    { hasModalities :: Frequency
hasModalities = Frequency -> Frequency -> Frequency
forall a. Ord a => a -> a -> a
max Frequency
m (Frequency -> Frequency) -> Frequency -> Frequency
forall a b. (a -> b) -> a -> b
$ Bool -> Frequency -> Frequency
minMod Bool
tm Frequency
ti
    , hasTermMods :: Bool
hasTermMods = Bool
tm
    , hasTransClos :: Bool
hasTransClos = Bool
tr
    , hasNominals :: Bool
hasNominals = Bool
n
    , hasTimeMods :: Frequency
hasTimeMods = Frequency
ti
    , hasFixPoints :: Bool
hasFixPoints = Bool
fi
    , hasFrameAxioms :: Bool
hasFrameAxioms = Bool
fr
    }, String
s7)