git.iko.soy/Idris-dev
on master help sign in
Add --help and --version options
c783299Edwin Brady
src/Main.hs+21−17
compare with master
unifiedsplit
@@ -30,7 +30,8 @@ import Paths_idris
30-- on with the REPL.
30-- on with the REPL.
31
31
32data Opt = Filename String
32data Opt = Filename String
33− | Version
33+ | Ver
34+ | Usage
34 | NoPrelude
35 | NoPrelude
35 | NoREPL
36 | NoREPL
36 | OLogging Int
37 | OLogging Int
@@ -48,6 +49,8 @@ runIdris opts =
48 do let inputs = opt getFile opts
49 do let inputs = opt getFile opts
49 let runrepl = not (NoREPL `elem` opts)
50 let runrepl = not (NoREPL `elem` opts)
50 let output = opt getOutput opts
51 let output = opt getOutput opts
52+ when (Ver `elem` opts) $ lift showver
53+ when (Usage `elem` opts) $ lift usage
51 setREPL runrepl
54 setREPL runrepl
52 mapM_ makeOption opts
55 mapM_ makeOption opts
53 elabPrims
56 elabPrims
@@ -80,8 +83,11 @@ getOutput _ = Nothing
80opt :: (Opt -> Maybe a) -> [Opt] -> [a]
83opt :: (Opt -> Maybe a) -> [Opt] -> [a]
81opt = mapMaybe
84opt = mapMaybe
82
85
83−usage = do putStrLn "You're doing it wrong"
86+usage = do putStrLn usagemsg
84− exitWith (ExitFailure 1)
87+ exitWith ExitSuccess
88+
89+showver = do putStrLn $ "Idris version " ++ ver
90+ exitWith ExitSuccess
85
91
86parseArgs :: [String] -> IO [Opt]
92parseArgs :: [String] -> IO [Opt]
87parseArgs [] = return []
93parseArgs [] = return []
@@ -91,22 +97,10 @@ parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
91parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
97parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)
92parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
98parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)
93parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
99parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)
100+parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)
101+parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)
94parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
102parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
95
103
96−{-
97−main'
98− = do f <- readFile "test.mi"
99− case parseFile f of
100− Left err -> print err
101− Right defs -> do
102− print defs
103− case checkProgram emptyContext defs of
104− OK ctxt -> do print (toAlist ctxt)
105− runShell (initState ctxt)
106− return ()
107− err -> print err
108− -}
109−
110ver = showVersion version
104ver = showVersion version
111
105
112banner = " ____ __ _ \n" ++
106banner = " ____ __ _ \n" ++
@@ -115,3 +109,13 @@ banner = " ____ __ _ \n" ++
115 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
109 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
116 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
110 " /___/\\__,_/_/ /_/____/ Type :? for help \n"
117
111
112+usagemsg = "Idris version " ++ ver ++ "\n" ++
113+ "--------------" ++ map (\x -> '-') ver ++ "\n" ++
114+ "Usage: idris [input file] [options]\n" ++
115+ "Options:\n" ++
116+ "\t--check Type check only\n" ++
117+ "\t-o [file] Generate executable\n" ++
118+ "\t--noprelude Don't import the prelude\n" ++
119+ "\t--typeintype Disable universe checking\n" ++
120+ "\t--log [level] Set debugging log level\n"
121+