git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Main.hs
92 lines 3.3 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 Pkg.Package
33import Paths_idris
35-- Main program reads command line options, parses the main program, and gets
36-- on with the REPL.
38main = do xs <- getArgs
39 let opts = parseArgs xs
40 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
42runIdris :: [Opt] -> Idris ()
43runIdris opts = do
44 when (Ver `elem` opts) $ liftIO showver
45 when (Usage `elem` opts) $ liftIO usage
46 when (ShowIncs `elem` opts) $ liftIO showIncs
47 when (ShowLibs `elem` opts) $ liftIO showLibs
48 when (ShowLibdir `elem` opts) $ liftIO showLibdir
49 case opt getPkgClean opts of
50 [] -> return ()
51 fs -> do liftIO $ mapM_ cleanPkg fs
52 liftIO $ exitWith ExitSuccess
53 case opt getPkg opts of
54 [] -> idrisMain opts -- in Idris.REPL
55 fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
57usage = do putStrLn usagemsg
58 exitWith ExitSuccess
60showver = do putStrLn $ "Idris version " ++ ver
61 exitWith ExitSuccess
63showLibs = do dir <- getDataDir
64 putStrLn $ "-L" ++ (dir </> "rts") ++ " -lidris_rts -lgmp -lpthread"
65 exitWith ExitSuccess
67showLibdir = do dir <- getDataDir
68 putStrLn $ addTrailingPathSeparator dir
69 exitWith ExitSuccess
71showIncs = do dir <- getDataDir
72 putStrLn $ "-I" ++ dir </> "rts"
73 exitWith ExitSuccess
75usagemsg = "Idris version " ++ ver ++ "\n" ++
76 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
77 "Usage: idris [input file] [options]\n" ++
78 "Options:\n" ++
79 "\t--check Type check only\n" ++
80 "\t-o [file] Specify output filename\n" ++
81 "\t-i [dir] Add directory to the list of import paths\n" ++
82 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
83 "\t--noprelude Don't import the prelude\n" ++
84 "\t--total Require functions to be total by default\n" ++
85 "\t--warnpartial Warn about undeclared partial functions\n" ++
86 "\t--typeintype Disable universe checking\n" ++
87 "\t--log [level] Set debugging log level\n" ++
88 "\t-S Do no further compilation of code generator output\n" ++
89 "\t-c Compile to object files rather than an executable\n" ++
90 "\t--libdir Show library install directory and exit\n" ++
91 "\t--link Show C library directories and exit (for C linking)\n" ++
92 "\t--include Show C include directories and exit (for C linking)\n"