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