content: {- |
  Module      : ./CMDL/ProveConsistency.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.ProveConsistency contains prove and consistency check command
  -}
  
  
  module CMDL.ProveConsistency
         ( cProver
         , cConsChecker
         , doLoop
         , sigIntHandler
         ) where
  
  import Interfaces.Command
  import Interfaces.DataTypes
  import Interfaces.GenericATPState (ATPTacticScript (..))
  import Interfaces.History
  import Interfaces.Utils
  
  import CMDL.DataTypes (CmdlState (intState), ProveCmdType (..))
  import CMDL.DataTypesUtils
  
  import Comorphisms.LogicGraph (logicGraph)
  
  import Proofs.AbstractState
  
  import Static.DevGraph
  import Static.DgUtils
  import Static.History
  
  import Common.DocUtils
  
  import Logic.Comorphism
  import Logic.Grothendieck
  import Logic.Logic
  import Logic.Prover as P
  import Logic.Coerce
  
  import Common.Consistency
  import Common.LibName (LibName)
  import Common.Result (Result (Result))
  import Common.Utils (trim)
  
  import qualified Common.OrderedMap as OMap
  import Common.AS_Annotation
  
  import Data.List
  import qualified Data.Map as Map
  
  import Control.Concurrent (ThreadId, killThread)
  import Control.Concurrent.MVar (MVar, newMVar, putMVar, takeMVar, readMVar,
                                 swapMVar, modifyMVar_)
  
  import Control.Monad
  
  import Data.Foldable (forM_)
  
  negate_th_with_cons_checker :: G_theory_with_cons_checker -> String ->
                                 Maybe G_theory_with_cons_checker
  negate_th_with_cons_checker g_th goal = case g_th of
    G_theory_with_cons_checker lid1 th cons_check ->
      case P.tTarget th of
        P.Theory lid2 sens -> case OMap.lookup goal sens of
          Nothing -> Nothing
          Just sen -> case negation lid1 $ sentence sen of
                                  Nothing -> Nothing
                                  Just sen' -> let
                                    negSen = sen { sentence = sen',
                                                   isAxiom = True }
                                    sens' = OMap.insert goal negSen $
                                             OMap.filter isAxiom sens
                                    target' = P.Theory lid2 sens'
                                   in Just $ G_theory_with_cons_checker lid1 th
                                              {P.tTarget = target'} cons_check
  
  getProversAutomatic :: G_sublogics -> IO [(G_prover, AnyComorphism)]
  getProversAutomatic sl = getUsableProvers P.ProveCMDLautomatic sl logicGraph
  
  -- | Select a prover
  cProver :: String -> CmdlState -> IO CmdlState
  cProver input state =
    do
     -- trimed input
     let inp = trim input
     case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
       -- check that some theories are selected
       case elements pS of
        [] -> return $ genMsgAndCode "Nothing selected" 1 state
        Element z _ : _ -> do
          prov <- getProversAutomatic (sublogicOfTheory z)
          let pl = filter ((== inp) . getProverName . fst) prov
              prover_names = map (getProverName . fst) prov
          case case cComorphism pS of
                     Nothing -> pl
                     Just x -> filter ((== x) . snd) pl ++ pl of
               [] -> if inp == "" then do
                              mapM_ putStrLn (nub prover_names)
                              return state
                                 else return (genMsgAndCode
                   ("No applicable prover with name \"" ++ inp ++ "\" found") 1
                   state)
               (p, nCm@(Comorphism cid)) : _ ->
                 return $ add2hist [ ProverChange $ prover pS
                                   , CComorphismChange $ cComorphism pS ]
                       $ genMessage "" ("Hint: Using comorphism `"
                              ++ language_name cid ++ "`")
                              state {
                                intState = (intState state) {
                                  i_state = Just pS
                                               { cComorphism = Just nCm
                                               , prover = Just p } } }
  
  -- | Selects a consistency checker
  cConsChecker :: String -> CmdlState -> IO CmdlState
  cConsChecker input state =
    do
     -- trimed input
     let inp = trim input
     case i_state $ intState state of
      Nothing -> return $ genMsgAndCode "Nothing selected" 1 state
      Just pS ->
       -- check that some theories are selected
       case elements pS of
        [] -> return $ genMsgAndCode "Nothing selected" 1 state
        Element z _ : _ ->
         do
          consCheckList <- getConsCheckers $ findComorphismPaths
                                  logicGraph $ sublogicOfTheory z
          -- see if any comorphism was used
          case cComorphism pS of
          {- if none use the theory of the first selected node
          to find possible comorphisms -}
           Nothing -> case find (\ (y, _) -> getCcName y == inp) consCheckList of
                      Nothing -> if inp == "" then do
                                              let shortConsCList = nub $ map
                                                   (\ (y, _) -> getCcName y)
                                                   consCheckList
                                              mapM_ putStrLn shortConsCList
                                              return state
                                            else return $ genMsgAndCode
                                  ("No applicable " ++
                                   "consistency checker with this name found") 1
                                   state
                      Just (p, _) -> return $ add2hist
                                      [ConsCheckerChange $ consChecker pS]
                                      state {
                                        intState = (intState state) {
                                           i_state = Just pS {
                                               consChecker = Just p }
                                            }
                                        }
           Just x -> do
            cs <- getConsCheckers [x]
            case find (\ (y, _) -> getCcName y == inp) cs of
             Nothing ->
              case find (\ (y, _) -> getCcName y == inp) consCheckList of
               Nothing -> if inp == "" then do
                                              let shortConsCList = nub $ map
                                                   (\ (y, _) -> getCcName y)
                                                   consCheckList
                                              mapM_ putStrLn shortConsCList
                                              return state
                                      else return $ genMsgAndCode
                                  ("No applicable " ++
                                   "consistency checker with this name found") 1
                                   state
               Just (p, nCm@(Comorphism cid)) ->
                 return $ add2hist [ ConsCheckerChange $ consChecker pS
                                   , CComorphismChange $ cComorphism pS ]
                    $ genMessage "" ("Hint: Using default comorphism `"
                        ++ language_name cid ++ "`")
                        state {
                         intState = (intState state) {
                           i_state = Just pS {
                                      cComorphism = Just nCm,
                                      consChecker = Just p } } }
             Just (p, _) -> return
                             $ add2hist [ConsCheckerChange $ consChecker pS]
                              $ state {
                              intState = (intState state) {
                                i_state = Just pS { consChecker = Just p } } }
  
  {- | Given a proofstatus the function does the actual call of the
  prover for consistency checking -}
  
  checkNode ::
                -- Tactic script
                ATPTacticScript ->
                {- proofState of the node that needs proving
                all theorems, goals and axioms should have
                been selected before, but the theory should have
                not been recomputed -}
                Int_NodeInfo ->
                -- node name
                String ->
                {- selected prover, if non one will be automatically
                selected -}
                Maybe G_cons_checker ->
                {- selected comorphism, if non one will be automatically
                selected -}
                Maybe AnyComorphism ->
                MVar (Maybe Int_NodeInfo) ->
                MVar IntState ->
                LibName ->
                -- returns an error message if anything happens
                IO String
  checkNode sTxt ndpf ndnm mp mcm mSt miSt ln =
    case ndpf of
      Element pf_st nd ->
       do
       {- recompute the theory (to make effective the selected axioms,
       goals) !? needed? -}
       let st = recalculateSublogicAndSelectedTheory pf_st
       {- compute a prover,comorphism pair to be used in preparing
       the theory -}
       p_cm@(_, acm) <- case mcm of
             Nothing -> lookupKnownConsChecker st
             Just cm' -> case mp of
               Nothing -> lookupKnownConsChecker st
               Just p' -> return (p', cm')
  
       -- try to prepare the theory
       prep <- case prepareForConsChecking st p_cm of
               Result _ Nothing ->
                 do
                  p_cm'@(prv', acm'@(Comorphism cid)) <-
                            lookupKnownConsChecker st
                  putStrLn ("Analyzing node for consistency " ++ ndnm)
                  putStrLn ("Using the comorphism " ++ language_name cid)
                  putStrLn ("Using consistency checker " ++ getCcName prv')
                  return $ case prepareForConsChecking st p_cm' of
                            Result _ Nothing -> Nothing
                            Result _ (Just sm) -> Just (sm, acm')
               Result _ (Just sm) -> return $ Just (sm, acm)
       case prep of
       -- theory could not be computed
        Nothing -> return "No suitable prover and comorphism found"
        Just (G_theory_with_cons_checker _ th p, _) ->
          case P.ccAutomatic p of
           fn ->
            do
            let st' = st { proverRunning = True}
            -- store initial input of the prover
            let tLimit = show $ tsTimeLimit sTxt
            swapMVar mSt $ Just $ Element st' nd
            cstat <- fn (theoryName st)
                        (P.TacticScript tLimit)
                        th []
            swapMVar mSt $ Just $ Element st nd
            putStrLn $ case P.ccResult cstat of
              Nothing -> "Timeout after " ++ tLimit ++ "seconds."
              Just b -> "node " ++ ndnm ++ " is "
                ++ (if b then "" else "in") ++ "consistent."
            ist <- readMVar miSt
            case i_state ist of
              Nothing -> return "no library"
              Just iist -> case P.ccResult cstat of
               Nothing -> return ""
               Just b -> do
                if showOutput iist then
                  do
                    putStrLn "____________________________"
                    print $ P.ccProofTree cstat
                    putStrLn "____________________________"
                                     else putStr ""
                let le = i_libEnv iist
                    dg = lookupDGraph ln le
                    nl = labDG dg nd
                    nn = getDGNodeName nl
                    newDg0 = changeDGH dg $ SetNodeLab nl (nd,
                      markNodeConsistency
                      (if b then Cons else Inconsistent) "" nl)
                    newDg = groupHistory dg (DGRule "Consistency check") newDg0
                    nst = add2history
                      (CommentCmd $ "consistency check done on " ++ nn ++ "\n")
                      ist [DgCommandChange ln]
                    nwst = nst { i_state =
                             Just iist { i_libEnv = Map.insert ln newDg le } }
                swapMVar miSt nwst
                return ""
  
  {- | Given a proofstatus the function does the actual call of the
  prover for proving the node or check consistency -}
  proveNode ::
                -- use theorems is subsequent proofs
                Bool ->
                -- save problem file for each goal
                Bool ->
                -- Tactic script
                ATPTacticScript ->
                {- proofState of the node that needs proving
                all theorems, goals and axioms should have
                been selected before,but the theory should have
                not beed recomputed -}
                Int_NodeInfo ->
                -- node name
                String ->
                {- selected prover, if non one will be automatically
                selected -}
                Maybe G_prover ->
                {- selected comorphism, if non one will be automatically
                selected -}
                Maybe AnyComorphism ->
                MVar (Maybe ThreadId) ->
                MVar (Maybe Int_NodeInfo) ->
                MVar IntState ->
                LibName ->
                -- returns an error message if anything happens
                IO String
  proveNode useTh save2File sTxt ndpf ndnm mp mcm mThr mSt miSt libname =
    case ndpf of
      Element pf_st nd ->
       do
       {- recompute the theory (to make effective the selected axioms,
       goals) -}
       let st = recalculateSublogicAndSelectedTheory pf_st
       {- compute a prover,comorphism pair to be used in preparing
       the theory -}
       p_cm@(_, acm) <- case mcm of
             Nothing -> lookupKnownProver st P.ProveCMDLautomatic
             Just cm' -> case mp of
               Nothing -> lookupKnownProver st P.ProveCMDLautomatic
               Just p' -> return (p', cm')
  
       -- try to prepare the theory
       prep <- case prepareForProving st p_cm of
               Result _ Nothing ->
                 do
                  p_cm'@(prv', acm'@(Comorphism cid)) <-
                            lookupKnownProver st P.ProveCMDLautomatic
                  putStrLn ("Analyzing node " ++ ndnm)
                  putStrLn ("Using the comorphism " ++ language_name cid)
                  putStrLn ("Using prover " ++ getProverName prv')
                  return $ case prepareForProving st p_cm' of
                            Result _ Nothing -> Nothing
                            Result _ (Just sm) -> Just (sm, acm')
               Result _ (Just sm) -> return $ Just (sm, acm)
       case prep of
       -- theory could not be computed
        Nothing -> return "No suitable prover and comorphism found"
        Just (G_theory_with_prover lid1 th p, cmp) -> 
          case P.proveCMDLautomaticBatch p of
           Nothing -> return "Error obtaining the prover"
           Just fn ->
            do
            -- mVar to poll the prover for results
            answ <- newMVar (return [])
            let st' = st { proverRunning = True}
            -- store initial input of the prover
            swapMVar mSt $ Just $ Element st' nd
            {- putStrLn ((theoryName st)++"\n"++
                      (showDoc sign "") ++
                      show (vsep (map (print_named lid1)
                                          $ P.toNamedList sens))) -}
            case selectedGoals st' of
             [] -> return "No goals selected. Nothing to prove"
             _ ->
              do
               putStrLn "selectedGoals:"
               putStrLn $ unlines (selectedGoals st')
               tmp <- fn useTh
                        save2File
                        answ
                        (theoryName st)
                        (P.TacticScript $ show sTxt)
                        th []
               swapMVar mThr $ Just $ fst tmp
               getResults lid1 cmp (snd tmp) answ mSt th
               swapMVar mThr Nothing
               ist <- readMVar miSt
               state <- readMVar mSt
               case state of
                Nothing -> return ""
                Just state' ->
                 do
                  swapMVar mSt Nothing
                  swapMVar miSt $ addResults ist libname state'
                  return ""
  
  disproveNode ::
                 -- Tactic script
                ATPTacticScript ->
                {- proofState of the node that needs proving
                all theorems, goals and axioms should have
                been selected before, but the theory should have
                not been recomputed -}
                Int_NodeInfo ->
                -- node name
                String ->
                {- selected prover, if non one will be automatically
                selected -}
                Maybe G_cons_checker ->
                {- selected comorphism, if non one will be automatically
                selected -}
                Maybe AnyComorphism ->
                MVar (Maybe Int_NodeInfo) ->
                MVar IntState ->
                LibName ->
                -- returns an error message if anything happens
                IO String
  disproveNode sTxt ndpf ndnm mp mcm mSt miSt ln =
    case ndpf of
      Element pf_st nd ->
       do
       {- recompute the theory (to make effective the selected axioms,
       goals) !? needed? -}
       let st = recalculateSublogicAndSelectedTheory pf_st
       {- compute a prover,comorphism pair to be used in preparing
       the theory -}
       p_cm@(_, acm) <- case mcm of
             Nothing -> lookupKnownConsChecker st
             Just cm' -> case mp of
               Nothing -> lookupKnownConsChecker st
               Just p' -> return (p', cm')
  
       -- try to prepare the theory
       prep <- case prepareForConsChecking st p_cm of
               Result _ Nothing ->
                 do
                  p_cm'@(prv', acm'@(Comorphism cid)) <-
                            lookupKnownConsChecker st
                  putStrLn ("Analyzing node for consistency " ++ ndnm)
                  putStrLn ("Using the comorphism " ++ language_name cid)
                  putStrLn ("Using consistency checker " ++ getCcName prv')
                  return $ case prepareForConsChecking st p_cm' of
                            Result _ Nothing -> Nothing
                            Result _ (Just sm) -> Just (sm, acm')
               Result _ (Just sm) -> return $ Just (sm, acm)
       case prep of
       -- theory could not be computed
        Nothing -> return "No suitable prover and comorphism found"
        Just (theory@(G_theory_with_cons_checker l _ p), _) ->
          case P.ccAutomatic p of
           fn ->
            do
            let goals = selectedGoals st
                st' = st { proverRunning = True }
                negate_theory = negate_th_with_cons_checker theory
                theories = map negate_theory goals
                th_and_goals = zip theories goals
                disprove_goal (theory', goal) =
                  case theory' of
                    Nothing -> return $ "Negating goal " ++ goal ++ " failed"
                    Just (G_theory_with_cons_checker l2 th' _) ->
                      do
                      -- store initial input of the prover
                      let tLimit = show $ tsTimeLimit sTxt
                      th2 <- coerceTheoryMorphism l2 l
                              "coerce error CMDL.ProveConsistency " th'
                      swapMVar mSt $ Just $ Element st' nd
                      cstat <- fn (theoryName st)
                            (P.TacticScript tLimit)
                            th2 []
                      swapMVar mSt $ Just $ Element st nd
                      putStrLn $ case P.ccResult cstat of
                        Nothing -> "Timeout after " ++ tLimit ++ "seconds."
                        Just b -> "goal " ++ goal ++ " is "
                          ++ (if b then "" else "not ") ++ "disproved."
                      ist <- readMVar miSt
                      case i_state ist of
                        Nothing -> return $ "goal " ++ goal ++ ": no library"
                        Just iist -> case P.ccResult cstat of
                         Nothing -> return ""
                         Just b -> do
                          let le = i_libEnv iist
                              dg = lookupDGraph ln le
                              nl = labDG dg nd
                              nn = getDGNodeName nl
                              newDg0 = changeDGH dg $ SetNodeLab nl (nd,
                                markNodeConsistency
                                (if b then Cons else Inconsistent) "" nl)
                              newDg = groupHistory dg
                                       (DGRule "Consistency check") newDg0
                              nst = add2history
                                (CommentCmd $ "disprove at goal " ++ goal ++
                                              ", node " ++ nn ++ "\n")
                                ist [DgCommandChange ln]
                              nwst = nst { i_state =
                                       Just iist { i_libEnv = Map.insert ln
                                                               newDg le } }
                          swapMVar miSt nwst
                          return ""
            mapM_ ((\ x -> do
                             y <- x
                             putStrLn y
                             return () ) . disprove_goal) th_and_goals
            return ""
  
  getResults :: (Logic lid sublogics basic_spec sentence
                       symb_items symb_map_items
                       sign morphism symbol raw_symbol proof_tree, Pretty sentence) =>
                lid ->
                AnyComorphism ->
                MVar () ->
                MVar (Result [P.ProofStatus proof_tree]) ->
                MVar (Maybe Int_NodeInfo) -> 
                P.Theory sign sentence proof_tree ->
                IO ()
  getResults lid acm mStop mData mState (P.Theory _ sensMap) =
    do
      takeMVar mStop
      d <- takeMVar mData
      case d of
        Result _ Nothing -> return ()
        Result _ (Just d') -> do
          mapM_ (\ gs -> let
                    uAx = map 
                            (\x -> let ax =  case OMap.lookup x sensMap of
                                              Nothing -> error "Proof using a missing axiom"
                                              Just s -> show $ pretty $ sentence s
                                    in x ++" : " ++ ax ++ "\n") $
                          P.usedAxioms gs
                  in  
                 putStrLn $ "Goal " ++ P.goalName gs
                 ++ " used \n" ++ unwords uAx)
            $ filter P.isProvedStat d'
          modifyMVar_ mState (\ s -> case s of
                    Nothing -> return s
                    Just (Element st node) -> return $ Just $ Element
                                              (markProved acm lid d' st) node)
  
  -- | inserts the results of the proof in the development graph
  addResults :: IntState -> LibName -> Int_NodeInfo -> IntState
  addResults ist libname ndps =
    case i_state ist of
      Nothing -> ist
      Just pS ->
        case ndps of
         Element ps'' node -> let
                 dGraph = lookupDGraph libname (i_libEnv pS)
                 nl = labDG dGraph node
                 in fst $ updateNodeProof libname ist (node, nl)
                        $ currentTheory ps''
  
  {- | Signal handler that stops the prover from running
  when SIGINT is send -}
  sigIntHandler :: MVar (Maybe ThreadId) ->
                   MVar IntState ->
                   MVar (Maybe Int_NodeInfo) ->
                   ThreadId ->
                   MVar IntState ->
                   LibName ->
                   IO ()
  sigIntHandler mthr miSt mSt thr mOut libname =
    do
     {- print a message
     ? shellputStr ! should be used ! -}
     putStrLn "Prover stopped."
     -- check if the prover is runnig
     tmp <- readMVar mthr
     Data.Foldable.forM_ tmp killThread
     -- kill the prove/prove-all thread
     killThread thr
     -- update LibEnv with intermidiar results !?
     ist <- readMVar miSt
  
     st <- readMVar mSt
     -- add to the output mvar results until now
     putMVar mOut $ case st of
       Nothing -> ist
       Just st' -> addResults ist libname st'
     return ()
  
  doLoop :: MVar IntState
         -> MVar (Maybe ThreadId)
         -> MVar (Maybe Int_NodeInfo)
         -> MVar IntState
         -> [Int_NodeInfo]
         -> ProveCmdType
         -> IO ()
  doLoop miSt mThr mSt mOut ls proveCmdType = do
    ist <- readMVar miSt
    case i_state ist of
      Nothing -> do
                   putMVar mOut ist
                   return ()
      Just pS ->
          case ls of
           -- we are done
            [] -> do
                   putMVar mOut ist
                   return ()
            x : l -> do
                   let nodeName x' = case x' of
                         Element _ t -> case lookup t $ getAllNodes pS of
                           Nothing -> "Unkown node"
                           Just ll -> getDGNodeName ll
                   putStrLn ("Analyzing node " ++ nodeName x)
                   err <- case proveCmdType of
                             ConsCheck -> checkNode (script pS)
                                            x
                                            (nodeName x)
                                            (consChecker pS)
                                            (cComorphism pS)
                                            mSt
                                            miSt
                                            (i_ln pS)
                             Prove -> proveNode (useTheorems pS)
                                            (save2file pS)
                                            (script pS)
                                            x
                                            (nodeName x)
                                            (prover pS)
                                            (cComorphism pS)
                                            mThr
                                            mSt
                                            miSt
                                            (i_ln pS)
                             Disprove -> disproveNode (script pS)
                                               x
                                               (nodeName x)
                                               (consChecker pS)
                                               (cComorphism pS)
                                               mSt
                                               miSt
                                               (i_ln pS)
                   unless (null err) (putStrLn err)
                   doLoop miSt mThr mSt mOut l proveCmdType
  