git.iko.soy/Idris-dev
on 1b6709f help sign in
Idris-dev/src/Main.hs
87 lines 2.3 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
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 return ()
50dumpDecls :: [PDecl] -> String
51dumpDecls [] = ""
52dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
54dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
55dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
56dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r
57dumpDecl (PData d) = "data " ++ showDImp True d
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":ns) = liftM (OLogging : ) (parseArgs ns)
72parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
74{-
75main'
76 = do f <- readFile "test.mi"
77 case parseFile f of
78 Left err -> print err
79 Right defs -> do
80 print defs
81 case checkProgram emptyContext defs of
82 OK ctxt -> do print (toAlist ctxt)
83 runShell (initState ctxt)
84 return ()
85 err -> print err
86 -}