git.iko.soy/Idris-dev
on e613365 help sign in
Idris-dev/src/Main.hs
93 lines 2.5 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 Int
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 mapM_ makeOption opts
39 mapM_ loadModule inputs
40 repl
41 where
42 makeOption (OLogging i) = setLogLevel i
43 makeOption _ = return ()
45loadModule :: FilePath -> Idris ()
46loadModule f = do iLOG ("Reading " ++ show f)
47 ds <- parseProg f
48 iLOG (dumpDecls ds)
49 i <- get
50 iLOG (show (idris_infixes i))
51 -- Now add all the declarations to the context
52 elabDecl (PData inferDecl) -- a handy primitive
53 mapM_ elabDecl ds
54 return ()
56dumpDecls :: [PDecl] -> String
57dumpDecls [] = ""
58dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
60dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
61dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
62dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
63dumpDecl (PData d) = showDImp True d
65getFile :: Opt -> Maybe String
66getFile (Filename str) = Just str
67getFile _ = Nothing
69opt :: (Opt -> Maybe a) -> [Opt] -> [a]
70opt = mapMaybe
72usage = do putStrLn "You're doing it wrong"
73 exitWith (ExitFailure 1)
75parseArgs :: [String] -> IO [Opt]
76parseArgs [] = return []
77parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
78parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
80{-
81main'
82 = do f <- readFile "test.mi"
83 case parseFile f of
84 Left err -> print err
85 Right defs -> do
86 print defs
87 case checkProgram emptyContext defs of
88 OK ctxt -> do print (toAlist ctxt)
89 runShell (initState ctxt)
90 return ()
91 err -> print err
92 -}