git.iko.soy/Idris-dev
on b1419b2 help sign in
Idris-dev/src/Main.hs
76 lines 1.8 kB history raw
1module Main where
3import System.Console.Readline
4import System.IO
5import System.Environment
6import System.Exit
8import Data.Maybe
9import Control.Monad.State
11import Core.CoreParser
12import Core.ShellParser
13import Core.TT
14import Core.Typecheck
15import Core.ProofShell
16import Core.Evaluate
18import Idris.AbsSyntax
19import Idris.Parser
20import Idris.REPL
21import Idris.ElabDecls
22import Idris.Primitives
23import Idris.Imports
25-- Main program reads command line options, parses the main program, and gets
26-- on with the REPL.
28data Opt = Filename String
29 | Version
30 | OLogging Int
31 deriving Eq
33main = do xs <- getArgs
34 opts <- parseArgs xs
35 execStateT (runIdris opts) idrisInit
37runIdris :: [Opt] -> Idris ()
38runIdris opts =
39 do let inputs = opt getFile opts
40 mapM_ makeOption opts
41 elabPrims
42 mapM_ loadModule inputs
43 repl
44 where
45 makeOption (OLogging i) = setLogLevel i
46 makeOption _ = return ()
48getFile :: Opt -> Maybe String
49getFile (Filename str) = Just str
50getFile _ = Nothing
52opt :: (Opt -> Maybe a) -> [Opt] -> [a]
53opt = mapMaybe
55usage = do putStrLn "You're doing it wrong"
56 exitWith (ExitFailure 1)
58parseArgs :: [String] -> IO [Opt]
59parseArgs [] = return []
60parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
61parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
63{-
64main'
65 = do f <- readFile "test.mi"
66 case parseFile f of
67 Left err -> print err
68 Right defs -> do
69 print defs
70 case checkProgram emptyContext defs of
71 OK ctxt -> do print (toAlist ctxt)
72 runShell (initState ctxt)
73 return ()
74 err -> print err
75 -}