{- |
Module      :  ./SoftFOL/CreateDFGDoc.hs
Description :  Generating DFG Doc out of SPASS theories.
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-protable(Logic)

Printing a (G_theory CASL _) into a DFG Doc.

-}

module SoftFOL.CreateDFGDoc (printTheoryAsSoftFOL) where

import Logic.Prover
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce

import Static.GTheory

import Common.AS_Annotation as AS_Anno
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.IRI (IRI)
import Common.ProofUtils
import Common.Result

import CASL.Logic_CASL
import CASL.Sublogic

import Comorphisms.CASL2SubCFOL
import Comorphisms.CASL2PCFOL
import Comorphisms.SuleCFOL2SoftFOL

import SoftFOL.Logic_SoftFOL
import SoftFOL.Conversions
import SoftFOL.Translate
import SoftFOL.Sign

import SoftFOL.PrintTPTP

spassConsTimeLimit :: Int
spassConsTimeLimit :: Int
spassConsTimeLimit = 500

printTheoryAsSoftFOL :: IRI
         -> Int -- ^ 0 = DFG, 1 = TPTP
         -> Bool
            {- ^ if True a conjecture false is added otherwise
                 its a theory without its own conjectures. -}
         -> G_theory -> IO (Maybe Doc)
printTheoryAsSoftFOL :: IRI -> Int -> Bool -> G_theory -> IO (Maybe Doc)
printTheoryAsSoftFOL sn :: IRI
sn lang :: Int
lang checkConsistency :: Bool
checkConsistency
  gth :: G_theory
gth@(G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _) _ thSens :: ThSens sentence (AnyComorphism, BasicProof)
thSens _) =
    IO (Maybe Doc)
-> ((Sign, [Named Sentence]) -> IO (Maybe Doc))
-> Maybe (Sign, [Named Sentence])
-> IO (Maybe Doc)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe Doc -> IO (Maybe Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Doc
forall a. Maybe a
Nothing)
          (\ (sign1 :: Sign
sign1, sens1 :: [Named Sentence]
sens1) ->
               do SPProblem
prob <- String -> SPLogicalPart -> Maybe (Named Sentence) -> IO SPProblem
genSoftFOLProblem
                              String
thName
                              (Sign -> [Named Sentence] -> SPLogicalPart
spLogicalPart Sign
sign1 [Named Sentence]
sens1)
                              (if Bool
checkConsistency
                               then Named Sentence -> Maybe (Named Sentence)
forall a. a -> Maybe a
Just Named Sentence
falseConj
                               else Maybe (Named Sentence)
forall a. Maybe a
Nothing)
                  Maybe Doc -> IO (Maybe Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Doc -> IO (Maybe Doc)) -> Maybe Doc -> IO (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ SPProblem -> Doc
printOut
                         SPProblem
prob {settings :: [SPSetting]
settings = [SPSettings :: SPSettingLabel -> [SPSettingBody] -> SPSetting
SPSettings
                                            {settingName :: SPSettingLabel
settingName = SPSettingLabel
SPASS,
                                             settingBody :: [SPSettingBody]
settingBody = [SPSettingBody]
flags}]})
                         -- (prob {settings = flags}))

      (Result (Sign, [Named Sentence]) -> Maybe (Sign, [Named Sentence])
forall a. Result a -> Maybe a
resultToMaybe (if G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_theory -> G_sublogics
sublogicOfTh G_theory
gth) (AnyComorphism -> Bool) -> AnyComorphism -> Bool
forall a b. (a -> b) -> a -> b
$
          GenSuleCFOL2SoftFOL PlainSoftFOL -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL
       then lid
-> CASL
-> String
-> (sign, [Named sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign
sign, [Named sentence]
sens)
              Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (Sign, [Named Sentence]))
-> Result (Sign, [Named Sentence])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenSuleCFOL2SoftFOL PlainSoftFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL
       else (if G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_theory -> G_sublogics
sublogicOfTh G_theory
gth) (AnyComorphism -> Bool) -> AnyComorphism -> Bool
forall a b. (a -> b) -> a -> b
$ InclComorphism CASL (CASL_SL ()) -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism InclComorphism CASL (CASL_SL ())
idCASL
        then lid
-> CASL
-> String
-> (sign, [Named sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign
sign, [Named sentence]
sens)
              Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (CASLSign, [Named CASLFORMULA]))
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= InclComorphism CASL (CASL_SL ())
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory InclComorphism CASL (CASL_SL ())
idCASL
              Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (CASLSign, [Named CASLFORMULA]))
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CASL2SubCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2SubCFOL
defaultCASL2SubCFOL
              Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (Sign, [Named Sentence]))
-> Result (Sign, [Named Sentence])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenSuleCFOL2SoftFOL PlainSoftFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL
        else if G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_theory -> G_sublogics
sublogicOfTh G_theory
gth) (AnyComorphism -> Bool) -> AnyComorphism -> Bool
forall a b. (a -> b) -> a -> b
$
                InclComorphism CASL (CASL_SL ()) -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism InclComorphism CASL (CASL_SL ())
idCASL_nosub
             then lid
-> CASL
-> String
-> (sign, [Named sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign
sign, [Named sentence]
sens)
                      Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (CASLSign, [Named CASLFORMULA]))
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= InclComorphism CASL (CASL_SL ())
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory InclComorphism CASL (CASL_SL ())
idCASL_nosub
                      Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (CASLSign, [Named CASLFORMULA]))
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CASL2PCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2PCFOL
CASL2PCFOL
                      Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (CASLSign, [Named CASLFORMULA]))
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CASL2SubCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2SubCFOL
defaultCASL2SubCFOL
                      Result (CASLSign, [Named CASLFORMULA])
-> ((CASLSign, [Named CASLFORMULA])
    -> Result (Sign, [Named Sentence]))
-> Result (Sign, [Named Sentence])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenSuleCFOL2SoftFOL PlainSoftFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory GenSuleCFOL2SoftFOL PlainSoftFOL
suleCFOL2SoftFOL
             else lid
-> SoftFOL
-> String
-> (sign, [Named sentence])
-> Result (Sign, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid SoftFOL
SoftFOL "" (sign
sign, [Named sentence]
sens))))
  where
        printOut :: SPProblem -> Doc
printOut = case Int
lang of
                     0 -> SPProblem -> Doc
forall a. Pretty a => a -> Doc
pretty
                     1 -> SPProblem -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP
                     _ -> SPProblem -> Doc
forall a. Pretty a => a -> Doc
pretty
        sens :: [Named sentence]
sens = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
thSens
        thName :: String
thName = IRI -> String
forall a. Show a => a -> String
show IRI
sn

        spLogicalPart :: Sign -> [Named Sentence] -> SPLogicalPart
spLogicalPart sig :: Sign
sig sen :: [Named Sentence]
sen =
                            (SPLogicalPart -> Named Sentence -> SPLogicalPart)
-> SPLogicalPart -> [Named Sentence] -> SPLogicalPart
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SPLogicalPart -> Named Sentence -> SPLogicalPart
insertSentence
                                  (Sign -> SPLogicalPart
signToSPLogicalPart Sign
sig)
                                  ([Named Sentence] -> [Named Sentence]
forall a. [a] -> [a]
reverse ([Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$
                                   (String -> String) -> [Named Sentence] -> [Named Sentence]
forall a. (String -> String) -> [Named a] -> [Named a]
prepareSenNames String -> String
transSenName [Named Sentence]
sen)

        flags :: [SPSettingBody]
flags = if Bool
checkConsistency
                then [String -> [String] -> SPSettingBody
SPFlag "set_flag" ["TimeLimit", Int -> String
forall a. Show a => a -> String
show Int
spassConsTimeLimit]
                     , String -> [String] -> SPSettingBody
SPFlag "set_flag" ["DocProof", "1"]]
                else []

        falseConj :: Named Sentence
falseConj = (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "inconsistent" Sentence
falseSen)
                    { isAxiom :: Bool
isAxiom = Bool
False }
        falseSen :: Sentence
falseSen = SPSymbol -> Sentence
simpTerm SPSymbol
SPFalse

        max_nosub_SPASS :: CASL_SL ()
max_nosub_SPASS = CASL_SL ()
forall a. Lattice a => CASL_SL a
caslTop { cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
emptyMapConsFeature }
        max_sub_SPASS :: CASL_SL ()
max_sub_SPASS = CASL_SL ()
forall a. Lattice a => CASL_SL a
caslTop { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub }
        idCASL :: InclComorphism CASL (CASL_SL ())
idCASL = CASL -> CASL_SL () -> InclComorphism CASL (CASL_SL ())
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism CASL
CASL CASL_SL ()
max_sub_SPASS
        idCASL_nosub :: InclComorphism CASL (CASL_SL ())
idCASL_nosub = CASL -> CASL_SL () -> InclComorphism CASL (CASL_SL ())
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism CASL
CASL CASL_SL ()
max_nosub_SPASS