git.iko.soy/Idris-dev
on 7b1336b help sign in
Idris-dev/src/Main.hs
101 lines 3.0 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_miniidris
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 | TypeCase
36 deriving Eq
38main = do xs <- getArgs
39 opts <- parseArgs xs
40 execStateT (runIdris opts) idrisInit
42runIdris :: [Opt] -> Idris ()
43runIdris opts =
44 do let inputs = opt getFile opts
45 let runrepl = not (NoREPL `elem` opts)
46 mapM_ makeOption opts
47 elabPrims
48 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"
49 return ()
50 when runrepl $ iputStrLn banner
51 mods <- mapM loadModule inputs
52 when runrepl $ repl (mkPrompt mods)
53 where
54 makeOption (OLogging i) = setLogLevel i
55 makeOption TypeCase = setTypeCase True
56 makeOption _ = return ()
58mkPrompt [] = "Idris"
59mkPrompt [x] = "*" ++ x
60mkPrompt (x:xs) = "*" ++ x ++ " " ++ mkPrompt xs
62getFile :: Opt -> Maybe String
63getFile (Filename str) = Just str
64getFile _ = Nothing
66opt :: (Opt -> Maybe a) -> [Opt] -> [a]
67opt = mapMaybe
69usage = do putStrLn "You're doing it wrong"
70 exitWith (ExitFailure 1)
72parseArgs :: [String] -> IO [Opt]
73parseArgs [] = return []
74parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
75parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
76parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
77parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
78parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
80{-
81main'
82 = do f <- readFile "test.mi"
83 case parseFile f of
84 Left err -> print err
85 Right defs -> do
86 print defs
87 case checkProgram emptyContext defs of
88 OK ctxt -> do print (toAlist ctxt)
89 runShell (initState ctxt)
90 return ()
91 err -> print err
92 -}
94ver = showVersion version
96banner = " ____ __ _ \n" ++
97 " / _/___/ /____(_)____ \n" ++
98 " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++
99 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
100 " /___/\\__,_/_/ /_/____/ Type :? for help \n"