git.iko.soy/Idris-dev
on 8bf44c2 help sign in
Idris-dev/src/Main.hs
128 lines 4.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.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
27import Paths_idris
29-- Main program reads command line options, parses the main program, and gets
30-- on with the REPL.
32data Opt = Filename String
33 | Ver
34 | Usage
35 | NoPrelude
36 | NoREPL
37 | OLogging Int
38 | Output String
39 | TypeCase
40 | TypeInType
41 | NoCoverage
42 | Verbose
43 deriving Eq
45main = do xs <- getArgs
46 opts <- parseArgs xs
47 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
49runIdris :: [Opt] -> Idris ()
50runIdris opts =
51 do let inputs = opt getFile opts
52 let runrepl = not (NoREPL `elem` opts)
53 let output = opt getOutput opts
54 when (Ver `elem` opts) $ liftIO showver
55 when (Usage `elem` opts) $ liftIO usage
56 setREPL runrepl
57 setVerbose runrepl
58 when (Verbose `elem` opts) $ setVerbose True
59 mapM_ makeOption opts
60 elabPrims
61 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
62 return ()
63 when runrepl $ iputStrLn banner
64 ist <- get
65 mods <- mapM loadModule inputs
66 ok <- noErrors
67 when ok $ case output of
68 [] -> return ()
69 (o:_) -> process "" (Compile o)
70 when runrepl $ repl ist inputs
71 ok <- noErrors
72 when (not ok) $ liftIO (exitWith (ExitFailure 1))
73 where
74 makeOption (OLogging i) = setLogLevel i
75 makeOption TypeCase = setTypeCase True
76 makeOption TypeInType = setTypeInType True
77 makeOption NoCoverage = setCoverage False
78 makeOption _ = return ()
80getFile :: Opt -> Maybe String
81getFile (Filename str) = Just str
82getFile _ = Nothing
84getOutput :: Opt -> Maybe String
85getOutput (Output str) = Just str
86getOutput _ = Nothing
88opt :: (Opt -> Maybe a) -> [Opt] -> [a]
89opt = mapMaybe
91usage = do putStrLn usagemsg
92 exitWith ExitSuccess
94showver = do putStrLn $ "Idris version " ++ ver
95 exitWith ExitSuccess
97parseArgs :: [String] -> IO [Opt]
98parseArgs [] = return []
99parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
100parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
101parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
102parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
103parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
104parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
105parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)
106parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
107parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
108parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)
109parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
111ver = showVersion version
113banner = " ____ __ _ \n" ++
114 " / _/___/ /____(_)____ \n" ++
115 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
116 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
117 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
119usagemsg = "Idris version " ++ ver ++ "\n" ++
120 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
121 "Usage: idris [input file] [options]\n" ++
122 "Options:\n" ++
123 "\t--check Type check only\n" ++
124 "\t-o [file] Generate executable\n" ++
125 "\t--noprelude Don't import the prelude\n" ++
126 "\t--typeintype Disable universe checking\n" ++
127 "\t--log [level] Set debugging log level\n"