{-# LANGUAGE CPP #-}
{- |
Module      : ./CMDL/Interface.hs
Description : The definition of CMDL interface for
              standard input and file input
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.Interface describes the interface specific function
for standard input and file input
-}

module CMDL.Interface where

#ifdef HASKELINE
import System.Console.Haskeline
import Interfaces.DataTypes
import Comorphisms.LogicGraph (logicGraph)
import Logic.Grothendieck
#endif

import Proofs.AbstractState (getListOfConsCheckers, usableCC)

import System.IO

import CMDL.Commands (getCommands)
import CMDL.DataTypes
import CMDL.DataTypesUtils
import CMDL.Shell
import CMDL.ProcessScript
import CMDL.Utils (stripComments)

import Interfaces.Command

import Common.Utils (trim)

import Data.List

import Data.IORef
import Control.Monad
import Control.Monad.Trans (MonadIO (..))

#ifdef HASKELINE
import Proofs.AbstractState (getAllConsCheckers, sublogicOfTheory, getCcName)

shellSettings :: IORef CmdlState -> Settings IO
shellSettings :: IORef CmdlState -> Settings IO
shellSettings st :: IORef CmdlState
st =
  Settings :: forall (m :: * -> *).
CompletionFunc m -> Maybe FilePath -> Bool -> Settings m
Settings {
      complete :: CompletionFunc IO
complete = IORef CmdlState -> CompletionFunc IO
cmdlComplete IORef CmdlState
st
    , historyFile :: Maybe FilePath
historyFile = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "consoleHistory.tmp"
    , autoAddHistory :: Bool
autoAddHistory = Bool
True
  }

{- We need an MVar here because our CmdlState is no Monad
   (and we use IO as Monad). -}

showCmdComplete :: CmdlState -> [String] -> [String] -> String ->
                    IO (String, [Completion])
showCmdComplete :: CmdlState
-> [FilePath]
-> [FilePath]
-> FilePath
-> IO (FilePath, [Completion])
showCmdComplete state :: CmdlState
state shortConsCList :: [FilePath]
shortConsCList comps :: [FilePath]
comps left :: FilePath
left = do
  let (_, nodes :: [LNode DGNodeLab]
nodes) = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
                     Nothing -> ("", [])
                     Just dgState :: IntIState
dgState -> IntIState -> (FilePath, [LNode DGNodeLab])
getSelectedDGNodes IntIState
dgState
      cmdss :: [FilePath]
cmdss = "prove-all" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: (CmdlCmdDescription -> FilePath)
-> [CmdlCmdDescription] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Command -> FilePath
cmdNameStr (Command -> FilePath)
-> (CmdlCmdDescription -> Command)
-> CmdlCmdDescription
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> Command
cmdDescription) [CmdlCmdDescription]
getCommands
      cmds :: [FilePath]
cmds = [FilePath]
cmdss [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ((FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ("cons-checker " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++) [FilePath]
shortConsCList)
      cmdcomps :: [FilePath]
cmdcomps = (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
left)) [FilePath]
cmds
      cmdcomps' :: [FilePath]
cmdcomps' = if [LNode DGNodeLab] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LNode DGNodeLab]
nodes
                          then (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "-current") [FilePath]
cmdcomps
                          else [FilePath]
cmdcomps
  (FilePath, [Completion]) -> IO (FilePath, [Completion])
forall (m :: * -> *) a. Monad m => a -> m a
return ("", (FilePath -> Completion) -> [FilePath] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Completion
simpleCompletion ([FilePath] -> [Completion]) -> [FilePath] -> [Completion]
forall a b. (a -> b) -> a -> b
$ [FilePath]
comps [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
cmdcomps')

cmdlComplete :: IORef CmdlState -> CompletionFunc IO
cmdlComplete :: IORef CmdlState -> CompletionFunc IO
cmdlComplete st :: IORef CmdlState
st (left :: FilePath
left, _) = do

  CmdlState
state <- IO CmdlState -> IO CmdlState
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CmdlState -> IO CmdlState) -> IO CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ IORef CmdlState -> IO CmdlState
forall a. IORef a -> IO a
readIORef IORef CmdlState
st
  [FilePath]
comps <- IO [FilePath] -> IO [FilePath]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [FilePath] -> IO [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall a b. (a -> b) -> a -> b
$ [CmdlCmdDescription] -> CmdlState -> FilePath -> IO [FilePath]
cmdlCompletionFn [CmdlCmdDescription]
getCommands CmdlState
state (FilePath -> IO [FilePath]) -> FilePath -> IO [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
left

  if FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
left) "cons-checker "
   then
    case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
     Just pS :: IntIState
pS ->
       case IntIState -> [Int_NodeInfo]
elements IntIState
pS of
        Element z :: ProofState
z _ : _ ->
          do
           let paths :: [AnyComorphism]
paths = LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph (G_sublogics -> [AnyComorphism]) -> G_sublogics -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ ProofState -> G_sublogics
sublogicOfTheory ProofState
z
               fullConsCheckerList :: [G_cons_checker]
fullConsCheckerList = ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> [(G_cons_checker, AnyComorphism)] -> [G_cons_checker]
forall a b. (a -> b) -> [a] -> [b]
map (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst ([(G_cons_checker, AnyComorphism)] -> [G_cons_checker])
-> [(G_cons_checker, AnyComorphism)] -> [G_cons_checker]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers ([AnyComorphism] -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism]
paths
               stateConsCheckList :: [G_cons_checker]
stateConsCheckList = CmdlState -> [G_cons_checker]
consCheckers CmdlState
state
               filteredConsCheckerList :: [G_cons_checker]
filteredConsCheckerList =
                 (G_cons_checker -> Bool) -> [G_cons_checker] -> [G_cons_checker]
forall a. (a -> Bool) -> [a] -> [a]
filter (\cc :: G_cons_checker
cc -> G_cons_checker -> [G_cons_checker] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem G_cons_checker
cc [G_cons_checker]
stateConsCheckList) [G_cons_checker]
fullConsCheckerList
               shortConsCList :: [FilePath]
shortConsCList = [FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a]
nub ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (G_cons_checker -> FilePath) -> [G_cons_checker] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map G_cons_checker -> FilePath
getCcName [G_cons_checker]
filteredConsCheckerList
           CmdlState
-> [FilePath]
-> [FilePath]
-> FilePath
-> IO (FilePath, [Completion])
showCmdComplete CmdlState
state [FilePath]
shortConsCList [FilePath]
comps FilePath
left
        [] -> CmdlState
-> [FilePath]
-> [FilePath]
-> FilePath
-> IO (FilePath, [Completion])
showCmdComplete CmdlState
state [] [FilePath]
comps FilePath
left
     Nothing -> CmdlState
-> [FilePath]
-> [FilePath]
-> FilePath
-> IO (FilePath, [Completion])
showCmdComplete CmdlState
state [] [FilePath]
comps FilePath
left
   else CmdlState
-> [FilePath]
-> [FilePath]
-> FilePath
-> IO (FilePath, [Completion])
showCmdComplete CmdlState
state [] [FilePath]
comps FilePath
left

#endif

#ifdef HASKELINE
getMultiLineT :: String -> String -> InputT IO (Maybe String)
getMultiLineT :: FilePath -> FilePath -> InputT IO (Maybe FilePath)
getMultiLineT prompt :: FilePath
prompt past :: FilePath
past = do
  Maybe FilePath
minput <- FilePath -> InputT IO (Maybe FilePath)
forall (m :: * -> *).
MonadException m =>
FilePath -> InputT m (Maybe FilePath)
getInputLine FilePath
prompt
  case Maybe FilePath
minput of
          Nothing -> Maybe FilePath -> InputT IO (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FilePath
forall a. Maybe a
Nothing
          Just input :: FilePath
input -> let
                  str :: FilePath
str = FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
input
                  has :: Bool
has = FilePath -> Bool
hasSlash FilePath
str
                in if Bool
has then
                  FilePath -> FilePath -> InputT IO (Maybe FilePath)
getMultiLineT FilePath
prompt ( FilePath
past FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath
takeOutSlash FilePath
str)))
                else
                  Maybe FilePath -> InputT IO (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath -> InputT IO (Maybe FilePath))
-> Maybe FilePath -> InputT IO (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
past FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
input
#endif

hasSlash :: String -> Bool
hasSlash :: FilePath -> Bool
hasSlash x :: FilePath
x = case FilePath
x of
        '\\' : _ -> Bool
True
        ' ' : ls :: FilePath
ls -> FilePath -> Bool
hasSlash FilePath
ls
        '\n' : ls :: FilePath
ls -> FilePath -> Bool
hasSlash FilePath
ls
        _ -> Bool
False

takeOutSlash :: String -> String
takeOutSlash :: FilePath -> FilePath
takeOutSlash str :: FilePath
str = case FilePath
str of
          '\\' : ls :: FilePath
ls -> FilePath
ls
          '\n' : ls :: FilePath
ls -> FilePath -> FilePath
takeOutSlash FilePath
ls
          ' ' : ls :: FilePath
ls -> FilePath -> FilePath
takeOutSlash FilePath
ls
          l :: FilePath
l -> FilePath
l


getLongLine :: IO String
getLongLine :: IO FilePath
getLongLine = do
  FilePath
l <- IO FilePath
getLine
  if FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf "\\" FilePath
l then (FilePath -> FilePath) -> IO FilePath -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath -> FilePath
forall a. [a] -> [a]
init FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++) IO FilePath
getLongLine else FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
l

shellLoop :: IORef CmdlState
          -> Bool
#ifdef HASKELINE
          -> InputT IO CmdlState
#else
          -> IO CmdlState
#endif
shellLoop :: IORef CmdlState -> Bool -> InputT IO CmdlState
shellLoop st :: IORef CmdlState
st isTerminal :: Bool
isTerminal =
  do
    CmdlState
state <- IO CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CmdlState -> InputT IO CmdlState)
-> IO CmdlState -> InputT IO CmdlState
forall a b. (a -> b) -> a -> b
$ IORef CmdlState -> IO CmdlState
forall a. IORef a -> IO a
readIORef IORef CmdlState
st
    let prompt :: FilePath
prompt = if Bool
isTerminal then CmdlState -> FilePath
generatePrompter CmdlState
state else ""
#ifdef HASKELINE
    Maybe FilePath
minput <- FilePath -> FilePath -> InputT IO (Maybe FilePath)
getMultiLineT FilePath
prompt ""
#else
    putStr prompt
    hFlush stdout
    eof <- isEOF
    minput <- if eof then return Nothing else liftM Just getLongLine

#endif
    case Maybe FilePath
minput of
      Nothing -> CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
      Just input :: FilePath
input ->
        do
          let echo :: FilePath
echo = FilePath -> FilePath
trim (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
stripComments FilePath
input
          Bool -> InputT IO () -> InputT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
isTerminal Bool -> Bool -> Bool
&& Bool -> Bool
not (FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
echo))
               (IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ CmdlState -> FilePath
generatePrompter CmdlState
state FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
echo)
          (state' :: CmdlState
state', mc :: Maybe Command
mc) <- IO (CmdlState, Maybe Command)
-> InputT IO (CmdlState, Maybe Command)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (CmdlState, Maybe Command)
 -> InputT IO (CmdlState, Maybe Command))
-> IO (CmdlState, Maybe Command)
-> InputT IO (CmdlState, Maybe Command)
forall a b. (a -> b) -> a -> b
$ FilePath
-> Int -> FilePath -> CmdlState -> IO (CmdlState, Maybe Command)
cmdlProcessString "" 0 FilePath
input CmdlState
state
          case Maybe Command
mc of
            Nothing -> if FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
input ["exit", ":q"] -- additional exit cmds
                         then CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state'
                         else do
                                IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Unknown command: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
input
                                IORef CmdlState -> Bool -> InputT IO CmdlState
shellLoop IORef CmdlState
st Bool
isTerminal
            Just ExitCmd -> CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state'
            Just c :: Command
c -> do
                        CmdlState
newState <- IO CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CmdlState -> InputT IO CmdlState)
-> IO CmdlState -> InputT IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IO CmdlState
printCmdResult CmdlState
state'
                        CmdlState
newState' <- IO CmdlState -> InputT IO CmdlState
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CmdlState -> InputT IO CmdlState)
-> IO CmdlState -> InputT IO CmdlState
forall a b. (a -> b) -> a -> b
$ case (CmdlCmdDescription -> Bool)
-> [CmdlCmdDescription] -> Maybe CmdlCmdDescription
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find
                                       (Command -> Command -> Bool
eqCmd Command
c (Command -> Bool)
-> (CmdlCmdDescription -> Command) -> CmdlCmdDescription -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CmdlCmdDescription -> Command
cmdDescription) [CmdlCmdDescription]
getCommands of
                                         Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
newState
                                         Just cm :: CmdlCmdDescription
cm -> CmdlCmdDescription -> CmdlState -> IO CmdlState
checkCom
                                              CmdlCmdDescription
cm { cmdDescription :: Command
cmdDescription = Command
c } CmdlState
newState
                        IO () -> InputT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> InputT IO ()) -> IO () -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ IORef CmdlState -> CmdlState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef CmdlState
st CmdlState
newState'
                        IORef CmdlState -> Bool -> InputT IO CmdlState
shellLoop IORef CmdlState
st Bool
isTerminal

saveConsCheckersInState :: CmdlState -> IO CmdlState
saveConsCheckersInState :: CmdlState -> IO CmdlState
saveConsCheckersInState state :: CmdlState
state = do
  [G_cons_checker]
consCheckerList <- (G_cons_checker -> IO Bool)
-> [G_cons_checker] -> IO [G_cons_checker]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM G_cons_checker -> IO Bool
usableCC [G_cons_checker]
getListOfConsCheckers
  CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state { consCheckers :: [G_cons_checker]
consCheckers = [G_cons_checker]
consCheckerList }

-- | The function runs hets in a shell
cmdlRunShell :: CmdlState -> IO CmdlState
cmdlRunShell :: CmdlState -> IO CmdlState
cmdlRunShell state :: CmdlState
state = do
  Bool
isTerminal <- Handle -> IO Bool
hIsTerminalDevice Handle
stdin
  CmdlState
st' <- CmdlState -> IO CmdlState
saveConsCheckersInState CmdlState
state
  IORef CmdlState
st <- CmdlState -> IO (IORef CmdlState)
forall a. a -> IO (IORef a)
newIORef CmdlState
st'
#ifdef HASKELINE
  Settings IO -> InputT IO CmdlState -> IO CmdlState
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
runInputT (IORef CmdlState -> Settings IO
shellSettings IORef CmdlState
st) (InputT IO CmdlState -> IO CmdlState)
-> InputT IO CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ IORef CmdlState -> Bool -> InputT IO CmdlState
shellLoop IORef CmdlState
st Bool
isTerminal
#else
  hSetBuffering stdin LineBuffering
  shellLoop st isTerminal
#endif