{-|
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 prog :: 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.
  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
err -> do
         String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "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 _ -> () -> IO ()
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 opts :: [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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts
       let nobanner :: Bool
nobanner = Opt
NoBanner Opt -> [Opt] -> 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts Bool -> Bool -> Bool
|| Opt
IdemodeSocket Opt -> [Opt] -> 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 (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
                        [] -> 1
                        xs :: [Int]
xs -> [Int] -> Int
forall a. [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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Opt]
opts then
                              OutputType
Object else OutputType
Executable
                     xs :: [OutputType]
xs -> [OutputType] -> OutputType
forall a. [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 "c"
                   xs :: [Codegen]
xs -> [Codegen] -> Codegen
forall a. [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

       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 (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
                   x :: String
x:y :: String
y:xs :: [String]
xs -> do String -> Idris ()
iputStrLn "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 1)
                   [expr :: String
expr] -> Maybe String -> StateT IState (ExceptT Err IO) (Maybe String)
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
                    Nothing -> PortNumber -> REPLPort
ListenPort PortNumber
defaultPort
                    Just p :: REPLPort
p  -> REPLPort
p

       Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Opt
DefaultTotal Opt -> [Opt] -> 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 :: DefaultTotality
default_total = DefaultTotality
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. [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 (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
== 0) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Int -> Idris ()
setVerbose 1

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

       Bool -> Idris ()
setNoBanner Bool
nobanner

       -- Check if listed packages are actually installed

       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 (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 "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 (\x :: String
x -> [String] -> String
unwords ["-", 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 1))
                  (\e :: Err
e -> () -> Idris ()
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 (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 "prelude"
           String -> Idris ()
addPkgDir "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 (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 "Builtins" (Bool -> IBCPhase
IBC_REPL Bool
False)
                                                String -> Idris ()
addAutoImport "Builtins"
                                                () -> Idris ()
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 (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 "Prelude" (Bool -> IBCPhase
IBC_REPL Bool
False)
                                               String -> Idris ()
addAutoImport "Prelude"
                                               () -> Idris ()
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 (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 (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
                        [] -> ""
                        (f :: String
f:_) -> 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 (m :: * -> *) a. Monad m => a -> m a
return ()
                    (o :: String
o:_) -> Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (String -> Command -> Idris ()
process "" (Codegen -> String -> Command
Compile Codegen
cgn String
o))
                               (\e :: 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 (m :: * -> *) a. Monad m => a -> m a
return ()
         exprs :: [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_ (\str :: 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 err :: 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 1)
                                         Right e :: PTerm
e -> String -> Command -> Idris ()
process "" (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
         Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Just expr :: String
expr -> String -> Idris ()
execScript String
expr

       -- Create Idris data dir + repl history and config dir
       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 1 ("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
</> "repl"))
         (\e :: Err
e -> () -> Idris ()
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
                      (f :: String
f : _) -> String -> Idris ()
writePkgIndex String
f
                      _ -> () -> Idris ()
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
--          clearOrigPats
         case REPLPort
port of
           DontListen -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           ListenPort port' :: PortNumber
port' -> PortNumber -> IState -> [String] -> Idris ()
startServer PortNumber
port' IState
orig [String]
mods
         Settings Idris -> InputT Idris () -> Idris ()
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
runInputT (Maybe String -> Settings Idris
replSettings (String -> Maybe String
forall a. a -> Maybe a
Just String
historyFile)) (InputT Idris () -> Idris ()) -> InputT Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> [String] -> String -> InputT Idris ()
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 (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 1))
  where
    makeOption :: Opt -> Idris ()
makeOption (OLogging i :: Int
i)     = Int -> Idris ()
setLogLevel Int
i
    makeOption (OLogCats cs :: [LogCat]
cs)    = [LogCat] -> Idris ()
setLogCats [LogCat]
cs
    makeOption (Verbose v :: Int
v)      = Int -> Idris ()
setVerbose Int
v
    makeOption TypeCase         = Bool -> Idris ()
setTypeCase Bool
True
    makeOption TypeInType       = Bool -> Idris ()
setTypeInType Bool
True
    makeOption NoCoverage       = Bool -> Idris ()
setCoverage Bool
False
    makeOption ErrContext       = Bool -> Idris ()
setErrContext Bool
True
    makeOption (IndentWith n :: Int
n)   = Int -> Idris ()
setIndentWith Int
n
    makeOption (IndentClause n :: Int
n) = Int -> Idris ()
setIndentClause Int
n
    makeOption _                = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

    addPkgDir :: String -> Idris ()
    addPkgDir :: String -> Idris ()
addPkgDir p :: 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))



-- | 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 opts :: [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
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 (m :: * -> *) a. Monad m => a -> m a
return Maybe IState
forall a. Maybe a
Nothing
                  Right ist :: IState
ist -> Maybe IState -> IO (Maybe IState)
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
fc, msg :: String
msg):_) -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (String -> Err) -> String -> Idris ()
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 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
$ "Could not build: "String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
msg
                           [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Execute the provided Idris expression.
execScript :: String -> Idris ()
execScript :: String -> Idris ()
execScript expr :: 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 err :: 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 1)
                          Right term :: PTerm
term -> do Context
ctxt <- Idris Context
getContext
                                           (tm :: Term
tm, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (String -> FC
fileFC "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

-- | Run the initialisation script
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)
                           (\e :: Err
e -> String -> Idris ()
iPrintError (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "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 h :: Handle
h = do Bool
eof <- ExceptT Err IO Bool -> Idris Bool
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 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 (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 i :: IState
i cmd :: String
cmd input :: String
input clr :: p
clr =
              case IState
-> String -> String -> Either ParseError (Either String Command)
parseCmd IState
i String
input String
cmd of
                   Left err :: ParseError
err -> ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                   Right (Right Reload) -> String -> Idris ()
iPrintError "Init scripts cannot reload the file"
                   Right (Right (Load f :: String
f _)) -> String -> Idris ()
iPrintError "Init scripts cannot load files"
                   Right (Right (ModImport f :: String
f)) -> String -> Idris ()
iPrintError "Init scripts cannot import modules"
                   Right (Right Edit) -> String -> Idris ()
iPrintError "Init scripts cannot invoke the editor"
                   Right (Right Proofs) -> IState -> Idris ()
proofs IState
i
                   Right (Right Quit) -> String -> Idris ()
iPrintError "Init scripts cannot quit Idris"
                   Right (Right cmd :: Command
cmd ) -> String -> Command -> Idris ()
process [] Command
cmd
                   Right (Left err :: 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