{-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}
{- |
Module      :  ./THF/Sublogic.hs
Description :  Sublogics for THF
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  experimental
Portability :  non-portable (via Logic.Logic)

Sublogics for THF
-}

module THF.Sublogic where

import THF.As

import Logic.Logic

import Data.Data

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

data THFSl = THFSl {
 THFSl -> THFCoreSl
core :: THFCoreSl,
 THFSl -> Bool
ext_Poly :: Bool } deriving (THFSl -> THFSl -> Bool
(THFSl -> THFSl -> Bool) -> (THFSl -> THFSl -> Bool) -> Eq THFSl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: THFSl -> THFSl -> Bool
$c/= :: THFSl -> THFSl -> Bool
== :: THFSl -> THFSl -> Bool
$c== :: THFSl -> THFSl -> Bool
Eq, Eq THFSl
Eq THFSl =>
(THFSl -> THFSl -> Ordering)
-> (THFSl -> THFSl -> Bool)
-> (THFSl -> THFSl -> Bool)
-> (THFSl -> THFSl -> Bool)
-> (THFSl -> THFSl -> Bool)
-> (THFSl -> THFSl -> THFSl)
-> (THFSl -> THFSl -> THFSl)
-> Ord THFSl
THFSl -> THFSl -> Bool
THFSl -> THFSl -> Ordering
THFSl -> THFSl -> THFSl
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 :: THFSl -> THFSl -> THFSl
$cmin :: THFSl -> THFSl -> THFSl
max :: THFSl -> THFSl -> THFSl
$cmax :: THFSl -> THFSl -> THFSl
>= :: THFSl -> THFSl -> Bool
$c>= :: THFSl -> THFSl -> Bool
> :: THFSl -> THFSl -> Bool
$c> :: THFSl -> THFSl -> Bool
<= :: THFSl -> THFSl -> Bool
$c<= :: THFSl -> THFSl -> Bool
< :: THFSl -> THFSl -> Bool
$c< :: THFSl -> THFSl -> Bool
compare :: THFSl -> THFSl -> Ordering
$ccompare :: THFSl -> THFSl -> Ordering
$cp1Ord :: Eq THFSl
Ord, Typeable, Typeable THFSl
Constr
DataType
Typeable THFSl =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> THFSl -> c THFSl)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c THFSl)
-> (THFSl -> Constr)
-> (THFSl -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c THFSl))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSl))
-> ((forall b. Data b => b -> b) -> THFSl -> THFSl)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r)
-> (forall u. (forall d. Data d => d -> u) -> THFSl -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> THFSl -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> THFSl -> m THFSl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> THFSl -> m THFSl)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> THFSl -> m THFSl)
-> Data THFSl
THFSl -> Constr
THFSl -> DataType
(forall b. Data b => b -> b) -> THFSl -> THFSl
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THFSl -> c THFSl
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c THFSl
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) -> THFSl -> u
forall u. (forall d. Data d => d -> u) -> THFSl -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> THFSl -> m THFSl
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> THFSl -> m THFSl
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c THFSl
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THFSl -> c THFSl
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c THFSl)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSl)
$cTHFSl :: Constr
$tTHFSl :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> THFSl -> m THFSl
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> THFSl -> m THFSl
gmapMp :: (forall d. Data d => d -> m d) -> THFSl -> m THFSl
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> THFSl -> m THFSl
gmapM :: (forall d. Data d => d -> m d) -> THFSl -> m THFSl
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> THFSl -> m THFSl
gmapQi :: Int -> (forall d. Data d => d -> u) -> THFSl -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> THFSl -> u
gmapQ :: (forall d. Data d => d -> u) -> THFSl -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> THFSl -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSl -> r
gmapT :: (forall b. Data b => b -> b) -> THFSl -> THFSl
$cgmapT :: (forall b. Data b => b -> b) -> THFSl -> THFSl
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSl)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSl)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c THFSl)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c THFSl)
dataTypeOf :: THFSl -> DataType
$cdataTypeOf :: THFSl -> DataType
toConstr :: THFSl -> Constr
$ctoConstr :: THFSl -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c THFSl
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c THFSl
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THFSl -> c THFSl
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THFSl -> c THFSl
$cp1Data :: Typeable THFSl
Data)

instance Show THFSl where
 show :: THFSl -> String
show sl :: THFSl
sl = THFCoreSl -> String
forall a. Show a => a -> String
show (THFSl -> THFCoreSl
core THFSl
sl) String -> ShowS
forall a. [a] -> [a] -> [a]
++
           (if THFSl -> Bool
ext_Poly THFSl
sl then
            "_P" else "")


joinCoreSl :: THFCoreSl -> THFCoreSl -> THFCoreSl
joinCoreSl :: THFCoreSl -> THFCoreSl -> THFCoreSl
joinCoreSl THF _ = THFCoreSl
THF
joinCoreSl _ THF = THFCoreSl
THF
joinCoreSl THFP _ = THFCoreSl
THFP
joinCoreSl _ THFP = THFCoreSl
THFP
joinCoreSl _ _ = THFCoreSl
THF0

joinSL :: THFSl -> THFSl -> THFSl
joinSL :: THFSl -> THFSl -> THFSl
joinSL sl1 :: THFSl
sl1 sl2 :: THFSl
sl2 = THFSl :: THFCoreSl -> Bool -> THFSl
THFSl {
 core :: THFCoreSl
core = THFCoreSl -> THFCoreSl -> THFCoreSl
joinCoreSl (THFSl -> THFCoreSl
core THFSl
sl1) (THFSl -> THFCoreSl
core THFSl
sl2),
 ext_Poly :: Bool
ext_Poly = THFSl -> Bool
ext_Poly THFSl
sl1 Bool -> Bool -> Bool
|| THFSl -> Bool
ext_Poly THFSl
sl2 }

tHF0, tHFP, tHF :: THFSl
tHF0 :: THFSl
tHF0 = THFSl :: THFCoreSl -> Bool -> THFSl
THFSl { core :: THFCoreSl
core = THFCoreSl
THF0, ext_Poly :: Bool
ext_Poly = Bool
False }
tHFP :: THFSl
tHFP = THFSl :: THFCoreSl -> Bool -> THFSl
THFSl { core :: THFCoreSl
core = THFCoreSl
THFP, ext_Poly :: Bool
ext_Poly = Bool
False }
tHF :: THFSl
tHF = THFSl :: THFCoreSl -> Bool -> THFSl
THFSl { core :: THFCoreSl
core = THFCoreSl
THF , ext_Poly :: Bool
ext_Poly = Bool
False }

tHF0_P, tHFP_P, tHF_P :: THFSl
tHF0_P :: THFSl
tHF0_P = THFSl
tHF0 { ext_Poly :: Bool
ext_Poly = Bool
True }
tHFP_P :: THFSl
tHFP_P = THFSl
tHFP { ext_Poly :: Bool
ext_Poly = Bool
True }
tHF_P :: THFSl
tHF_P = THFSl
tHF { ext_Poly :: Bool
ext_Poly = Bool
True }

sublogics_all :: [THFSl]
sublogics_all :: [THFSl]
sublogics_all = [THFSl
tHF0, THFSl
tHF0_P,
                 THFSl
tHFP, THFSl
tHFP_P,
                 THFSl
tHF, THFSl
tHF_P]

instance MinSublogic THFSl THFFormula where
 minSublogic :: THFFormula -> THFSl
minSublogic f :: THFFormula
f = case THFFormula
f of
   TF_THF_Logic_Formula f' :: THFLogicFormula
f' -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f'
   TF_THF_Sequent s :: THFSequent
s -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFSequent -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFSequent
s
   T0F_THF_Typed_Const tc :: THFTypedConst
tc -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFTypedConst -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTypedConst
tc -- fixme: Not in THF?

instance MinSublogic THFSl THFLogicFormula where
 minSublogic :: THFLogicFormula -> THFSl
minSublogic f :: THFLogicFormula
f = case THFLogicFormula
f of
   TLF_THF_Binary_Formula b :: THFBinaryFormula
b -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryFormula
b
   TLF_THF_Unitary_Formula u :: THFUnitaryFormula
u -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
u
   TLF_THF_Type_Formula tf :: THFTypeFormula
tf -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFTypeFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTypeFormula
tf
   TLF_THF_Sub_Type st :: THFSubType
st -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFSubType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFSubType
st

instance MinSublogic THFSl THFSequent where
 minSublogic :: THFSequent -> THFSl
minSublogic _ = THFSl
tHF

instance MinSublogic THFSl THFTypedConst where
 minSublogic :: THFTypedConst -> THFSl
minSublogic c :: THFTypedConst
c = case THFTypedConst
c of
   T0TC_Typed_Const _ tp :: THFTopLevelType
tp -> THFTopLevelType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTopLevelType
tp
   T0TC_THF_TypedConst_Par tp :: THFTypedConst
tp -> THFTypedConst -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTypedConst
tp

instance MinSublogic THFSl THFBinaryFormula where
 minSublogic :: THFBinaryFormula -> THFSl
minSublogic b :: THFBinaryFormula
b = case THFBinaryFormula
b of
   TBF_THF_Binary_Pair f1 :: THFUnitaryFormula
f1 c :: THFPairConnective
c f2 :: THFUnitaryFormula
f2 -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl -> THFSl
joinSL (THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
f1)
    (THFSl -> THFSl -> THFSl
joinSL (THFPairConnective -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFPairConnective
c) (THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
f2)))
   TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFBinaryTuple -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryTuple
bt
   TBF_THF_Binary_Type bt :: THFBinaryType
bt -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFBinaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryType
bt

instance MinSublogic THFSl THFUnitaryFormula where
 minSublogic :: THFUnitaryFormula -> THFSl
minSublogic u :: THFUnitaryFormula
u = case THFUnitaryFormula
u of
   TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFQuantifiedFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFQuantifiedFormula
qf
   TUF_THF_Unary_Formula uc :: THFUnaryConnective
uc f :: THFLogicFormula
f -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFSl -> THFSl -> THFSl
joinSL (THFUnaryConnective -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnaryConnective
uc)
                                                  (THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f)
   TUF_THF_Atom a :: THFAtom
a -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFAtom
a
   TUF_THF_Tuple uts :: THFTuple
uts -> (THFLogicFormula -> THFSl -> THFSl) -> THFSl -> THFTuple -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFLogicFormula -> THFSl) -> THFLogicFormula -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHFP THFTuple
uts
   TUF_THF_Conditional f1 :: THFLogicFormula
f1 f2 :: THFLogicFormula
f2 f3 :: THFLogicFormula
f3 -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFSl -> THFSl -> THFSl
joinSL (THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f1)
                                 (THFSl -> THFSl -> THFSl
joinSL (THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f2) (THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f3))
   TUF_THF_Logic_Formula_Par f :: THFLogicFormula
f -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f
   T0UF_THF_Abstraction vs :: THFVariableList
vs u' :: THFUnitaryFormula
u' -> THFSl -> THFSl -> THFSl
joinSL ((THFVariable -> THFSl -> THFSl)
-> THFSl -> THFVariableList -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFVariable -> THFSl) -> THFVariable -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFVariable -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 THFVariableList
vs) (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$
                                       THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
u'

instance MinSublogic THFSl THFTypeFormula where
 minSublogic :: THFTypeFormula -> THFSl
minSublogic tf :: THFTypeFormula
tf = case THFTypeFormula
tf of
   TTF_THF_Type_Formula tf' :: THFTypeableFormula
tf' tp :: THFTopLevelType
tp -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFSl -> THFSl -> THFSl
joinSL (THFTypeableFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTypeableFormula
tf')
                                                  (THFTopLevelType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTopLevelType
tp)
   TTF_THF_Typed_Const _ tp :: THFTopLevelType
tp -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFTopLevelType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTopLevelType
tp

instance MinSublogic THFSl THFSubType where
 minSublogic :: THFSubType -> THFSl
minSublogic _ = THFSl
tHF

instance MinSublogic THFSl THFPairConnective where
 minSublogic :: THFPairConnective -> THFSl
minSublogic _ = THFSl
tHF0

instance MinSublogic THFSl THFBinaryTuple where
 minSublogic :: THFBinaryTuple -> THFSl
minSublogic bt :: THFBinaryTuple
bt = case THFBinaryTuple
bt of
   TBT_THF_Or_Formula ufs :: [THFUnitaryFormula]
ufs -> (THFUnitaryFormula -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryFormula] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryFormula -> THFSl)
-> THFUnitaryFormula
-> THFSl
-> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 [THFUnitaryFormula]
ufs
   TBT_THF_And_Formula ufs :: [THFUnitaryFormula]
ufs -> (THFUnitaryFormula -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryFormula] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryFormula -> THFSl)
-> THFUnitaryFormula
-> THFSl
-> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 [THFUnitaryFormula]
ufs
   TBT_THF_Apply_Formula ufs :: [THFUnitaryFormula]
ufs -> (THFUnitaryFormula -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryFormula] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryFormula -> THFSl)
-> THFUnitaryFormula
-> THFSl
-> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 [THFUnitaryFormula]
ufs

instance MinSublogic THFSl THFBinaryType where
 minSublogic :: THFBinaryType -> THFSl
minSublogic bt :: THFBinaryType
bt = case THFBinaryType
bt of
   TBT_THF_Mapping_Type uts :: [THFUnitaryType]
uts ->
    THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ (THFUnitaryType -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryType] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryType -> THFSl) -> THFUnitaryType -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 [THFUnitaryType]
uts
   TBT_THF_Xprod_Type uts :: [THFUnitaryType]
uts ->
    (THFUnitaryType -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryType] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryType -> THFSl) -> THFUnitaryType -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHFP [THFUnitaryType]
uts
   TBT_THF_Union_Type uts :: [THFUnitaryType]
uts ->
    (THFUnitaryType -> THFSl -> THFSl)
-> THFSl -> [THFUnitaryType] -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFUnitaryType -> THFSl) -> THFUnitaryType -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFUnitaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF [THFUnitaryType]
uts
   T0BT_THF_Binary_Type_Par bt' :: THFBinaryType
bt' -> THFBinaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryType
bt'
  {- fixme: maybe we need to check TUT_THF_Unitary_Formula for ShortTypes
  fixme: how does this differ from THF? -}

instance MinSublogic THFSl THFQuantifiedFormula where
 minSublogic :: THFQuantifiedFormula -> THFSl
minSublogic qf :: THFQuantifiedFormula
qf = case THFQuantifiedFormula
qf of
   TQF_THF_Quantified_Formula qf' :: THFQuantifier
qf' vs :: THFVariableList
vs u :: THFUnitaryFormula
u -> THFSl -> THFSl -> THFSl
joinSL (THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
u) (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$
                                         THFSl -> THFSl -> THFSl
joinSL (THFQuantifier -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFQuantifier
qf')
                                          ((THFVariable -> THFSl -> THFSl)
-> THFSl -> THFVariableList -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFVariable -> THFSl) -> THFVariable -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFVariable -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 THFVariableList
vs)
   T0QF_THF_Quantified_Var qf' :: Quantifier
qf' vs :: THFVariableList
vs u :: THFUnitaryFormula
u -> THFSl -> THFSl -> THFSl
joinSL (THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
u) (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$
                                         THFSl -> THFSl -> THFSl
joinSL (Quantifier -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic Quantifier
qf')
                                          ((THFVariable -> THFSl -> THFSl)
-> THFSl -> THFVariableList -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFVariable -> THFSl) -> THFVariable -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFVariable -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHF0 THFVariableList
vs)
 {- note: T0QF_THF_Quantified_Var in THF0 is pretty much the same as
 TQF_THF_Quantified_Formula in THF (cf. As.hs 190 ff.)
 Maybe we should merge the two constructors? -}
   T0QF_THF_Quantified_Novar qf' :: THFQuantifier
qf' u :: THFUnitaryFormula
u -> THFSl -> THFSl -> THFSl
joinSL (THFQuantifier -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFQuantifier
qf')
                                           (THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
u)
 -- fixme: not in THF?!?

instance MinSublogic THFSl THFUnaryConnective where
 minSublogic :: THFUnaryConnective -> THFSl
minSublogic uc :: THFUnaryConnective
uc = case THFUnaryConnective
uc of
   Negation -> THFSl
tHF0
   PiForAll -> THFSl
tHF
   SigmaExists -> THFSl
tHF

instance MinSublogic THFSl THFAtom where
 minSublogic :: THFAtom -> THFSl
minSublogic a :: THFAtom
a = case THFAtom
a of
   TA_Term _ -> THFSl
tHF
   TA_THF_Conn_Term conn :: THFConnTerm
conn ->
     case THFConnTerm
conn of
       TCT_THF_Pair_Connective pc :: THFPairConnective
pc -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFPairConnective -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFPairConnective
pc
       TCT_Assoc_Connective _ -> THFSl
tHF0
       TCT_THF_Unary_Connective uc :: THFUnaryConnective
uc -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFUnaryConnective -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnaryConnective
uc
       T0CT_THF_Quantifier qf :: THFQuantifier
qf -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFQuantifier -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFQuantifier
qf
   TA_Defined_Type df :: DefinedType
df -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic DefinedType
df
   TA_Defined_Plain_Formula _ -> THFSl
tHF
   TA_System_Type _ -> THFSl
tHF
   TA_System_Atomic_Formula _ -> THFSl
tHF
   T0A_Constant _ -> THFSl
tHF0
   T0A_Defined_Constant _ -> THFSl
tHF0
   T0A_System_Constant _ -> THFSl
tHF0
   T0A_Variable _ -> THFSl
tHF0
 -- fixme: how do these in THF0 differ from THF?

instance MinSublogic THFSl THFVariable where
 minSublogic :: THFVariable -> THFSl
minSublogic v :: THFVariable
v = case THFVariable
v of
   TV_THF_Typed_Variable _ t :: THFTopLevelType
t -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFTopLevelType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFTopLevelType
t
   _ -> THFSl
tHF0

instance MinSublogic THFSl THFQuantifier where
 minSublogic :: THFQuantifier -> THFSl
minSublogic qf :: THFQuantifier
qf = case THFQuantifier
qf of
  T0Q_PiForAll -> THFSl
tHF0
  T0Q_SigmaExists -> THFSl
tHF0
  _ -> THFSl
tHF

instance MinSublogic THFSl Quantifier where
 minSublogic :: Quantifier -> THFSl
minSublogic _ = THFSl
tHF0

instance MinSublogic THFSl THFTopLevelType where
 minSublogic :: THFTopLevelType -> THFSl
minSublogic tp :: THFTopLevelType
tp = case THFTopLevelType
tp of
   TTLT_THF_Logic_Formula f :: THFLogicFormula
f -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f
   -- fixme: maybe we need to check for ShortTypes extension?
   T0TLT_Constant _ -> THFSl
tHF0
   T0TLT_Variable _ -> THFSl
tHF0_P
   T0TLT_Defined_Type df :: DefinedType
df -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic DefinedType
df
   T0TLT_System_Type _ -> THFSl
tHF0
   T0TLT_THF_Binary_Type bt :: THFBinaryType
bt -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFBinaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryType
bt
 -- fixme: how do all these THF0 types differ from THF?

instance MinSublogic THFSl THFTypeableFormula where
 minSublogic :: THFTypeableFormula -> THFSl
minSublogic tf :: THFTypeableFormula
tf = case THFTypeableFormula
tf of
   TTyF_THF_Atom a :: THFAtom
a -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFAtom
a
   TTyF_THF_Tuple ts :: THFTuple
ts -> (THFLogicFormula -> THFSl -> THFSl) -> THFSl -> THFTuple -> THFSl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (THFSl -> THFSl -> THFSl
joinSL (THFSl -> THFSl -> THFSl)
-> (THFLogicFormula -> THFSl) -> THFLogicFormula -> THFSl -> THFSl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic) THFSl
tHFP THFTuple
ts
   TTyF_THF_Logic_Formula f :: THFLogicFormula
f -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFLogicFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFLogicFormula
f

instance MinSublogic THFSl DefinedType where
 minSublogic :: DefinedType -> THFSl
minSublogic df :: DefinedType
df = case DefinedType
df of
   DT_oType -> THFSl
tHF0
   DT_o -> THFSl
tHF0
   DT_iType -> THFSl
tHF0
   DT_i -> THFSl
tHF0
   DT_tType -> THFSl
tHF0
   DT_real -> THFSl
tHF
   DT_rat -> THFSl
tHF
   DT_int -> THFSl
tHF

instance MinSublogic THFSl THFUnitaryType where
 minSublogic :: THFUnitaryType -> THFSl
minSublogic ut :: THFUnitaryType
ut = case THFUnitaryType
ut of
   TUT_THF_Unitary_Formula f :: THFUnitaryFormula
f -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFUnitaryFormula
f
   T0UT_Constant _ -> THFSl
tHF0
   T0UT_Variable _ -> THFSl
tHF0
   T0UT_Defined_Type df :: DefinedType
df -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic DefinedType
df
   T0UT_System_Type _ -> THFSl
tHF0
   T0UT_THF_Binary_Type_Par bt :: THFBinaryType
bt -> THFSl -> THFSl -> THFSl
joinSL THFSl
tHF0 (THFSl -> THFSl) -> THFSl -> THFSl
forall a b. (a -> b) -> a -> b
$ THFBinaryType -> THFSl
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic THFBinaryType
bt
 -- fixme: how do all these THF0 types differ from THF?