git.iko.soy/Idris-dev
on 43ffd25 help sign in
Idris-dev/src/Main.hs
139 lines 4.6 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 | IBCSubDir String
44 deriving Eq
46main = do xs <- getArgs
47 opts <- parseArgs xs
48 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
50runIdris :: [Opt] -> Idris ()
51runIdris opts =
52 do let inputs = opt getFile opts
53 let runrepl = not (NoREPL `elem` opts)
54 let output = opt getOutput opts
55 let ibcsubdir = opt getIBCSubDir opts
56 when (Ver `elem` opts) $ liftIO showver
57 when (Usage `elem` opts) $ liftIO usage
58 setREPL runrepl
59 setVerbose runrepl
60 when (Verbose `elem` opts) $ setVerbose True
61 mapM_ makeOption opts
62 case ibcsubdir of
63 [] -> setIBCSubDir ""
64 (d:_) -> setIBCSubDir d
65 elabPrims
66 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
67 return ()
68 when runrepl $ iputStrLn banner
69 ist <- get
70 mods <- mapM loadModule inputs
71 ok <- noErrors
72 when ok $ case output of
73 [] -> return ()
74 (o:_) -> process "" (Compile o)
75 when runrepl $ repl ist inputs
76 ok <- noErrors
77 when (not ok) $ liftIO (exitWith (ExitFailure 1))
78 where
79 makeOption (OLogging i) = setLogLevel i
80 makeOption TypeCase = setTypeCase True
81 makeOption TypeInType = setTypeInType True
82 makeOption NoCoverage = setCoverage False
83 makeOption _ = return ()
85getFile :: Opt -> Maybe String
86getFile (Filename str) = Just str
87getFile _ = Nothing
89getOutput :: Opt -> Maybe String
90getOutput (Output str) = Just str
91getOutput _ = Nothing
93getIBCSubDir :: Opt -> Maybe String
94getIBCSubDir (IBCSubDir str) = Just str
95getIBCSubDir _ = Nothing
97opt :: (Opt -> Maybe a) -> [Opt] -> [a]
98opt = mapMaybe
100usage = do putStrLn usagemsg
101 exitWith ExitSuccess
103showver = do putStrLn $ "Idris version " ++ ver
104 exitWith ExitSuccess
106parseArgs :: [String] -> IO [Opt]
107parseArgs [] = return []
108parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
109parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
110parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
111parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
112parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
113parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
114parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)
115parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
116parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
117parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)
118parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)
119parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
121ver = showVersion version
123banner = " ____ __ _ \n" ++
124 " / _/___/ /____(_)____ \n" ++
125 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
126 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
127 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
129usagemsg = "Idris version " ++ ver ++ "\n" ++
130 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
131 "Usage: idris [input file] [options]\n" ++
132 "Options:\n" ++
133 "\t--check Type check only\n" ++
134 "\t-o [file] Generate executable\n" ++
135 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++
136 "\t--noprelude Don't import the prelude\n" ++
137 "\t--typeintype Disable universe checking\n" ++
138 "\t--log [level] Set debugging log level\n"