{-# 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