1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederModule : $Header$

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederDescription : Interface for the SPASS theorem prover.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Rene Wagner, Klaus Luettich, Rainer Grabbe,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Uni Bremen 2005-2006

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : rainer25@informatik.uni-bremen.de

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederPortability : needs POSIX

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederInterface for the SPASS theorem prover, uses GUI.GenericATP.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederSee <http://spass.mpi-sb.mpg.de/> for details on SPASS.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{-

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder - check if the theorem is used in the proof;

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder if not, the theory is inconsistent;

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder mark goal as proved and emmit a warning...

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder - Implement a consistency checker based on GUI

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule SoftFOL.ProveSPASS (spassProver,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder spassProveGUI,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder spassProveCMDLautomatic,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder spassProveCMDLautomaticBatch) where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport Logic.Prover

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport SoftFOL.Sign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport SoftFOL.Translate

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport SoftFOL.ProverState

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport ChildProcess as CP

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport ProcessClasses

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HTk

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport GUI.GenericATP

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport GUI.GenericATPState

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport Proofs.BatchProcessing

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport qualified Common.AS_Annotation as AS_Anno

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport qualified Common.Result as Result

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport Common.ProofTree

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Utils (splitOn)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Control.Concurrent as Concurrent

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Control.Exception as Exception

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport System.Exit

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Text.Regex

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport Data.List

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport Data.Maybe

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederimport Data.Time (TimeOfDay(..),midnight -- only in ghc-6.6.1: ,parseTime

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder )

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- * Prover implementation

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder The Prover implementation.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Implemented are: a prover GUI, and both commandline prover interfaces.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederspassProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederspassProver = (mkProverTemplate "SPASS" () spassProveGUI)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder { proveCMDLautomatic = Just spassProveCMDLautomatic

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder , proveCMDLautomaticBatch = Just spassProveCMDLautomaticBatch }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder-- * Main prover functions

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder-- ** Utility functions

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Record for prover specific functions. This is used by both GUI and command

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder line interface.

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederatpFun :: String -- ^ theory name

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> ATPFunctions Sign Sentence ProofTree SoftFOLProverState

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederatpFun thName = ATPFunctions

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder { initialProverState = spassProverState,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder atpTransSenName = transSenName,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder atpInsertSentence = insertSentenceGen,

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder goalOutput = showDFGProblem thName,

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder proverHelpText = "http://www.spass-prover.org/\n",

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder fileExtensions = FileExtensions{problemOutput = ".dfg",

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder proverOutput = ".spass",

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder theoryConfiguration = ".spcf"},

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder runProver = runSpass,

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder createProverOptions = createSpassOptions }

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Parses a given default tactic script into a

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder 'GUI.GenericATPState.ATPTactic_script' if possible. Otherwise a default

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder SPASS tactic script is returned.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

67869d63d1725c79e4c07b51acd466a31932b275Christian MaederparseSpassTactic_script :: Tactic_script

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> ATPTactic_script

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederparseSpassTactic_script =

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder parseTactic_script batchTimeLimit ["-Stdin", "-DocProof"]

-- ** GUI

{- |

Invokes the generic prover GUI. SPASS specific functions are omitted by

data type ATPFunctions.

-}

spassProveGUI :: String -- ^ theory name

-> Theory Sign Sentence ProofTree -- ^ theory consisting of a

-- 'SPASS.Sign.Sign' and a list of Named 'SPASS.Sign.Sentence'

-> IO([Proof_status ProofTree]) -- ^ proof status for each goal

spassProveGUI thName th =

genericATPgui (atpFun thName) True (prover_name spassProver) thName th

emptyProofTree

-- ** command line functions

{- |

Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an

automatic command line interface for a single goal.

SPASS specific functions are omitted by data type ATPFunctions.

-}

spassProveCMDLautomatic ::

String -- ^ theory name

-> Tactic_script -- ^ default tactic script

-> Theory Sign Sentence ProofTree -- ^ theory consisting of a

-- signature and a list of Named sentence

-> IO (Result.Result ([Proof_status ProofTree]))

-- ^ Proof status for goals and lemmas

spassProveCMDLautomatic thName defTS th =

genericCMDLautomatic (atpFun thName) (prover_name spassProver) thName

(parseSpassTactic_script defTS) th emptyProofTree

{- |

Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

automatic command line interface to the SPASS prover.

SPASS specific functions are omitted by data type ATPFunctions.

-}

spassProveCMDLautomaticBatch ::

Bool -- ^ True means include proved theorems

-> Bool -- ^ True means save problem file

-> Concurrent.MVar (Result.Result [Proof_status ProofTree])

-- ^ used to store the result of the batch run

-> String -- ^ theory name

-> Tactic_script -- ^ default tactic script

-> Theory Sign Sentence ProofTree -- ^ theory consisting of a

-- 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence'

-> IO (Concurrent.ThreadId,Concurrent.MVar ())

-- ^ fst: identifier of the batch thread for killing it

-- snd: MVar to wait for the end of the thread

spassProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (prover_name spassProver) thName

(parseSpassTactic_script defTS) th emptyProofTree

-- * SPASS Interfacing Code

{- |

Reads and parses the output of SPASS.

-}

parseSpassOutput :: ChildProcess -- ^ the SPASS process

-> IO (Maybe String, [String], [String], TimeOfDay)

-- ^ (result, used axioms, complete output, used time)

parseSpassOutput spass = parseProtected (parseStart True)

(Nothing, [], [], midnight)

where

-- check for errors. unfortunately we cannot just read from SPASS until an

-- EOF since readMsg will just wait forever on EOF.

parseProtected f (res, usedAxs, output, tUsed) = do

e <- getToolStatus spass

case e of

Nothing

-- still running

-> f (res, usedAxs, output, tUsed)

Just (ExitFailure retval)

-- returned error

-> do

_ <- waitForChildProcess spass

return (Nothing, [],

["SPASS returned error: "++(show retval)]

, tUsed)

Just ExitSuccess

-- completed successfully. read remaining output.

-> f (res, usedAxs, output, tUsed)

-- the first line of SPASS output is always empty.

-- the second contains SPASS-START in the usual case

-- and an error message in case of an error

parseStart firstline (res, usedAxs, output, tUsed) = do

line <- readMsg spass

if firstline

-- ignore empty first line

then parseProtected (parseStart False)

(res, usedAxs, output ++ [""], tUsed)

-- check for a potential error

else do

let startMatch = matchRegex re_start line

if isJust startMatch

-- got SPASS-START. continue parsing

then parseProtected parseIt (res, usedAxs, output ++ [line], tUsed)

-- error. abort parsing

else do

e <- waitForChildProcess spass

case e of

ChildTerminated ->

return (Nothing, [], output ++

[line, "", "SPASS has been terminated."]

, tUsed)

ChildExited retval ->

return (Nothing, [], output ++

[line, "", "SPASS returned error: " ++ (show retval)]

, tUsed)

-- actual parsing. tries to read from SPASS until ".*SPASS-STOP.*" matches.

parseIt (res, usedAxs, output, tUsed) = do

line <- readMsg spass

-- replace tabulators with each 8 spaces

let line' = foldr (\ch li -> if ch == '\x9'

then " "++li

else ch:li) "" line

resMatch = matchRegex re_sb line'

res' = maybe res (Just . head) resMatch

usedAxsMatch = matchRegex re_ua line'

usedAxs' = maybe usedAxs (\ uas -> words (uas !! 1)) usedAxsMatch

tUsed' = maybe tUsed calculateTime $ matchRegex re_tu line

if seq (length line) $ isJust (matchRegex re_stop line')

then do

_ <- waitForChildProcess spass

return (res', usedAxs', output ++ [line'], tUsed')

else

parseProtected parseIt (res', usedAxs', output ++ [line'], tUsed')

-- regular expressions used for parsing

re_start = mkRegex "(.*)SPASS-START(.*)"

re_stop = mkRegex "(.*)SPASS-STOP(.*)"

re_sb = mkRegex "SPASS beiseite: (.*)$"

re_ua = mkRegex "Formulae used in the proof(.*):(.*)$"

re_tu = mkRegex $ "SPASS spent\t([0-9:.]+) "

++ "on the problem.$"

calculateTime str =

if null str then midnight

else

-- the following line is only nice with ghc-6.6.1

-- (maybe midnight id . parseTime defaultTimeLocale "%k:%M:%S%Q")

parseTimeOfDay $ head str

parseTimeOfDay :: String -> TimeOfDay

parseTimeOfDay str =

case splitOn ':' str of

[h,m,s] -> TimeOfDay { todHour = read h

, todMin = read m

, todSec = realToFrac ((read s)::Double)

}

_ -> error "SoftFOL.Prove: wrong time format"

{- |

Runs SPASS. SPASS is assumed to reside in PATH.

-}

runSpass :: SoftFOLProverState -- ^ logical part containing the input Sign and

-- axioms and possibly goals that have been proved

-- earlier as additional axioms

-> GenericConfig ProofTree -- ^ configuration to use

-> Bool -- ^ True means save DFG file

-> String -- ^ name of the theory in the DevGraph

-> AS_Anno.Named SPTerm -- ^ goal to prove

-> IO (ATPRetval, GenericConfig ProofTree)

-- ^ (retval, configuration with proof status and complete output)

runSpass sps cfg saveDFG thName nGoal = do

-- putStrLn ("running 'SPASS" ++ (concatMap (' ':) allOptions) ++ "'")

spass <- newChildProcess "SPASS" [CP.arguments allOptions]

Exception.catch (runSpassReal spass)

(\ excep -> do

-- kill spass process

destroy spass

_ <- waitForChildProcess spass

excepToATPResult (prover_name spassProver) nGoal excep)

where

runSpassReal spass = do

-- check if SPASS is running

e <- getToolStatus spass

if isJust e

then return

(ATPError "Could not start SPASS. Is SPASS in your $PATH?",

emptyConfig (prover_name spassProver)

(AS_Anno.senAttr nGoal) emptyProofTree)

else do

prob <- showDFGProblem thName sps nGoal (createSpassOptions cfg)

when saveDFG

(writeFile (thName++'_':AS_Anno.senAttr nGoal++".dfg") prob)

sendMsg spass prob

(res, usedAxs, output, tUsed) <- parseSpassOutput spass

let (err, retval) = proof_stat res usedAxs extraOptions output

return (err,

cfg{proof_status = retval,

resultOutput = output,

timeUsed = tUsed})

allOptions = ("-Stdin"):(createSpassOptions cfg)

extraOptions = ("-DocProof"):(cleanOptions cfg)

defaultProof_status opts =

(openProof_status (AS_Anno.senAttr nGoal) (prover_name spassProver) $

emptyProofTree)

{tacticScript = Tactic_script $ show $ ATPTactic_script

{ts_timeLimit = configTimeLimit cfg,

ts_extraOpts = opts} }

proof_stat res usedAxs options out

| isJust res && elem (fromJust res) proved =

(ATPSuccess,

(defaultProof_status options)

{ goalStatus = Proved $ if elem (AS_Anno.senAttr nGoal) usedAxs

then Nothing

else Just False

, usedAxioms = filter (/=(AS_Anno.senAttr nGoal)) usedAxs

, proofTree = ProofTree $ spassProof out })

| isJust res && elem (fromJust res) disproved =

(ATPSuccess,

(defaultProof_status options) { goalStatus = Disproved } )

| isJust res && elem (fromJust res) timelimit =

(ATPTLimitExceeded, defaultProof_status options)

| isNothing res =

(ATPError (unlines ("Internal error.":out)),

defaultProof_status options)

| otherwise = (ATPSuccess, defaultProof_status options)

proved = ["Proof found."]

disproved = ["Completion found."]

timelimit = ["Ran out of time."]

{- |

Creates a list of all options the SPASS prover runs with.

That includes the defaults -DocProof and -Timelimit.

-}

createSpassOptions :: GenericConfig ProofTree -> [String]

createSpassOptions cfg =

(cleanOptions cfg) ++ ["-DocProof", "-TimeLimit="

++ (show $ configTimeLimit cfg)]

{- |

Filters extra options and just returns the non standard options.

-}

cleanOptions :: GenericConfig ProofTree -> [String]

cleanOptions cfg =

filter (\ opt -> not (or (map (flip isPrefixOf opt)

filterOptions)))

(extraOpts cfg)

where

filterOptions = ["-DocProof", "-Stdin", "-TimeLimit"]

{- |

Extract proof tree from SPASS output. This will be the String between

"Here is a proof" and "Formulae used in the proof"

-}

spassProof :: [String] -- ^ SPASS output containing proof tree

-> String -- ^ extracted proof tree

spassProof =

unlines . fst . break (isPrefixOf "Formulae used in the proof")

. (\ l -> if null l then l else tail l)

. snd . break (isPrefixOf "Here is a proof with depth")