git.iko.soy/Idris-dev
on be2b9bc help sign in
Idris-dev/src/Main.hs
89 lines 2.4 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
23-- Main program reads command line options, parses the main program, and gets
24-- on with the REPL.
26data Opt = Filename String
27 | Version
28 | OLogging
29 deriving Eq
31main = do xs <- getArgs
32 opts <- parseArgs xs
33 execStateT (runIdris opts) idrisInit
35runIdris :: [Opt] -> Idris ()
36runIdris opts =
37 do let inputs = opt getFile opts
38 when (OLogging `elem` opts) (setOpt Logging True)
39 mapM_ loadModule inputs
40 repl
42loadModule :: FilePath -> Idris ()
43loadModule f = do iLOG ("Reading " ++ show f)
44 ds <- parseProg f
45 iLOG (dumpDecls ds)
46 i <- get
47 iLOG (show (idris_infixes i))
48 -- Now add all the declarations to the context
49 mapM_ elabDecl ds
50 return ()
52dumpDecls :: [PDecl] -> String
53dumpDecls [] = ""
54dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
56dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
57dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
58dumpDecl (PClauses cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
59dumpDecl (PData d) = showDImp True d
61getFile :: Opt -> Maybe String
62getFile (Filename str) = Just str
63getFile _ = Nothing
65opt :: (Opt -> Maybe a) -> [Opt] -> [a]
66opt = mapMaybe
68usage = do putStrLn "You're doing it wrong"
69 exitWith (ExitFailure 1)
71parseArgs :: [String] -> IO [Opt]
72parseArgs [] = return []
73parseArgs ("--log":ns) = liftM (OLogging : ) (parseArgs ns)
74parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
76{-
77main'
78 = do f <- readFile "test.mi"
79 case parseFile f of
80 Left err -> print err
81 Right defs -> do
82 print defs
83 case checkProgram emptyContext defs of
84 OK ctxt -> do print (toAlist ctxt)
85 runShell (initState ctxt)
86 return ()
87 err -> print err
88 -}