git.iko.soy/Idris-dev
on ddba413 help sign in
Idris-dev/src/Main.hs
109 lines 3.2 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
19import Idris.AbsSyntax
20import Idris.Parser
21import Idris.REPL
22import Idris.ElabDecls
23import Idris.Primitives
24import Idris.Imports
25import Paths_idris
27-- Main program reads command line options, parses the main program, and gets
28-- on with the REPL.
30data Opt = Filename String
31 | Version
32 | NoPrelude
33 | NoREPL
34 | OLogging Int
35 | Output String
36 | TypeCase
37 deriving Eq
39main = do xs <- getArgs
40 opts <- parseArgs xs
41 execStateT (runIdris opts) idrisInit
43runIdris :: [Opt] -> Idris ()
44runIdris opts =
45 do let inputs = opt getFile opts
46 let runrepl = not (NoREPL `elem` opts)
47 let output = opt getOutput opts
48 mapM_ makeOption opts
49 elabPrims
50 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
51 return ()
52 when runrepl $ iputStrLn banner
53 ist <- get
54 mods <- mapM loadModule inputs
55 ok <- noErrors
56 when ok $ case output of
57 [] -> return ()
58 (o:_) -> process (Compile o)
59 when runrepl $ repl ist inputs
60 where
61 makeOption (OLogging i) = setLogLevel i
62 makeOption TypeCase = setTypeCase True
63 makeOption _ = return ()
65getFile :: Opt -> Maybe String
66getFile (Filename str) = Just str
67getFile _ = Nothing
69getOutput :: Opt -> Maybe String
70getOutput (Output str) = Just str
71getOutput _ = Nothing
73opt :: (Opt -> Maybe a) -> [Opt] -> [a]
74opt = mapMaybe
76usage = do putStrLn "You're doing it wrong"
77 exitWith (ExitFailure 1)
79parseArgs :: [String] -> IO [Opt]
80parseArgs [] = return []
81parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
82parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
83parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
84parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
85parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
86parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
88{-
89main'
90 = do f <- readFile "test.mi"
91 case parseFile f of
92 Left err -> print err
93 Right defs -> do
94 print defs
95 case checkProgram emptyContext defs of
96 OK ctxt -> do print (toAlist ctxt)
97 runShell (initState ctxt)
98 return ()
99 err -> print err
100 -}
102ver = showVersion version
104banner = " ____ __ _ \n" ++
105 " / _/___/ /____(_)____ \n" ++
106 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
107 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
108 " /___/\\__,_/_/ /_/____/ Type :? for help \n"