hets/CMDL/ProveCommands.hs

	ProveCommands.hs revision c3f7e132e0c214b755c6c4b485f4748c4dd1595c
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{-# LANGUAGE CPP #-}
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{- |
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederModule      : $Header$
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeDescription : CMDL interface commands
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright   : uni-bremen and DFKI
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeLicense     : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeMaintainer  : r.pascanu@jacobs-university.de
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability   : provisional
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : portable
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederCMDL.ProveCommands contains all commands (except prove\/consistency check)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederrelated to prove mode
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-}
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkemodule CMDL.ProveCommands
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       ( cTranslate
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cDropTranslations
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cGoalsAxmGeneral
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cDoLoop
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cProve
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cProveAll
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cSetUseThms
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       , cSetSave2File
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       , cEndScript
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       , cStartScript
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       , cTimeLimit
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       , cNotACommand
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       ) where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport CMDL.DataTypes(CmdlState(intState), CmdlGoalAxiom(..),
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                      CmdlListAction(..))
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport CMDL.DataTypesUtils(add2hist, genErrorMsg, genMessage, getIdComorphism)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport CMDL.DgCommands(selectANode)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport CMDL.ProveConsistency(doLoop, sigIntHandler)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport CMDL.Utils(checkIntString)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Static.GTheory(G_theory(G_theory))
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Common.Result(Result(Result))
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Common.OrderedMap as OMap
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Common.Utils(trim)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Data.List (find, nub)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Comorphisms.LogicGraph(lookupComorphism_in_LG)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Proofs.AbstractState(ProofState(..))
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Logic.Comorphism(compComorphism)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Control.Concurrent(forkIO)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Control.Concurrent.MVar(newEmptyMVar, newMVar, takeMVar)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke#ifdef UNIX
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport System.Posix.Signals(Handler(Catch), installHandler, sigINT)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke#endif
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Interfaces.GenericATPState(ATPTacticScript(tsTimeLimit, tsExtraOpts))
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Interfaces.DataTypes(ListChange(..), IntIState(..), Int_NodeInfo(..),
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke                            UndoRedoElem(..), IntState(i_state))
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder-- | Drops any seleceted comorphism
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecDropTranslations :: CmdlState -> IO CmdlState
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercDropTranslations state =
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case i_state $ intState state of
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke   Nothing -> return $ genErrorMsg "Nothing selected" state
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke   Just pS ->
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder    case cComorphism pS of
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder     Nothing -> return state
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke     Just _ -> return $
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       add2hist [CComorphismChange $ cComorphism pS] $
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke        state {
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke          intState = (intState state ) {
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke           i_state = Just $ pS {
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke              cComorphism = getIdComorphism $ elements pS } }
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke         }
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | select comorphisms
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecTranslate::String -> CmdlState -> IO CmdlState
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercTranslate input state =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder case i_state $ intState state of
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke  -- nothing selected !
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke  Nothing -> return $ genErrorMsg "Nothing selected" state
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke  Just pS ->
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder   -- parse the comorphism name
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder   case lookupComorphism_in_LG $ trim input of
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder    Result _ Nothing -> return $ genErrorMsg "Wrong comorphism name" state
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder    Result _ (Just cm) ->
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder      case cComorphism pS of
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       -- when selecting some theory the Id comorphism is automatically
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder       -- generated
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       Nothing -> return $ genErrorMsg "No theory selected" state
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke       Just ocm ->
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke        case compComorphism ocm cm of
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke            Result _ Nothing ->
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke             return $ genErrorMsg "Can not add comorphism" state
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke            Result _ (Just smth) ->
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke              return $ genMessage [] "Adding comorphism"
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke                     $ add2hist [CComorphismChange $ cComorphism pS] $
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                      state {
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                        intState = (intState state) {
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                         i_state = Just pS {
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                                    cComorphism = Just smth } }
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                          }
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeparseElements :: CmdlListAction -> [String] -> CmdlGoalAxiom
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke                 -> [Int_NodeInfo]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder                 -> ([Int_NodeInfo],[ListChange])
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke                 -> ([Int_NodeInfo],[ListChange])
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeparseElements action gls gls_axm elems (acc1,acc2)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke = case elems of
    [] -> (acc1,acc2)
    (Element st nb):ll ->
      let allgls = case gls_axm of
                    ChangeGoals -> OMap.keys $ goalMap st
                    ChangeAxioms-> case theory st of
                                 G_theory _ _ _ aMap _ ->
                                  OMap.keys aMap
          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 $ genErrorMsg "Nothing selected" state
    Just pS ->
     case elements pS of
      [] -> return $ genErrorMsg "Nothing selected" 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 :: Bool -- True = prove, False = consChecker
        -> CmdlState
        -> IO CmdlState
cDoLoop prvr state
 = case i_state $ intState state of
    Nothing -> return $ genErrorMsg "Nothing selected" state
    Just pS ->
        case elements pS of
         [] -> return $ genErrorMsg "Nothing selected" state
         ls ->
           do
            --create initial mVars to comunicate
            mlbEnv <- newMVar $ i_libEnv pS
            mSt    <- newMVar Nothing
            mThr   <- newMVar Nothing
            mW     <- newEmptyMVar
            -- fork
            thrID <- forkIO(doLoop mlbEnv mThr mSt mW pS ls prvr)
            -- install the handler that waits for SIG_INT
#ifdef UNIX
            oldHandler <- installHandler sigINT (Catch $
                     sigIntHandler mThr mlbEnv 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 = pS { i_libEnv = answ }
            let nwls = concatMap(\(Element _ x) -> selectANode x nwpS) ls
                hst = concatMap(\(Element stt x)  ->
                                 [(AxiomsChange (includedAxioms stt) x),
                                  (GoalsChange (selectedGoals stt) x)]) ls
            return $ add2hist [(DgCommandChange $ i_ln nwpS),
                               (ListChange hst)] $
                         state {
                           intState = (intState state) {
                             i_state = Just $ pS { elements = nwls } }
                         }

-- | Proves only selected goals from all nodes using selected
-- axioms
cProve :: CmdlState -> IO CmdlState
cProve = cDoLoop True

-- | 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$ genErrorMsg "Nothing selected" state
    Just pS ->
        case elements pS of
         [] -> return $ genErrorMsg "Nothing selected" state
         ls ->
           do
            let ls' = map (\(Element st nb) ->
                              case theory st of
                               G_theory _ _ _ aMap _ ->
                                Element
                                  (st {
                                     selectedGoals = OMap.keys $
                                                       goalMap st,
                                     includedAxioms = OMap.keys aMap,
                                     includedTheorems = OMap.keys $
                                                         goalMap st
                                    }) nb ) ls
            let nwSt = add2hist [ListChange [NodesChange $ elements pS]] $
                      state {
                       intState = (intState state) {
                         i_state = Just $ pS {
                                           elements = ls' } } }
            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 $ genErrorMsg "Norhing selected" state
    Just pS ->
      return $ add2hist [UseThmChange $ useTheorems pS] $
          state {
           intState = (intState state) {
             i_state=  Just pS {
                             useTheorems = val } } }

-- | 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 $ genErrorMsg "Nothing selected" 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 $ genErrorMsg ("Error on input line :"++s) 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 $ genErrorMsg ("Error on input line :"++s) 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 $ genErrorMsg "Nothing selected" 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 $ genErrorMsg "No previous call of begin-script" 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 $ genErrorMsg "Nothing selected" 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 $ genErrorMsg "Nothing selected" 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 $ genErrorMsg "Please insert a number of seconds" state