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