7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{- |

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Interface for the SPASS theorem prover.

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederCopyright : (c) Rene Wagner, Klaus Lttich, Uni Bremen 2005-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : luettich@tzi.de

7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederPortability : needs POSIX

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederInterface for the SPASS theorem prover.

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

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder{-

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder todo:

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder - window opens too small on linux; why? ... maybe fixed

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder --> failure still there, opens sometimes too small (using KDE),

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder but not twice in a row

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder - keep focus of listboxes if updated (also relevant for

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder in GUI.ProofManagement)

8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maeder

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

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder if not, the theory is inconsistent;

d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maeder mark goal as proved and emmit a warning...

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder - Implement a consistency checker based on GUI

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-}

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maedermodule SPASS.Prove (spassProver,spassProveGUI,spassProveBatch) where

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Logic.Prover

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport SPASS.Sign

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport SPASS.Conversions

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport SPASS.ProveHelp

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport SPASS.Translate

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport SPASS.Print (genSPASSProblem)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederimport qualified Common.AS_Annotation as AS_Anno

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Common.ProofUtils

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Common.PrettyPrint

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport ChildProcess

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport ProcessClasses

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Text.Regex

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Data.List

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederimport Data.Maybe

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Data.IORef

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport qualified Control.Exception as Exception

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport qualified Control.Concurrent as Concurrent

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport GHC.Read

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport System

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport System.IO.Error

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport HTk

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maederimport SpinButton

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport Messages

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport TextDisplay

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederimport Separator

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport XSelection

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport Space

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport GUI.HTkUtils

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport qualified Common.Lib.Map as Map

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- debugging

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maederimport Debug.Trace

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- * Prover implementation

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder{- |

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder The Prover implementation. First runs the batch prover (with graphical

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder feedback), then starts the GUI prover.

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-}

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederspassProver :: Prover Sign Sentence ()

b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederspassProver =

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder Prover { prover_name = "SPASS",

b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder prover_sublogic = "SPASS",

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder prove = spassProveGUI

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder }

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder-- * Shared data structures and assorted utility functions

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder{- |

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Represents a prover configuration used when proving a goal.

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maederdata SPASSConfig = SPASSConfig {

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- | time limit in seconds passed

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder -- to SPASS via -TimeLimit. Default will be used if Nothing.

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder timeLimit :: Maybe Int,

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- | True if timelimit exceed during last prover run

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder timeLimitExceeded :: Bool,

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder -- | extra options passed verbatimely to SPASS.

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- -DocProof, -Stdin, and -TimeLimit will be overridden.

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder extraOpts :: [String]

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder } deriving (Eq, Ord, Show)

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder{- |

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder Creates an empty SPASSConfig. Default time limit and no extra options.

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder-}

5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaederemptyConfig :: SPASSConfig

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederemptyConfig = SPASSConfig {timeLimit = Nothing,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder timeLimitExceeded = False,

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder extraOpts = []}

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder{- |

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Utility function to set the time limit of a SPASSConfig.

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder For values <= 0 a default value is used.

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder-}

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedersetTimeLimit :: Int -> SPASSConfig -> SPASSConfig

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedersetTimeLimit n c = if n > 0 then c{timeLimit = Just n}

72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder else c{timeLimit = Nothing}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder{- |

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder Utility function to set the extra options of a SPASSConfig.

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder-}

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian MaedersetExtraOpts :: [String] -> SPASSConfig -> SPASSConfig

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaedersetExtraOpts opts c = c{extraOpts = opts}

2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Represents the general return value of a prover run.

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-}

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maederdata SpassProverRetval

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder -- | SPASS completed successfully

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder = SpassSuccess

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder -- | SPASS did not terminate before the time limit exceeded

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder | SpassTLimitExceeded

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder -- | an error occured while running SPASS

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder | SpassError String

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder deriving (Eq, Show)

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder{- |

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder Checks whether a SpassProverRetval indicates that the time limit was

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder exceeded.

d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder-}

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederisTimeLimitExceeded :: SpassProverRetval -> Bool

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederisTimeLimitExceeded SpassTLimitExceeded = True

89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaederisTimeLimitExceeded _ = False

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder{- |

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Represents the result of a prover run.

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder (Proof_status, full output)

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-}

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maedertype SPASSResult = (Proof_status (), [String])

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederopenResult :: String -> SPASSResult

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederopenResult n = (openSPASSProof_status n,[])

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederopenSPASSProof_status :: String -> Proof_status ()

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederopenSPASSProof_status n =

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder ((openProof_status n (prover_name spassProver))::Proof_status ())

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder {proofTree = ()}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- * GUI Prover

8dcc70ff9afdfe4aff258676718677a4d7076fd0Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- ** Constants

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder{- |

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Default time limit for the GUI mode prover in seconds.

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-}

35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederguiDefaultTimeLimit :: Int

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederguiDefaultTimeLimit = 10

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- ** Data Structures

d48085f765fca838c1d972d2123601997174583dChristian Maeder

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder{- |

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder We need to store one SPASSConfig per goal.

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder-}

d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maedertype SPASSConfigsMap = Map.Map SPIdentifier SPASSConfig

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder{- |

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Adjusts the configuration associated to a goal by applying the supplied

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder function or inserts a new emptyConfig with the function applied if there's

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder no configuration associated yet.

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Uses Map.member, Map.adjust, and Map.insert for the corresponding tasks

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder internally.

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder-}

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederadjustOrSetConfig :: (SPASSConfig -> SPASSConfig)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- ^ function to be applied against the current

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- configuration or a new emptyConfig

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> SPIdentifier -- ^ name of the goal

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> SPASSConfigsMap -- ^ current SPASSConfigsMap

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -> SPASSConfigsMap

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- ^ resulting SPASSConfigsMap with the changes applied

2ac1742771a267119f1d839054b5e45d0a468085Christian MaederadjustOrSetConfig f k m = if (Map.member k m)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder then Map.adjust f k m

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else Map.insert k (f emptyConfig) m

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder{- |

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Performs a lookup on the ConfigsMap. Returns the config for the goal or an

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder empty config if none is set yet.

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder-}

2ac1742771a267119f1d839054b5e45d0a468085Christian MaedergetConfig :: SPIdentifier -> SPASSConfigsMap -> SPASSConfig

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaedergetConfig spid m = if (isJust lookupId)

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder then fromJust lookupId

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder else emptyConfig

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder where

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder lookupId = Map.lookup spid m

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder{- |

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Store one result per goal.

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maedertype SPASSResultsMap = Map.Map SPIdentifier SPASSResult

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder{- |

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Map to SPASS compliant identifiers

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-}

2ac1742771a267119f1d839054b5e45d0a468085Christian Maedertype SPASSGoalNameMap = Map.Map String String

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

2143841e2b81aa0eaafa6bf81eb57cef33cf29e6Christian Maeder{- |

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Represents the global state of the prover GUI.

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder-}

e3deb984f8f0a06e1b5ed101fb42aa11b8673ffaChristian Maederdata State = State { -- | currently selected goal or Nothing

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder currentGoal :: Maybe SPIdentifier,

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder -- | theory to work on

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder theory :: Theory Sign Sentence (),

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder -- | stores the prover configurations for each goal

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder configsMap :: SPASSConfigsMap,

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder -- | stores the results retrieved by running

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder -- SPASS for each goal

5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder resultsMap :: SPASSResultsMap,

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder -- | stores a mapping to SPASS compliant

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder -- identifiers for all goals

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder namesMap :: SPASSGoalNameMap,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder -- | list of all goals

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder goalsList :: [AS_Anno.Named SPTerm],

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- | logical part without theorems

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder initialLogicalPart :: SPLogicalPart,

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder batchModeIsRunning :: Bool,

d48085f765fca838c1d972d2123601997174583dChristian Maeder mainDestroyed :: Bool

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder }

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder

7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maederdata ThreadState = TSt { batchId :: Maybe Concurrent.ThreadId

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder , batchStopped :: Bool

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder }

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederinitialThreadState :: ThreadState

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederinitialThreadState = TSt { batchId = Nothing

d9953bc9d3d8aa7290bf6d3c2c86b84c984a0f09Christian Maeder , batchStopped = False}

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder{- |

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Creates an initial State around a Theory.

f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-}

81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederinitialState :: Theory Sign Sentence () -> SPASS.Prove.State

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederinitialState th =

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder State {currentGoal = Nothing,

35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder theory = th,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder configsMap = Map.fromList (map (\ g -> (AS_Anno.senName g,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder emptyConfig)) goals),

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder resultsMap = Map.fromList $

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder map (\ g -> let gName = AS_Anno.senName g

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder in (gName,openResult gName)) goals,

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder namesMap = collectNameMapping nSens oSens',

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder goalsList = goals,

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder initialLogicalPart = foldl insertSentence

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (signToSPLogicalPart sign)

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (reverse axioms),

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder batchModeIsRunning = False,

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder mainDestroyed = False

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder }

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder where Theory sign oSens = th

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder oSens' = toNamedList oSens

840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder nSens = prepareSenNames transSenName oSens'

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder (axioms, goals) = partition AS_Anno.isAxiom nSens

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder

bb13d067514a3f474166f345e098b81f3de11dbeChristian Maeder-- ** Defining the view

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder{- |

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder Colors used by the GUI to indicate the status of a goal.

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maeder-}

9fb0db7f56cbb44c3df49552c04afc881267b84eChristian Maederdata ProofStatusColour

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder -- | Proved

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder = Green

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder -- | Proved, but theory is inconsitent

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder | Brown

-- | Disproved

| Red

-- | Open

| Black

-- | Running

| Blue

deriving (Bounded,Enum,Show)

{- |

Generates a ('ProofStatusColour', 'String') tuple representing a Proved proof

status.

-}

statusProved :: (ProofStatusColour, String)

statusProved = (Green, "Proved")

statusProvedButInconsistent :: (ProofStatusColour, String)

statusProvedButInconsistent = (Brown, "Proved (Theory inconsistent!)")

{- |

Generates a ('ProofStatusColour', 'String') tuple representing a Disproved

proof status.

-}

statusDisproved :: (ProofStatusColour, String)

statusDisproved = (Red, "Disproved")

{- |

Generates a ('ProofStatusColour', 'String') tuple representing a Open proof

status.

-}

statusOpen :: (ProofStatusColour, String)

statusOpen = (Black, "Open")

{- |

Generates a ('ProofStatusColour', 'String') tuple representing a Open proof

status in case the time limit has been exceeded.

-}

statusOpenTExceeded :: (ProofStatusColour, String)

statusOpenTExceeded = (Black, "Open (Time is up!)")

{- |

Generates a ('ProofStatusColour', 'String') tuple representing a Running proof

status.

-}

statusRunning :: (ProofStatusColour, String)

statusRunning = (Blue, "Running")

{- |

Converts a 'Proof_status' into a ('ProofStatusColour', 'String') tuple to be

displayed by the GUI.

-}

toGuiStatus :: SPASSConfig -- ^ current prover configuration

-> (Proof_status a) -- ^ status to convert

-> (ProofStatusColour, String)

toGuiStatus cf st = case goalStatus st of

Proved mc -> maybe (statusProved)

( \ c -> if c

then statusProved

else statusProvedButInconsistent)

mc

Disproved -> statusDisproved

_ -> if timeLimitExceeded cf

then statusOpenTExceeded

else statusOpen

{-| stores widgets of an options frame and the frame itself -}

data OpFrame = OpFrame { of_Frame :: Frame

, of_timeSpinner :: SpinButton

, of_timeEntry :: Entry Int

, of_optionsEntry :: Entry String

}

filterOpenGoals :: SPASSResultsMap -> SPASSResultsMap

filterOpenGoals = Map.filter isOpenGoal

where isOpenGoal (st,_) = case goalStatus st of

Open -> True

_ -> False

{- |

Generates a list of 'GUI.HTkUtils.LBGoalView' representations of all goals

from a 'SPASS.Prove.State'.

-}

goalsView :: SPASS.Prove.State -- ^ current global prover state

-> [LBGoalView] -- ^ resulting ['LBGoalView'] list

goalsView s = map (\ g ->

let res = Map.lookup g (resultsMap s)

statind = maybe LBIndicatorOpen

(indicatorFromProof_status . fst)

res

in

LBGoalView {statIndicator = statind,

goalDescription = g})

(map AS_Anno.senName (goalsList s))

-- ** GUI Implementation

-- *** Utility Functions

{- |

Retrieves the value of the time limit 'Entry'. Ignores invalid input.

-}

getValueSafe :: Int -- ^ default time limt

-> Entry Int -- ^ time limit 'Entry'

-> IO Int -- ^ user-requested time limit or default in case of a parse error

getValueSafe defaultTimeLimit timeEntry =

Exception.catchJust Exception.userErrors ((getValue timeEntry) :: IO Int)

(\ s -> trace ("Warning: Error "++show s++" was ignored")

(return defaultTimeLimit))

{- |

Text displayed by the batch mode window.

-}

batchInfoText :: Int -- ^ batch time limt

-> Int -- ^ total number of goals

-> Int -- ^ number of that have been processed

-> String

batchInfoText tl gTotal gDone =

let totalSecs = (gTotal - gDone) * tl

(remMins,secs) = divMod totalSecs 60

(hours,mins) = divMod remMins 60

in

"Batch mode runnig\n"++

show gDone ++ "/" ++ show gTotal ++ " goals processed.\n" ++

"At most "++show hours++"h "++show mins++"m "++show secs++"s remaining."

-- *** Callbacks

{- |

Called every time a goal has been processed in the batch mode gui.

-}

goalProcessed :: IORef SPASS.Prove.State

-- ^ IORef pointing to the backing State data structure

-> Int -- ^ batch time limit

-- -> String -- ^ extra options

-> Int -- ^ total number of goals

-> Label -- ^ info label

-> Int -- ^ number of goals processed so far

-> AS_Anno.Named SPTerm -- ^ goal that has just been processed

-> (SpassProverRetval, SPASSResult)

-> IO Bool

goalProcessed stateRef tLimit numGoals label

processedGoalsSoFar nGoal (retval, res) = do

s <- readIORef stateRef

let s' = s{resultsMap = Map.insert (AS_Anno.senName nGoal)

res (resultsMap s),

configsMap = adjustOrSetConfig

(\ c -> c{timeLimitExceeded =

isTimeLimitExceeded retval,

timeLimit = Just tLimit})

(AS_Anno.senName nGoal)

(configsMap s)}

writeIORef stateRef s'

let notReady = numGoals - processedGoalsSoFar > 0

label # text (if notReady

then (batchInfoText tLimit numGoals processedGoalsSoFar)

else "Batch mode finished\n\n")

return notReady

{- |

Updates the display of the status of the current goal.

-}

updateDisplay :: SPASS.Prove.State -- ^ current global prover state

-> Bool -- ^ set to 'True' if you want the 'ListBox' to be updated

-> ListBox String -- ^ 'ListBox' displaying the status of all goals (see 'goalsView')

-> Label -- ^ 'Label' displaying the status of the currently selected goal (see 'toGuiStatus')

-> Entry Int -- ^ 'Entry' containing the time limit of the current goal

-> Entry String -- ^ 'Entry' containing the extra options

-> ListBox String -- ^ 'ListBox' displaying all axioms used to prove a goal (if any)

-> IO ()

updateDisplay st updateLb goalsLb statusLabel timeEntry optionsEntry axiomsLb = do

when updateLb

(populateGoalsListBox goalsLb (goalsView st))

maybe (return ())

(\ go ->

let mprfst = Map.lookup go (resultsMap st)

cf = Map.findWithDefault

(error "updateDisplay: configsMap \

\was not initialised!!")

go (configsMap st)

t' = maybe guiDefaultTimeLimit id (timeLimit cf)

opts' = unwords (extraOpts cf)

(color, label) = maybe statusOpen

((toGuiStatus cf) . fst)

mprfst

usedAxs = maybe [] (usedAxioms . fst) mprfst

in do

statusLabel # text label

statusLabel # foreground (show color)

timeEntry # HTk.value t'

optionsEntry # HTk.value opts'

axiomsLb # HTk.value (usedAxs::[String])

return ())

(currentGoal st)

newOptionsFrame :: Container par =>

par -- ^ the parent container

-> (Entry Int -> Spin -> IO a)

-- ^ Function called by pressing one spin button

-> IO OpFrame

newOptionsFrame con updateFn = do

right <- newFrame con []

-- contents of newOptionsFrame

l1 <- newLabel right [text "Options:"]

pack l1 [Anchor NorthWest]

opFrame <- newFrame right []

pack opFrame [Expand On, Fill X, Anchor North]

spacer <- newLabel opFrame [text " "]

pack spacer [Side AtLeft]

opFrame2 <- newVBox opFrame []

pack opFrame2 [Expand On, Fill X, Anchor NorthWest]

timeLimitFrame <- newFrame opFrame2 []

pack timeLimitFrame [Expand On, Fill X, Anchor West]

l2 <- newLabel timeLimitFrame [text "TimeLimit"]

pack l2 [Side AtLeft]

-- extra HBox for time limit display

timeLimitLine <- newHBox timeLimitFrame []

pack timeLimitLine [Expand On, Side AtRight, Anchor East]

(timeEntry :: Entry Int) <- newEntry timeLimitLine [width 18,

HTk.value guiDefaultTimeLimit]

pack timeEntry []

timeSpinner <- newSpinButton timeLimitLine (updateFn timeEntry) []

pack timeSpinner []

l3 <- newLabel opFrame2 [text "Extra Options:"]

pack l3 [Anchor West]

(optionsEntry :: Entry String) <- newEntry opFrame2 [width 37]

pack optionsEntry [Fill X, PadX (cm 0.1)]

return $ OpFrame { of_Frame = right

, of_timeSpinner = timeSpinner

, of_timeEntry = timeEntry

, of_optionsEntry = optionsEntry}

-- *** Main GUI

{- |

Invokes the prover GUI. First runs the batch prover on all goals,

then drops the user into a detailed GUI.

-}

spassProveGUI :: String -- ^ theory name

-> Theory Sign Sentence () -- ^ theory consisting of a SPASS.Sign.Sign and a list of Named SPASS.Sign.Sentence

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

spassProveGUI thName th = do

-- create initial backing data structure

let initState = initialState th

stateRef <- newIORef initState

batchTLimit <- getBatchTimeLimit

-- main window

main <- createToplevel [text $ thName ++ " - SPASS Prover"]

pack main [Expand On, Fill Both]

-- VBox for the whole window

b <- newVBox main []

pack b [Expand On, Fill Both]

-- HBox for the upper part (goals on the left, options/results on the right)

b2 <- newHBox b []

pack b2 [Expand On, Fill Both]

-- left frame (goals)

left <- newFrame b2 []

pack left [Expand On, Fill Both]

b3 <- newVBox left []

pack b3 [Expand On, Fill Both]

l0 <- newLabel b3 [text "Goals:"]

pack l0 [Anchor NorthWest]

lbFrame <- newFrame b3 []

pack lbFrame [Expand On, Fill Both]

lb <- newListBox lbFrame [bg "white",exportSelection False,

selectMode Single, height 15] :: IO (ListBox String)

populateGoalsListBox lb (goalsView initState)

pack lb [Expand On, Side AtLeft, Fill Both]

sb <- newScrollBar lbFrame []

pack sb [Expand On, Side AtRight, Fill Y, Anchor West]

lb # scrollbar Vertical sb

-- right frame (options/results)

OpFrame { of_Frame = right

, of_timeSpinner = timeSpinner

, of_timeEntry = timeEntry

, of_optionsEntry = optionsEntry}

<- newOptionsFrame b2

(\ timeEntry sp -> synchronize main

(do

s <- readIORef stateRef

maybe noGoalSelected

(\ goal ->

do

curEntTL <- getValueSafe guiDefaultTimeLimit timeEntry

let sEnt = s {configsMap =

adjustOrSetConfig

(setTimeLimit curEntTL)

goal (configsMap s)}

cfg = getConfig goal (configsMap sEnt)

t = timeLimit cfg

t' = (case sp of

Up -> maybe (guiDefaultTimeLimit + 10)

(+10)

t

_ -> maybe (guiDefaultTimeLimit - 10)

(\ t1 -> t1-10)

t)

s' = sEnt {configsMap =

adjustOrSetConfig

(setTimeLimit t')

goal (configsMap sEnt)}

writeIORef stateRef s'

timeEntry # HTk.value

(maybe guiDefaultTimeLimit

id

(timeLimit $ getConfig goal $

configsMap s'))

done)

(currentGoal s)))

pack right [Expand On, Fill Both, Anchor NorthWest]

-- buttons for options

buttonsHb1 <- newHBox right []

pack buttonsHb1 [Anchor NorthEast]

saveDFGButton <- newButton buttonsHb1 [text "Save DFG File"]

pack saveDFGButton [Side AtLeft]

proveButton <- newButton buttonsHb1 [text "Prove"]

pack proveButton [Side AtRight]

-- result frame

resultFrame <- newFrame right []

pack resultFrame [Expand On, Fill Both]

l4 <- newLabel resultFrame [text "Results:"]

pack l4 [Anchor NorthWest]

spacer <- newLabel resultFrame [text " "]

pack spacer [Side AtLeft]

resultContentBox <- newHBox resultFrame []

pack resultContentBox [Expand On, Anchor West, Fill Both]

-- labels on the left side

rc1 <- newVBox resultContentBox []

pack rc1 [Expand Off, Anchor North]

l5 <- newLabel rc1 [text "Status"]

pack l5 [Anchor West]

l6 <- newLabel rc1 [text "Used Axioms"]

pack l6 [Anchor West]

-- contents on the right side

rc2 <- newVBox resultContentBox []

pack rc2 [Expand On, Fill Both, Anchor North]

statusLabel <- newLabel rc2 [text " -- "]

pack statusLabel [Anchor West]

axiomsFrame <- newFrame rc2 []

pack axiomsFrame [Expand On, Anchor West, Fill Both]

axiomsLb <- newListBox axiomsFrame [HTk.value $ ([]::[String]),

bg "white",exportSelection False,

selectMode Browse,

height 6, width 19] :: IO (ListBox String)

pack axiomsLb [Side AtLeft, Expand On, Fill Both]

axiomsSb <- newScrollBar axiomsFrame []

pack axiomsSb [Side AtRight, Fill Y, Anchor West]

axiomsLb # scrollbar Vertical axiomsSb

detailsButton <- newButton resultFrame [text "Show Details"]

pack detailsButton [Anchor NorthEast]

-- separator

sp1 <- newSpace b (cm 0.15) []

pack sp1 [Expand Off, Fill X, Side AtBottom]

newHSeparator b

sp2 <- newSpace b (cm 0.15) []

pack sp2 [Expand Off, Fill X, Side AtBottom]

-- batch mode frame

batch <- newFrame b []

pack batch [Expand Off, Fill X]

batchTitle <- newLabel batch [text "SPASS Batch Mode:"]

pack batchTitle [Side AtTop]

batchLeft <- newVBox batch []

pack batchLeft [Expand On, Fill X, Side AtLeft]

batchBtnBox <- newHBox batchLeft []

pack batchBtnBox [Expand On, Fill X, Side AtLeft]

stopBatchButton <- newButton batchBtnBox [text "Stop"]

pack stopBatchButton []

runBatchButton <- newButton batchBtnBox [text "Run"]

pack runBatchButton []

batchSpacer <- newSpace batchLeft (pp 150) [orient Horizontal]

pack batchSpacer [Side AtLeft]

batchStatusLabel <- newLabel batchLeft [text "\n\n"]

pack batchStatusLabel []

OpFrame { of_Frame = batchRight

, of_timeSpinner = batchTimeSpinner

, of_timeEntry = batchTimeEntry

, of_optionsEntry = batchOptionsEntry}

<- newOptionsFrame batch

(\ tEntry sp -> synchronize main

(do

curEntTL <- getValueSafe batchTLimit tEntry

let t' = case sp of

Up -> curEntTL+10

_ -> max batchTLimit (curEntTL-10)

tEntry # HTk.value t'

done))

pack batchRight [Expand On, Fill X, Anchor NorthWest,Side AtRight]

batchTimeEntry # HTk.value batchTLimit

-- separator 2

sp1_2 <- newSpace b (cm 0.15) []

pack sp1_2 [Expand Off, Fill X, Side AtBottom]

newHSeparator b

sp2_2 <- newSpace b (cm 0.15) []

pack sp2_2 [Expand Off, Fill X, Side AtBottom]

-- global options frame

globalOptsFr <- newFrame b []

pack globalOptsFr [Expand Off, Fill Both]

gOptsTitle <- newLabel globalOptsFr [text "Global Options:"]

pack gOptsTitle [Side AtTop]

inclProvedThsTK <- createTkVariable True

inclProvedThsCheckButton <-

newCheckButton globalOptsFr

[variable inclProvedThsTK,

text ("include preceeding proven therorems"++

" in next proof attempt")]

pack inclProvedThsCheckButton [Side AtLeft]

-- separator 3

sp1_3 <- newSpace b (cm 0.15) []

pack sp1_3 [Expand Off, Fill X, Side AtBottom]

newHSeparator b

sp2_3 <- newSpace b (cm 0.15) []

pack sp2_3 [Expand Off, Fill X, Side AtBottom]

-- bottom frame (help/save/exit buttons)

bottom <- newHBox b []

pack bottom [Expand Off, Fill Both]

helpButton <- newButton bottom [text "Help"]

pack helpButton [PadX (cm 0.3), IPadX (cm 0.1)] -- wider "Help" button

saveButton <- newButton bottom [text "Save Prover Configuration"]

pack saveButton [PadX (cm 0.3)]

exitButton <- newButton bottom [text "Exit Prover"]

pack exitButton [PadX (cm 0.3)]

putWinOnTop main

-- IORef for batch thread

threadStateRef <- newIORef initialThreadState

-- events

(selectGoal, _) <- bindSimple lb (ButtonPress (Just 1))

doProve <- clicked proveButton

saveDFG <- clicked saveDFGButton

showDetails <- clicked detailsButton

runBatch <- clicked runBatchButton

stopBatch <- clicked stopBatchButton

help <- clicked helpButton

saveConfiguration <- clicked saveButton

exit <- clicked exitButton

(closeWindow,_) <- bindSimple main Destroy

let goalSpecificWids = [EnW timeEntry, EnW timeSpinner,EnW optionsEntry] ++

map EnW [proveButton,detailsButton,saveDFGButton]

wids = EnW lb : goalSpecificWids ++

[EnW batchTimeEntry, EnW batchTimeSpinner,

EnW batchOptionsEntry,EnW inclProvedThsCheckButton] ++

map EnW [helpButton,saveButton,exitButton,runBatchButton]

disableWids goalSpecificWids

disable stopBatchButton

-- event handlers

spawnEvent

(forever

((selectGoal >>> do

s <- readIORef stateRef

let oldGoal = currentGoal s

curEntTL <- (getValueSafe guiDefaultTimeLimit timeEntry) :: IO Int

let s' = maybe s

(\ og -> s

{configsMap =

adjustOrSetConfig (setTimeLimit curEntTL)

og (configsMap s)})

oldGoal

sel <- (getSelection lb) :: IO (Maybe [Int])

let s'' = maybe s' (\ sg -> s' {currentGoal =

Just $ AS_Anno.senName

(goalsList s' !! head sg)})

sel

writeIORef stateRef s''

when (isJust sel && not (batchModeIsRunning s''))

(enableWids goalSpecificWids)

when (isJust sel) $ enableWids [EnW detailsButton,EnW saveDFGButton]

updateDisplay s'' False lb statusLabel timeEntry optionsEntry axiomsLb

done)

+> (saveDFG >>> do

rs <- readIORef stateRef

inclProvedThs <- readTkVariable inclProvedThsTK

maybe (return ())

(\ goal -> do

let (nGoal,lp') =

prepareLP (initialLogicalPart rs) rs

goal inclProvedThs

prob <- genSPASSProblem thName lp' (Just nGoal)

createTextSaveDisplay ("SPASS Problem for Goal "++goal)

(thName++goal++".dfg")

(showPretty prob "")

)

$ currentGoal rs

done)

+> (doProve >>> do

rs <- readIORef stateRef

if isNothing $ currentGoal rs

then noGoalSelected

else (do

curEntTL <- (getValueSafe guiDefaultTimeLimit

timeEntry) :: IO Int

inclProvedThs <- readTkVariable inclProvedThsTK

let goal = fromJust $ currentGoal rs

s = rs {configsMap = adjustOrSetConfig

(setTimeLimit curEntTL)

goal

(configsMap rs)}

(nGoal,lp') = prepareLP (initialLogicalPart rs) rs

goal inclProvedThs

extraOptions <- (getValue optionsEntry) :: IO String

let s' = s {configsMap = adjustOrSetConfig

(setExtraOpts (words extraOptions))

goal

(configsMap s)}

statusLabel # text (snd statusRunning)

statusLabel # foreground (show $ fst statusRunning)

disableWids wids

(retval, (res, output)) <-

runSpass lp' (getConfig goal (configsMap s')) thName nGoal

-- check if main is still there

curSt <- readIORef stateRef

if mainDestroyed curSt

then done

else do

enableWids wids

case retval of

SpassError message -> errorMess message

_ -> return ()

let s'' = s'{resultsMap = Map.insert goal (res, output)

(resultsMap s'),

configsMap =

adjustOrSetConfig

(\ c -> c {timeLimitExceeded =

isTimeLimitExceeded retval})

goal (configsMap s')}

writeIORef stateRef s''

updateDisplay s'' True lb statusLabel timeEntry

optionsEntry axiomsLb

done)

done)

+> (showDetails >>> do

s <- readIORef stateRef

if isNothing $ currentGoal s

then noGoalSelected

else (do

let goal = fromJust $ currentGoal s

let result = Map.lookup goal (resultsMap s)

let output = if isJust result

then snd (fromJust result)

else ["This goal hasn't been run through "++

"the prover yet."]

let detailsText = concatMap ('\n':) output

createTextSaveDisplay ("SPASS Output for Goal "++goal)

(goal ++ ".spass")

(seq (length detailsText) detailsText)

done)

done)

+> (runBatch >>> do

cleanupThread threadStateRef

s <- readIORef stateRef

-- get options for this batch run

curEntTL <- (getValueSafe batchTLimit batchTimeEntry) :: IO Int

let tLimit = if curEntTL > 0 then curEntTL else batchTLimit

batchTimeEntry # HTk.value tLimit

extOpts <- (getValue batchOptionsEntry) :: IO String

writeIORef stateRef (s {batchModeIsRunning = True})

let numGoals = Map.size $ filterOpenGoals $ resultsMap s

if numGoals > 0

then do

batchStatusLabel # text (batchInfoText tLimit numGoals 0)

disableWids wids

enable stopBatchButton

enableWidsUponSelection lb [EnW detailsButton,EnW saveDFGButton]

enable lb

inclProvedThs <- readTkVariable inclProvedThsTK

batchProverId <- Concurrent.forkIO

(do spassProveBatch tLimit extOpts inclProvedThs

(\ gPSF nSen res -> do

cont <- goalProcessed stateRef tLimit numGoals

batchStatusLabel

gPSF nSen res

st <- readIORef stateRef

updateDisplay st True lb statusLabel timeEntry

optionsEntry axiomsLb

when (not cont)

(do

-- putStrLn "Batch ended"

disable stopBatchButton

enableWids wids

enableWidsUponSelection lb goalSpecificWids

writeIORef stateRef

(st {batchModeIsRunning = False})

cleanupThread threadStateRef)

return cont)

thName s

return ())

modifyIORef threadStateRef

(\ ts -> ts{batchId = Just batchProverId})

done

else do

batchStatusLabel # text ("No further open goals\n\n")

done)

+> (stopBatch >>> do

cleanupThread threadStateRef

modifyIORef threadStateRef (\ s -> s {batchStopped = True})

-- putStrLn "Batch stopped"

disable stopBatchButton

enableWids wids

enableWidsUponSelection lb goalSpecificWids

batchStatusLabel # text "Batch mode stopped\n\n"

st <- readIORef stateRef

writeIORef stateRef

(st {batchModeIsRunning = False})

updateDisplay st True lb statusLabel timeEntry

optionsEntry axiomsLb

done)

+> (help >>> do

createTextDisplay "SPASS Help" spassHelpText [size (80, 30)]

done)

+> (saveConfiguration >>> do

s <- readIORef stateRef

let cfgText = concatMap ((++"\n")) ["Configuration:\n",

show $ configsMap s,

"\nResults:\n",

showResMap (resultsMap s)]

createTextSaveDisplay ("SPASS Configuration for Theory " ++ thName)

(thName ++ ".spcf") cfgText

done)

))

sync ( (exit >>> destroy main)

+> (closeWindow >>> do cleanupThread threadStateRef

modifyIORef stateRef

(\ s -> s{mainDestroyed = True})

destroy main)

)

s <- readIORef stateRef

let proof_stats = map (\g -> let res = Map.lookup g (resultsMap s)

g' = Map.findWithDefault

(error ("Lookup of name failed: (1) "

++"should not happen \""

++g++"\""))

g (namesMap s)

pStat = fst $ fromJust res

in if isJust res

then transNames (namesMap s) pStat

else openSPASSProof_status g')

(map AS_Anno.senName $ goalsList s)

return proof_stats

where

cleanupThread tRef = do

st <- readIORef tRef

-- cleaning up

maybe (return ())

(\ tId -> do

Concurrent.killThread tId

writeIORef tRef initialThreadState)

(batchId st)

noGoalSelected = errorMess "Please select a goal first."

prepareLP iLP s goal inclProvedThs =

let (beforeThis, afterThis) =

splitAt (fromJust $

findIndex (\sen -> AS_Anno.senName sen == goal)

(goalsList s))

(goalsList s)

proved = filter (\sen-> checkGoal (resultsMap s)

(AS_Anno.senName sen)) beforeThis

in if inclProvedThs

then (head afterThis,

foldl (\lp provedGoal ->

insertSentence lp (provedGoal{AS_Anno.isAxiom = True}))

iLP

(reverse proved))

else (maybe (error ("SPASS.Prove.prepareLP: Goal "++goal++

" not found!!"))

id (find ((==goal) . AS_Anno.senName) (goalsList s)),

iLP)

showResMap mp =

'{':(foldr (\ (k,(r,outp)) resF ->

shows k .

(++) ":=\n (" .

shows r . (++) ",\n \"" .

(++) (unlines outp) . (++) "\")\n" . resF) id

(Map.toList mp)) "}"

transNames nm pStat =

pStat { goalName = trN $ goalName pStat

, usedAxioms = foldr (fil $ trN $ goalName pStat) [] $

usedAxioms pStat }

where trN x' = Map.findWithDefault

(error ("Lookup of name failed: (2) "++

"should not happen \""++x'++"\""))

x' nm

fil g ax axs =

maybe (trace ("*** SPASS Warning: unknown axiom \""++

ax++"\" omitted from list of used\n"++

" axioms of goal \""++g++"\"")

axs) (:axs) (Map.lookup ax nm)

-- * Non-interactive Batch Prover

-- ** Constants

{- |

Time limit used by the batch mode prover.

-}

batchTimeLimit :: Int

batchTimeLimit = 20

-- ** Utility Functions

{- |

reads ENV-variable HETS_SPASS_BATCH_TIME_LIMIT and if it exists and has an Int-value this value is returned otherwise the value of 'batchTimeLimit' is returned.

-}

getBatchTimeLimit :: IO Int

getBatchTimeLimit = do

is <- Exception.catch (getEnv "HETS_SPASS_BATCH_TIME_LIMIT")

(\e -> case e of

Exception.IOException ie ->

if isDoesNotExistError ie -- == NoSuchThing

then return $ show batchTimeLimit

else Exception.throwIO e

_ -> Exception.throwIO e)

return (either (const batchTimeLimit) id (readEither is))

{- |

Checks whether a goal in the results map is marked as proved.

-}

checkGoal :: SPASSResultsMap -> SPIdentifier -> Bool

checkGoal resMap goal =

isJust g && isProvedStat (fst $ fromJust g)

where

g = Map.lookup goal resMap

-- ** Implementation

{- |

A non-GUI batch mode prover. Uses default configuration for SPASS.

The list of goals is processed sequentially. Proved goals are inserted

as axioms.

-}

spassProveBatch :: Int -- ^ batch time limit

-> String -- ^ extra options passed

-> Bool -- ^ True means include proved theorems

-> (Int

-> AS_Anno.Named SPTerm

-> (SpassProverRetval, SPASSResult)

-> IO Bool)

-- ^ called after every prover run.

-- return True if you want the prover to continue.

-> String -- ^ theory name

-> SPASS.Prove.State

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

spassProveBatch tLimit extraOptions inclProvedThs f thName st =

batchProve (initialLogicalPart st) 0 [] (goalsList st)

{- do -- putStrLn $ showPretty initialLogicalPart ""

-- read batchTimeLimit from ENV variable if set otherwise use constant

pstl <- {- trace (showPretty initialLogicalPart (show goals)) -}

batchProve (initialLogicalPart st) [] (goalsList st)

-- putStrLn ("Outcome of proofs:\n" ++ unlines (map show pstl) ++ "\n")

return pstl -}

where

openGoals = filterOpenGoals (resultsMap st)

addToLP g res lp =

if isProvedStat res && inclProvedThs

then insertSentence lp (g{AS_Anno.isAxiom = True})

else lp

batchProve _ _ resDone [] = return (reverse resDone)

batchProve lp goalsProcessedSoFar resDone (g:gs) =

let gName = AS_Anno.senName g

in

if Map.member gName openGoals

then do

putStrLn $ "Trying to prove goal: " ++ gName

-- putStrLn $ show g

(err, (res, full)) <-

runSpass lp (emptyConfig { timeLimit = Just tLimit

, extraOpts = words extraOptions })

thName g

putStrLn $ "SPASS returned: " ++ (show err)

-- if the batch prover runs in a separate thread

-- that's killed via killThread

-- runSpass will return SpassError. we have to stop the

-- recursion in that case

case err of

SpassError _ -> return ((reverse (res:resDone)) ++

(map (openSPASSProof_status .

AS_Anno.senName) gs))

_ -> do

-- add proved goals as axioms

let lp' = addToLP g res lp

goalsProcessedSoFar' = goalsProcessedSoFar+1

cont <- f goalsProcessedSoFar' g (err, (res, full))

if cont

then batchProve lp' goalsProcessedSoFar' (res:resDone) gs

else return ((reverse (res:resDone)) ++

(map (openSPASSProof_status .

AS_Anno.senName) gs))

else batchProve (addToLP g (fst $

Map.findWithDefault (openResult gName)

gName $ resultsMap st)

lp)

goalsProcessedSoFar resDone gs

-- * SPASS Interfacing Code

{- |

Reads and parses the output of SPASS.

-}

parseSpassOutput :: ChildProcess -- ^ the SPASS process

-> IO (Maybe String, [String], [String]) -- ^ (result, used axioms, complete output)

parseSpassOutput spass = parseProtected (parseStart True) (Nothing, [], [])

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) = do

e <- getToolStatus spass

case e of

Nothing

-- still running

-> f (res, usedAxs, output)

Just (ExitFailure retval)

-- returned error

-> do

_ <- waitForChildProcess spass

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

Just ExitSuccess

-- completed successfully. read remaining output.

-> f (res, usedAxs, output)

-- the first line of SPASS output it 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) = do

line <- readMsg spass

if firstline

-- ignore empty first line

then parseProtected (parseStart False) (res, usedAxs, output ++ [""])

-- 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])

-- error. abort parsing

else do

e <- waitForChildProcess spass

case e of

ChildTerminated ->

return (Nothing, [], output ++ [line, "", "SPASS has been terminated."])

ChildExited retval ->

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

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

parseIt (res, usedAxs, output) = do

line <- readMsg spass

let resMatch = matchRegex re_sb line

let res' = if isJust resMatch then (Just $ head $ fromJust resMatch) else res

let usedAxsMatch = matchRegex re_ua line

let usedAxs' = if isJust usedAxsMatch then (words $ head $ fromJust usedAxsMatch) else usedAxs

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

then do

_ <- waitForChildProcess spass

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

else

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

-- 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.*:(.*)$"

{- |

Runs SPASS. SPASS is assumed to reside in PATH.

-}

runSpass :: SPLogicalPart -- ^ logical part containing the input Sign and axioms and possibly goals that have been proved earlier as additional axioms

-> SPASSConfig -- ^ configuration to use

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

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

-> IO (SpassProverRetval, SPASSResult) -- ^ (retval, (proof status, complete output))

runSpass lp cfg thName nGoal = do

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

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

Exception.catch (runSpassReal spass)

(\ excep -> do

-- kill spass process

destroy spass

_ <- waitForChildProcess spass

return (case excep of

-- this is supposed to distinguish "fd ... vanished"

-- errors from other exceptions

Exception.IOException e ->

(SpassError ("Internal error communicating "++

"with SPASS.\n"++show e),

(openResult $ AS_Anno.senName nGoal))

_ -> (SpassError ("Error running SPASS.\n"++show excep),

(openResult $ AS_Anno.senName nGoal))))

where

runSpassReal spass = do

-- check if SPASS is running

e <- getToolStatus spass

if isJust e

then return

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

(openResult $ AS_Anno.senName nGoal))

else do

prob <- genSPASSProblem thName lp (Just nGoal)

sendMsg spass (showPretty prob "")

(res, usedAxs, output) <- parseSpassOutput spass

let (err, retval) = proof_status res usedAxs cleanOptions

return (err, (retval, output))

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

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

filterOptions)))

(extraOpts cfg)

tLimit = if isJust (timeLimit cfg)

then fromJust (timeLimit cfg)

-- this is OK. the batch prover always has the time limit set

else guiDefaultTimeLimit

allOptions = cleanOptions ++ ["-DocProof", "-Stdin", "-TimeLimit=" ++ (show tLimit)]

defaultProof_status opts =

(openSPASSProof_status (AS_Anno.senName nGoal))

{tacticScript = Tactic_script $ concatMap (' ':) opts}

proof_status res usedAxs options

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

(SpassSuccess,

(defaultProof_status options)

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

then Nothing

else Just False

, usedAxioms = filter (/=(AS_Anno.senName nGoal)) usedAxs })

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

(SpassSuccess,

(defaultProof_status options) { goalStatus = Disproved } )

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

(SpassTLimitExceeded, defaultProof_status options)

| isNothing res =

(SpassError "Internal error.", defaultProof_status options)

| otherwise = (SpassSuccess, defaultProof_status options)

proved = ["Proof found."]

disproved = ["Completion found."]

timelimit = ["Ran out of time."]