git.iko.soy/Idris-dev
on ccc0f67 help sign in
Idris-dev/src/Main.hs
183 lines 6.6 kB history raw
1module Main where
3import System.Console.Haskeline
4import System.IO
5import System.Environment
6import System.Exit
8import Data.Maybe
9import Data.Version
10import Control.Monad.State
12import Core.CoreParser
13import Core.ShellParser
14import Core.TT
15import Core.Typecheck
16import Core.ProofShell
17import Core.Evaluate
18import Core.Constraints
20import Idris.AbsSyntax
21import Idris.Parser
22import Idris.REPL
23import Idris.ElabDecls
24import Idris.Primitives
25import Idris.Imports
26import Idris.Error
28import IRTS.Lang
29import IRTS.LParser
31import Paths_idris
33-- Main program reads command line options, parses the main program, and gets
34-- on with the REPL.
36main = do xs <- getArgs
37 opts <- parseArgs xs
38 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
40runIdris :: [Opt] -> Idris ()
41runIdris opts =
42 do let inputs = opt getFile opts
43 let runrepl = not (NoREPL `elem` opts)
44 let output = opt getOutput opts
45 let newoutput = opt getNewOutput opts
46 let ibcsubdir = opt getIBCSubDir opts
47 let importdirs = opt getImportDir opts
48 let bcs = opt getBC opts
49 let vm = opt getFOVM opts
51 when (Ver `elem` opts) $ liftIO showver
52 when (Usage `elem` opts) $ liftIO usage
53 when (ShowIncs `elem` opts) $ liftIO showIncs
54 when (ShowLibs `elem` opts) $ liftIO showLibs
55 setREPL runrepl
56 setVerbose runrepl
57 when (Verbose `elem` opts) $ setVerbose True
58 mapM_ makeOption opts
59 -- if we have the --fovm flag, drop into the first order VM testing
60 case vm of
61 [] -> return ()
62 xs -> liftIO $ mapM_ fovm xs
63 -- if we have the --bytecode flag, drop into the bytecode assembler
64 case bcs of
65 [] -> return ()
66 xs -> return () -- liftIO $ mapM_ bcAsm xs
67 case ibcsubdir of
68 [] -> setIBCSubDir ""
69 (d:_) -> setIBCSubDir d
70 setImportDirs importdirs
71 elabPrims
72 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
73 return ()
74 when runrepl $ iputStrLn banner
75 ist <- get
76 mods <- mapM loadModule inputs
77 ok <- noErrors
78 when ok $ case output of
79 [] -> return ()
80 (o:_) -> process "" (Compile o)
81 when ok $ case newoutput of
82 [] -> return ()
83 (o:_) -> process "" (NewCompile o)
84 when runrepl $ repl ist inputs
85 ok <- noErrors
86 when (not ok) $ liftIO (exitWith (ExitFailure 1))
87 where
88 makeOption (OLogging i) = setLogLevel i
89 makeOption TypeCase = setTypeCase True
90 makeOption TypeInType = setTypeInType True
91 makeOption NoCoverage = setCoverage False
92 makeOption ErrContext = setErrContext True
93 makeOption _ = return ()
95getFile :: Opt -> Maybe String
96getFile (Filename str) = Just str
97getFile _ = Nothing
99getBC :: Opt -> Maybe String
100getBC (BCAsm str) = Just str
101getBC _ = Nothing
103getFOVM :: Opt -> Maybe String
104getFOVM (FOVM str) = Just str
105getFOVM _ = Nothing
107getOutput :: Opt -> Maybe String
108getOutput (Output str) = Just str
109getOutput _ = Nothing
111getNewOutput :: Opt -> Maybe String
112getNewOutput (NewOutput str) = Just str
113getNewOutput _ = Nothing
115getIBCSubDir :: Opt -> Maybe String
116getIBCSubDir (IBCSubDir str) = Just str
117getIBCSubDir _ = Nothing
119getImportDir :: Opt -> Maybe String
120getImportDir (ImportDir str) = Just str
121getImportDir _ = Nothing
123opt :: (Opt -> Maybe a) -> [Opt] -> [a]
124opt = mapMaybe
126usage = do putStrLn usagemsg
127 exitWith ExitSuccess
129showver = do putStrLn $ "Idris version " ++ ver
130 exitWith ExitSuccess
132showLibs = do dir <- getDataDir
133 putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts"
134 exitWith ExitSuccess
136showIncs = do dir <- getDataDir
137 putStrLn $ "-I" ++ dir ++ "/rts"
138 exitWith ExitSuccess
140parseArgs :: [String] -> IO [Opt]
141parseArgs [] = return []
142parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
143parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
144parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
145parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
146parseArgs ("-no":n:ns) = liftM (\x -> NoREPL : NewOutput n : x) (parseArgs ns)
147parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
148parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
149parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)
150parseArgs ("--errorcontext":ns) = liftM (ErrContext : ) (parseArgs ns)
151parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
152parseArgs ("--link":ns) = liftM (ShowLibs : ) (parseArgs ns)
153parseArgs ("--include":ns) = liftM (ShowIncs : ) (parseArgs ns)
154parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
155parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)
156parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)
157parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)
158parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs ns)
159parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)
160parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
162ver = showVersion version
164banner = " ____ __ _ \n" ++
165 " / _/___/ /____(_)____ \n" ++
166 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
167 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
168 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
170usagemsg = "Idris version " ++ ver ++ "\n" ++
171 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
172 "Usage: idris [input file] [options]\n" ++
173 "Options:\n" ++
174 "\t--check Type check only\n" ++
175 "\t-o [file] Generate executable\n" ++
176 "\t-i [dir] Add directory to the list of import paths\n" ++
177 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
178 "\t--noprelude Don't import the prelude\n" ++
179 "\t--typeintype Disable universe checking\n" ++
180 "\t--log [level] Set debugging log level\n" ++
181 "\t--link Show library directories and exit (for C linking)\n" ++
182 "\t--include Show include directories and exit (for C linking)\n"