git.iko.soy/Idris-dev
on cbc8a13 help sign in
Idris-dev/src/Main.hs
95 lines 3.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.State.Strict ( execStateT, get, put )
12import Control.Monad.Trans ( liftIO )
13import Control.Monad ( when )
15import Core.CoreParser
16import Core.ShellParser
17import Core.TT
18import Core.Typecheck
19import Core.ProofShell
20import Core.Evaluate
21import Core.Constraints
23import Idris.AbsSyntax
24import Idris.Parser
25import Idris.REPL
26import Idris.ElabDecls
27import Idris.Primitives
28import Idris.Imports
29import Idris.Error
31import Util.System ( getLibFlags, getIdrisLibDir, getIncFlags )
33import Pkg.Package
35import Paths_idris
37-- Main program reads command line options, parses the main program, and gets
38-- on with the REPL.
40main = do xs <- getArgs
41 let opts = parseArgs xs
42 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
44runIdris :: [Opt] -> Idris ()
45runIdris opts = do
46 when (Ver `elem` opts) $ liftIO showver
47 when (Usage `elem` opts) $ liftIO usage
48 when (ShowIncs `elem` opts) $ liftIO showIncs
49 when (ShowLibs `elem` opts) $ liftIO showLibs
50 when (ShowLibdir `elem` opts) $ liftIO showLibdir
51 case opt getPkgClean opts of
52 [] -> return ()
53 fs -> do liftIO $ mapM_ cleanPkg fs
54 liftIO $ exitWith ExitSuccess
55 case opt getPkg opts of
56 [] -> idrisMain opts -- in Idris.REPL
57 fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
59usage = do putStrLn usagemsg
60 exitWith ExitSuccess
62showver = do putStrLn $ "Idris version " ++ ver
63 exitWith ExitSuccess
65showLibs = do libFlags <- getLibFlags
66 putStrLn libFlags
67 exitWith ExitSuccess
69showLibdir = do dir <- getIdrisLibDir
70 putStrLn dir
71 exitWith ExitSuccess
73showIncs = do incFlags <- getIncFlags
74 putStrLn incFlags
75 exitWith ExitSuccess
77usagemsg = "Idris version " ++ ver ++ "\n" ++
78 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
79 "Usage: idris [input file] [options]\n" ++
80 "Options:\n" ++
81 "\t--check Type check only\n" ++
82 "\t-o [file] Specify output filename\n" ++
83 "\t-i [dir] Add directory to the list of import paths\n" ++
84 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
85 "\t--noprelude Don't import the prelude\n" ++
86 "\t--total Require functions to be total by default\n" ++
87 "\t--warnpartial Warn about undeclared partial functions\n" ++
88 "\t--typeintype Disable universe checking\n" ++
89 "\t--log [level] Type debugging log level\n" ++
90 "\t-S Do no further compilation of code generator output\n" ++
91 "\t-c Compile to object files rather than an executable\n" ++
92 "\t--libdir Show library install directory and exit\n" ++
93 "\t--link Show C library directories and exit (for C linking)\n" ++
94 "\t--include Show C include directories and exit (for C linking)\n" ++
95 "\t--target [target] Type the target: C, Java, bytecode\n"