{-|
Module      : Idris.REPL
Description : Main function to decide Idris' mode of use.
License     : BSD3
Maintainer  : The Idris Community.
-}
module Idris.Main
  ( idrisMain
  , idris
  , runMain
  , runClient -- taken from Idris.REPL.
  , loadInputs -- taken from Idris.ModeCommon
  ) where

import Idris.AbsSyntax
import Idris.Core.Execute (execute)
import Idris.Core.TT
import Idris.Elab.Term
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import Idris.IBC
import Idris.Info
import Idris.ModeCommon
import Idris.Options
import Idris.Output
import Idris.Parser hiding (indent)
import Idris.REPL
import Idris.REPL.Commands
import Idris.REPL.Parser
import IRTS.CodegenCommon

import Util.System

import Control.Category
import Control.DeepSeq
import Control.Monad
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Except (runExceptT)
import Control.Monad.Trans.State.Strict (execStateT)
import Data.List
import Data.Maybe
import Prelude hiding (id, (.), (<$>))
import System.Console.Haskeline as H
import System.Directory
import System.Exit
import System.FilePath
import System.IO
import System.IO.CodePage (withCP65001)

-- | How to run Idris programs.
runMain :: Idris () -> IO ()
runMain :: Idris () -> IO ()
runMain Idris ()
prog = IO () -> IO ()
forall a. IO a -> IO a
withCP65001 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
               -- Run in codepage 65001 on Windows so that UTF-8 characters can
               -- be displayed properly. See #3000.
  res <- ExceptT Err IO IState -> IO (Either Err IState)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Err IO IState -> IO (Either Err IState))
-> ExceptT Err IO IState -> IO (Either Err IState)
forall a b. (a -> b) -> a -> b
$ Idris () -> IState -> ExceptT Err IO IState
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Idris ()
prog IState
idrisInit
  case res of
       Left Err
err -> do
         String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Uncaught error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
err
         IO ()
forall a. IO a
exitFailure
       Right IState
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | The main function of Idris that when given a set of Options will
-- launch Idris into the desired interaction mode either: REPL;
-- Compiler; Script execution; or IDE Mode.
idrisMain :: [Opt] -> Idris ()
idrisMain :: [Opt] -> Idris ()
idrisMain [Opt]
opts =
  do   (ConsoleWidth -> Idris ()) -> [ConsoleWidth] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ConsoleWidth -> Idris ()
setWidth ((Opt -> Maybe ConsoleWidth) -> [Opt] -> [ConsoleWidth]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe ConsoleWidth
getConsoleWidth [Opt]
opts)
       let inputs :: [String]
inputs = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getFile [Opt]
opts
       let quiet :: Bool
quiet = Opt
Quiet Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let nobanner :: Bool
nobanner = Opt
NoBanner Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let idesl :: Bool
idesl = Opt
Idemode Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts Bool -> Bool -> Bool
|| Opt
IdemodeSocket Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let runrepl :: Bool
runrepl = Bool -> Bool
not (Opt
NoREPL Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)
       let output :: [String]
output = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getOutput [Opt]
opts
       let ibcsubdir :: [String]
ibcsubdir = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getIBCSubDir [Opt]
opts
       let importdirs :: [String]
importdirs = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getImportDir [Opt]
opts
       let sourcedirs :: [String]
sourcedirs = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getSourceDir [Opt]
opts
       [String] -> Idris ()
setSourceDirs [String]
sourcedirs
       let bcs :: [String]
bcs = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getBC [Opt]
opts
       let pkgdirs :: [String]
pkgdirs = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getPkgDir [Opt]
opts
       -- Set default optimisations
       let optimise :: Int
optimise = case (Opt -> Maybe Int) -> [Opt] -> [Int]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe Int
getOptLevel [Opt]
opts of
                        [] -> Int
1
                        [Int]
xs -> [Int] -> Int
forall a. HasCallStack => [a] -> a
last [Int]
xs

       Int -> Idris ()
setOptLevel Int
optimise
       let outty :: OutputType
outty = case (Opt -> Maybe OutputType) -> [Opt] -> [OutputType]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe OutputType
getOutputTy [Opt]
opts of
                     [] -> if Opt
Interface Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts then
                              OutputType
Object else OutputType
Executable
                     [OutputType]
xs -> [OutputType] -> OutputType
forall a. HasCallStack => [a] -> a
last [OutputType]
xs
       let cgn :: Codegen
cgn = case (Opt -> Maybe Codegen) -> [Opt] -> [Codegen]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe Codegen
getCodegen [Opt]
opts of
                   [] -> IRFormat -> String -> Codegen
Via IRFormat
IBCFormat String
"c"
                   [Codegen]
xs -> [Codegen] -> Codegen
forall a. HasCallStack => [a] -> a
last [Codegen]
xs
       let cgFlags :: [String]
cgFlags = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getCodegenArgs [Opt]
opts

       -- Now set/unset specifically chosen optimisations
       let os :: [(Bool, Optimisation)]
os = (Opt -> Maybe (Bool, Optimisation))
-> [Opt] -> [(Bool, Optimisation)]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe (Bool, Optimisation)
getOptimisation [Opt]
opts

       ((Bool, Optimisation) -> Idris ())
-> [(Bool, Optimisation)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool, Optimisation) -> Idris ()
processOptimisation [(Bool, Optimisation)]
os

       script <- case (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getExecScript [Opt]
opts of
                   []     -> Maybe String -> StateT IState (ExceptT Err IO) (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
                   String
x:String
y:[String]
xs -> do String -> Idris ()
iputStrLn String
"More than one interpreter expression found."
                                IO (Maybe String) -> StateT IState (ExceptT Err IO) (Maybe String)
forall a. IO a -> Idris a
runIO (IO (Maybe String)
 -> StateT IState (ExceptT Err IO) (Maybe String))
-> IO (Maybe String)
-> StateT IState (ExceptT Err IO) (Maybe String)
forall a b. (a -> b) -> a -> b
$ ExitCode -> IO (Maybe String)
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
                   [String
expr] -> Maybe String -> StateT IState (ExceptT Err IO) (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
expr)
       let immediate = (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getEvalExpr [Opt]
opts
       let port = case [Opt] -> Maybe REPLPort
getPort [Opt]
opts of
                    Maybe REPLPort
Nothing -> PortNumber -> REPLPort
ListenPort PortNumber
defaultPort
                    Just REPLPort
p  -> REPLPort
p

       when (DefaultTotal `elem` opts) $ do i <- getIState
                                            putIState (i { default_total = DefaultCheckingTotal })
       tty <- runIO isATTY
       setColourise $ not quiet && last (tty : opt getColour opts)
       runIO $ hSetBuffering stdout LineBuffering



       mapM_ addLangExt (opt getLanguageExt opts)
       setREPL runrepl
       setQuiet (quiet || isJust script || not (null immediate))

       setCmdLine opts
       setOutputTy outty
       setNoBanner nobanner
       setCodegen cgn
       mapM_ (addFlag cgn) cgFlags
       mapM_ makeOption opts
       vlevel <- verbose
       when (runrepl && vlevel == 0) $ setVerbose 1

       -- if we have the --bytecode flag, drop into the bytecode assembler
       case bcs of
         [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         [String]
xs -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- runIO $ mapM_ bcAsm xs
       case ibcsubdir of
         [] -> String -> Idris ()
setIBCSubDir String
""
         (String
d:[String]
_) -> String -> Idris ()
setIBCSubDir String
d
       setImportDirs importdirs

       setNoBanner nobanner

       -- Check if listed packages are actually installed

       idrisCatch (do ipkgs <- runIO $ getIdrisInstalledPackages
                      let diff_pkgs = [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
(\\) [String]
pkgdirs [String]
ipkgs

                      when (not $ null diff_pkgs) $ do
                        iputStrLn "The following packages were specified but cannot be found:"
                        iputStr $ unlines $ map (\String
x -> [String] -> String
unwords [String
"-", String
x]) diff_pkgs
                        runIO $ exitWith (ExitFailure 1))
                  (\Err
e -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

       when (not (NoBasePkgs `elem` opts)) $ do
           addPkgDir "prelude"
           addPkgDir "base"

       mapM_ addPkgDir pkgdirs
       elabPrims
       when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL False)
                                                addAutoImport "Builtins"
                                                return ()
       when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL False)
                                               addAutoImport "Prelude"
                                               return ()
       when (runrepl && not idesl) initScript

       nobanner <- getNoBanner

       when (runrepl &&
             not quiet &&
             not idesl &&
             not (isJust script) &&
             not nobanner &&
             null immediate) $
         iputStrLn banner

       orig <- getIState

       mods <- if idesl then return [] else loadInputs inputs Nothing
       let efile = case [String]
inputs of
                        [] -> String
""
                        (String
f:[String]
_) -> String
f

       ok <- noErrors
       when ok $ case output of
                    [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    (String
o:[String]
_) -> Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (String -> Command -> Idris ()
process String
"" (Codegen -> String -> Command
Compile Codegen
cgn String
o))
                               (\Err
e -> do ist <- Idris IState
getIState ; iputStrLn $ pshow ist e)

       case immediate of
         [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         [String]
exprs -> do ConsoleWidth -> Idris ()
setWidth ConsoleWidth
InfinitelyWide
                     (String -> Idris ()) -> [String] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\String
str -> do ist <- Idris IState
getIState
                                       c <- colourise
                                       case parseExpr ist str of
                                         Left ParseError
err -> do ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                                                        IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ ExitCode -> IO ()
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
                                         Right PTerm
e -> String -> Command -> Idris ()
process String
"" (PTerm -> Command
Eval PTerm
e))
                           [String]
exprs
                     IO () -> Idris ()
forall a. IO a -> Idris a
runIO IO ()
forall a. IO a
exitSuccess


       case script of
         Maybe String
Nothing -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Just String
expr -> String -> Idris ()
execScript String
expr

       -- Create Idris data dir + repl history and config dir
       idrisCatch (do dir <- runIO $ getIdrisUserDataDir
                      exists <- runIO $ doesDirectoryExist dir
                      unless exists $ logLvl 1 ("Creating " ++ dir)
                      runIO $ createDirectoryIfMissing True (dir </> "repl"))
         (\Err
e -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

       historyFile <- runIO $ getIdrisHistoryFile

       when ok $ case opt getPkgIndex opts of
                      (String
f : [String]
_) -> String -> Idris ()
writePkgIndex String
f
                      [String]
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

       when (runrepl && not idesl) $ do
--          clearOrigPats
         case port of
           REPLPort
DontListen -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           ListenPort PortNumber
port' -> PortNumber -> IState -> [String] -> Idris ()
startServer PortNumber
port' IState
orig [String]
mods
         runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile
       let idesock = Opt
IdemodeSocket Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       when (idesl) $ idemodeStart idesock orig inputs
       ok <- noErrors
       when (not ok) $ runIO (exitWith (ExitFailure 1))
  where
    makeOption :: Opt -> Idris ()
makeOption (OLogging Int
i)     = Int -> Idris ()
setLogLevel Int
i
    makeOption (OLogCats [LogCat]
cs)    = [LogCat] -> Idris ()
setLogCats [LogCat]
cs
    makeOption (Verbose Int
v)      = Int -> Idris ()
setVerbose Int
v
    makeOption Opt
TypeCase         = Bool -> Idris ()
setTypeCase Bool
True
    makeOption Opt
TypeInType       = Bool -> Idris ()
setTypeInType Bool
True
    makeOption Opt
NoCoverage       = Bool -> Idris ()
setCoverage Bool
False
    makeOption Opt
ErrContext       = Bool -> Idris ()
setErrContext Bool
True
    makeOption (IndentWith Int
n)   = Int -> Idris ()
setIndentWith Int
n
    makeOption (IndentClause Int
n) = Int -> Idris ()
setIndentClause Int
n
    makeOption Opt
_                = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    processOptimisation :: (Bool,Optimisation) -> Idris ()
    processOptimisation :: (Bool, Optimisation) -> Idris ()
processOptimisation (Bool
True,  Optimisation
p) = Optimisation -> Idris ()
addOptimise Optimisation
p
    processOptimisation (Bool
False, Optimisation
p) = Optimisation -> Idris ()
removeOptimise Optimisation
p

    addPkgDir :: String -> Idris ()
    addPkgDir :: String -> Idris ()
addPkgDir String
p = do ddir <- IO String -> Idris String
forall a. IO a -> Idris a
runIO IO String
getIdrisLibDir
                     addImportDir (ddir </> p)
                     addIBC (IBCImportDir (ddir </> p))



-- | Invoke as if from command line. It is an error if there are
-- unresolved totality problems.
idris :: [Opt] -> IO (Maybe IState)
idris :: [Opt] -> IO (Maybe IState)
idris [Opt]
opts = do res <- ExceptT Err IO IState -> IO (Either Err IState)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Err IO IState -> IO (Either Err IState))
-> ExceptT Err IO IState -> IO (Either Err IState)
forall a b. (a -> b) -> a -> b
$ Idris () -> IState -> ExceptT Err IO IState
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Idris ()
totalMain IState
idrisInit
                case res of
                  Left Err
err -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> String
pshow IState
idrisInit Err
err
                                 Maybe IState -> IO (Maybe IState)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IState
forall a. Maybe a
Nothing
                  Right IState
ist -> Maybe IState -> IO (Maybe IState)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IState -> Maybe IState
forall a. a -> Maybe a
Just IState
ist)
    where totalMain :: Idris ()
totalMain = do [Opt] -> Idris ()
idrisMain [Opt]
opts
                         ist <- Idris IState
getIState
                         case idris_totcheckfail ist of
                           ((FC
fc, String
msg):[(FC, String)]
_) -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (String -> Err) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> (String -> Err) -> String -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> Err
forall t. String -> Err' t
Msg (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Could not build: "String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
msg
                           [] -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Execute the provided Idris expression.
execScript :: String -> Idris ()
execScript :: String -> Idris ()
execScript String
expr = do i <- Idris IState
getIState
                     c <- colourise
                     case parseExpr i expr of
                          Left ParseError
err -> do ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                                         IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ ExitCode -> IO ()
forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
1)
                          Right PTerm
term -> do ctxt <- Idris Context
getContext
                                           (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
                                           res <- execute tm
                                           runIO $ exitSuccess

-- | Run the initialisation script
initScript :: Idris ()
initScript :: Idris ()
initScript = do script <- IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ IO String
getIdrisInitScript
                idrisCatch (do go <- runIO $ doesFileExist script
                               when go $ do
                                 h <- runIO $ openFile script ReadMode
                                 runInit h
                                 runIO $ hClose h)
                           (\Err
e -> String -> Idris ()
iPrintError (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Error reading init file: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e)
    where runInit :: Handle -> Idris ()
          runInit :: Handle -> Idris ()
runInit Handle
h = do eof <- ExceptT Err IO Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => m a -> StateT IState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT Err IO Bool -> Idris Bool)
-> (IO Bool -> ExceptT Err IO Bool) -> IO Bool -> Idris Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IO Bool -> ExceptT Err IO Bool
forall (m :: * -> *) a. Monad m => m a -> ExceptT Err m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ Handle -> IO Bool
hIsEOF Handle
h
                         ist <- getIState
                         unless eof $ do
                           line <- runIO $ hGetLine h
                           script <- runIO $ getIdrisInitScript
                           c <- colourise
                           processLine ist line script c
                           runInit h
          processLine :: IState -> String -> String -> p -> Idris ()
processLine IState
i String
cmd String
input p
clr =
              case IState
-> String -> String -> Either ParseError (Either String Command)
parseCmd IState
i String
input String
cmd of
                   Left ParseError
err -> ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                   Right (Right Command
Reload) -> String -> Idris ()
iPrintError String
"Init scripts cannot reload the file"
                   Right (Right (Load String
f Maybe Int
_)) -> String -> Idris ()
iPrintError String
"Init scripts cannot load files"
                   Right (Right (ModImport String
f)) -> String -> Idris ()
iPrintError String
"Init scripts cannot import modules"
                   Right (Right Command
Edit) -> String -> Idris ()
iPrintError String
"Init scripts cannot invoke the editor"
                   Right (Right Command
Proofs) -> IState -> Idris ()
proofs IState
i
                   Right (Right Command
Quit) -> String -> Idris ()
iPrintError String
"Init scripts cannot quit Idris"
                   Right (Right Command
cmd ) -> String -> Command -> Idris ()
process [] Command
cmd
                   Right (Left String
err) -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. Show a => a -> IO ()
print String
err