content: {- |
  Module      : ./CMDL/Shell.hs
  Description : shell related functions
  Copyright   : uni-bremen and DFKI
  License     : GPLv2 or higher, see LICENSE.txt
  Maintainer  : r.pascanu@jacobs-university.de
  Stability   : provisional
  Portability : portable
  
  CMDL.Shell contains almost all functions related
  the CMDL shell or haskeline
  -}
  
  module CMDL.Shell
         ( cComment
         , cOpenComment
         , cCloseComment
         , nodeNames
         , cmdlCompletionFn
         , checkCom
         ) where
  
  import CMDL.DataTypes
  import CMDL.Utils
  import CMDL.DataTypesUtils
  
  import Common.Utils (trimLeft, trimRight, nubOrd, splitOn)
  import Common.Result (Result (Result))
  
  import Comorphisms.LogicGraph (comorphismList, logicGraph,
                                 lookupComorphism_in_LG)
  
  import Interfaces.Command (Command (CommentCmd))
  import Interfaces.DataTypes
  import Interfaces.Utils
  import Interfaces.GenericATPState
  
  import Logic.Comorphism
  import Logic.Grothendieck (logics, findComorphismPaths,
                             G_sublogics (..))
  import Logic.Prover
  import Logic.Logic
  import Logic.Coerce (coerceSublogic)
  
  import Proofs.AbstractState
  
  import Static.DevGraph
  import Static.GTheory
  
  import Data.Char (isSpace)
  import Data.List
  import qualified Data.Map
  import Data.Maybe (mapMaybe, isNothing)
  import System.Directory (doesDirectoryExist, getDirectoryContents)
  
  register2history :: CmdlCmdDescription -> CmdlState -> IO CmdlState
  register2history dscr state = do
      let oldHistory = i_hist $ intState state
      case undoList oldHistory of
         [] -> return state
         h : r -> case command h of
                 CommentCmd _ -> do
                       let nwh = h {
                                  command = cmdDescription dscr }
                       return $ state {
                           intState = (intState state) {
                              i_hist = oldHistory {
                                 undoList = nwh : r,
                                 redoList = []
                               } } }
                 _ -> return state
  
  -- process a comment line
  processComment :: CmdlState -> String -> CmdlState
  processComment st inp =
    if isInfixOf "}%" inp then st { openComment = False } else st
  
  -- adds a line to the script
  addToScript :: CmdlState -> IntIState -> String -> CmdlState
  addToScript st ist str
   = let olds = script ist
         oldextOpts = tsExtraOpts olds
     in st {
          intState = (intState st) {
                       i_state = Just ist {
                         script = olds { tsExtraOpts = str : oldextOpts } }
            } }
  
  checkCom :: CmdlCmdDescription -> CmdlState -> IO CmdlState
  checkCom descr state =
      -- check the priority of the current command
      case cmdPriority descr of
       CmdNoPriority ->
        -- check if there is open comment
        if openComment state
         then return $ processComment state $ cmdInput descr
         else
          case i_state $ intState state of
           Nothing -> register2history descr state
           Just ist ->
            -- check if there is inside a script
            if loadScript ist
              then return $ addToScript state ist
                          $ cmdName descr ++ " " ++ cmdInput descr
              else register2history descr state
       CmdGreaterThanComments ->
        case i_state $ intState state of
         Nothing -> register2history descr state
         Just ist ->
          if loadScript ist
            then return $ addToScript state ist
                        $ cmdName descr ++ " " ++ cmdInput descr
            else register2history descr state
       CmdGreaterThanScriptAndComments -> return state
  
  -- | Function handle a comment line
  cComment :: String -> CmdlState -> IO CmdlState
  cComment _ = return
  
  -- For normal keyboard input
  
  cOpenComment :: String -> CmdlState -> IO CmdlState
  cOpenComment _ state = return state { openComment = True }
  
  cCloseComment :: CmdlState -> IO CmdlState
  cCloseComment state = return state { openComment = False }
  
  {- | given an input it assumes that it starts with a
     command name and tries to remove this command name -}
  subtractCommandName :: [CmdlCmdDescription] -> String -> String
  subtractCommandName allcmds input =
    let inp = trimLeft input
    in case mapMaybe ((`stripPrefix` inp) . cmdName) allcmds of
         [] -> inp
         hd : _ -> hd
  
  {- This function tries to extract the name of command. In most cases this
     would be the first word of the string but we have a few exceptions :
     dg * commands
     dg-all * commands
     del * commands
     del-all * commands
     add * commands
     set * commands
     set-all * commands -}
  getCmdName :: String -> String
  getCmdName inp = case words inp of
      [] -> []
      hw : tws -> case tws of
        [] -> hw
        hwd : _ -> let
          cs = ["dg", "del", "set"]
          csa = "add" : cs ++ map (++ "-all") cs
          in if elem hw csa then hw ++ ' ' : hwd else hw
  
  {- | The function determines the requirements of the command
     name found at the begining of the string -}
  getTypeOf :: [CmdlCmdDescription] -> String -> CmdlCmdRequirements
  getTypeOf allcmds input
   = let nwInput = getCmdName input
         tmp = concatMap (\ x -> case find (== nwInput) [cmdName x] of
                                  Nothing -> []
                                  Just _ -> [cmdReq x]) allcmds
     in case tmp of
         result : [] -> result
         _ -> ReqUnknown
  
  nodeNames :: [(a, DGNodeLab)] -> [String]
  nodeNames = map (getDGNodeName . snd)
  
  {- | The function provides a list of possible completion
     to a given input if any -}
  cmdlCompletionFn :: [CmdlCmdDescription] -> CmdlState -> String -> IO [String]
  cmdlCompletionFn allcmds allState input =
     let s0_9 = map show [0 .. (9 :: Int)]
         app h = (h ++) . (' ' :)
     in case getTypeOf allcmds input of
     ReqNodesOrEdges mn mf ->
      case i_state $ intState allState of
       Nothing -> return []
       Just state -> do
         {- a pair, where the first element is what needs
            to be completed while the second is what is
            before the word that needs to be completed
         -}
         let -- get all nodes
             ns = getAllNodes state
             fns = nodeNames $ maybe id (\ f -> filter (\ (_, nd) ->
                       case f of
                         OpenCons -> hasOpenNodeConsStatus False nd
                         OpenGoals -> hasOpenGoals nd))
                       mf ns
             es = map fst
                  $ maybe id (\ f -> filter $ case f of
                      OpenCons -> isOpenConsEdge
                      OpenGoals -> edgeContainsGoals
                    . snd) mf
                  $ createEdgeNames ns (getAllEdges state)
             allNames = case mn of
               Nothing -> es ++ fns
               Just b -> if b then fns else es
             (fins, tC) = finishedNames allNames
                $ subtractCommandName allcmds input
             -- what is before tC
             bC = reverse $ trimLeft $ drop (length tC) $ reverse input
        {- filter out words that do not start with the word
           that needs to be completed and add the word that
           was before the word that needs to be completed -}
         return $ map (app bC) $ filter (isPrefixOf tC) $ allNames \\ fins
     ReqConsCheck -> do
         let tC = if isSpace $ lastChar input
                   then []
                   else lastString $ words input
             bC = if isSpace $ lastChar input
                   then trimRight input
                   else unwords $ init $ words input
             getCCName (G_cons_checker _ p) = ccName p
             createConsCheckersList = map (getCCName . fst) . getAllConsCheckers
         case i_state $ intState allState of
          Nothing ->
           {- not in proving mode !? you can not choose a consistency
              checker here -}
                 return []
          Just proofState ->
           case cComorphism proofState of
            -- some comorphism was used
            Just c -> return $ map (app bC) $ filter (isPrefixOf tC)
                     $ createConsCheckersList [c]
            Nothing ->
             case elements proofState of
              -- no elements selected
              [] -> return []
              c : _ -> case c of
                 Element z _ -> return $ map (app bC)
                                 $ filter (isPrefixOf tC)
                                 $ createConsCheckersList
                                 $ findComorphismPaths logicGraph
                                     (sublogicOfTheory z)
     ReqProvers -> do
         let bC : tl = words input
             tC = unwords tl
        {- find the last comorphism used if none use the
           the comorphism of the first selected node -}
         case i_state $ intState allState of
          Nothing ->
         {- not in proving mode !? you can not choose
            provers here -}
                  return []
          Just proofState ->
             case elements proofState of
               -- no elements selected
               [] -> return []
               -- use the first element to get a comorphism
               c : _ -> case c of
                  Element z _ -> do
                    ps <- getUsableProvers ProveCMDLautomatic
                            (sublogicOfTheory z) logicGraph
                    let lst = nub $ map (getProverName . fst) ps
                    return $ map (app bC) $ filter (isPrefixOf tC) lst
     ReqComorphism ->
      let input'' = case words input of
                     cmd : s' -> unwords (cmd : concatMap (splitOn ':')
                                                 (concatMap (splitOn ';') s'))
                     _ -> input
          input' = if elem (lastChar input) ";: " then
                     input'' ++ " " else input''
      in case i_state $ intState allState of
           Nothing -> return []
           Just pS ->
            case elements pS of
             [] -> return []
             Element st _ : _ ->
                let tC = if isSpace $ lastChar input'
                          then []
                          else lastString $ words input'
                    appendC' =
                     map (\ coname -> case lookupComorphism_in_LG coname of
                                      Result _ cmor -> cmor) $
                      tail $ words input'
                    appendC = sequence $ (if not (null appendC') &&
                                              isNothing (last appendC')
                                           then init else id) appendC'
                    comor = case appendC of
                             Nothing -> cComorphism pS
                             Just cs ->
                              foldl (\ c1 c2 -> maybe Nothing
                               (`compComorphism` c2) c1)
                               (cComorphism pS) cs
                    bC = if isSpace $ lastChar input'
                          then trimRight input'
                          else unwords $ init $ words input'
                    sl = case comor of
                          Just (Comorphism cid) ->
                           case sublogicOfTheory st of
                            G_sublogics lid sl2 ->
                             case coerceSublogic lid (sourceLogic cid) "" sl2 of
                              Just sl2' -> case mapSublogic cid sl2' of
                               Just sl1 -> G_sublogics (targetLogic cid) sl1
                               Nothing -> G_sublogics (targetLogic cid)
                                            (top_sublogic $ targetLogic cid)
                              Nothing -> G_sublogics (targetLogic cid)
                                          (top_sublogic $ targetLogic cid)
                          Nothing -> sublogicOfTheory st
                    cL = concatMap (\ (Comorphism cid) ->
                                    [ language_name cid
                                      | isSubElemG sl (G_sublogics
                                           (sourceLogic cid)
                                           (sourceSublogic cid)) ]
                                   ) comorphismList
                in return $ map (app bC)
                          $ filter (isPrefixOf tC) cL
     ReqLogic ->
      let l' = lastString $ words input
          i = unwords (init $ words input) ++ " "
      in if elem '.' l'
         then let (l, _ : sl) = Data.List.break (== '.') l'
              in case Data.Map.lookup l $ logics logicGraph of
                  Just (Logic lid) -> return $ map ((i ++ l ++ ".") ++) $
                                       filter (Data.List.isPrefixOf sl)
                                       (map sublogicName $ all_sublogics lid)
                  Nothing -> return []
         else return $ concatMap
                       (\ (n, Logic lid) ->
                          case map sublogicName $ all_sublogics lid of
                           [_] -> [i ++ n]
                           sls -> (i ++ n) : map
                            (\ sl -> i ++ n ++ "." ++ sl) sls) $
                       filter (Data.List.isPrefixOf l' . fst) $
                       Data.Map.toList $ logics logicGraph
     ReqFile -> do
          -- the incomplete path introduced until now
          let initwd = if isSpace $ lastChar input
                        then []
                        else lastString $ words input
          {- the folder in which to look for (it might be
             empty) -}
              tmpPath = reverse $ dropWhile (/= '/') $ reverse initwd
          {- in case no folder was introduced yet look into
             current folder -}
              lastPath = case tmpPath of
                         [] -> "./"
                         _ -> tmpPath
          {- the name of file/directory that needs to be
             completed from the already introduced path -}
              tC = reverse $ takeWhile (/= '/') $ reverse initwd
              bC = if isSpace $ lastChar input
                    then input
                    else unwords (init $ words input) ++ " " ++ tmpPath
          -- leave just folders and files with extenstion .casl
          b' <- doesDirectoryExist lastPath
          ls <- if b' then getDirectoryContents lastPath else return []
          names <- fileFilter lastPath ls []
          {- case list contains only one name
             then if it is a folder extend it -}
          let names' = filter (isPrefixOf tC) names
          names'' <- case safeTail names' of
                     {- check CMDL.Utils to see how it
                        works, function should be done with
                        something like map but that can handle
                        functions with IO
                        (mapIO !? couldn't make it work though) -}
                     [] -> fileExtend lastPath names' []
                     _ -> return names'
          return $ map (bC ++) names''
     ReqAxm b ->
        case i_state $ intState allState of
         Nothing -> return []
         Just pS ->
          do
           let tC = if isSpace $ lastChar input
                      then []
                      else lastString $ words input
               bC = if isSpace $ lastChar input
                      then trimRight input
                      else unwords $ init $ words input
           return $ map (app bC) $ filter (isPrefixOf tC) $ nubOrd
             $ concatMap (\ (Element st nb) ->
                 if b then map fst $ getAxioms st else
                          case getTh Do_translate nb allState of
                          Nothing -> []
                          Just th -> map fst $ filter
                              (maybe False (not . isProvedBasically) . snd)
                              $ getThGoals th)
                  $ elements pS
     ReqNumber -> case words input of
                     [hd] -> return $ map (app hd) s0_9
                     _ : _ : [] -> return $ if isSpace $ lastChar input
                            then []
                            else map (input ++) s0_9
                     _ -> return []
     ReqNothing -> return []
     ReqUnknown -> return []
  