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 prog = withCP65001 $ do
res <- runExceptT $ execStateT prog idrisInit
case res of
Left err -> do
putStrLn $ "Uncaught error: " ++ show err
exitFailure
Right _ -> return ()
idrisMain :: [Opt] -> Idris ()
idrisMain opts =
do mapM_ setWidth (opt getConsoleWidth opts)
let inputs = opt getFile opts
let quiet = Quiet `elem` opts
let nobanner = NoBanner `elem` opts
let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts
let runrepl = not (NoREPL `elem` opts)
let output = opt getOutput opts
let ibcsubdir = opt getIBCSubDir opts
let importdirs = opt getImportDir opts
let sourcedirs = opt getSourceDir opts
setSourceDirs sourcedirs
let bcs = opt getBC opts
let pkgdirs = opt getPkgDir opts
let optimise = case opt getOptLevel opts of
[] -> 1
xs -> last xs
setOptLevel optimise
let outty = case opt getOutputTy opts of
[] -> if Interface `elem` opts then
Object else Executable
xs -> last xs
let cgn = case opt getCodegen opts of
[] -> Via IBCFormat "c"
xs -> last xs
let cgFlags = opt getCodegenArgs opts
let os = opt getOptimisation opts
mapM_ processOptimisation os
script <- case opt getExecScript opts of
[] -> return Nothing
x:y:xs -> do iputStrLn "More than one interpreter expression found."
runIO $ exitWith (ExitFailure 1)
[expr] -> return (Just expr)
let immediate = opt getEvalExpr opts
let port = case getPort opts of
Nothing -> ListenPort defaultPort
Just p -> p
when (DefaultTotal `elem` opts) $ do i <- getIState
putIState (i { default_total = DefaultCheckingTotal })
tty <- runIO isATTY
setColourise $ not quiet && last (tty : opt getColour opts)
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
case bcs of
[] -> return ()
xs -> return ()
case ibcsubdir of
[] -> setIBCSubDir ""
(d:_) -> setIBCSubDir d
setImportDirs importdirs
setNoBanner nobanner
idrisCatch (do ipkgs <- runIO $ getIdrisInstalledPackages
let diff_pkgs = (\\) pkgdirs ipkgs
when (not $ null diff_pkgs) $ do
iputStrLn "The following packages were specified but cannot be found:"
iputStr $ unlines $ map (\x -> unwords ["-", x]) diff_pkgs
runIO $ exitWith (ExitFailure 1))
(\e -> 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 inputs of
[] -> ""
(f:_) -> f
runIO $ hSetBuffering stdout LineBuffering
ok <- noErrors
when ok $ case output of
[] -> return ()
(o:_) -> idrisCatch (process "" (Compile cgn o))
(\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
case immediate of
[] -> return ()
exprs -> do setWidth InfinitelyWide
mapM_ (\str -> do ist <- getIState
c <- colourise
case parseExpr ist str of
Left err -> do emitWarning err
runIO $ exitWith (ExitFailure 1)
Right e -> process "" (Eval e))
exprs
runIO exitSuccess
case script of
Nothing -> return ()
Just expr -> execScript expr
idrisCatch (do dir <- runIO $ getIdrisUserDataDir
exists <- runIO $ doesDirectoryExist dir
unless exists $ logLvl 1 ("Creating " ++ dir)
runIO $ createDirectoryIfMissing True (dir </> "repl"))
(\e -> return ())
historyFile <- runIO $ getIdrisHistoryFile
when ok $ case opt getPkgIndex opts of
(f : _) -> writePkgIndex f
_ -> return ()
when (runrepl && not idesl) $ do
case port of
DontListen -> return ()
ListenPort port' -> startServer port' orig mods
runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile
let idesock = IdemodeSocket `elem` opts
when (idesl) $ idemodeStart idesock orig inputs
ok <- noErrors
when (not ok) $ runIO (exitWith (ExitFailure 1))
where
makeOption (OLogging i) = setLogLevel i
makeOption (OLogCats cs) = setLogCats cs
makeOption (Verbose v) = setVerbose v
makeOption TypeCase = setTypeCase True
makeOption TypeInType = setTypeInType True
makeOption NoCoverage = setCoverage False
makeOption ErrContext = setErrContext True
makeOption (IndentWith n) = setIndentWith n
makeOption (IndentClause n) = setIndentClause n
makeOption _ = return ()
processOptimisation :: (Bool,Optimisation) -> Idris ()
processOptimisation (True, p) = addOptimise p
processOptimisation (False, p) = removeOptimise p
addPkgDir :: String -> Idris ()
addPkgDir p = do ddir <- runIO getIdrisLibDir
addImportDir (ddir </> p)
addIBC (IBCImportDir (ddir </> p))
idris :: [Opt] -> IO (Maybe IState)
idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
case res of
Left err -> do putStrLn $ pshow idrisInit err
return Nothing
Right ist -> return (Just ist)
where totalMain = do idrisMain opts
ist <- getIState
case idris_totcheckfail ist of
((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
[] -> return ()
execScript :: String -> Idris ()
execScript expr = do i <- getIState
c <- colourise
case parseExpr i expr of
Left err -> do emitWarning err
runIO $ exitWith (ExitFailure 1)
Right term -> do ctxt <- getContext
(tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
res <- execute tm
runIO $ exitSuccess
initScript :: Idris ()
initScript = do script <- runIO $ getIdrisInitScript
idrisCatch (do go <- runIO $ doesFileExist script
when go $ do
h <- runIO $ openFile script ReadMode
runInit h
runIO $ hClose h)
(\e -> iPrintError $ "Error reading init file: " ++ show e)
where runInit :: Handle -> Idris ()
runInit h = do eof <- lift . lift $ hIsEOF h
ist <- getIState
unless eof $ do
line <- runIO $ hGetLine h
script <- runIO $ getIdrisInitScript
c <- colourise
processLine ist line script c
runInit h
processLine i cmd input clr =
case parseCmd i input cmd of
Left err -> emitWarning err
Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"
Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
Right (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
Right (Right Proofs) -> proofs i
Right (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
Right (Right cmd ) -> process [] cmd
Right (Left err) -> runIO $ print err