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