{-|
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 = forall a. IO a -> IO a
withCP65001 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.
  Either Err IState
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Idris ()
prog IState
idrisInit
  case Either Err IState
res of
       Left Err
err -> do
         String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Uncaught error: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
err
         forall a. IO a
exitFailure
       Right IState
_ -> 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   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ConsoleWidth -> Idris ()
setWidth (forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe ConsoleWidth
getConsoleWidth [Opt]
opts)
       let inputs :: [String]
inputs = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getFile [Opt]
opts
       let quiet :: Bool
quiet = Opt
Quiet forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let nobanner :: Bool
nobanner = Opt
NoBanner forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let idesl :: Bool
idesl = Opt
Idemode forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts Bool -> Bool -> Bool
|| Opt
IdemodeSocket forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let runrepl :: Bool
runrepl = Bool -> Bool
not (Opt
NoREPL forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)
       let output :: [String]
output = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getOutput [Opt]
opts
       let ibcsubdir :: [String]
ibcsubdir = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getIBCSubDir [Opt]
opts
       let importdirs :: [String]
importdirs = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getImportDir [Opt]
opts
       let sourcedirs :: [String]
sourcedirs = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getSourceDir [Opt]
opts
       [String] -> Idris ()
setSourceDirs [String]
sourcedirs
       let bcs :: [String]
bcs = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getBC [Opt]
opts
       let pkgdirs :: [String]
pkgdirs = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getPkgDir [Opt]
opts
       -- Set default optimisations
       let optimise :: Int
optimise = case forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe Int
getOptLevel [Opt]
opts of
                        [] -> Int
1
                        [Int]
xs -> forall a. [a] -> a
last [Int]
xs

       Int -> Idris ()
setOptLevel Int
optimise
       let outty :: OutputType
outty = case forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe OutputType
getOutputTy [Opt]
opts of
                     [] -> if Opt
Interface forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts then
                              OutputType
Object else OutputType
Executable
                     [OutputType]
xs -> forall a. [a] -> a
last [OutputType]
xs
       let cgn :: Codegen
cgn = case 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 -> forall a. [a] -> a
last [Codegen]
xs
       let cgFlags :: [String]
cgFlags = 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 = forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe (Bool, Optimisation)
getOptimisation [Opt]
opts

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

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

       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Opt
DefaultTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts) forall a b. (a -> b) -> a -> b
$ do IState
i <- Idris IState
getIState
                                            IState -> Idris ()
putIState (IState
i { default_total :: DefaultTotality
default_total = DefaultTotality
DefaultCheckingTotal })
       Bool
tty <- forall a. IO a -> Idris a
runIO IO Bool
isATTY
       Bool -> Idris ()
setColourise forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
quiet Bool -> Bool -> Bool
&& forall a. [a] -> a
last (Bool
tty forall a. a -> [a] -> [a]
: forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe Bool
getColour [Opt]
opts)
       forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdout BufferMode
LineBuffering



       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt (forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe LanguageExt
getLanguageExt [Opt]
opts)
       Bool -> Idris ()
setREPL Bool
runrepl
       Bool -> Idris ()
setQuiet (Bool
quiet Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust Maybe String
script Bool -> Bool -> Bool
|| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
immediate))

       [Opt] -> Idris ()
setCmdLine [Opt]
opts
       OutputType -> Idris ()
setOutputTy OutputType
outty
       Bool -> Idris ()
setNoBanner Bool
nobanner
       Codegen -> Idris ()
setCodegen Codegen
cgn
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Codegen -> String -> Idris ()
addFlag Codegen
cgn) [String]
cgFlags
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Opt -> Idris ()
makeOption [Opt]
opts
       Int
vlevel <- Idris Int
verbose
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&& Int
vlevel forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$ Int -> Idris ()
setVerbose Int
1

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

       Bool -> Idris ()
setNoBanner Bool
nobanner

       -- Check if listed packages are actually installed

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

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

       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoBasePkgs forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) forall a b. (a -> b) -> a -> b
$ do
           String -> Idris ()
addPkgDir String
"prelude"
           String -> Idris ()
addPkgDir String
"base"

       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> Idris ()
addPkgDir [String]
pkgdirs
       Idris ()
elabPrims
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoBuiltins forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) forall a b. (a -> b) -> a -> b
$ do Maybe String
x <- String -> IBCPhase -> StateT IState (ExceptT Err IO) (Maybe String)
loadModule String
"Builtins" (Bool -> IBCPhase
IBC_REPL Bool
False)
                                                String -> Idris ()
addAutoImport String
"Builtins"
                                                forall (m :: * -> *) a. Monad m => a -> m a
return ()
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoPrelude forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) forall a b. (a -> b) -> a -> b
$ do Maybe String
x <- String -> IBCPhase -> StateT IState (ExceptT Err IO) (Maybe String)
loadModule String
"Prelude" (Bool -> IBCPhase
IBC_REPL Bool
False)
                                               String -> Idris ()
addAutoImport String
"Prelude"
                                               forall (m :: * -> *) a. Monad m => a -> m a
return ()
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
idesl) Idris ()
initScript

       Bool
nobanner <- Idris Bool
getNoBanner

       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&&
             Bool -> Bool
not Bool
quiet Bool -> Bool -> Bool
&&
             Bool -> Bool
not Bool
idesl Bool -> Bool -> Bool
&&
             Bool -> Bool
not (forall a. Maybe a -> Bool
isJust Maybe String
script) Bool -> Bool -> Bool
&&
             Bool -> Bool
not Bool
nobanner Bool -> Bool -> Bool
&&
             forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
immediate) forall a b. (a -> b) -> a -> b
$
         String -> Idris ()
iputStrLn String
banner

       IState
orig <- Idris IState
getIState

       [String]
mods <- if Bool
idesl then forall (m :: * -> *) a. Monad m => a -> m a
return [] else [String] -> Maybe Int -> Idris [String]
loadInputs [String]
inputs forall a. Maybe a
Nothing
       let efile :: String
efile = case [String]
inputs of
                        [] -> String
""
                        (String
f:[String]
_) -> String
f

       Bool
ok <- Idris Bool
noErrors
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok forall a b. (a -> b) -> a -> b
$ case [String]
output of
                    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    (String
o:[String]
_) -> 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 IState
ist <- Idris IState
getIState ; String -> Idris ()
iputStrLn forall a b. (a -> b) -> a -> b
$ IState -> Err -> String
pshow IState
ist Err
e)

       case [String]
immediate of
         [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
         [String]
exprs -> do ConsoleWidth -> Idris ()
setWidth ConsoleWidth
InfinitelyWide
                     forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\String
str -> do IState
ist <- Idris IState
getIState
                                       Bool
c <- Idris Bool
colourise
                                       case IState -> String -> Either ParseError PTerm
parseExpr IState
ist String
str of
                                         Left ParseError
err -> do forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                                                        forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ 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
                     forall a. IO a -> Idris a
runIO forall a. IO a
exitSuccess


       case Maybe String
script of
         Maybe String
Nothing -> 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
       forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do String
dir <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ IO String
getIdrisUserDataDir
                      Bool
exists <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesDirectoryExist String
dir
                      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logLvl Int
1 (String
"Creating " forall a. [a] -> [a] -> [a]
++ String
dir)
                      forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
dir String -> String -> String
</> String
"repl"))
         (\Err
e -> forall (m :: * -> *) a. Monad m => a -> m a
return ())

       String
historyFile <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ IO String
getIdrisHistoryFile

       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok forall a b. (a -> b) -> a -> b
$ case forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getPkgIndex [Opt]
opts of
                      (String
f : [String]
_) -> String -> Idris ()
writePkgIndex String
f
                      [String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
idesl) forall a b. (a -> b) -> a -> b
$ do
--          clearOrigPats
         case REPLPort
port of
           REPLPort
DontListen -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
           ListenPort PortNumber
port' -> PortNumber -> IState -> [String] -> Idris ()
startServer PortNumber
port' IState
orig [String]
mods
         forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (Maybe String -> Settings (StateT IState (ExceptT Err IO))
replSettings (forall a. a -> Maybe a
Just String
historyFile)) forall a b. (a -> b) -> a -> b
$ IState
-> [String] -> String -> InputT (StateT IState (ExceptT Err IO)) ()
repl (forall a. NFData a => a -> a
force IState
orig) [String]
mods String
efile
       let idesock :: Bool
idesock = Opt
IdemodeSocket forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
idesl) forall a b. (a -> b) -> a -> b
$ Bool -> IState -> [String] -> Idris ()
idemodeStart Bool
idesock IState
orig [String]
inputs
       Bool
ok <- Idris Bool
noErrors
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
ok) forall a b. (a -> b) -> a -> b
$ forall a. IO a -> Idris a
runIO (forall a. ExitCode -> IO a
exitWith (Int -> ExitCode
ExitFailure Int
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
_                = 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 String
ddir <- forall a. IO a -> Idris a
runIO IO String
getIdrisLibDir
                     String -> Idris ()
addImportDir (String
ddir String -> String -> String
</> String
p)
                     IBCWrite -> Idris ()
addIBC (String -> IBCWrite
IBCImportDir (String
ddir String -> String -> String
</> String
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 Either Err IState
res <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Idris ()
totalMain IState
idrisInit
                case Either Err IState
res of
                  Left Err
err -> do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ IState -> Err -> String
pshow IState
idrisInit Err
err
                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                  Right IState
ist -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just IState
ist)
    where totalMain :: Idris ()
totalMain = do [Opt] -> Idris ()
idrisMain [Opt]
opts
                         IState
ist <- Idris IState
getIState
                         case IState -> [(FC, String)]
idris_totcheckfail IState
ist of
                           ((FC
fc, String
msg):[(FC, String)]
_) -> forall a. Err -> Idris a
ierror forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall t. FC -> Err' t -> Err' t
At FC
fc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Could not build: "forall a. [a] -> [a] -> [a]
++  String
msg
                           [] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()


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

-- | Run the initialisation script
initScript :: Idris ()
initScript :: Idris ()
initScript = do String
script <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ IO String
getIdrisInitScript
                forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do Bool
go <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
script
                               forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
go forall a b. (a -> b) -> a -> b
$ do
                                 Handle
h <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IOMode -> IO Handle
openFile String
script IOMode
ReadMode
                                 Handle -> Idris ()
runInit Handle
h
                                 forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> IO ()
hClose Handle
h)
                           (\Err
e -> String -> Idris ()
iPrintError forall a b. (a -> b) -> a -> b
$ String
"Error reading init file: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Err
e)
    where runInit :: Handle -> Idris ()
          runInit :: Handle -> Idris ()
runInit Handle
h = do Bool
eof <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Handle -> IO Bool
hIsEOF Handle
h
                         IState
ist <- Idris IState
getIState
                         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
eof forall a b. (a -> b) -> a -> b
$ do
                           String
line <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
h
                           String
script <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ IO String
getIdrisInitScript
                           Bool
c <- Idris Bool
colourise
                           forall {p}. IState -> String -> String -> p -> Idris ()
processLine IState
ist String
line String
script Bool
c
                           Handle -> Idris ()
runInit Handle
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 -> 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) -> forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> IO ()
print String
err