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