0N/ADescription : provides a map of provers to their most useful composed
0N/ACopyright : (c) Klaus L�ttich, Uni Bremen 2005
0N/AMaintainer : luecke@informatik.uni-bremen.de
0N/AStability : provisional
0N/APortability : non-portable(Logic)
0N/AThis module provides a map of provers to their most useful composed
0N/A KnownConsCheckersMap,
0N/A knownProversWithKind,
0N/A showAllKnownProvers) where
import
Logic.Prover (prover_name,hasProverKind,ProverKind(..))
type KnownProversMap =
Map.Map String [AnyComorphism]
type KnownConsCheckersMap =
Map.Map String [AnyComorphism]
-- | the default prover selected in the GUI
defaultGUIProver :: String
defaultGUIProver = "SPASS"
-- | a map of known prover names implemanting a GUI interface
knownProversGUI :: Result KnownProversMap
knownProversGUI = knownProversWithKind ProveGUI
-- | a map of known prover names for a specific prover kind
-- to a list of simple (composed) comorphisms
knownProversWithKind :: ProverKind -> Result KnownProversMap
knownProversWithKind pk =
do isaCs <- isaComorphisms
spassCs <- spassComorphisms
zchaffCS <- zchaffComorphisms
qCs <- quickCheckComorphisms
pelletCS <- pelletComorphisms
isaCs ++ spassCs ++ zchaffCS ++ qCs ++ pelletCS
where insProvers kpm cm =
let prs = provers (targetLogic cid)
in foldl (\ m p -> if hasProverKind pk p
shrinkKnownProvers :: G_sublogics -> KnownProversMap -> KnownProversMap
shrinkKnownProvers sub =
Map.filter (not . null) .
Map.map (filter $ lessSublogicComor sub)
isaComorphisms :: Result [AnyComorphism]
compComorphism (Comorphism CASL2PCFOL) (Comorphism CASL2HasCASL)
>>= ( \ x -> compComorphism x
$ Comorphism PCoClTyConsHOL2PairsInIsaHOL)
compComorphism (Comorphism CASL2PCFOL)
(Comorphism defaultCASL2SubCFOL)
>>= ( \ x -> compComorphism x $ Comorphism CFOL2IsabelleHOL)
compComorphism (Comorphism HasCASL2PCoClTyConsHOL)
$ Comorphism PCoClTyConsHOL2PairsInIsaHOL
casl_dl2CASL <- compComorphism (Comorphism CASL_DL2CASL) subpc2IHOL
compComorphism (Comorphism CoCASL2CoPCFOL)
(Comorphism CoCASL2CoSubCFOL)
>>= (\ x -> compComorphism x (Comorphism CoCFOL2IsabelleHOL))
mod2IHOL <- compComorphism (Comorphism Modal2CASL) subpc2IHOL
prop2IHOL <- compComorphism (Comorphism Prop2CASL) subpc2IHOL
return [Comorphism (mkIdComorphism Isabelle ()),
Comorphism CFOL2IsabelleHOL, subpc2IHOLviaHasCASL, subpc2IHOL,
co2IHOL, mod2IHOL,casl_dl2CASL,
Comorphism Haskell2IsabelleHOLCF,
subHasCASL, Comorphism PCoClTyConsHOL2PairsInIsaHOL,
spassComorphisms :: Result [AnyComorphism]
caslTop {cons_features = emptyMapConsFeature}
max_sub_SPASS = max_nosub_SPASS { sub_features = LocFilSub }
idCASL_sub = Comorphism (mkIdComorphism CASL max_sub_SPASS)
idCASL_nosub = Comorphism (mkIdComorphism CASL max_nosub_SPASS)
compSPASS x = compComorphism x (Comorphism SuleCFOL2SoftFOL)
partOut <- (compComorphism idCASL_sub (Comorphism defaultCASL2SubCFOL)
partSubOut <- (compComorphism (Comorphism CASL2PCFOL)
(Comorphism defaultCASL2SubCFOL)
>>= (compComorphism idCASL_nosub)
prop2SPASS <- compComorphism (Comorphism Prop2CASL) partOut
casl_dl2SPASS <- compComorphism (Comorphism CASL_DL2CASL) partOut
-- Fixme: constraint empty mapping is not available after Modal2CASL
-- mod2SPASS <- compComorphism (Comorphism Modal2CASL) partSubOut
return [Comorphism (mkIdComorphism SoftFOL ()),
Comorphism SuleCFOL2SoftFOL,partOut,partSubOut
,prop2SPASS,casl_dl2SPASS
zchaffComorphisms :: Result [AnyComorphism]
zchaffComorphisms = return
pelletComorphisms :: Result [AnyComorphism]
pelletComorphisms = return
Comorphism (mkIdComorphism OWL11 ())
quickCheckComorphisms :: Result [AnyComorphism]
quickCheckComorphisms = do
c <- compComorphism (Comorphism CASL2PCFOL)
(Comorphism defaultCASL2SubCFOL)
return [c, Comorphism $ mkIdComorphism CASL
(top {has_part = False})]
showAllKnownProvers :: IO ()
do let Result ds mkpMap = knownProversGUI
putStrLn $ unlines $ map show ds
maybe exitFailure showKnownProvers mkpMap
showKnownProvers :: KnownProversMap -> IO ()
do putStrLn "-----------\nKnownProvers:"
name ++ concatMap (\c -> "\n "++show c) cl