git.iko.soy/Idris-dev
on 2a68244 help sign in
Idris-dev/src/Idris/Main.hs
293 lines 11 kB history raw
1{-|
2Module : Idris.REPL
3Description : Main function to decide Idris' mode of use.
4License : BSD3
5Maintainer : The Idris Community.
6-}
7module Idris.Main
8 ( idrisMain
9 , idris
10 , runMain
11 , runClient -- taken from Idris.REPL.
12 , loadInputs -- taken from Idris.ModeCommon
13 ) where
15import Idris.AbsSyntax
16import Idris.Core.Execute (execute)
17import Idris.Core.TT
18import Idris.Elab.Term
19import Idris.Elab.Value
20import Idris.ElabDecls
21import Idris.Error
22import Idris.IBC
23import Idris.Info
24import Idris.ModeCommon
25import Idris.Output
26import Idris.Parser hiding (indent)
27import Idris.REPL
28import Idris.REPL.Commands
29import Idris.REPL.Parser
30import IRTS.CodegenCommon
32import Util.System
34import Prelude hiding (id, (.), (<$>))
36import Control.Category
37import Control.DeepSeq
38import Control.Monad
39import Control.Monad.Trans (lift)
40import Control.Monad.Trans.Except (runExceptT)
41import Control.Monad.Trans.State.Strict (execStateT)
42import Data.Maybe
43import System.Console.Haskeline as H
44import System.Directory
45import System.Exit
46import System.FilePath
47import System.IO
48import Text.Trifecta.Result (ErrInfo(..), Result(..))
50-- | How to run Idris programs.
51runMain :: Idris () -> IO ()
52runMain prog = do res <- runExceptT $ execStateT prog idrisInit
53 case res of
54 Left err -> do
55 putStrLn $ "Uncaught error: " ++ show err
56 exitFailure
57 Right _ -> return ()
60-- | The main function of Idris that when given a set of Options will
61-- launch Idris into the desired interaction mode either: REPL;
62-- Compiler; Script execution; or IDE Mode.
63idrisMain :: [Opt] -> Idris ()
64idrisMain opts =
65 do mapM_ setWidth (opt getConsoleWidth opts)
66 let inputs = opt getFile opts
67 let quiet = Quiet `elem` opts
68 let nobanner = NoBanner `elem` opts
69 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts
70 let runrepl = not (NoREPL `elem` opts)
71 let output = opt getOutput opts
72 let ibcsubdir = opt getIBCSubDir opts
73 let importdirs = opt getImportDir opts
74 let sourcedirs = opt getSourceDir opts
75 setSourceDirs sourcedirs
76 let bcs = opt getBC opts
77 let pkgdirs = opt getPkgDir opts
78 -- Set default optimisations
79 let optimise = case opt getOptLevel opts of
80 [] -> 2
81 xs -> last xs
83 setOptLevel optimise
84 let outty = case opt getOutputTy opts of
85 [] -> if Interface `elem` opts then
86 Object else Executable
87 xs -> last xs
88 let cgn = case opt getCodegen opts of
89 [] -> Via IBCFormat "c"
90 xs -> last xs
91 let cgFlags = opt getCodegenArgs opts
93 -- Now set/unset specifically chosen optimisations
94 let os = opt getOptimisation opts
96 mapM_ processOptimisation os
98 script <- case opt getExecScript opts of
99 [] -> return Nothing
100 x:y:xs -> do iputStrLn "More than one interpreter expression found."
101 runIO $ exitWith (ExitFailure 1)
102 [expr] -> return (Just expr)
103 let immediate = opt getEvalExpr opts
104 let port = case getPort opts of
105 Nothing -> ListenPort defaultPort
106 Just p -> p
108 when (DefaultTotal `elem` opts) $ do i <- getIState
109 putIState (i { default_total = DefaultCheckingTotal })
110 tty <- runIO isATTY
111 setColourise $ not quiet && last (tty : opt getColour opts)
115 mapM_ addLangExt (opt getLanguageExt opts)
116 setREPL runrepl
117 setQuiet (quiet || isJust script || not (null immediate))
119 setCmdLine opts
120 setOutputTy outty
121 setNoBanner nobanner
122 setCodegen cgn
123 mapM_ (addFlag cgn) cgFlags
124 mapM_ makeOption opts
125 vlevel <- verbose
126 when (runrepl && vlevel == 0) $ setVerbose 1
128 -- if we have the --bytecode flag, drop into the bytecode assembler
129 case bcs of
130 [] -> return ()
131 xs -> return () -- runIO $ mapM_ bcAsm xs
132 case ibcsubdir of
133 [] -> setIBCSubDir ""
134 (d:_) -> setIBCSubDir d
135 setImportDirs importdirs
137 setNoBanner nobanner
139 when (not (NoBasePkgs `elem` opts)) $ do
140 addPkgDir "prelude"
141 addPkgDir "base"
142 mapM_ addPkgDir pkgdirs
143 elabPrims
144 when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)
145 addAutoImport "Builtins"
146 return ()
147 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)
148 addAutoImport "Prelude"
149 return ()
150 when (runrepl && not idesl) initScript
152 nobanner <- getNoBanner
154 when (runrepl &&
155 not quiet &&
156 not idesl &&
157 not (isJust script) &&
158 not nobanner &&
159 null immediate) $
160 iputStrLn banner
162 orig <- getIState
164 mods <- if idesl then return [] else loadInputs inputs Nothing
165 let efile = case inputs of
166 [] -> ""
167 (f:_) -> f
169 runIO $ hSetBuffering stdout LineBuffering
171 ok <- noErrors
172 when ok $ case output of
173 [] -> return ()
174 (o:_) -> idrisCatch (process "" (Compile cgn o))
175 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)
177 case immediate of
178 [] -> return ()
179 exprs -> do setWidth InfinitelyWide
180 mapM_ (\str -> do ist <- getIState
181 c <- colourise
182 case parseExpr ist str of
183 Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
184 runIO $ exitWith (ExitFailure 1)
185 Success e -> process "" (Eval e))
186 exprs
187 runIO exitSuccess
190 case script of
191 Nothing -> return ()
192 Just expr -> execScript expr
194 -- Create Idris data dir + repl history and config dir
195 idrisCatch (do dir <- runIO $ getIdrisUserDataDir
196 exists <- runIO $ doesDirectoryExist dir
197 unless exists $ logLvl 1 ("Creating " ++ dir)
198 runIO $ createDirectoryIfMissing True (dir </> "repl"))
199 (\e -> return ())
201 historyFile <- runIO $ getIdrisHistoryFile
203 when ok $ case opt getPkgIndex opts of
204 (f : _) -> writePkgIndex f
205 _ -> return ()
207 when (runrepl && not idesl) $ do
208-- clearOrigPats
209 case port of
210 DontListen -> return ()
211 ListenPort port' -> startServer port' orig mods
212 runInputT (replSettings (Just historyFile)) $ repl (force orig) mods efile
213 let idesock = IdemodeSocket `elem` opts
214 when (idesl) $ idemodeStart idesock orig inputs
215 ok <- noErrors
216 when (not ok) $ runIO (exitWith (ExitFailure 1))
217 where
218 makeOption (OLogging i) = setLogLevel i
219 makeOption (OLogCats cs) = setLogCats cs
220 makeOption (Verbose v) = setVerbose v
221 makeOption TypeCase = setTypeCase True
222 makeOption TypeInType = setTypeInType True
223 makeOption NoCoverage = setCoverage False
224 makeOption ErrContext = setErrContext True
225 makeOption _ = return ()
227 processOptimisation :: (Bool,Optimisation) -> Idris ()
228 processOptimisation (True, p) = addOptimise p
229 processOptimisation (False, p) = removeOptimise p
231 addPkgDir :: String -> Idris ()
232 addPkgDir p = do ddir <- runIO getIdrisLibDir
233 addImportDir (ddir </> p)
234 addIBC (IBCImportDir (ddir </> p))
238-- | Invoke as if from command line. It is an error if there are
239-- unresolved totality problems.
240idris :: [Opt] -> IO (Maybe IState)
241idris opts = do res <- runExceptT $ execStateT totalMain idrisInit
242 case res of
243 Left err -> do putStrLn $ pshow idrisInit err
244 return Nothing
245 Right ist -> return (Just ist)
246 where totalMain = do idrisMain opts
247 ist <- getIState
248 case idris_totcheckfail ist of
249 ((fc, msg):_) -> ierror . At fc . Msg $ "Could not build: "++ msg
250 [] -> return ()
253-- | Execute the provided Idris expression.
254execScript :: String -> Idris ()
255execScript expr = do i <- getIState
256 c <- colourise
257 case parseExpr i expr of
258 Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
259 runIO $ exitWith (ExitFailure 1)
260 Success term -> do ctxt <- getContext
261 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
262 res <- execute tm
263 runIO $ exitSuccess
265-- | Run the initialisation script
266initScript :: Idris ()
267initScript = do script <- runIO $ getIdrisInitScript
268 idrisCatch (do go <- runIO $ doesFileExist script
269 when go $ do
270 h <- runIO $ openFile script ReadMode
271 runInit h
272 runIO $ hClose h)
273 (\e -> iPrintError $ "Error reading init file: " ++ show e)
274 where runInit :: Handle -> Idris ()
275 runInit h = do eof <- lift . lift $ hIsEOF h
276 ist <- getIState
277 unless eof $ do
278 line <- runIO $ hGetLine h
279 script <- runIO $ getIdrisInitScript
280 c <- colourise
281 processLine ist line script c
282 runInit h
283 processLine i cmd input clr =
284 case parseCmd i input cmd of
285 Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)
286 Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
287 Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
288 Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
289 Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"
290 Success (Right Proofs) -> proofs i
291 Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"
292 Success (Right cmd ) -> process [] cmd
293 Success (Left err) -> runIO $ print err