KnownProvers.hs revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner{-# LANGUAGE CPP #-}
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederModule : $Header$
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerDescription : provides a map of provers to their most useful composed
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerCopyright : (c) Klaus Luettich, Uni Bremen 2005
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerPortability : non-portable(Logic)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerThis module provides a map of provers to their most useful composed
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner ( KnownProversMap
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , KnownConsCheckersMap
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , defaultGUIProver
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , knownProversGUI
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , knownProversWithKind
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , shrinkKnownProvers
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , showKnownProvers
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , showAllKnownProvers
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , isaComorphisms
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerimport qualified Data.Map as Map
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerimport System.Exit (exitFailure)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerimport Logic.Logic (provers, AnyLogic (Logic), top_sublogic) -- hiding (top)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerimport Logic.Prover (proverName, hasProverKind, ProverKind (..))
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder#ifdef CASLEXTENSIONS
ce5b44277ea06257548ff625e928cb1290c6d297cmaeder#ifndef NOOWLLOGIC
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Comorphisms.HasCASL2PCoClTyConsHOL
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder#ifdef PROGRAMATICA
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederimport Comorphisms.Haskell2IsabelleHOLCF
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroedertype KnownProversMap = Map.Map String [AnyComorphism]
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroedertype KnownConsCheckersMap = Map.Map String [AnyComorphism]
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- | the default prover selected in the GUI
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian MaederdefaultGUIProver :: String
3dde4051c307b609159a097f08a05108fdd036efJonathan von SchroederdefaultGUIProver = "SPASS"
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder-- | a map of known prover names implemanting a GUI interface
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederknownProversGUI :: Result KnownProversMap
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederknownProversGUI = knownProversWithKind ProveGUI
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederidComorphisms :: [AnyComorphism]
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederidComorphisms = map (\ (Logic lid) ->
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder Comorphism $ mkIdComorphism lid $ top_sublogic lid) logicList
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder{- | a map of known prover names for a specific prover kind
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maederto a list of simple (composed) comorphisms -}
d62661e54e2662d53b583ae48609f5037701078dcmaederknownProversWithKind :: ProverKind -> Result KnownProversMap
8cacad2a09782249243b80985f28e9387019fe40Christian MaederknownProversWithKind pk =
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maeder do isaCs <- isaComorphisms
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder spassCs <- spassComorphisms
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder qCs <- quickCheckComorphisms
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder return $ foldl insProvers Map.empty
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich $ idComorphisms ++ isaCs ++ spassCs ++ qCs
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder#ifdef CASLEXTENSIONS
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder ++ [Comorphism cspCASLTrace]
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder where insProvers kpm cm =
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder Comorphism cid ->
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder let prs = provers (targetLogic cid)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder in foldl (\ m p -> if hasProverKind pk p
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder then Map.insertWith (flip (++))
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder (proverName p) [cm] m
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder else m) kpm prs
961087225d1d2b9534152a346d1a3755ed952fcdJens ElknershrinkKnownProvers :: G_sublogics -> KnownProversMap -> KnownProversMap
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknershrinkKnownProvers sub = Map.filter (not . null) .
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner Map.map (filter $ lessSublogicComor sub)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederisaComorphisms :: Result [AnyComorphism]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederisaComorphisms = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder subpc2IHOLviaHasCASL <-
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder compComorphism (Comorphism CASL2PCFOL) (Comorphism CASL2HasCASL)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner >>= ( \ x -> compComorphism x
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner $ Comorphism PCoClTyConsHOL2PairsInIsaHOL)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder subpc2IHOL <-
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder compComorphism (Comorphism CASL2PCFOL)
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder (Comorphism defaultCASL2SubCFOL)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder >>= ( \ x -> compComorphism x $ Comorphism CFOL2IsabelleHOL)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder subHasCASL <-
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder compComorphism (Comorphism HasCASL2PCoClTyConsHOL)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder $ Comorphism PCoClTyConsHOL2PairsInIsaHOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder#ifdef CASLEXTENSIONS
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder casl_dl2CASL <- compComorphism (Comorphism CASL_DL2CASL) subpc2IHOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder compComorphism (Comorphism CoCASL2CoPCFOL)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Comorphism CoCASL2CoSubCFOL)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder >>= (\ x -> compComorphism x (Comorphism CoCFOL2IsabelleHOL))
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mod2IHOL <- compComorphism (Comorphism Modal2CASL) subpc2IHOL
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder maude2IHOL <- compComorphism (Comorphism Maude2CASL) subpc2IHOL
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder commonlogic2IHOL <-
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder compComorphism (Comorphism $ CL2CFOL folsl) subpc2IHOL
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner#ifndef NOOWLLOGIC
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder owl2HOL <- compComorphism (Comorphism OWL22CASL) subpc2IHOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Propositional
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder prop2IHOL <- compComorphism (Comorphism Prop2CASL) subpc2IHOL
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner -- CommonLogic
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [ Comorphism CFOL2IsabelleHOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism CommonLogic2IsabelleHOL
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , Comorphism QBF2Prop
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Comorphism Prop2QBF
8037b7d21021a94b69e4a092f5c98e491333d939cmaeder , subpc2IHOLviaHasCASL
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner , subpc2IHOL
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder#ifdef CASLEXTENSIONS
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , casl_dl2CASL
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder , commonlogic2IHOL
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder#ifdef PROGRAMATICA
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner , Comorphism Haskell2IsabelleHOLCF
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner#ifndef NOOWLLOGIC
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , Comorphism PCoClTyConsHOL2PairsInIsaHOL
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder , prop2IHOL ]
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian MaederspassComorphisms :: Result [AnyComorphism]
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian MaederspassComorphisms =
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder do let max_nosub_SPASS =
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder caslTop {cons_features = emptyMapConsFeature}
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett max_sub_SPASS = max_nosub_SPASS { sub_features = LocFilSub }
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder idCASL_sub = Comorphism (mkIdComorphism CASL max_sub_SPASS)
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder idCASL_nosub = Comorphism (mkIdComorphism CASL max_nosub_SPASS)
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder compSPASS x = compComorphism x (Comorphism suleCFOL2SoftFOL)
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder partOut <- compComorphism idCASL_sub (Comorphism defaultCASL2SubCFOL)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers >>= compSPASS
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder partSubOut <- compComorphism (Comorphism CASL2PCFOL)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder (Comorphism defaultCASL2SubCFOL)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder >>= compComorphism idCASL_nosub
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder >>= compSPASS
140287998aa8592c9c403bd9e308e447ba92ae11Christian Maeder#ifdef CASLEXTENSIONS
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder hybr2SPASS <- compComorphism (Comorphism Hybrid2CASL) partOut
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder prop2SPASS <- compComorphism (Comorphism Prop2CASL) partOut
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder casl_dl2SPASS <- compComorphism (Comorphism CASL_DL2CASL) partOut
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers maude2SPASS <- compComorphism (Comorphism Maude2CASL) partOut
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder commonlogic2SPASS <- compComorphism (Comorphism $ CL2CFOL folsl)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder adl2SPASS <- compSPASS (Comorphism Adl2CASL)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder#ifndef NOOWLLOGIC
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder owl2spass <- compComorphism (Comorphism OWL22CASL) partOut
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder {- Fixme: constraint empty mapping is not available after Modal2CASL
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder mod2SPASS <- compComorphism (Comorphism Modal2CASL) partSubOut
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder CommonLogic -}
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder [ Comorphism suleCFOL2SoftFOL
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder#ifdef CASLEXTENSIONS
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , casl_dl2SPASS
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , maude2SPASS
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder , commonlogic2SPASS
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder#ifndef NOOWLLOGIC
54ea981a0503c396c2923a1c06421c6235baf27fChristian MaederquickCheckComorphisms :: Result [AnyComorphism]
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian MaederquickCheckComorphisms = do
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder c <- compComorphism (Comorphism CASL2PCFOL)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (Comorphism defaultCASL2SubCFOL)
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder return [c, Comorphism $ mkIdComorphism CASL
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder (top {has_part = False})]
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaedershowAllKnownProvers :: IO ()
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaedershowAllKnownProvers =
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder do let Result ds mkpMap = knownProversGUI
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder putStrLn "Diagnoses:"
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder putStrLn $ unlines $ map show ds
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder maybe exitFailure showKnownProvers mkpMap
254df6f22d01eacf7c57b85729e0445747b630d9Christian MaedershowKnownProvers :: KnownProversMap -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedershowKnownProvers km =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do putStrLn "-----------\nKnownProvers:"
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder putStrLn $ unlines $ map form $ Map.toList km
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder where form (name, cl) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder name ++ concatMap (("\n " ++) . show) cl