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