git.iko.soy/Idris-dev
on 3dfa841 help sign in
Idris-dev/main/Main.hs
112 lines 4.4 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 getPkgClean opts of
57 [] -> return ()
58 fs -> do runIO $ mapM_ cleanPkg fs
59 runIO $ exitWith ExitSuccess
60 case opt getPkg opts of
61 [] -> idrisMain opts -- in Idris.REPL
62 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
64usage = do putStrLn usagemsg
65 exitWith ExitSuccess
67showver = do putStrLn $ "Idris version " ++ ver
68 exitWith ExitSuccess
70showLibs = do libFlags <- getLibFlags
71 putStrLn libFlags
72 exitWith ExitSuccess
74showLibdir = do dir <- getIdrisLibDir
75 putStrLn dir
76 exitWith ExitSuccess
78showIncs = do incFlags <- getIncFlags
79 putStrLn incFlags
80 exitWith ExitSuccess
82usagemsg = "Idris version " ++ ver ++ "\n" ++
83 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
84 "Usage: idris [input file] [options]\n" ++
85 "Options:\n" ++
86 "\t--quiet Quiet mode (for editors)\n" ++
87 "\t--[no]colour Control REPL colour highlighting\n" ++
88 "\t--check Type check only\n" ++
89 "\t-o [file] Specify output filename\n" ++
90 "\t-i [dir] Add directory to the list of import paths\n" ++
91 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
92 "\t--noprelude Don't import the prelude\n" ++
93 "\t--total Require functions to be total by default\n" ++
94 "\t--warnpartial Warn about undeclared partial functions\n" ++
95 "\t--typeintype Disable universe checking\n" ++
96 "\t--log [level] Type debugging log level\n" ++
97 "\t-S Do no further compilation of code generator output\n" ++
98 "\t-c Compile to object files rather than an executable\n" ++
99 "\t--mvn Create a maven project (for Java codegen)\n" ++
100 "\t--exec [expr] Execute the expression expr in the interpreter,\n" ++
101 "\t defaulting to Main.main if none provided, and exit.\n" ++
102 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in \n" ++
103 "\t s-expressions)\n" ++
104 "\t--libdir Show library install directory and exit\n" ++
105 "\t--link Show C library directories and exit (for C linking)\n" ++
106 "\t--include Show C include directories and exit (for C linking)\n" ++
107 "\t--codegen [cg] Select code generator: C, Java, bytecode, javascript,\n" ++
108 "\t node or llvm\n" ++
109 "\t--target [triple] Select target triple (for LLVM codegen)\n" ++
110 "\t--cpu [cpu] Select target CPU (e.g. corei7 or cortex-m3) (for LLVM codegen)\n"