git.iko.soy/Idris-dev
on 0bc69fb help sign in
Idris-dev/src/Main.hs
121 lines 3.8 kB history raw
1module Main where
3import System.Console.Readline
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 deriving Eq
43main = do xs <- getArgs
44 opts <- parseArgs xs
45 execStateT (runIdris opts) idrisInit
47runIdris :: [Opt] -> Idris ()
48runIdris opts =
49 do let inputs = opt getFile opts
50 let runrepl = not (NoREPL `elem` opts)
51 let output = opt getOutput opts
52 when (Ver `elem` opts) $ lift showver
53 when (Usage `elem` opts) $ lift usage
54 setREPL runrepl
55 mapM_ makeOption opts
56 elabPrims
57 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
58 return ()
59 when runrepl $ iputStrLn banner
60 ist <- get
61 mods <- mapM loadModule inputs
62 ok <- noErrors
63 when ok $ case output of
64 [] -> return ()
65 (o:_) -> process (Compile o)
66 when runrepl $ repl ist inputs
67 ok <- noErrors
68 when (not ok) $ lift (exitWith (ExitFailure 1))
69 where
70 makeOption (OLogging i) = setLogLevel i
71 makeOption TypeCase = setTypeCase True
72 makeOption TypeInType = setTypeInType True
73 makeOption _ = return ()
75getFile :: Opt -> Maybe String
76getFile (Filename str) = Just str
77getFile _ = Nothing
79getOutput :: Opt -> Maybe String
80getOutput (Output str) = Just str
81getOutput _ = Nothing
83opt :: (Opt -> Maybe a) -> [Opt] -> [a]
84opt = mapMaybe
86usage = do putStrLn usagemsg
87 exitWith ExitSuccess
89showver = do putStrLn $ "Idris version " ++ ver
90 exitWith ExitSuccess
92parseArgs :: [String] -> IO [Opt]
93parseArgs [] = return []
94parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
95parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
96parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
97parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
98parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
99parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
100parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
101parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
102parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
104ver = showVersion version
106banner = " ____ __ _ \n" ++
107 " / _/___/ /____(_)____ \n" ++
108 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
109 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
110 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
112usagemsg = "Idris version " ++ ver ++ "\n" ++
113 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
114 "Usage: idris [input file] [options]\n" ++
115 "Options:\n" ++
116 "\t--check Type check only\n" ++
117 "\t-o [file] Generate executable\n" ++
118 "\t--noprelude Don't import the prelude\n" ++
119 "\t--typeintype Disable universe checking\n" ++
120 "\t--log [level] Set debugging log level\n"