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