ProveCommands.hs revision 260192a59aed3dbf3b339ea86d4009a7d1c0d728
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantz{-# LANGUAGE CPP #-}
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantz{- |
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzModule : $Header$
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzDescription : CMDL interface commands
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzCopyright : uni-bremen and DFKI
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzLicense : GPLv2 or higher, see LICENSE.txt
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndMaintainer : r.pascanu@jacobs-university.de
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndStability : provisional
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndPortability : portable
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenCMDL.ProveCommands contains all commands (except prove\/consistency check)
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenrelated to prove mode
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndmodule CMDL.ProveCommands
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ( cTranslate
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cDropTranslations
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen , cGoalsAxmGeneral
3f08db06526d6901aa08c110b5bc7dde6bc39905nd , cDoLoop
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cProve
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cDisprove
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cProveAll
3f08db06526d6901aa08c110b5bc7dde6bc39905nd , cSetUseThms
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cSetSave2File
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd , cEndScript
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd , cStartScript
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd , cTimeLimit
0066eddda7203f6345b56f77d146a759298dc635gryzor , cNotACommand
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd , cShowOutput
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung ) where
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd
864d6d55a72bdb982ebabbc95cf8f051c43fa6ddrbowenimport CMDL.DataTypes (CmdlState (intState), CmdlGoalAxiom (..),
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd CmdlListAction (..), ProveCmdType(..))
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport CMDL.DataTypesUtils (add2hist, genMsgAndCode, genMessage,
b09fcdfc59ada4712150e7bcc7b502bb9e4601d8rjung genAddMessage, getIdComorphism)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport CMDL.DgCommands (selectANode)
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzimport CMDL.ProveConsistency (doLoop, sigIntHandler)
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantzimport CMDL.Utils (checkIntString)
f43ed9051a7f4db461d67ed4f7ece175b3dbca7cjerenkrantz
e4ca72aa494fed7b6948012734b9c9c098fbba07ndimport Common.Result (Result (Result))
e4ca72aa494fed7b6948012734b9c9c098fbba07ndimport Common.Utils (trim, splitOn)
e4ca72aa494fed7b6948012734b9c9c098fbba07nd
e4ca72aa494fed7b6948012734b9c9c098fbba07ndimport Data.List (find, nub)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Data.Maybe (fromMaybe)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Comorphisms.LogicGraph (lookupComorphism_in_LG)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinimport Proofs.AbstractState
117c1f888a14e73cdd821dc6c23eb0411144a41cnd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdimport Logic.Comorphism (compComorphism, AnyComorphism (..))
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Logic.Logic (language_name)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Control.Concurrent (forkIO)
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15ndimport Control.Concurrent.MVar (newEmptyMVar, newMVar, takeMVar)
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15ndimport Control.Monad (foldM)
99ca75ffd7b9d0e6573ba8858c6e59d4a6d2fa15nd
b12f74e1aaac71d21e4b9a376b31d7307a8d87d8nd#ifdef UNIX
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedoohimport System.Posix.Signals (Handler (Catch), installHandler, sigINT)
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd#endif
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Interfaces.GenericATPState (ATPTacticScript (tsTimeLimit, tsExtraOpts))
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndimport Interfaces.DataTypes (ListChange (..), IntIState (..), Int_NodeInfo (..),
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd UndoRedoElem (..), IntState (i_state))
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd-- | Drops any seleceted comorphism
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcDropTranslations :: CmdlState -> IO CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcDropTranslations state =
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd case i_state $ intState state of
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Just pS ->
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd case cComorphism pS of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Nothing -> return state
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Just _ -> return $
e4ca72aa494fed7b6948012734b9c9c098fbba07nd add2hist [CComorphismChange $ cComorphism pS] $
e4ca72aa494fed7b6948012734b9c9c098fbba07nd state {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd intState = (intState state ) {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd i_state = Just $ pS {
e4ca72aa494fed7b6948012734b9c9c098fbba07nd cComorphism = getIdComorphism $ elements pS } }
e4ca72aa494fed7b6948012734b9c9c098fbba07nd }
e4ca72aa494fed7b6948012734b9c9c098fbba07nd
e4ca72aa494fed7b6948012734b9c9c098fbba07nd
e4ca72aa494fed7b6948012734b9c9c098fbba07nd-- | select comorphisms
e4ca72aa494fed7b6948012734b9c9c098fbba07ndcTranslate :: String -> CmdlState -> IO CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcTranslate input state' =
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin foldM (\ state c -> case i_state $ intState state of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -- nothing selected !
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Just pS -> case lookupComorphism_in_LG c of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result m Nothing -> return $ genMsgAndCode (show m) 1 state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ (Just cm) ->
7e9d90004f580231e0376880710dc25408950ab9rbowen case cComorphism pS of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin {- when selecting some theory the Id comorphism is automatically
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin generated -}
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Nothing -> return $ genMsgAndCode "No theory selected" 1 state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Just ocm ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case compComorphism ocm cm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ Nothing ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return $ genMsgAndCode "Can not add comorphism" 1 state
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Result _ (Just smth) ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin return $ genAddMessage [] ("Adding comorphism " ++
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin (\ (Comorphism c') -> language_name c') cm)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin $ add2hist [CComorphismChange $ cComorphism pS] $
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin state {
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin intState = (intState state) {
7e9d90004f580231e0376880710dc25408950ab9rbowen i_state = Just pS {
7e9d90004f580231e0376880710dc25408950ab9rbowen cComorphism = Just smth } }
7e9d90004f580231e0376880710dc25408950ab9rbowen }) (genMessage "" "" state')
7e9d90004f580231e0376880710dc25408950ab9rbowen (concatMap (splitOn ';') $
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin concatMap (splitOn ':') $
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin words $ trim input)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinparseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> [Int_NodeInfo]
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> ([Int_NodeInfo], [ListChange])
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin -> ([Int_NodeInfo], [ListChange])
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrinparseElements action gls gls_axm elems (acc1, acc2)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin = case elems of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin [] -> (acc1, acc2)
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Element st nb : ll ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin let allgls = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> map fst $ getGoals st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeAxioms -> map fst $ getAxioms st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin selgls = case gls_axm of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeGoals -> selectedGoals st
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ChangeAxioms -> includedAxioms st
7e9d90004f580231e0376880710dc25408950ab9rbowen fn' x y = x == y
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin fn ks x = case find (fn' x) ks of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Just _ ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case action of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDel -> False
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin _ -> True
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin Nothing ->
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin case action of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDel -> True
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin _ -> False
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin gls' = case action of
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDelAll -> []
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionDel -> filter (fn selgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionSetAll -> allgls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionSet -> filter (fn allgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin ActionAdd -> nub $ selgls ++ filter (fn allgls) gls
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin nwelm = case gls_axm of
7e9d90004f580231e0376880710dc25408950ab9rbowen ChangeGoals -> Element (st {selectedGoals = gls'}) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen ChangeAxioms -> Element (st {includedAxioms = gls'}) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen hchg = case gls_axm of
7e9d90004f580231e0376880710dc25408950ab9rbowen ChangeGoals -> GoalsChange (selectedGoals st) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen ChangeAxioms -> AxiomsChange (includedAxioms st) nb
7e9d90004f580231e0376880710dc25408950ab9rbowen in parseElements action gls gls_axm ll (nwelm : acc1, hchg : acc2)
7e9d90004f580231e0376880710dc25408950ab9rbowen
15a7e433cd5ddbb53d48a11f2f8732d9ea6a48caminfrin{- | A general function that implements the actions of setting,
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd adding or deleting goals or axioms from the selection list -}
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom ->
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd String -> CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd -> IO CmdlState
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4ndcGoalsAxmGeneral action gls_axm input state
e4ca72aa494fed7b6948012734b9c9c098fbba07nd = case i_state $ intState state of
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
e4ca72aa494fed7b6948012734b9c9c098fbba07nd Just pS ->
5bc7abb0ed18f8dbc491d0be0a09bc02e6ee9d85nd case elements pS of
5bc7abb0ed18f8dbc491d0be0a09bc02e6ee9d85nd [] -> return $ genMsgAndCode "Nothing selected" 1 state
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd ls ->
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd do
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd let gls = words input
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf let (ls', hst) = parseElements action gls
aa0b2780958e9b1467c9d0153a05738e399811a5nd gls_axm
e4ca72aa494fed7b6948012734b9c9c098fbba07nd ls ([], [])
e4ca72aa494fed7b6948012734b9c9c098fbba07nd return $ add2hist [ListChange hst] $
e4ca72aa494fed7b6948012734b9c9c098fbba07nd state {
e487d6c09669296f94a5190cc34586a98e624a00nd intState = (intState state) {
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic i_state = Just pS {
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic elements = ls'
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic }
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic }
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic }
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igaliccDoLoop ::
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic ProveCmdType
f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic -> CmdlState
e487d6c09669296f94a5190cc34586a98e624a00nd -> IO CmdlState
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovenercDoLoop proveCmdType state
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf = case i_state $ intState state of
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener Just pS ->
41618b507c149c7adf89bd92a0cc2c6962a29dcfcovener case elements pS of
e4ca72aa494fed7b6948012734b9c9c098fbba07nd [] -> return $ genMsgAndCode "Nothing selected" 1 state
e4ca72aa494fed7b6948012734b9c9c098fbba07nd ls ->
a29610af88e278144045bfa1bc63b4a1a4b5ff14trawick do
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd -- create initial mVars to comunicate
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd miSt <- newMVar $ intState state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd mSt <- newMVar Nothing
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd mThr <- newMVar Nothing
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd mW <- newEmptyMVar
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd -- fork
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd thrID <- forkIO (doLoop miSt mThr mSt mW ls proveCmdType)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd -- install the handler that waits for SIG_INT
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd#ifdef UNIX
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd oldHandler <- installHandler sigINT (Catch $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd sigIntHandler mThr miSt mSt thrID mW (i_ln pS)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd ) Nothing
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd#endif
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd -- block and wait for answers
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd answ <- takeMVar mW
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd#ifdef UNIX
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd installHandler sigINT oldHandler Nothing
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd#endif
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd let nwpS = fromMaybe pS (i_state answ)
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd nwls = concatMap (\ (Element _ x) -> selectANode x nwpS) ls
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd hst = concatMap (\ (Element stt x) ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd [ AxiomsChange (includedAxioms stt) x
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd , GoalsChange (selectedGoals stt) x ]) ls
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd return $ add2hist [ListChange hst] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd state { intState = answ {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state = Just $ nwpS { elements = nwls }}}
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd{- | Proves only selected goals from all nodes using selected
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd axioms -}
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProve :: CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProve = cDoLoop Prove
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcDisprove :: CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcDisprove = cDoLoop Disprove
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd{- | Proves all goals in the nodes selected using all axioms and
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd theorems -}
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProveAll :: CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcProveAll state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd = case i_state $ intState state of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Just pS ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd case elements pS of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd [] -> return $ genMsgAndCode "Nothing selected" 1 state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd ls ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd let ls' = map (\ (Element st nb) ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Element (resetSelection st) nb) ls
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd nwSt = add2hist [ListChange [NodesChange $ elements pS]] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd state {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd intState = (intState state) {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state = Just $ pS { elements = ls' } } }
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd in cProve nwSt
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd-- | Sets the use theorems flag of the interface
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcSetUseThms :: Bool -> CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcSetUseThms val state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd = case i_state $ intState state of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Just pS ->
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd return $ add2hist [UseThmChange $ useTheorems pS] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd state {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd intState = (intState state) {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd i_state = Just pS {
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd useTheorems = val } } }
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcShowOutput :: Bool -> CmdlState -> IO CmdlState
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisdcShowOutput b state = do
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd case i_state $ intState state of
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd Just pS -> do
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd return $ add2hist [ChShowOutput $ showOutput pS] $
fa49f9755c1dcaf2f0ab6c57676592951e7b8282chrisd state {
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd intState = (intState state) {
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd i_state = Just pS {
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd showOutput = b } } }
ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd
0066eddda7203f6345b56f77d146a759298dc635gryzor-- | Sets the save2File value to either true or false
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0ndcSetSave2File :: Bool -> CmdlState -> IO CmdlState
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungcSetSave2File val state
727872d18412fc021f03969b8641810d8896820bhumbedooh = case i_state $ intState state of
0d0ba3a410038e179b695446bb149cce6264e0abnd Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
727872d18412fc021f03969b8641810d8896820bhumbedooh Just ps ->
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh return $ add2hist [Save2FileChange $ save2file ps] $
0d0ba3a410038e179b695446bb149cce6264e0abnd state {
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh intState = (intState state) {
727872d18412fc021f03969b8641810d8896820bhumbedooh i_state = Just ps { save2file = val } } }
0d0ba3a410038e179b695446bb149cce6264e0abnd
0d0ba3a410038e179b695446bb149cce6264e0abnd
0d0ba3a410038e179b695446bb149cce6264e0abnd{- | The function is called everytime when the input could
ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh not be parsed as a command -}
0d0ba3a410038e179b695446bb149cce6264e0abndcNotACommand :: String -> CmdlState -> IO CmdlState
0d0ba3a410038e179b695446bb149cce6264e0abndcNotACommand input state
0d0ba3a410038e179b695446bb149cce6264e0abnd = case input of
727872d18412fc021f03969b8641810d8896820bhumbedooh -- if input line is empty do nothing
0d0ba3a410038e179b695446bb149cce6264e0abnd [] -> return state
0d0ba3a410038e179b695446bb149cce6264e0abnd -- anything else see if it is in a blocl of command
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh s ->
1a1356f375e36db7bee379ea0684ab389579f798rbowen case i_state $ intState state of
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen Nothing -> return $ genMsgAndCode ("Error on input line :" ++ s) 1 state
0d0ba3a410038e179b695446bb149cce6264e0abnd Just pS ->
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd if loadScript pS
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd then
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd do
bdd978e5ecd8daa2542d4d4e1988c78a622cd7f4nd let olds = script pS
oldextOpts = tsExtraOpts olds
let nwSt = state {
intState = (intState state) {
i_state = Just pS {
script = olds { tsExtraOpts = s : oldextOpts }
} } }
return $ add2hist [ScriptChange $ script pS] nwSt
else return $ genMsgAndCode ("Error on input line :" ++ s) 1 state
-- | Function to signal the interface that the script has ended
cEndScript :: CmdlState -> IO CmdlState
cEndScript state
= case i_state $ intState state of
Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
Just ps ->
if loadScript ps
then
do
let nwSt = state {
intState = (intState state) {
i_state = Just ps {
loadScript = False } } }
return $ add2hist [LoadScriptChange $ loadScript ps] nwSt
else return $ genMsgAndCode "No previous call of begin-script" 1 state
{- | Function to signal the interface that a scrips starts so it should
not try to parse the input -}
cStartScript :: CmdlState -> IO CmdlState
cStartScript state
= case i_state $ intState state of
Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
Just ps ->
return $ add2hist [LoadScriptChange $ loadScript ps] $
state {
intState = (intState state) {
i_state = Just ps {
loadScript = True } } }
-- sets a time limit
cTimeLimit :: String -> CmdlState -> IO CmdlState
cTimeLimit input state
= case i_state $ intState state of
Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
Just ps ->
if checkIntString $ trim input
then
do
let inpVal = read $ trim input
let oldS = script ps
return $ add2hist [ScriptChange $ script ps] $
state {
intState = (intState state) {
i_state = Just ps {
script = oldS { tsTimeLimit = inpVal } } } }
else return $ genMsgAndCode "Please insert a number of seconds" 1 state