git.iko.soy/Idris-dev
on ec87a69 help sign in
Idris-dev/src/Main.hs
81 lines 2.1 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 | NoPrelude
31 | NoREPL
32 | OLogging Int
33 deriving Eq
35main = do xs <- getArgs
36 opts <- parseArgs xs
37 execStateT (runIdris opts) idrisInit
39runIdris :: [Opt] -> Idris ()
40runIdris opts =
41 do let inputs = opt getFile opts
42 mapM_ makeOption opts
43 elabPrims
44 when (not (NoPrelude `elem` opts)) $ loadModule "prelude"
45 mapM_ loadModule inputs
46 when (not (NoREPL `elem` opts)) $ repl
47 where
48 makeOption (OLogging i) = setLogLevel i
49 makeOption _ = return ()
51getFile :: Opt -> Maybe String
52getFile (Filename str) = Just str
53getFile _ = Nothing
55opt :: (Opt -> Maybe a) -> [Opt] -> [a]
56opt = mapMaybe
58usage = do putStrLn "You're doing it wrong"
59 exitWith (ExitFailure 1)
61parseArgs :: [String] -> IO [Opt]
62parseArgs [] = return []
63parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
64parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
65parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
66parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
68{-
69main'
70 = do f <- readFile "test.mi"
71 case parseFile f of
72 Left err -> print err
73 Right defs -> do
74 print defs
75 case checkProgram emptyContext defs of
76 OK ctxt -> do print (toAlist ctxt)
77 runShell (initState ctxt)
78 return ()
79 err -> print err
80 -}