git.iko.soy/Idris-dev
on 92bf28e help sign in
Idris-dev/src/Main.hs
98 lines 2.9 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 | 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 ist <- get
52 mods <- mapM loadModule inputs
53 when runrepl $ repl ist inputs
54 where
55 makeOption (OLogging i) = setLogLevel i
56 makeOption TypeCase = setTypeCase True
57 makeOption _ = return ()
59getFile :: Opt -> Maybe String
60getFile (Filename str) = Just str
61getFile _ = Nothing
63opt :: (Opt -> Maybe a) -> [Opt] -> [a]
64opt = mapMaybe
66usage = do putStrLn "You're doing it wrong"
67 exitWith (ExitFailure 1)
69parseArgs :: [String] -> IO [Opt]
70parseArgs [] = return []
71parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
72parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
73parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
74parseArgs ("--typecase":ns) = liftM (TypeCase : ) (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"