module Idris.Main
( idrisMain
, idris
, runMain
, runClient
, loadInputs
) 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)
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
Either Err IState
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 Either Err IState
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 ()
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
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
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
Maybe String
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 :: [String]
immediate = (Opt -> Maybe String) -> [Opt] -> [String]
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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Opt
DefaultTotal Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do IState
i <- Idris IState
getIState
IState -> Idris ()
putIState (IState
i { default_total = DefaultCheckingTotal })
Bool
tty <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO IO Bool
isATTY
Bool -> Idris ()
setColourise (Bool -> Idris ()) -> Bool -> Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
quiet Bool -> Bool -> Bool
&& [Bool] -> Bool
forall a. HasCallStack => [a] -> a
last (Bool
tty Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (Opt -> Maybe Bool) -> [Opt] -> [Bool]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe Bool
getColour [Opt]
opts)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdout BufferMode
LineBuffering
(LanguageExt -> Idris ()) -> [LanguageExt] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LanguageExt -> Idris ()
addLangExt ((Opt -> Maybe LanguageExt) -> [Opt] -> [LanguageExt]
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
|| Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
script Bool -> Bool -> Bool
|| Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
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
(String -> Idris ()) -> [String] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Codegen -> String -> Idris ()
addFlag Codegen
cgn) [String]
cgFlags
(Opt -> Idris ()) -> [Opt] -> Idris ()
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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&& Int
vlevel Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> Idris ()
setVerbose Int
1
case [String]
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 ()
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
Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do [String]
ipkgs <- 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]
getIdrisInstalledPackages
let diff_pkgs :: [String]
diff_pkgs = [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
(\\) [String]
pkgdirs [String]
ipkgs
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
diff_pkgs) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
String -> Idris ()
iputStrLn String
"The following packages were specified but cannot be found:"
String -> Idris ()
iputStr (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> [String] -> String
unwords [String
"-", String
x]) [String]
diff_pkgs
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))
(\Err
e -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoBasePkgs Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
String -> Idris ()
addPkgDir String
"prelude"
String -> Idris ()
addPkgDir String
"base"
(String -> Idris ()) -> [String] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> Idris ()
addPkgDir [String]
pkgdirs
Idris ()
elabPrims
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoBuiltins Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) (Idris () -> Idris ()) -> Idris () -> Idris ()
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"
() -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Opt
NoPrelude Opt -> [Opt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts)) (Idris () -> Idris ()) -> Idris () -> Idris ()
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"
() -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool -> Idris () -> Idris ()
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
Bool -> Idris () -> Idris ()
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 (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
script) Bool -> Bool -> Bool
&&
Bool -> Bool
not Bool
nobanner Bool -> Bool -> Bool
&&
[String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
immediate) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
String -> Idris ()
iputStrLn String
banner
IState
orig <- Idris IState
getIState
[String]
mods <- if Bool
idesl then [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [String] -> Maybe Int -> Idris [String]
loadInputs [String]
inputs Maybe Int
forall a. Maybe a
Nothing
let efile :: String
efile = case [String]
inputs of
[] -> String
""
(String
f:[String]
_) -> String
f
Bool
ok <- Idris Bool
noErrors
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ case [String]
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 IState
ist <- Idris IState
getIState ; String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> String
pshow IState
ist Err
e)
case [String]
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 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 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 Maybe String
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
Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do String
dir <- 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
getIdrisUserDataDir
Bool
exists <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesDirectoryExist String
dir
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> Idris ()
logLvl Int
1 (String
"Creating " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
dir)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String
dir String -> String -> String
</> String
"repl"))
(\Err
e -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
String
historyFile <- 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
getIdrisHistoryFile
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ case (Opt -> Maybe String) -> [Opt] -> [String]
forall a. (Opt -> Maybe a) -> [Opt] -> [a]
opt Opt -> Maybe String
getPkgIndex [Opt]
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 ()
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
runrepl Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
idesl) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
case REPLPort
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
Settings (StateT IState (ExceptT Err IO))
-> InputT (StateT IState (ExceptT Err IO)) () -> Idris ()
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (Maybe String -> Settings (StateT IState (ExceptT Err IO))
replSettings (String -> Maybe String
forall a. a -> Maybe a
Just String
historyFile)) (InputT (StateT IState (ExceptT Err IO)) () -> Idris ())
-> InputT (StateT IState (ExceptT Err IO)) () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
-> [String] -> String -> InputT (StateT IState (ExceptT Err IO)) ()
repl (IState -> IState
forall a. NFData a => a -> a
force IState
orig) [String]
mods String
efile
let idesock :: Bool
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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
idesl) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> IState -> [String] -> Idris ()
idemodeStart Bool
idesock IState
orig [String]
inputs
Bool
ok <- Idris Bool
noErrors
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
ok) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IO () -> Idris ()
forall a. IO a -> Idris a
runIO (ExitCode -> IO ()
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
_ = () -> 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 String
ddir <- IO String -> Idris String
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))
idris :: [Opt] -> IO (Maybe IState)
idris :: [Opt] -> IO (Maybe IState)
idris [Opt]
opts = do Either Err IState
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 Either Err IState
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
IState
ist <- Idris IState
getIState
case IState -> [(FC, String)]
idris_totcheckfail IState
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 ()
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 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 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
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IO ()
forall a. IO a
exitSuccess
initScript :: Idris ()
initScript :: Idris ()
initScript = do String
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
Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do Bool
go <- IO Bool -> Idris Bool
forall a. IO a -> Idris a
runIO (IO Bool -> Idris Bool) -> IO Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
script
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
go (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
Handle
h <- IO Handle -> Idris Handle
forall a. IO a -> Idris a
runIO (IO Handle -> Idris Handle) -> IO Handle -> Idris Handle
forall a b. (a -> b) -> a -> b
$ String -> IOMode -> IO Handle
openFile String
script IOMode
ReadMode
Handle -> Idris ()
runInit Handle
h
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Handle -> IO ()
hClose Handle
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 Bool
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
IState
ist <- Idris IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
eof (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
String
line <- 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
$ Handle -> IO String
hGetLine Handle
h
String
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
Bool
c <- Idris Bool
colourise
IState -> String -> String -> Bool -> Idris ()
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 -> 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