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