git.iko.soy/Idris-dev
on e88a135 help sign in
Idris-dev/src/Main.hs
86 lines 2.8 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.State
12import Core.CoreParser
13import Core.ShellParser
14import Core.TT
15import Core.Typecheck
16import Core.ProofShell
17import Core.Evaluate
18import Core.Constraints
20import Idris.AbsSyntax
21import Idris.Parser
22import Idris.REPL
23import Idris.ElabDecls
24import Idris.Primitives
25import Idris.Imports
26import Idris.Error
28import Pkg.Package
30import Paths_idris
32-- Main program reads command line options, parses the main program, and gets
33-- on with the REPL.
35main = do xs <- getArgs
36 let opts = parseArgs xs
37 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
39runIdris :: [Opt] -> Idris ()
40runIdris opts = do
41 when (Ver `elem` opts) $ liftIO showver
42 when (Usage `elem` opts) $ liftIO usage
43 when (ShowIncs `elem` opts) $ liftIO showIncs
44 when (ShowLibs `elem` opts) $ liftIO showLibs
45 when (ShowLibdir `elem` opts) $ liftIO showLibdir
46 case opt getPkgClean opts of
47 [] -> return ()
48 fs -> do liftIO $ mapM_ cleanPkg fs
49 liftIO $ exitWith ExitSuccess
50 case opt getPkg opts of
51 [] -> idrisMain opts -- in Idris.REPL
52 fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
54usage = do putStrLn usagemsg
55 exitWith ExitSuccess
57showver = do putStrLn $ "Idris version " ++ ver
58 exitWith ExitSuccess
60showLibs = do dir <- getDataDir
61 putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts -lgmp -lpthread"
62 exitWith ExitSuccess
64showLibdir = do dir <- getDataDir
65 putStrLn $ dir ++ "/"
66 exitWith ExitSuccess
68showIncs = do dir <- getDataDir
69 putStrLn $ "-I" ++ dir ++ "/rts"
70 exitWith ExitSuccess
72usagemsg = "Idris version " ++ ver ++ "\n" ++
73 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
74 "Usage: idris [input file] [options]\n" ++
75 "Options:\n" ++
76 "\t--check Type check only\n" ++
77 "\t-o [file] Generate executable\n" ++
78 "\t-i [dir] Add directory to the list of import paths\n" ++
79 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
80 "\t--noprelude Don't import the prelude\n" ++
81 "\t--typeintype Disable universe checking\n" ++
82 "\t--log [level] Set debugging log level\n" ++
83 "\t--libdir Show library install directory and exit\n" ++
84 "\t--link Show C library directories and exit (for C linking)\n" ++
85 "\t--include Show C include directories and exit (for C linking)\n"