hets/CMDL/ProveCommands.hs

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