{-# LANGUAGE CPP #-} {- | Module : ./CMDL/ProveCommands.hs Description : CMDL interface commands Copyright : uni-bremen and DFKI License : GPLv2 or higher, see LICENSE.txt Maintainer : r.pascanu@jacobs-university.de Stability : provisional Portability : portable CMDL.ProveCommands contains all commands (except prove\/consistency check) related to prove mode -} module CMDL.ProveCommands ( cTranslate , cDropTranslations , cGoalsAxmGeneral , cDoLoop , cProve , cDisprove , cProveAll , cSetUseThms , cSetSave2File , cEndScript , cStartScript , cTimeLimit , cNotACommand , cShowOutput ) where import CMDL.DataTypes (CmdlState (intState), CmdlGoalAxiom (..), CmdlListAction (..), ProveCmdType (..)) import CMDL.DataTypesUtils (add2hist, genMsgAndCode, genMessage, genAddMessage, getIdComorphism) import CMDL.DgCommands (selectANode) import CMDL.ProveConsistency (doLoop, sigIntHandler) import CMDL.Utils (checkIntString) import Common.Result (Result (Result)) import Common.Utils (trim, splitOn) import Data.List (find, nub) import Data.Maybe (fromMaybe) import Comorphisms.LogicGraph (lookupComorphism_in_LG) import Proofs.AbstractState import Logic.Comorphism (compComorphism, AnyComorphism (..)) import Logic.Logic (language_name) import Control.Concurrent (forkIO) import Control.Concurrent.MVar (newEmptyMVar, newMVar, takeMVar) import Control.Monad (foldM) #ifdef UNIX import System.Posix.Signals (Handler (Catch), installHandler, sigINT) #endif import Interfaces.GenericATPState (ATPTacticScript (tsTimeLimit, tsExtraOpts)) import Interfaces.DataTypes (ListChange (..), IntIState (..), Int_NodeInfo (..), UndoRedoElem (..), IntState (i_state)) -- | Drops any seleceted comorphism cDropTranslations :: CmdlState -> IO CmdlState cDropTranslations :: CmdlState -> IO CmdlState cDropTranslations state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> case IntIState -> Maybe AnyComorphism cComorphism IntIState pS of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return CmdlState state Just _ -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Maybe AnyComorphism -> UndoRedoElem CComorphismChange (Maybe AnyComorphism -> UndoRedoElem) -> Maybe AnyComorphism -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Maybe AnyComorphism cComorphism IntIState pS] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state ) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ IntIState pS { cComorphism :: Maybe AnyComorphism cComorphism = [Int_NodeInfo] -> Maybe AnyComorphism getIdComorphism ([Int_NodeInfo] -> Maybe AnyComorphism) -> [Int_NodeInfo] -> Maybe AnyComorphism forall a b. (a -> b) -> a -> b $ IntIState -> [Int_NodeInfo] elements IntIState pS } } } -- | select comorphisms cTranslate :: String -> CmdlState -> IO CmdlState cTranslate :: String -> CmdlState -> IO CmdlState cTranslate input :: String input state' :: CmdlState state' = (CmdlState -> String -> IO CmdlState) -> CmdlState -> [String] -> IO CmdlState forall (t :: * -> *) (m :: * -> *) b a. (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b foldM (\ state :: CmdlState state c :: String c -> case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of -- nothing selected ! Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> case String -> Result AnyComorphism lookupComorphism_in_LG String c of Result m :: [Diagnosis] m Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode ([Diagnosis] -> String forall a. Show a => a -> String show [Diagnosis] m) 1 CmdlState state Result _ (Just cm :: AnyComorphism cm) -> case IntIState -> Maybe AnyComorphism cComorphism IntIState pS of {- when selecting some theory the Id comorphism is automatically generated -} Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "No theory selected" 1 CmdlState state Just ocm :: AnyComorphism ocm -> case AnyComorphism -> AnyComorphism -> Result AnyComorphism forall (m :: * -> *). MonadFail m => AnyComorphism -> AnyComorphism -> m AnyComorphism compComorphism AnyComorphism ocm AnyComorphism cm of Result _ Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Can not add comorphism" 1 CmdlState state Result _ (Just smth :: AnyComorphism smth) -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> String -> CmdlState -> CmdlState genAddMessage [] ("Adding comorphism " String -> String -> String forall a. [a] -> [a] -> [a] ++ (\ (Comorphism c' :: cid c') -> cid -> String forall lid. Language lid => lid -> String language_name cid c') AnyComorphism cm) (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Maybe AnyComorphism -> UndoRedoElem CComorphismChange (Maybe AnyComorphism -> UndoRedoElem) -> Maybe AnyComorphism -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Maybe AnyComorphism cComorphism IntIState pS] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState pS { cComorphism :: Maybe AnyComorphism cComorphism = AnyComorphism -> Maybe AnyComorphism forall a. a -> Maybe a Just AnyComorphism smth } } }) (String -> String -> CmdlState -> CmdlState genMessage "" "" CmdlState state') ((String -> [String]) -> [String] -> [String] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (Char -> String -> [String] forall a. Eq a => a -> [a] -> [[a]] splitOn ';') ([String] -> [String]) -> [String] -> [String] forall a b. (a -> b) -> a -> b $ (String -> [String]) -> [String] -> [String] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (Char -> String -> [String] forall a. Eq a => a -> [a] -> [[a]] splitOn ':') ([String] -> [String]) -> [String] -> [String] forall a b. (a -> b) -> a -> b $ String -> [String] words (String -> [String]) -> String -> [String] forall a b. (a -> b) -> a -> b $ String -> String trim String input) parseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom -> [Int_NodeInfo] -> ([Int_NodeInfo], [ListChange]) -> ([Int_NodeInfo], [ListChange]) parseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom -> [Int_NodeInfo] -> ([Int_NodeInfo], [ListChange]) -> ([Int_NodeInfo], [ListChange]) parseElements action :: CmdlListAction action gls :: [String] gls gls_axm :: CmdlGoalAxiom gls_axm elems :: [Int_NodeInfo] elems (acc1 :: [Int_NodeInfo] acc1, acc2 :: [ListChange] acc2) = case [Int_NodeInfo] elems of [] -> ([Int_NodeInfo] acc1, [ListChange] acc2) Element st :: ProofState st nb :: Int nb : ll :: [Int_NodeInfo] ll -> let allgls :: [String] allgls = case CmdlGoalAxiom gls_axm of ChangeGoals -> ((String, Maybe BasicProof) -> String) -> [(String, Maybe BasicProof)] -> [String] forall a b. (a -> b) -> [a] -> [b] map (String, Maybe BasicProof) -> String forall a b. (a, b) -> a fst ([(String, Maybe BasicProof)] -> [String]) -> [(String, Maybe BasicProof)] -> [String] forall a b. (a -> b) -> a -> b $ ProofState -> [(String, Maybe BasicProof)] getGoals ProofState st ChangeAxioms -> ((String, Bool) -> String) -> [(String, Bool)] -> [String] forall a b. (a -> b) -> [a] -> [b] map (String, Bool) -> String forall a b. (a, b) -> a fst ([(String, Bool)] -> [String]) -> [(String, Bool)] -> [String] forall a b. (a -> b) -> a -> b $ ProofState -> [(String, Bool)] getAxioms ProofState st selgls :: [String] selgls = case CmdlGoalAxiom gls_axm of ChangeGoals -> ProofState -> [String] selectedGoals ProofState st ChangeAxioms -> ProofState -> [String] includedAxioms ProofState st fn' :: a -> a -> Bool fn' x :: a x y :: a y = a x a -> a -> Bool forall a. Eq a => a -> a -> Bool == a y fn :: t a -> a -> Bool fn ks :: t a ks x :: a x = case (a -> Bool) -> t a -> Maybe a forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find (a -> a -> Bool forall a. Eq a => a -> a -> Bool fn' a x) t a ks of Just _ -> case CmdlListAction action of ActionDel -> Bool False _ -> Bool True Nothing -> case CmdlListAction action of ActionDel -> Bool True _ -> Bool False gls' :: [String] gls' = case CmdlListAction action of ActionDelAll -> [] ActionDel -> (String -> Bool) -> [String] -> [String] forall a. (a -> Bool) -> [a] -> [a] filter ([String] -> String -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> a -> Bool fn [String] selgls) [String] gls ActionSetAll -> [String] allgls ActionSet -> (String -> Bool) -> [String] -> [String] forall a. (a -> Bool) -> [a] -> [a] filter ([String] -> String -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> a -> Bool fn [String] allgls) [String] gls ActionAdd -> [String] -> [String] forall a. Eq a => [a] -> [a] nub ([String] -> [String]) -> [String] -> [String] forall a b. (a -> b) -> a -> b $ [String] selgls [String] -> [String] -> [String] forall a. [a] -> [a] -> [a] ++ (String -> Bool) -> [String] -> [String] forall a. (a -> Bool) -> [a] -> [a] filter ([String] -> String -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> a -> Bool fn [String] allgls) [String] gls nwelm :: Int_NodeInfo nwelm = case CmdlGoalAxiom gls_axm of ChangeGoals -> ProofState -> Int -> Int_NodeInfo Element (ProofState st {selectedGoals :: [String] selectedGoals = [String] gls'}) Int nb ChangeAxioms -> ProofState -> Int -> Int_NodeInfo Element (ProofState st {includedAxioms :: [String] includedAxioms = [String] gls'}) Int nb hchg :: ListChange hchg = case CmdlGoalAxiom gls_axm of ChangeGoals -> [String] -> Int -> ListChange GoalsChange (ProofState -> [String] selectedGoals ProofState st) Int nb ChangeAxioms -> [String] -> Int -> ListChange AxiomsChange (ProofState -> [String] includedAxioms ProofState st) Int nb in CmdlListAction -> [String] -> CmdlGoalAxiom -> [Int_NodeInfo] -> ([Int_NodeInfo], [ListChange]) -> ([Int_NodeInfo], [ListChange]) parseElements CmdlListAction action [String] gls CmdlGoalAxiom gls_axm [Int_NodeInfo] ll (Int_NodeInfo nwelm Int_NodeInfo -> [Int_NodeInfo] -> [Int_NodeInfo] forall a. a -> [a] -> [a] : [Int_NodeInfo] acc1, ListChange hchg ListChange -> [ListChange] -> [ListChange] forall a. a -> [a] -> [a] : [ListChange] acc2) {- | A general function that implements the actions of setting, adding or deleting goals or axioms from the selection list -} cGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState cGoalsAxmGeneral :: CmdlListAction -> CmdlGoalAxiom -> String -> CmdlState -> IO CmdlState cGoalsAxmGeneral action :: CmdlListAction action gls_axm :: CmdlGoalAxiom gls_axm input :: String input state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> case IntIState -> [Int_NodeInfo] elements IntIState pS of [] -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state ls :: [Int_NodeInfo] ls -> do let gls :: [String] gls = String -> [String] words String input let (ls' :: [Int_NodeInfo] ls', hst :: [ListChange] hst) = CmdlListAction -> [String] -> CmdlGoalAxiom -> [Int_NodeInfo] -> ([Int_NodeInfo], [ListChange]) -> ([Int_NodeInfo], [ListChange]) parseElements CmdlListAction action [String] gls CmdlGoalAxiom gls_axm [Int_NodeInfo] ls ([], []) CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [[ListChange] -> UndoRedoElem ListChange [ListChange] hst] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState pS { elements :: [Int_NodeInfo] elements = [Int_NodeInfo] ls' } } } cDoLoop :: ProveCmdType -> CmdlState -> IO CmdlState cDoLoop :: ProveCmdType -> CmdlState -> IO CmdlState cDoLoop proveCmdType :: ProveCmdType proveCmdType state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> case IntIState -> [Int_NodeInfo] elements IntIState pS of [] -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state ls :: [Int_NodeInfo] ls -> do -- create initial mVars to comunicate MVar IntState miSt <- IntState -> IO (MVar IntState) forall a. a -> IO (MVar a) newMVar (IntState -> IO (MVar IntState)) -> IntState -> IO (MVar IntState) forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state MVar (Maybe Int_NodeInfo) mSt <- Maybe Int_NodeInfo -> IO (MVar (Maybe Int_NodeInfo)) forall a. a -> IO (MVar a) newMVar Maybe Int_NodeInfo forall a. Maybe a Nothing MVar (Maybe ThreadId) mThr <- Maybe ThreadId -> IO (MVar (Maybe ThreadId)) forall a. a -> IO (MVar a) newMVar Maybe ThreadId forall a. Maybe a Nothing MVar IntState mW <- IO (MVar IntState) forall a. IO (MVar a) newEmptyMVar -- fork ThreadId thrID <- IO () -> IO ThreadId forkIO (MVar IntState -> MVar (Maybe ThreadId) -> MVar (Maybe Int_NodeInfo) -> MVar IntState -> [Int_NodeInfo] -> ProveCmdType -> IO () doLoop MVar IntState miSt MVar (Maybe ThreadId) mThr MVar (Maybe Int_NodeInfo) mSt MVar IntState mW [Int_NodeInfo] ls ProveCmdType proveCmdType) -- install the handler that waits for SIG_INT #ifdef UNIX Handler oldHandler <- Signal -> Handler -> Maybe SignalSet -> IO Handler installHandler Signal sigINT (IO () -> Handler Catch (IO () -> Handler) -> IO () -> Handler forall a b. (a -> b) -> a -> b $ MVar (Maybe ThreadId) -> MVar IntState -> MVar (Maybe Int_NodeInfo) -> ThreadId -> MVar IntState -> LibName -> IO () sigIntHandler MVar (Maybe ThreadId) mThr MVar IntState miSt MVar (Maybe Int_NodeInfo) mSt ThreadId thrID MVar IntState mW (IntIState -> LibName i_ln IntIState pS) ) Maybe SignalSet forall a. Maybe a Nothing #endif -- block and wait for answers IntState answ <- MVar IntState -> IO IntState forall a. MVar a -> IO a takeMVar MVar IntState mW #ifdef UNIX Signal -> Handler -> Maybe SignalSet -> IO Handler installHandler Signal sigINT Handler oldHandler Maybe SignalSet forall a. Maybe a Nothing #endif let nwpS :: IntIState nwpS = IntIState -> Maybe IntIState -> IntIState forall a. a -> Maybe a -> a fromMaybe IntIState pS (IntState -> Maybe IntIState i_state IntState answ) nwls :: [Int_NodeInfo] nwls = (Int_NodeInfo -> [Int_NodeInfo]) -> [Int_NodeInfo] -> [Int_NodeInfo] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (\ (Element _ x :: Int x) -> Int -> IntIState -> [Int_NodeInfo] selectANode Int x IntIState nwpS) [Int_NodeInfo] ls hst :: [ListChange] hst = (Int_NodeInfo -> [ListChange]) -> [Int_NodeInfo] -> [ListChange] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (\ (Element stt :: ProofState stt x :: Int x) -> [ [String] -> Int -> ListChange AxiomsChange (ProofState -> [String] includedAxioms ProofState stt) Int x , [String] -> Int -> ListChange GoalsChange (ProofState -> [String] selectedGoals ProofState stt) Int x ]) [Int_NodeInfo] ls CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [[ListChange] -> UndoRedoElem ListChange [ListChange] hst] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = IntState answ { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ IntIState nwpS { elements :: [Int_NodeInfo] elements = [Int_NodeInfo] nwls }}} {- | Proves only selected goals from all nodes using selected axioms -} cProve :: CmdlState -> IO CmdlState cProve :: CmdlState -> IO CmdlState cProve = ProveCmdType -> CmdlState -> IO CmdlState cDoLoop ProveCmdType Prove cDisprove :: CmdlState -> IO CmdlState cDisprove :: CmdlState -> IO CmdlState cDisprove = ProveCmdType -> CmdlState -> IO CmdlState cDoLoop ProveCmdType Disprove {- | Proves all goals in the nodes selected using all axioms and theorems -} cProveAll :: CmdlState -> IO CmdlState cProveAll :: CmdlState -> IO CmdlState cProveAll state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> case IntIState -> [Int_NodeInfo] elements IntIState pS of [] -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state ls :: [Int_NodeInfo] ls -> let ls' :: [Int_NodeInfo] ls' = (Int_NodeInfo -> Int_NodeInfo) -> [Int_NodeInfo] -> [Int_NodeInfo] forall a b. (a -> b) -> [a] -> [b] map (\ (Element st :: ProofState st nb :: Int nb) -> ProofState -> Int -> Int_NodeInfo Element (ProofState -> ProofState resetSelection ProofState st) Int nb) [Int_NodeInfo] ls nwSt :: CmdlState nwSt = [UndoRedoElem] -> CmdlState -> CmdlState add2hist [[ListChange] -> UndoRedoElem ListChange [[Int_NodeInfo] -> ListChange NodesChange ([Int_NodeInfo] -> ListChange) -> [Int_NodeInfo] -> ListChange forall a b. (a -> b) -> a -> b $ IntIState -> [Int_NodeInfo] elements IntIState pS]] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ IntIState pS { elements :: [Int_NodeInfo] elements = [Int_NodeInfo] ls' } } } in CmdlState -> IO CmdlState cProve CmdlState nwSt -- | Sets the use theorems flag of the interface cSetUseThms :: Bool -> CmdlState -> IO CmdlState cSetUseThms :: Bool -> CmdlState -> IO CmdlState cSetUseThms val :: Bool val state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Bool -> UndoRedoElem UseThmChange (Bool -> UndoRedoElem) -> Bool -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Bool useTheorems IntIState pS] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState pS { useTheorems :: Bool useTheorems = Bool val } } } cShowOutput :: Bool -> CmdlState -> IO CmdlState cShowOutput :: Bool -> CmdlState -> IO CmdlState cShowOutput b :: Bool b state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just pS :: IntIState pS -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Bool -> UndoRedoElem ChShowOutput (Bool -> UndoRedoElem) -> Bool -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Bool showOutput IntIState pS] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState pS { showOutput :: Bool showOutput = Bool b } } } -- | Sets the save2File value to either true or false cSetSave2File :: Bool -> CmdlState -> IO CmdlState cSetSave2File :: Bool -> CmdlState -> IO CmdlState cSetSave2File val :: Bool val state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just ps :: IntIState ps -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Bool -> UndoRedoElem Save2FileChange (Bool -> UndoRedoElem) -> Bool -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Bool save2file IntIState ps] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState ps { save2file :: Bool save2file = Bool val } } } {- | The function is called everytime when the input could not be parsed as a command -} cNotACommand :: String -> CmdlState -> IO CmdlState cNotACommand :: String -> CmdlState -> IO CmdlState cNotACommand input :: String input state :: CmdlState state = case String input of -- if input line is empty do nothing [] -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return CmdlState state -- anything else see if it is in a blocl of command s :: String s -> case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode ("Error on input line :" String -> String -> String forall a. [a] -> [a] -> [a] ++ String s) 1 CmdlState state Just pS :: IntIState pS -> if IntIState -> Bool loadScript IntIState pS then do let olds :: ATPTacticScript olds = IntIState -> ATPTacticScript script IntIState pS oldextOpts :: [String] oldextOpts = ATPTacticScript -> [String] tsExtraOpts ATPTacticScript olds let nwSt :: CmdlState nwSt = CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState pS { script :: ATPTacticScript script = ATPTacticScript olds { tsExtraOpts :: [String] tsExtraOpts = String s String -> [String] -> [String] forall a. a -> [a] -> [a] : [String] oldextOpts } } } } CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [ATPTacticScript -> UndoRedoElem ScriptChange (ATPTacticScript -> UndoRedoElem) -> ATPTacticScript -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> ATPTacticScript script IntIState pS] CmdlState nwSt else CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode ("Error on input line :" String -> String -> String forall a. [a] -> [a] -> [a] ++ String s) 1 CmdlState state -- | Function to signal the interface that the script has ended cEndScript :: CmdlState -> IO CmdlState cEndScript :: CmdlState -> IO CmdlState cEndScript state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just ps :: IntIState ps -> if IntIState -> Bool loadScript IntIState ps then do let nwSt :: CmdlState nwSt = CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState ps { loadScript :: Bool loadScript = Bool False } } } CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Bool -> UndoRedoElem LoadScriptChange (Bool -> UndoRedoElem) -> Bool -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Bool loadScript IntIState ps] CmdlState nwSt else CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "No previous call of begin-script" 1 CmdlState state {- | Function to signal the interface that a scrips starts so it should not try to parse the input -} cStartScript :: CmdlState -> IO CmdlState cStartScript :: CmdlState -> IO CmdlState cStartScript state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just ps :: IntIState ps -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [Bool -> UndoRedoElem LoadScriptChange (Bool -> UndoRedoElem) -> Bool -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> Bool loadScript IntIState ps] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState ps { loadScript :: Bool loadScript = Bool True } } } -- sets a time limit cTimeLimit :: String -> CmdlState -> IO CmdlState cTimeLimit :: String -> CmdlState -> IO CmdlState cTimeLimit input :: String input state :: CmdlState state = case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState state of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Nothing selected" 1 CmdlState state Just ps :: IntIState ps -> if String -> Bool checkIntString (String -> Bool) -> String -> Bool forall a b. (a -> b) -> a -> b $ String -> String trim String input then do let inpVal :: Int inpVal = String -> Int forall a. Read a => String -> a read (String -> Int) -> String -> Int forall a b. (a -> b) -> a -> b $ String -> String trim String input let oldS :: ATPTacticScript oldS = IntIState -> ATPTacticScript script IntIState ps CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ [UndoRedoElem] -> CmdlState -> CmdlState add2hist [ATPTacticScript -> UndoRedoElem ScriptChange (ATPTacticScript -> UndoRedoElem) -> ATPTacticScript -> UndoRedoElem forall a b. (a -> b) -> a -> b $ IntIState -> ATPTacticScript script IntIState ps] (CmdlState -> CmdlState) -> CmdlState -> CmdlState forall a b. (a -> b) -> a -> b $ CmdlState state { intState :: IntState intState = (CmdlState -> IntState intState CmdlState state) { i_state :: Maybe IntIState i_state = IntIState -> Maybe IntIState forall a. a -> Maybe a Just IntIState ps { script :: ATPTacticScript script = ATPTacticScript oldS { tsTimeLimit :: Int tsTimeLimit = Int inpVal } } } } else CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> Int -> CmdlState -> CmdlState genMsgAndCode "Please insert a number of seconds" 1 CmdlState state