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