{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./TPTP/Sublogic.hs
Description :  Data structures representing TPTP sublogics.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional

Data structures representing TPTP sublogics.
-}

module TPTP.Sublogic where

import TPTP.AS
import TPTP.Morphism
import TPTP.Sign

import Common.AS_Annotation (item)
import Common.DefaultMorphism

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

              --  | EPR -- Effectively Propositional CNF
data Sublogic = CNF -- Clausal Normal Form
              | FOF -- First Order Form
              --  | TCF
              | TFF -- Typed First Order Form
              --  | TFX
              | THF -- Typed Higher Order Form
              --  | TPI
                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, 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, 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, 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)
$cTHF :: Constr
$cTFF :: Constr
$cFOF :: Constr
$cCNF :: 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, Typeable)

{- ----------------------------------------------------------------------------
 - Special Sublogics
---------------------------------------------------------------------------- -}
top :: Sublogic
top :: Sublogic
top = Sublogic
THF

bottom :: Sublogic
bottom :: Sublogic
bottom = Sublogic
CNF


{- ----------------------------------------------------------------------------
 - Utility functions
---------------------------------------------------------------------------- -}
sublogicName :: Sublogic -> String
sublogicName :: Sublogic -> String
sublogicName = Sublogic -> String
forall a. Show a => a -> String
show

leastUpperBound :: Sublogic -> Sublogic -> Sublogic
leastUpperBound :: Sublogic -> Sublogic -> Sublogic
leastUpperBound = Sublogic -> Sublogic -> Sublogic
forall a. Ord a => a -> a -> a
max


{- ----------------------------------------------------------------------------
 - Determine sublogics
---------------------------------------------------------------------------- -}
sublogicOfUnit :: Sublogic -> () -> Sublogic
sublogicOfUnit :: Sublogic -> () -> Sublogic
sublogicOfUnit minimumSublogic :: Sublogic
minimumSublogic () = Sublogic
minimumSublogic

sublogicOfBaiscSpec :: Sublogic -> BASIC_SPEC -> Sublogic
sublogicOfBaiscSpec :: Sublogic -> BASIC_SPEC -> Sublogic
sublogicOfBaiscSpec minimumSublogic :: Sublogic
minimumSublogic basicSpec :: BASIC_SPEC
basicSpec = case BASIC_SPEC
basicSpec of
  Basic_spec annotedTPTPs :: [Annoted TPTP]
annotedTPTPs -> (Sublogic -> Sublogic -> Sublogic)
-> Sublogic -> [Sublogic] -> Sublogic
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
    (Annoted TPTP -> Sublogic) -> [Annoted TPTP] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map (TPTP -> Sublogic
sublogicOfTPTP (TPTP -> Sublogic)
-> (Annoted TPTP -> TPTP) -> Annoted TPTP -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted TPTP -> TPTP
forall a. Annoted a -> a
item) [Annoted TPTP]
annotedTPTPs
  where
    sublogicOfTPTP :: TPTP -> Sublogic
    sublogicOfTPTP :: TPTP -> Sublogic
sublogicOfTPTP tptp :: TPTP
tptp = case TPTP
tptp of
      TPTP tptp_inputs :: [TPTP_input]
tptp_inputs -> (Sublogic -> Sublogic -> Sublogic)
-> Sublogic -> [Sublogic] -> Sublogic
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic ([Sublogic] -> Sublogic) -> [Sublogic] -> Sublogic
forall a b. (a -> b) -> a -> b
$
        (TPTP_input -> Sublogic) -> [TPTP_input] -> [Sublogic]
forall a b. (a -> b) -> [a] -> [b]
map TPTP_input -> Sublogic
sublogicOfTPTPInput [TPTP_input]
tptp_inputs

    sublogicOfTPTPInput :: TPTP_input -> Sublogic
    sublogicOfTPTPInput :: TPTP_input -> Sublogic
sublogicOfTPTPInput tptp_input :: TPTP_input
tptp_input = case TPTP_input
tptp_input of
      Annotated_formula annotated_formula :: Annotated_formula
annotated_formula ->
        Sublogic -> Annotated_formula -> Sublogic
sublogicOfSentence Sublogic
minimumSublogic Annotated_formula
annotated_formula
      _ -> Sublogic
minimumSublogic

sublogicOfSentence :: Sublogic -> Sentence -> Sublogic
sublogicOfSentence :: Sublogic -> Annotated_formula -> Sublogic
sublogicOfSentence minimumSublogic :: Sublogic
minimumSublogic sentence :: Annotated_formula
sentence = case Annotated_formula
sentence of
  AF_THF_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
THF
  AF_TFX_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
THF
  AF_TFF_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
TFF
  AF_TCF_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
TFF
  AF_FOF_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
FOF
  AF_CNF_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
CNF
  AF_TPI_Annotated _ -> Sublogic -> Sublogic -> Sublogic
leastUpperBound Sublogic
minimumSublogic Sublogic
THF

sublogicOfSymbol :: Sublogic -> Symbol -> Sublogic
sublogicOfSymbol :: Sublogic -> Symbol -> Sublogic
sublogicOfSymbol minimumSublogic :: Sublogic
minimumSublogic _ = Sublogic
minimumSublogic

sublogicOfSign :: Sublogic -> Sign -> Sublogic
sublogicOfSign :: Sublogic -> Sign -> Sublogic
sublogicOfSign minimumSublogic :: Sublogic
minimumSublogic sign :: Sign
sign = case () of
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map THFTypeable THF_top_level_type -> Bool)
-> Map THFTypeable THF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfTypeConstantMap Sign
sign -> Sublogic
THF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map THFTypeable THF_top_level_type -> Bool)
-> Map THFTypeable THF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfTypeFunctorMap Sign
sign -> Sublogic
THF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map THFTypeable THF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map THFTypeable THF_top_level_type -> Bool)
-> Map THFTypeable THF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map THFTypeable THF_top_level_type
thfPredicateMap Sign
sign -> Sublogic
THF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map THF_atom THF_atom -> Bool
forall k a. Map k a -> Bool
Map.null (Map THF_atom THF_atom -> Bool) -> Map THF_atom THF_atom -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map THF_atom THF_atom
thfSubtypeMap Sign
sign -> Sublogic
THF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map Untyped_atom TFF_top_level_type -> Bool)
-> Map Untyped_atom TFF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeConstantMap Sign
sign -> Sublogic
TFF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map Untyped_atom TFF_top_level_type -> Bool)
-> Map Untyped_atom TFF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffTypeFunctorMap Sign
sign -> Sublogic
TFF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom TFF_top_level_type -> Bool
forall k a. Map k a -> Bool
Map.null (Map Untyped_atom TFF_top_level_type -> Bool)
-> Map Untyped_atom TFF_top_level_type -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom TFF_top_level_type
tffPredicateMap Sign
sign -> Sublogic
TFF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Untyped_atom Atom -> Bool
forall k a. Map k a -> Bool
Map.null (Map Untyped_atom Atom -> Bool) -> Map Untyped_atom Atom -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Untyped_atom Atom
tffSubtypeMap Sign
sign -> Sublogic
TFF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Number -> Bool
forall a. Set a -> Bool
Set.null (Set Number -> Bool) -> Set Number -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Number
numberSet Sign
sign -> Sublogic
TFF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Predicate (Set Int) -> Bool
forall k a. Map k a -> Bool
Map.null (Map Predicate (Set Int) -> Bool)
-> Map Predicate (Set Int) -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Predicate (Set Int)
fofPredicateMap Sign
sign -> Sublogic
FOF
  _ | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Predicate (Set Int) -> Bool
forall k a. Map k a -> Bool
Map.null (Map Predicate (Set Int) -> Bool)
-> Map Predicate (Set Int) -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Map Predicate (Set Int)
fofFunctorMap Sign
sign -> Sublogic
FOF
  _ -> Sublogic
minimumSublogic

sublogicOfMorphism :: Sublogic -> Morphism -> Sublogic
sublogicOfMorphism :: Sublogic -> Morphism -> Sublogic
sublogicOfMorphism minimumSublogic :: Sublogic
minimumSublogic morphism :: Morphism
morphism =
  Sublogic -> Sublogic -> Sublogic
leastUpperBound
    (Sublogic -> Sign -> Sublogic
sublogicOfSign Sublogic
minimumSublogic (Sign -> Sublogic) -> Sign -> Sublogic
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
domOfDefaultMorphism Morphism
morphism)
    (Sublogic -> Sign -> Sublogic
sublogicOfSign Sublogic
minimumSublogic (Sign -> Sublogic) -> Sign -> Sublogic
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
codOfDefaultMorphism Morphism
morphism)


{- ----------------------------------------------------------------------------
 - Determine projections
---------------------------------------------------------------------------- -}
-- TODO: complete the projections

projectSublogicBasicSpec :: Sublogic -> BASIC_SPEC -> BASIC_SPEC
projectSublogicBasicSpec :: Sublogic -> BASIC_SPEC -> BASIC_SPEC
projectSublogicBasicSpec _ basicSpec :: BASIC_SPEC
basicSpec = BASIC_SPEC
basicSpec

projectSublogicSign :: Sublogic -> Sign -> Sign
projectSublogicSign :: Sublogic -> Sign -> Sign
projectSublogicSign _ sign :: Sign
sign = Sign
sign

projectSublogicSentence :: Sublogic -> Sentence -> Sentence
projectSublogicSentence :: Sublogic -> Annotated_formula -> Annotated_formula
projectSublogicSentence _ sentence :: Annotated_formula
sentence = Annotated_formula
sentence

projectSublogicMorphism :: Sublogic -> Morphism -> Morphism
projectSublogicMorphism :: Sublogic -> Morphism -> Morphism
projectSublogicMorphism _ morphism :: Morphism
morphism = Morphism
morphism


projectSublogicMUnit :: Sublogic -> () -> Maybe ()
projectSublogicMUnit :: Sublogic -> () -> Maybe ()
projectSublogicMUnit _ = () -> Maybe ()
forall a. a -> Maybe a
Just

projectSublogicMSymbol :: Sublogic -> Symbol -> Maybe Symbol
projectSublogicMSymbol :: Sublogic -> Symbol -> Maybe Symbol
projectSublogicMSymbol _ symbol :: Symbol
symbol = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
symbol