ProveSatallax.hs revision 87d946b3c13ffd7f6391aa796e786c2b31b122b1
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederDescription : Interface to the Satallax theorem prover.
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : non-portable
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederSatallax theorem prover for THF0
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedermodule THF.ProveSatallax ( satallaxProver ) where
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport Data.List (stripPrefix)
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maederimport Data.Maybe (fromMaybe)
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederpfun :: ProverFuncs
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederpfun = ProverFuncs {
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder cfgTimeout = maybe 10 (+ 1) . timeLimit,
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder proverCommand = \ tout tmpFile _ ->
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder return ("time", ["satallax", "-t", show tout, tmpFile]),
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder getMessage = \ res' _ _ -> res',
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder [] -> Nothing
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder s -> let sp p str = case dropWhile p str of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder s' -> w : sp p s''
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder where (w, s'') = break p s'
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (m : secs : _) = sp (== 'm') s
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder in Just $ read m * 60 + read secs }
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedersatallaxProver :: ProverType
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedersatallaxProver = createSZSProver "Satallax"
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ("Satallax is an automated theorem prover for higher-order logic."
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ++ " The particular form of higher-order logic supported by Satallax"
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder ++ " is Church's simple type theory with extensionality and choice operators.")