content: {-# 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 state =
   case i_state $ intState state of
     Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
     Just pS ->
      case cComorphism pS of
       Nothing -> return state
       Just _ -> return $
         add2hist [CComorphismChange $ cComorphism pS] $
          state {
            intState = (intState state ) {
             i_state = Just $ pS {
                cComorphism = getIdComorphism $ elements pS } }
           }
  
  
  -- | select comorphisms
  cTranslate :: String -> CmdlState -> IO CmdlState
  cTranslate input state' =
   foldM (\ state c -> case i_state $ intState state of
     -- nothing selected !
     Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
     Just pS -> case lookupComorphism_in_LG c of
      Result m Nothing -> return $ genMsgAndCode (show m) 1 state
      Result _ (Just cm) ->
        case cComorphism pS of
         {- when selecting some theory the Id comorphism is automatically
            generated -}
         Nothing -> return $ genMsgAndCode "No theory selected" 1 state
         Just ocm ->
          case compComorphism ocm cm of
              Result _ Nothing ->
               return $ genMsgAndCode "Can not add comorphism" 1 state
              Result _ (Just smth) ->
                return $ genAddMessage [] ("Adding comorphism " ++
                          (\ (Comorphism c') -> language_name c') cm)
                       $ add2hist [CComorphismChange $ cComorphism pS] $
                        state {
                          intState = (intState state) {
                           i_state = Just pS {
                                      cComorphism = Just smth } }
                            }) (genMessage "" "" state')
                               (concatMap (splitOn ';') $
                                concatMap (splitOn ':') $
                                words $ trim input)
  
  
  parseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom
                   -> [Int_NodeInfo]
                   -> ([Int_NodeInfo], [ListChange])
                   -> ([Int_NodeInfo], [ListChange])
  parseElements action gls gls_axm elems (acc1, acc2)
   = case elems of
      [] -> (acc1, acc2)
      Element st nb : ll ->
        let allgls = case gls_axm of
                      ChangeGoals -> map fst $ getGoals st
                      ChangeAxioms -> map fst $ getAxioms st
            selgls = case gls_axm of
                      ChangeGoals -> selectedGoals st
                      ChangeAxioms -> includedAxioms st
            fn' x y = x == y
            fn ks x = case find (fn' x) ks of
                       Just _ ->
                        case action of
                         ActionDel -> False
                         _ -> True
                       Nothing ->
                        case action of
                         ActionDel -> True
                         _ -> False
            gls' = case action of
                     ActionDelAll -> []
                     ActionDel -> filter (fn selgls) gls
                     ActionSetAll -> allgls
                     ActionSet -> filter (fn allgls) gls
                     ActionAdd -> nub $ selgls ++ filter (fn allgls) gls
            nwelm = case gls_axm of
                     ChangeGoals -> Element (st {selectedGoals = gls'}) nb
                     ChangeAxioms -> Element (st {includedAxioms = gls'}) nb
            hchg = case gls_axm of
                     ChangeGoals -> GoalsChange (selectedGoals st) nb
                     ChangeAxioms -> AxiomsChange (includedAxioms st) nb
         in parseElements action gls gls_axm ll (nwelm : acc1, hchg : 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 action gls_axm input state
   = case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
       case elements pS of
        [] -> return $ genMsgAndCode "Nothing selected" 1 state
        ls ->
         do
          let gls = words input
          let (ls', hst) = parseElements action gls
                             gls_axm
                             ls ([], [])
          return $ add2hist [ListChange hst] $
                      state {
                        intState = (intState state) {
                          i_state = Just pS {
                                           elements = ls'
                                           }
                               }
                       }
  
  cDoLoop ::
          ProveCmdType
          -> CmdlState
          -> IO CmdlState
  cDoLoop proveCmdType state
   = case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
          case elements pS of
           [] -> return $ genMsgAndCode "Nothing selected" 1 state
           ls ->
             do
              -- create initial mVars to comunicate
              miSt <- newMVar $ intState state
              mSt <- newMVar Nothing
              mThr <- newMVar Nothing
              mW <- newEmptyMVar
              -- fork
              thrID <- forkIO (doLoop miSt mThr mSt mW ls proveCmdType)
              -- install the handler that waits for SIG_INT
  #ifdef UNIX
              oldHandler <- installHandler sigINT (Catch $
                       sigIntHandler mThr miSt mSt thrID mW (i_ln pS)
                                    ) Nothing
  #endif
              -- block and wait for answers
              answ <- takeMVar mW
  #ifdef UNIX
              installHandler sigINT oldHandler Nothing
  #endif
              let nwpS = fromMaybe pS (i_state answ)
                  nwls = concatMap (\ (Element _ x) -> selectANode x nwpS) ls
                  hst = concatMap (\ (Element stt x) ->
                                   [ AxiomsChange (includedAxioms stt) x
                                   , GoalsChange (selectedGoals stt) x ]) ls
              return $ add2hist [ListChange hst] $
                         state { intState = answ {
                           i_state = Just $ nwpS { elements = nwls }}}
  
  {- | Proves only selected goals from all nodes using selected
     axioms -}
  cProve :: CmdlState -> IO CmdlState
  cProve = cDoLoop Prove
  
  cDisprove :: CmdlState -> IO CmdlState
  cDisprove = cDoLoop Disprove
  
  {- | Proves all goals in the nodes selected using all axioms and
     theorems -}
  cProveAll :: CmdlState -> IO CmdlState
  cProveAll state
   = case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
          case elements pS of
           [] -> return $ genMsgAndCode "Nothing selected" 1 state
           ls ->
              let ls' = map (\ (Element st nb) ->
                                 Element (resetSelection st) nb) ls
                  nwSt = add2hist [ListChange [NodesChange $ elements pS]] $
                        state {
                         intState = (intState state) {
                           i_state = Just $ pS { elements = ls' } } }
              in cProve nwSt
  
  -- | Sets the use theorems flag of the interface
  cSetUseThms :: Bool -> CmdlState -> IO CmdlState
  cSetUseThms val state
   = case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
        return $ add2hist [UseThmChange $ useTheorems pS] $
            state {
             intState = (intState state) {
               i_state = Just pS {
                               useTheorems = val } } }
  
  cShowOutput :: Bool -> CmdlState -> IO CmdlState
  cShowOutput b state =
    case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS -> return $ add2hist [ChShowOutput $ showOutput pS] $
         state {
                  intState = (intState state) {
                    i_state = Just pS {
                                    showOutput = b } } }
  
  -- | Sets the save2File value to either true or false
  cSetSave2File :: Bool -> CmdlState -> IO CmdlState
  cSetSave2File val state
   = case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just ps ->
        return $ add2hist [Save2FileChange $ save2file ps] $
            state {
              intState = (intState state) {
               i_state = Just ps { save2file = val } } }
  
  
  {- | The function is called everytime when the input could
     not be parsed as a command -}
  cNotACommand :: String -> CmdlState -> IO CmdlState
  cNotACommand input state
   = case input of
       -- if input line is empty do nothing
       [] -> return state
       -- anything else see if it is in a blocl of command
       s ->
        case i_state $ intState state of
          Nothing -> return $ genMsgAndCode ("Error on input line :" ++ s) 1 state
          Just pS ->
            if loadScript pS
              then
               do
                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
  