on master help sign in
Merge pull request #3333 from steshaw/filename-args-in-order

Keep filename args in the order specified on the cmd line

commit54fadffed1bc5fc6484129b6477d3696ee269e80 authorNiklas Larsson <metaniklas@gmail.com> dateSun 7 Aug 2016, 13:31 (10 years ago) parent691e704fa6e061
2 files changed+27−37
src/Idris/CmdOptions.hs+26−36 test/dsl003/expected+1−1
src/Idris/CmdOptions.hs+26−36
@@ -22,8 +22,6 @@ import Text.ParserCombinators.ReadP hiding (many, option)
2222
2323import Safe (lastMay)
2424
25−
26−
2725import qualified Text.PrettyPrint.ANSI.Leijen as PP
2826
2927runArgParser :: IO [Opt]
@@ -33,7 +31,7 @@ runArgParser = do opts <- execParser $ info parser
3331 <> progDescDoc (Just idrisProgDesc)
3432 <> footerDoc (Just idrisFooter)
3533 )
36− return $ preProcOpts opts []
34+ return $ preProcOpts opts
3735 where
3836 idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2016"]
3937 idrisProgDesc = PP.vsep [PP.empty,
@@ -43,7 +41,7 @@ runArgParser = do opts <- execParser $ info parser
4341 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
4442 PP.text "and ML.",
4543 PP.empty,
46− PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [
44+ PP.vsep $ map (PP.indent 4 . PP.text) [
4745 "+ Full dependent types with dependent pattern matching",
4846 "+ Simple case expressions, where-clauses, with-rule",
4947 "+ Pattern matching let- and lambda-bindings",
@@ -66,12 +64,9 @@ runArgParser = do opts <- execParser $ info parser
6664 PP.empty,
6765 PP.indent 4 (PP.text "http://www.idris-lang.org/")]
6866
69−
70−
71−
7267pureArgParser :: [String] -> [Opt]
7368pureArgParser args = case getParseResult $ execParserPure (prefs idm) (info parser idm) args of
74− Just opts -> preProcOpts opts []
69+ Just opts -> preProcOpts opts
7570 Nothing -> []
7671
7772parser :: Parser [Opt]
@@ -80,7 +75,6 @@ parser = runA $ proc () -> do
8075 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()
8176 A parseVersion >>> A helper -< (flags ++ files)
8277
83−
8478parseFlags :: Parser [Opt]
8579parseFlags = many $
8680 flag' NoBanner (long "nobanner" <> help "Suppress the banner")
@@ -153,14 +147,13 @@ parseFlags = many $
153147 <|> (DumpDefun <$> strOption (long "dumpdefuns"))
154148 <|> (DumpCases <$> strOption (long "dumpcases"))
155149
156− <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"
157− <> metavar "TARGET"
158− <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))
150+ <|> (UseCodegen . parseCodegen) <$> strOption (long "codegen"
151+ <> metavar "TARGET"
152+ <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris")
159153
160−
161− <|> ((\s -> UseCodegen $ Via JSONFormat s) <$> strOption (long "portable-codegen"
162− <> metavar "TARGET"
163− <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))
154+ <|> ((UseCodegen . Via JSONFormat) <$> strOption (long "portable-codegen"
155+ <> metavar "TARGET"
156+ <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))
164157
165158 <|> (CodegenArgs <$> strOption (long "cg-opt"
166159 <> metavar "ARG"
@@ -171,10 +164,10 @@ parseFlags = many $
171164 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")
172165 <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))
173166
174− <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension"
175− <> short 'X'
176− <> metavar "EXT"
177− <> help "Turn on language extension (TypeProviders or ErrorReflection)"))
167+ <|> ((Extension . getExt) <$> strOption (long "extension"
168+ <> short 'X'
169+ <> metavar "EXT"
170+ <> help "Turn on language extension (TypeProviders or ErrorReflection)"))
178171
179172 -- Optimisation Levels
180173 <|> flag' (OptLevel 3) (long "O3")
@@ -201,30 +194,29 @@ parseFlags = many $
201194 <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")
202195 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")
203196
204− where
205− getExt s = case maybeRead s of
206− Just ext -> ext
207− Nothing -> error ("Unknown extension " ++ s)
208− maybeRead = fmap fst . listToMaybe . reads
197+ where
198+ getExt :: String -> LanguageExt
199+ getExt s = fromMaybe (error ("Unknown extension " ++ s)) (maybeRead s)
200+ maybeRead :: String -> Maybe LanguageExt
201+ maybeRead = fmap fst . listToMaybe . reads
209202
210203parseVersion :: Parser (a -> a)
211204parseVersion = infoOption ver (short 'v' <> long "version" <> help "Print version information")
212205
213−preProcOpts :: [Opt] -> [Opt] -> [Opt]
214−preProcOpts [] ys = ys
215−preProcOpts (NoBuiltins:xs) ys = NoBuiltins : NoPrelude : preProcOpts xs ys
216−preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys
217−preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys
218−preProcOpts (x:xs) ys = preProcOpts xs (x:ys)
206+preProcOpts :: [Opt] -> [Opt]
207+preProcOpts (NoBuiltins : xs) = NoBuiltins : NoPrelude : preProcOpts xs
208+preProcOpts (Output s : xs) = Output s : NoREPL : preProcOpts xs
209+preProcOpts (BCAsm s : xs) = BCAsm s : NoREPL : preProcOpts xs
210+preProcOpts (x:xs) = x : preProcOpts xs
211+preProcOpts [] = []
219212
220213parseCodegen :: String -> Codegen
221214parseCodegen "bytecode" = Bytecode
222215parseCodegen cg = Via IBCFormat (map toLower cg)
223216
224−
225217parseLogCats :: Monad m => String -> m [LogCat]
226218parseLogCats s =
227− case lastMay (readP_to_S (doParse) s) of
219+ case lastMay (readP_to_S doParse s) of
228220 Just (xs, _) -> return xs
229221 _ -> fail "Incorrect categories specified"
230222 where
@@ -252,12 +244,10 @@ parseConsoleWidth :: Monad m => String -> m ConsoleWidth
252244parseConsoleWidth "auto" = return AutomaticWidth
253245parseConsoleWidth "infinite" = return InfinitelyWide
254246parseConsoleWidth s =
255− case lastMay (readP_to_S (integerReader) s) of
247+ case lastMay (readP_to_S integerReader s) of
256248 Just (r, _) -> return $ ColsWide r
257249 _ -> fail $ "Cannot parse: " ++ s
258250
259−
260−
261251integerReader :: ReadP Int
262252integerReader = do
263253 digits <- many1 $ satisfy isDigit
test/dsl003/expected+1−1
@@ -1,2 +1,2 @@
1−ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []
21Refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)
2+ForAll INT (ForAll INT (ItHolds (Var (FS FZ) === Var FZ))) : Spec []