git.iko.soy/Idris-dev
on dcdebfc help sign in
Idris-dev/main/Main.hs
140 lines 6.1 kB history raw
1module Main where
3import System.Console.Haskeline
4import System.IO
5import System.Environment
6import System.Exit
7import System.FilePath ((</>), addTrailingPathSeparator)
9import Data.Maybe
10import Data.Version
11import Control.Monad.Trans.Error ( ErrorT(..) )
12import Control.Monad.Trans.State.Strict ( execStateT, get, put )
13import Control.Monad ( when )
15import Idris.Core.TT
16import Idris.Core.Typecheck
17import Idris.Core.Evaluate
18import Idris.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.System ( getLibFlags, getIdrisLibDir, getIncFlags )
30import Util.DynamicLinker
32import Pkg.Package
34import Paths_idris
36-- Main program reads command line options, parses the main program, and gets
37-- on with the REPL.
39main = do xs <- getArgs
40 let opts = parseArgs xs
41 result <- runErrorT $ execStateT (runIdris opts) idrisInit
42 case result of
43 Left err -> putStrLn $ "Uncaught error: " ++ show err
44 Right _ -> return ()
46runIdris :: [Opt] -> Idris ()
47runIdris [Client c] = do setVerbose False
48 setQuiet True
49 runIO $ runClient c
50runIdris opts = do
51 when (Ver `elem` opts) $ runIO showver
52 when (Usage `elem` opts) $ runIO usage
53 when (ShowIncs `elem` opts) $ runIO showIncs
54 when (ShowLibs `elem` opts) $ runIO showLibs
55 when (ShowLibdir `elem` opts) $ runIO showLibdir
56 case opt getPkgCheck opts of
57 [] -> return ()
58 fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs
59 runIO $ exitWith ExitSuccess
60 case opt getPkgClean opts of
61 [] -> return ()
62 fs -> do runIO $ mapM_ cleanPkg fs
63 runIO $ exitWith ExitSuccess
64 case opt getPkg opts of
65 [] -> case opt getPkgREPL opts of
66 [] -> idrisMain opts
67 [f] -> replPkg f
68 _ -> ifail "Too many packages"
69 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
71usage = do putStrLn usagemsg
72 exitWith ExitSuccess
74showver = do putStrLn $ "Idris version " ++ ver
75 exitWith ExitSuccess
77showLibs = do libFlags <- getLibFlags
78 putStrLn libFlags
79 exitWith ExitSuccess
81showLibdir = do dir <- getIdrisLibDir
82 putStrLn dir
83 exitWith ExitSuccess
85showIncs = do incFlags <- getIncFlags
86 putStrLn incFlags
87 exitWith ExitSuccess
89usagemsghdr = "Idris version " ++ ver ++ ", (C) The Idris Community 2014"
91usagemsg = usagemsghdr ++ "\n" ++
92 map (\x -> '-') usagemsghdr ++ "\n" ++
93 "idris [OPTIONS] [FILE]\n\n" ++
94 "Common flags:\n" ++
95 "\t --install IPKG Install package\n" ++
96 "\t --clean IPKG Clean package\n" ++
97 "\t --build IPKG Build package\n" ++
98 "\t --exec EXPR Execute as idris\n" ++
99 "\t --libdir Display library directory\n" ++
100 "\t --link Display link directory\n" ++
101 "\t --include Display the includes directory\n" ++
102 "\t --nobanner Suppress the banner\n" ++
103 "\t --color, --colour Force coloured output\n" ++
104 "\t --nocolor, --nocolour Disable coloured output\n" ++
105 "\t --errorcontent Undocumented\n" ++
106 "\t --nocoverage Undocumented\n" ++
107 "\t -o --output FILE Specify output file\n" ++
108 "\t --check Undocumented\n" ++
109 "\t --total Require functions to be total by default\n" ++
110 "\t --partial Undocumented\n" ++
111 "\t --warnpartial Warn about undeclared partial functions.\n" ++
112 "\t --warn Undocumented\n" ++
113 "\t --typecase Undocumented\n" ++
114 "\t --typeintype Undocumented\n" ++
115 "\t --nobasepkgs Undocumented\n" ++
116 "\t --noprelude Undocumented\n" ++
117 "\t --nobuiltins Undocumented\n" ++
118 "\t -O --level LEVEL Undocumented\n" ++
119 "\t -i --idrispath DIR Add directory to the list of import paths\n" ++
120 "\t --package ITEM Undocumented\n" ++
121 "\t --ibcsubdir FILE Write IBC files into sub directory\n" ++
122 "\t --codegen TARGET Select code generator: C, Java, bytecode,\n" ++
123 "\t javascript, node, or llvm\n" ++
124 "\t --mvn Create a maven project (for Java codegen)\n" ++
125 "\t --cpu=CPU Select target CPU e.g. corei7 or cortex-m3\n" ++
126 "\t (for LLVM codegen)\n" ++
127 "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++
128 "\t -S --codegenonly Do no further compilation of code generator output\n" ++
129 "\t -c --compileonly Compile to object files rather than an executable\n" ++
130 "\t -X --extension EXT Turn on langage extension (TypeProviders or ErrorReflection)\n" ++
131 "\t --dumpdefuns Undocumented\n" ++
132 "\t --dumpcases Undocumented\n" ++
133 "\t --log LEVEL --loglevel Debugging log level\n" ++
134 "\t --ideslave Undocumented\n" ++
135 "\t --client Undocumented\n" ++
136 "\t -h --help Display help message\n" ++
137 "\t -v --version Print version information\n" ++
138 "\t -V --verbose Loud verbosity\n" ++
139 "\t -q --quiet Quiet verbosity\n"