Provers.hs revision b78522b8f7a01953b0eda02cbc89b3984033676b
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{-# LANGUAGE CPP, TypeFamilies, DeriveDataTypeable #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski ( formatProvers
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport PGIP.Query (ProverMode (..))
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport Logic.Comorphism (AnyComorphism)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Json (ppJson, asJson)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Text.XML.Light (ppTopElement)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maedertype ProversFormatter = ProverMode ->
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder [(AnyComorphism, [String])] -> (String, String)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian MaederformatProvers :: Maybe String -> ProversFormatter
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian MaederformatProvers format proverMode availableProvers = case format of
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder Just "json" -> formatAsJSON
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder _ -> formatAsXML
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder computedProvers :: Provers
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder computedProvers =
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder let proverNames = showProversOnly availableProvers in
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder case proverMode of
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder GlProofs -> emptyProvers { provers = Just proverNames }
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder GlConsistency -> emptyProvers { consistencyCheckers = Just proverNames }
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder formatAsJSON :: (String, String)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder formatAsJSON = (jsonC, ppJson $ asJson computedProvers)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder formatAsXML :: (String, String)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder formatAsXML = (xmlC, ppTopElement $ asXml computedProvers)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederdata Provers = Provers
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder { provers :: Maybe [String]
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder , consistencyCheckers :: Maybe [String]
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder } deriving (Show, Typeable, Data)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian MaederemptyProvers :: Provers
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederemptyProvers = Provers { provers = Nothing, consistencyCheckers = Nothing }