{-# LANGUAGE CPP #-}
{- |
Module      :  ./Comorphisms/KnownProvers.hs
Description :  provides a map of provers to their most useful composed
  comorphisms
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

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

This module provides a map of provers to their most useful composed
comorphisms.
-}

module Comorphisms.KnownProvers
  ( KnownProversMap
  , KnownConsCheckersMap
  , defaultGUIProver
  , knownProversGUI
  , knownProversWithKind
  , shrinkKnownProvers
  , showKnownProvers
  , showAllKnownProvers
  , isaComorphisms
  ) where

import qualified Data.Map as Map

import System.Exit (exitFailure)

import Common.Result

import Logic.Logic (provers, AnyLogic (Logic), top_sublogic) -- hiding (top)
import Logic.Coerce ()
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Prover (proverName, hasProverKind, ProverKind (..))

import CASL.Logic_CASL
import CASL.Sublogic

import Comorphisms.QBF2Prop
import Comorphisms.Prop2QBF
import Comorphisms.Prop2CASL
import Comorphisms.CASL2SubCFOL
import Comorphisms.CASL2PCFOL
import Comorphisms.CASL2HasCASL
import Comorphisms.CFOL2IsabelleHOL
import Comorphisms.CommonLogic2IsabelleHOL
import Comorphisms.CSMOF2CASL
#ifdef CASLEXTENSIONS
import Comorphisms.CoCASL2CoPCFOL
import Comorphisms.CoCASL2CoSubCFOL
import Comorphisms.CoCFOL2IsabelleHOL
import Comorphisms.Modal2CASL
import Comorphisms.CASL_DL2CASL
import Comorphisms.Maude2CASL
import Comorphisms.CommonLogic2CASL
import CommonLogic.Sublogic (folsl)
import Comorphisms.Adl2CASL
import CspCASL.Comorphisms
-- hybrid
import Comorphisms.Hybrid2CASL
#endif
#ifndef NOOWLLOGIC
import OWL2.OWL22CASL
#endif
import Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
import Comorphisms.HasCASL2PCoClTyConsHOL
#ifdef PROGRAMATICA
import Comorphisms.Haskell2IsabelleHOLCF
#endif
import Comorphisms.SuleCFOL2TPTP
import Comorphisms.LogicList

type KnownProversMap = Map.Map String [AnyComorphism]
type KnownConsCheckersMap = Map.Map String [AnyComorphism]

-- | the default prover selected in the GUI
defaultGUIProver :: String
defaultGUIProver :: String
defaultGUIProver = "SPASS"

-- | a map of known prover names implemanting a GUI interface
knownProversGUI :: Result KnownProversMap
knownProversGUI :: Result KnownProversMap
knownProversGUI = ProverKind -> Result KnownProversMap
knownProversWithKind ProverKind
ProveGUI

idComorphisms :: [AnyComorphism]
idComorphisms :: [AnyComorphism]
idComorphisms = (AnyLogic -> AnyComorphism) -> [AnyLogic] -> [AnyComorphism]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Logic lid :: lid
lid) ->
   InclComorphism lid sublogics -> 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 lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> InclComorphism lid sublogics
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 lid
lid (sublogics -> InclComorphism lid sublogics)
-> sublogics -> InclComorphism lid sublogics
forall a b. (a -> b) -> a -> b
$ lid -> sublogics
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
top_sublogic lid
lid) [AnyLogic]
logicList

{- | a map of known prover names for a specific prover kind
to a list of simple (composed) comorphisms -}
knownProversWithKind :: ProverKind -> Result KnownProversMap
knownProversWithKind :: ProverKind -> Result KnownProversMap
knownProversWithKind pk :: ProverKind
pk =
    do [AnyComorphism]
isaCs <- Result [AnyComorphism]
isaComorphisms
       [AnyComorphism]
spassCs <- Result [AnyComorphism]
spassComorphisms
       [AnyComorphism]
qCs <- Result [AnyComorphism]
quickCheckComorphisms
       KnownProversMap -> Result KnownProversMap
forall (m :: * -> *) a. Monad m => a -> m a
return (KnownProversMap -> Result KnownProversMap)
-> KnownProversMap -> Result KnownProversMap
forall a b. (a -> b) -> a -> b
$ (KnownProversMap -> AnyComorphism -> KnownProversMap)
-> KnownProversMap -> [AnyComorphism] -> KnownProversMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl KnownProversMap -> AnyComorphism -> KnownProversMap
insProvers KnownProversMap
forall k a. Map k a
Map.empty
         ([AnyComorphism] -> KnownProversMap)
-> [AnyComorphism] -> KnownProversMap
forall a b. (a -> b) -> a -> b
$ [AnyComorphism]
idComorphisms [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
++ [AnyComorphism]
isaCs [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
++ [AnyComorphism]
spassCs [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
++ [AnyComorphism]
qCs
#ifdef CASLEXTENSIONS
              [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
++ [CspCASL2CspCASL () Trace -> 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 CspCASL2CspCASL () Trace
cspCASLTrace]
#endif
       where insProvers :: KnownProversMap -> AnyComorphism -> KnownProversMap
insProvers kpm :: KnownProversMap
kpm cm :: AnyComorphism
cm =
              case AnyComorphism
cm of
                Comorphism cid :: cid
cid ->
                 let prs :: [Prover sign2 sentence2 morphism2 sublogics2 proof_tree2]
prs = lid2 -> [Prover sign2 sentence2 morphism2 sublogics2 proof_tree2]
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 -> [Prover sign sentence morphism sublogics proof_tree]
provers (cid -> lid2
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 -> lid2
targetLogic cid
cid)
                 in (KnownProversMap
 -> Prover sign2 sentence2 morphism2 sublogics2 proof_tree2
 -> KnownProversMap)
-> KnownProversMap
-> [Prover sign2 sentence2 morphism2 sublogics2 proof_tree2]
-> KnownProversMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: KnownProversMap
m p :: Prover sign2 sentence2 morphism2 sublogics2 proof_tree2
p -> if ProverKind
-> Prover sign2 sentence2 morphism2 sublogics2 proof_tree2 -> Bool
forall x s m y z. ProverKind -> ProverTemplate x s m y z -> Bool
hasProverKind ProverKind
pk Prover sign2 sentence2 morphism2 sublogics2 proof_tree2
p
                                    then ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> String -> [AnyComorphism] -> KnownProversMap -> KnownProversMap
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++))
                                          (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2 -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover sign2 sentence2 morphism2 sublogics2 proof_tree2
p) [AnyComorphism
cm] KnownProversMap
m
                                    else KnownProversMap
m) KnownProversMap
kpm [Prover sign2 sentence2 morphism2 sublogics2 proof_tree2]
prs

shrinkKnownProvers :: G_sublogics -> KnownProversMap -> KnownProversMap
shrinkKnownProvers :: G_sublogics -> KnownProversMap -> KnownProversMap
shrinkKnownProvers sub :: G_sublogics
sub = ([AnyComorphism] -> Bool) -> KnownProversMap -> KnownProversMap
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool)
-> ([AnyComorphism] -> Bool) -> [AnyComorphism] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyComorphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (KnownProversMap -> KnownProversMap)
-> (KnownProversMap -> KnownProversMap)
-> KnownProversMap
-> KnownProversMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         ([AnyComorphism] -> [AnyComorphism])
-> KnownProversMap -> KnownProversMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism])
-> (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ G_sublogics -> AnyComorphism -> Bool
lessSublogicComor G_sublogics
sub)

isaComorphisms :: Result [AnyComorphism]
isaComorphisms :: Result [AnyComorphism]
isaComorphisms = do
       -- CASL
       AnyComorphism
subpc2IHOLviaHasCASL <-
           AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL2PCFOL -> 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 CASL2PCFOL
CASL2PCFOL) (CASL2HasCASL -> 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 CASL2HasCASL
CASL2HasCASL)
           Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ( \ x :: AnyComorphism
x -> AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
x
                 (AnyComorphism -> Result AnyComorphism)
-> AnyComorphism -> Result AnyComorphism
forall a b. (a -> b) -> a -> b
$ PCoClTyConsHOL2PairsInIsaHOL -> 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 PCoClTyConsHOL2PairsInIsaHOL
PCoClTyConsHOL2PairsInIsaHOL)
       AnyComorphism
subpc2IHOL <-
           AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL2PCFOL -> 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 CASL2PCFOL
CASL2PCFOL)
               (CASL2SubCFOL -> 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 CASL2SubCFOL
defaultCASL2SubCFOL)
           Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ( \ x :: AnyComorphism
x -> AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
x (AnyComorphism -> Result AnyComorphism)
-> AnyComorphism -> Result AnyComorphism
forall a b. (a -> b) -> a -> b
$ CFOL2IsabelleHOL -> 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 CFOL2IsabelleHOL
CFOL2IsabelleHOL)
       -- HasCASL
       AnyComorphism
subHasCASL <-
           AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (HasCASL2PCoClTyConsHOL -> 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 HasCASL2PCoClTyConsHOL
HasCASL2PCoClTyConsHOL)
                          (AnyComorphism -> Result AnyComorphism)
-> AnyComorphism -> Result AnyComorphism
forall a b. (a -> b) -> a -> b
$ PCoClTyConsHOL2PairsInIsaHOL -> 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 PCoClTyConsHOL2PairsInIsaHOL
PCoClTyConsHOL2PairsInIsaHOL
#ifdef CASLEXTENSIONS
       -- CoCASL
       AnyComorphism
casl_dl2CASL <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL_DL2CASL -> 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 CASL_DL2CASL
CASL_DL2CASL) AnyComorphism
subpc2IHOL
       AnyComorphism
co2IHOL <-
           AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CoCASL2CoPCFOL -> 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 CoCASL2CoPCFOL
CoCASL2CoPCFOL)
                              (CoCASL2CoSubCFOL -> 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 CoCASL2CoSubCFOL
CoCASL2CoSubCFOL)
            Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\ x :: AnyComorphism
x -> AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
x (CoCFOL2IsabelleHOL -> 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 CoCFOL2IsabelleHOL
CoCFOL2IsabelleHOL))
       -- ModalCASL
       AnyComorphism
mod2IHOL <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Modal2CASL -> 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 Modal2CASL
Modal2CASL) AnyComorphism
subpc2IHOL
       AnyComorphism
maude2IHOL <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Maude2CASL -> 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 Maude2CASL
Maude2CASL) AnyComorphism
subpc2IHOL
       AnyComorphism
commonlogic2IHOL <-
           AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CL2CFOL -> 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 (CL2CFOL -> AnyComorphism) -> CL2CFOL -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ CommonLogicSL -> CL2CFOL
CL2CFOL CommonLogicSL
folsl) AnyComorphism
subpc2IHOL
#endif
#ifndef NOOWLLOGIC
       AnyComorphism
owl2HOL <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (OWL22CASL -> 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 OWL22CASL
OWL22CASL) AnyComorphism
subpc2IHOL
#endif
       -- Propositional
       AnyComorphism
prop2IHOL <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Prop2CASL -> 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 Prop2CASL
Prop2CASL) AnyComorphism
subpc2IHOL
       [AnyComorphism] -> Result [AnyComorphism]
forall (m :: * -> *) a. Monad m => a -> m a
return
         [ CFOL2IsabelleHOL -> 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 CFOL2IsabelleHOL
CFOL2IsabelleHOL
         , CommonLogic2IsabelleHOL -> 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 CommonLogic2IsabelleHOL
CommonLogic2IsabelleHOL
         , QBF2Prop -> 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 QBF2Prop
QBF2Prop
         , Prop2QBF -> 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 Prop2QBF
Prop2QBF
         , AnyComorphism
subpc2IHOLviaHasCASL
         , AnyComorphism
subpc2IHOL
#ifdef CASLEXTENSIONS
         , AnyComorphism
co2IHOL
         , AnyComorphism
mod2IHOL
         , AnyComorphism
maude2IHOL
         , AnyComorphism
casl_dl2CASL
         , AnyComorphism
commonlogic2IHOL
#endif
#ifdef PROGRAMATICA
         , Comorphism Haskell2IsabelleHOLCF
#endif
#ifndef NOOWLLOGIC
         , AnyComorphism
owl2HOL
#endif
         , AnyComorphism
subHasCASL
         , PCoClTyConsHOL2PairsInIsaHOL -> 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 PCoClTyConsHOL2PairsInIsaHOL
PCoClTyConsHOL2PairsInIsaHOL
         , AnyComorphism
prop2IHOL ]

spassComorphisms :: Result [AnyComorphism]
spassComorphisms :: Result [AnyComorphism]
spassComorphisms =
    do let 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 ()
max_nosub_SPASS { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub }
           idCASL_sub :: AnyComorphism
idCASL_sub = 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 (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 :: AnyComorphism
idCASL_nosub = 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 (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)
           compSPASS :: AnyComorphism -> m AnyComorphism
compSPASS x :: AnyComorphism
x = AnyComorphism -> AnyComorphism -> m AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
x (GenSuleCFOL2TPTP -> 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 GenSuleCFOL2TPTP
suleCFOL2TPTP) 
                         -- use translation to TPTP instead of one to SoftFOL
       AnyComorphism
partOut <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
idCASL_sub (CASL2SubCFOL -> 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 CASL2SubCFOL
defaultCASL2SubCFOL)
                   Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> m AnyComorphism
compSPASS
       AnyComorphism
partSubOut <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL2PCFOL -> 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 CASL2PCFOL
CASL2PCFOL)
                                     (CASL2SubCFOL -> 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 CASL2SubCFOL
defaultCASL2SubCFOL)
                      Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
idCASL_nosub
                      Result AnyComorphism
-> (AnyComorphism -> Result AnyComorphism) -> Result AnyComorphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> m AnyComorphism
compSPASS
       AnyComorphism
csmof2casl <- AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> m AnyComorphism
compSPASS (CSMOF2CASL -> 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 CSMOF2CASL
CSMOF2CASL)
#ifdef CASLEXTENSIONS
-- hybrid
       AnyComorphism
hybr2SPASS <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Hybrid2CASL -> 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 Hybrid2CASL
Hybrid2CASL) AnyComorphism
partOut
       AnyComorphism
prop2SPASS <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Prop2CASL -> 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 Prop2CASL
Prop2CASL) AnyComorphism
partOut
       AnyComorphism
casl_dl2SPASS <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL_DL2CASL -> 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 CASL_DL2CASL
CASL_DL2CASL) AnyComorphism
partOut
       AnyComorphism
maude2SPASS <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Maude2CASL -> 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 Maude2CASL
Maude2CASL) AnyComorphism
partOut
       AnyComorphism
commonlogic2SPASS <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CL2CFOL -> 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 (CL2CFOL -> AnyComorphism) -> CL2CFOL -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ CommonLogicSL -> CL2CFOL
CL2CFOL CommonLogicSL
folsl)
         AnyComorphism
partOut
       AnyComorphism
adl2SPASS <- AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> m AnyComorphism
compSPASS (Adl2CASL -> 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 Adl2CASL
Adl2CASL)
#endif
#ifndef NOOWLLOGIC
       AnyComorphism
owl2spass <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (OWL22CASL -> 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 OWL22CASL
OWL22CASL) AnyComorphism
partOut
#endif
       {- Fixme: constraint empty mapping is not available after Modal2CASL
       mod2SPASS <- compComorphism (Comorphism Modal2CASL) partSubOut
       CommonLogic -}
       [AnyComorphism] -> Result [AnyComorphism]
forall (m :: * -> *) a. Monad m => a -> m a
return
         [ GenSuleCFOL2TPTP -> 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 GenSuleCFOL2TPTP
suleCFOL2TPTP
         , AnyComorphism
partOut
         , AnyComorphism
partSubOut
#ifdef CASLEXTENSIONS
         , AnyComorphism
prop2SPASS
         , AnyComorphism
casl_dl2SPASS
         , AnyComorphism
maude2SPASS
         , AnyComorphism
commonlogic2SPASS
         , AnyComorphism
csmof2casl
         , AnyComorphism
adl2SPASS
-- hybrid
         , AnyComorphism
hybr2SPASS
#endif
#ifndef NOOWLLOGIC
         , AnyComorphism
owl2spass
#endif
         ]

quickCheckComorphisms :: Result [AnyComorphism]
quickCheckComorphisms :: Result [AnyComorphism]
quickCheckComorphisms = do
   AnyComorphism
c <- AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (CASL2PCFOL -> 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 CASL2PCFOL
CASL2PCFOL)
                       (CASL2SubCFOL -> 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 CASL2SubCFOL
defaultCASL2SubCFOL)
   [AnyComorphism] -> Result [AnyComorphism]
forall (m :: * -> *) a. Monad m => a -> m a
return [AnyComorphism
c, 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 ()) -> AnyComorphism)
-> InclComorphism CASL (CASL_SL ()) -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ 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 ()
forall a. Lattice a => CASL_SL a
top {has_part :: Bool
has_part = Bool
False})]

showAllKnownProvers :: IO ()
showAllKnownProvers :: IO ()
showAllKnownProvers =
    do let Result ds :: [Diagnosis]
ds mkpMap :: Maybe KnownProversMap
mkpMap = Result KnownProversMap
knownProversGUI
       String -> IO ()
putStrLn "Diagnoses:"
       String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
forall a. Show a => a -> String
show [Diagnosis]
ds
       IO ()
-> (KnownProversMap -> IO ()) -> Maybe KnownProversMap -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. IO a
exitFailure KnownProversMap -> IO ()
showKnownProvers Maybe KnownProversMap
mkpMap

showKnownProvers :: KnownProversMap -> IO ()
showKnownProvers :: KnownProversMap -> IO ()
showKnownProvers km :: KnownProversMap
km =
    do String -> IO ()
putStrLn "-----------\nKnownProvers:"
       String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, [AnyComorphism]) -> String)
-> [(String, [AnyComorphism])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, [AnyComorphism]) -> String
forall (t :: * -> *) a.
(Foldable t, Show a) =>
(String, t a) -> String
form ([(String, [AnyComorphism])] -> [String])
-> [(String, [AnyComorphism])] -> [String]
forall a b. (a -> b) -> a -> b
$ KnownProversMap -> [(String, [AnyComorphism])]
forall k a. Map k a -> [(k, a)]
Map.toList KnownProversMap
km
    where form :: (String, t a) -> String
form (name :: String
name, cl :: t a
cl) =
              String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a -> String) -> t a -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (("\n       " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show) t a
cl