9be5866 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

started working on new cmd arg parser

9be5866klrr12 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -550,6 +550,7 @@ Library

550 , Idris.Transforms

551 , Idris.Unlit

552 , Idris.WhoCalls

553+ , Idris.CmdOptions

553

554

554 , IRTS.BCImp

555 , IRTS.BCImp

555 , IRTS.Bytecode

556 , IRTS.Bytecode

@@ -619,6 +620,7 @@ Library

619 , xml

620 , xml

620 , deepseq

621 , deepseq

621 , zlib

622 , zlib

623+ , optparse-applicative

622 Extensions: MultiParamTypeClasses

624 Extensions: MultiParamTypeClasses

623 , FunctionalDependencies

625 , FunctionalDependencies

624 , FlexibleContexts

626 , FlexibleContexts

main/Main.hs+2−63

@@ -24,6 +24,7 @@ import Idris.ElabDecls

24import Idris.Primitives

25import Idris.Imports

26import Idris.Error

27+import Idris.CmdOptions

28import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )

29import IRTS.System ( getLibFlags, getIdrisLibDir, getIncFlags )

@@ -36,8 +37,7 @@ import Paths_idris

36-- Main program reads command line options, parses the main program, and gets

37-- Main program reads command line options, parses the main program, and gets

37-- on with the REPL.

38-- on with the REPL.

39−main = do xs <- getArgs

40+main = do opts <- runArgParser

40− let opts = parseArgs xs

41 result <- runErrorT $ execStateT (runIdris opts) idrisInit

42 case result of

43 Left err -> putStrLn $ "Uncaught error: " ++ show err

@@ -48,8 +48,6 @@ runIdris [Client c] = do setVerbose False

48 setQuiet True

49 runIO $ runClient c

50runIdris opts = do

51− when (Ver `elem` opts) $ runIO showver

52− when (Usage `elem` opts) $ runIO usage

53 when (ShowIncs `elem` opts) $ runIO showIncs

51 when (ShowIncs `elem` opts) $ runIO showIncs

54 when (ShowLibs `elem` opts) $ runIO showLibs

52 when (ShowLibs `elem` opts) $ runIO showLibs

55 when (ShowLibdir `elem` opts) $ runIO showLibdir

53 when (ShowLibdir `elem` opts) $ runIO showLibdir

@@ -72,9 +70,6 @@ runIdris opts = do

72 _ -> ifail "Too many packages"

70 _ -> ifail "Too many packages"

73 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

71 fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs

75−usage = do putStrLn usagemsg

76− exitWith ExitSuccess

77−

78showver = do putStrLn $ "Idris version " ++ ver

73showver = do putStrLn $ "Idris version " ++ ver

79 exitWith ExitSuccess

74 exitWith ExitSuccess

@@ -89,59 +84,3 @@ showLibdir = do dir <- getIdrisLibDir

89showIncs = do incFlags <- getIncFlags

84showIncs = do incFlags <- getIncFlags

90 putStrLn incFlags

85 putStrLn incFlags

91 exitWith ExitSuccess

86 exitWith ExitSuccess

92−

93−usagemsghdr = "Idris version " ++ ver ++ ", (C) The Idris Community 2014"

94−

95−usagemsg = usagemsghdr ++ "\n" ++

96− map (\x -> '-') usagemsghdr ++ "\n" ++

97− "idris [OPTIONS] [FILE]\n\n" ++

98− "Common flags:\n" ++

99− "\t --install IPKG Install package\n" ++

100− "\t --clean IPKG Clean package\n" ++

101− "\t --build IPKG Build package\n" ++

102− "\t --mkdoc IPKG Generate IdrisDoc for package\n" ++

103− "\t -e --eval EXPR Evaluate an expression without loading the REPL\n" ++

104− "\t --exec EXPR Execute as idris\n" ++

105− "\t --libdir Display library directory\n" ++

106− "\t --link Display link flags\n" ++

107− "\t --include Display the includes flags\n" ++

108− "\t --nobanner Suppress the banner\n" ++

109− "\t --color, --colour Force coloured output\n" ++

110− "\t --nocolor, --nocolour Disable coloured output\n" ++

111− "\t --errorcontent Undocumented\n" ++

112− "\t --nocoverage Undocumented\n" ++

113− "\t -o --output FILE Specify output file\n" ++

114− "\t --check Undocumented\n" ++

115− "\t --total Require functions to be total by default\n" ++

116− "\t --partial Undocumented\n" ++

117− "\t --warnreach Warn about reachable but inaccessible arguments\n" ++

118− "\t --warnpartial Warn about undeclared partial functions.\n" ++

119− "\t --warn Undocumented\n" ++

120− "\t --typecase Undocumented\n" ++

121− "\t --typeintype Undocumented\n" ++

122− "\t --nobasepkgs Undocumented\n" ++

123− "\t --noprelude Undocumented\n" ++

124− "\t --nobuiltins Undocumented\n" ++

125− "\t -O --level LEVEL Undocumented\n" ++

126− "\t -i --idrispath DIR Add directory to the list of import paths\n" ++

127− "\t --package ITEM Undocumented\n" ++

128− "\t --ibcsubdir FILE Write IBC files into sub directory\n" ++

129− "\t --codegen TARGET Select code generator: C, Java, bytecode,\n" ++

130− "\t javascript, node, or llvm\n" ++

131− "\t --mvn Create a maven project (for Java codegen)\n" ++

132− "\t --cpu=CPU Select target CPU e.g. corei7 or cortex-m3\n" ++

133− "\t (for LLVM codegen)\n" ++

134− "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++

135− "\t -S --codegenonly Do no further compilation of code generator output\n" ++

136− "\t -c --compileonly Compile to object files rather than an executable\n" ++

137− "\t -X --extension EXT Turn on langage extension (TypeProviders or ErrorReflection)\n" ++

138− "\t --dumpdefuns Undocumented\n" ++

139− "\t --dumpcases Undocumented\n" ++

140− "\t --log LEVEL --loglevel Debugging log level\n" ++

141− "\t --ideslave Undocumented\n" ++

142− "\t --client Undocumented\n" ++

143− "\t -h --help Display help message\n" ++

144− "\t -v --version Print version information\n" ++

145− "\t -V --verbose Loud verbosity\n" ++

146− "\t -q --quiet Quiet verbosity\n"

147−

src/Idris/AbsSyntaxTree.hs−2

@@ -315,8 +315,6 @@ data Command = Quit

315

316

317data Opt = Filename String

318− | Ver

319− | Usage

320 | Quiet

318 | Quiet

321 | NoBanner

319 | NoBanner

322 | ColourREPL Bool

320 | ColourREPL Bool

src/Idris/CmdOptions.hsnew file+108

@@ -0,0 +1,108 @@

1+{-# LANGUAGE Arrows #-}

2+module Idris.CmdOptions where

4+import Idris.AbsSyntaxTree

5+import Idris.REPL

7+import IRTS.CodegenCommon

9+import Options.Applicative

10+import Options.Applicative.Arrows

11+import Data.Maybe

12+

13+runArgParser :: IO [Opt]

14+runArgParser = do opts <- execParser $ info parser $

15+ header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")

16+ return $ preProcOpts opts []

17+

18+pureArgParser :: [String] -> [Opt]

19+pureArgParser args = case execParserMaybe (info parser idm) args of

20+ Just opts -> preProcOpts opts []

21+ Nothing -> []

22+

23+parser :: Parser [Opt]

24+parser = runA $ proc () -> do

25+ flags <- asA parseFlags -< ()

26+ files <- asA (many $ argument ((fmap . fmap) Filename str) (metavar "FILES")) -< ()

27+ A parseVersion >>> A helper -< (flags ++ files)

28+

29+parseFlags :: Parser [Opt]

30+parseFlags = many $

31+ flag' NoBanner (long "nobanner" <> help "Suppress the banner")

32+ <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

33+ <|> flag' Ideslave (long "ideslave")

34+ <|> (Client <$> strOption (long "client"))

35+ <|> (OLogging <$> option (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

36+ <|> flag' NoBasePkgs (long "nobasepkgs")

37+ <|> flag' NoPrelude (long "noprelude")

38+ <|> flag' NoBuiltins (long "nobuiltins")

39+ <|> flag' NoREPL (long "check")

40+ <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

41+ <|> flag' TypeCase (long "typecase")

42+ <|> flag' TypeInType (long "typeintype")

43+ <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

44+ <|> flag' DefaultPartial (long "partial")

45+ <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")

46+ <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")

47+ <|> flag' NoCoverage (long "nocoverage")

48+ <|> flag' ErrContext (long "errorcontext")

49+ <|> flag' ShowLibs (long "link" <> help "Display link flags")

50+ <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

51+ <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

52+ <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

53+ <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

54+ <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

55+ <|> flag' WarnOnly (long "warn")

56+ <|> (Pkg <$> strOption (short 'p' <> long "package"))

57+ -- Package commands

58+ <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

59+ <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

60+ <|> (PkgREPL <$> strOption (long "repl"))

61+ <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

62+ <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

63+ <|> (PkgCheck <$> strOption (long "check"))

64+ -- Misc options

65+ <|> (BCAsm <$> strOption (long "bytecode"))

66+ <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

67+ <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

68+ <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")

69+ <|> (DumpDefun <$> strOption (long "dumpdefuns"))

70+ <|> (DumpCases <$> strOption (long "dumpcases"))

71+ <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Java, bytecode"))

72+ <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

73+ <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

74+ <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

75+ <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension" <> short 'X' <> metavar "EXT" <> help "Turn on langage extension (TypeProviders or ErrorReflection)"))

76+ <|> flag' (OptLevel 3) (long "O3")

77+ <|> flag' (OptLevel 2) (long "O2")

78+ <|> flag' (OptLevel 1) (long "O1")

79+ <|> flag' (OptLevel 0) (long "O0")

80+ <|> (OptLevel <$> option (short 'O' <> long "level"))

81+ <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))

82+ <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))

83+ <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

84+ <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")

85+ where

86+ getExt s = case maybeRead s of

87+ Just ext -> ext

88+ Nothing -> error ("Unknown extension " ++ s)

89+ maybeRead = fmap fst . listToMaybe . reads

90+

91+parseVersion :: Parser (a -> a)

92+parseVersion = infoOption ver (short 'v' <> long "version" <> help "Print version information")

93+

94+preProcOpts :: [Opt] -> [Opt] -> [Opt]

95+preProcOpts [] ys = ys

96+preProcOpts (NoBuiltins:xs) ys = NoBuiltins : NoPrelude : preProcOpts xs ys

97+preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys

98+preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys

99+preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

100+

101+parseCodegen :: String -> Codegen

102+parseCodegen "C" = ViaC

103+parseCodegen "Java" = ViaJava

104+parseCodegen "bytecode" = Bytecode

105+parseCodegen "javascript" = ViaJavaScript

106+parseCodegen "node" = ViaNode

107+parseCodegen "llvm" = ViaLLVM

108+parseCodegen _ = error "unknown codegen" -- FIXME: partial function

src/Idris/REPL.hs−77

@@ -1116,83 +1116,6 @@ displayHelp = let vstr = showVersion version in

1116 l ++ take (c1 - length l) (repeat ' ') ++

1117 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

1118

1119−parseCodegen :: String -> Codegen

1120−parseCodegen "C" = ViaC

1121−parseCodegen "Java" = ViaJava

1122−parseCodegen "bytecode" = Bytecode

1123−parseCodegen "javascript" = ViaJavaScript

1124−parseCodegen "node" = ViaNode

1125−parseCodegen "llvm" = ViaLLVM

1126−parseCodegen _ = error "unknown codegen" -- FIXME: partial function

1127−

1128−parseArgs :: [String] -> [Opt]

1129−parseArgs [] = []

1130−parseArgs ("--nobanner":ns) = NoBanner : (parseArgs ns)

1131−parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

1132−parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)

1133−parseArgs ("--client":ns) = [Client (showSep " " ns)]

1134−parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

1135−parseArgs ("--nobasepkgs":ns) = NoBasePkgs : (parseArgs ns)

1136−parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

1137−parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)

1138−parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

1139−parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

1140−parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

1141−parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

1142−parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

1143−parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

1144−parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

1145−parseArgs ("--warnreach":ns) = WarnReach : (parseArgs ns)

1146−parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

1147−parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

1148−parseArgs ("--help":ns) = Usage : (parseArgs ns)

1149−parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

1150−parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

1151−parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

1152−parseArgs ("--version":ns) = Ver : (parseArgs ns)

1153−parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

1154−parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

1155−parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

1156−parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

1157−-- Package Related options

1158−parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

1159−parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

1160−parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

1161−parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

1162−parseArgs ("--repl":n:ns) = PkgREPL n : (parseArgs ns)

1163−parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

1164−parseArgs ("--mkdoc":n:ns) = PkgMkDoc n : (parseArgs ns) -- IdrisDoc

1165−parseArgs ("--checkpkg":n:ns) = PkgCheck n : (parseArgs ns)

1166−-- Misc Options

1167−parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

1168−parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

1169−parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

1170−parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

1171−parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

1172−parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

1173−parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

1174−parseArgs ("--eval":expr:ns) = EvalExpr expr : parseArgs ns

1175−parseArgs ("-e":expr:ns) = EvalExpr expr : parseArgs ns

1176−parseArgs ["--exec"] = InterpretScript "Main.main" : []

1177−parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

1178−parseArgs (('-':'X':extName):ns) = case maybeRead extName of

1179− Just ext -> Extension ext : parseArgs ns

1180− -- Not sure what to do for the Nothing case

1181− Nothing -> error ("Unknown extension " ++ extName)

1182− where maybeRead = fmap fst . listToMaybe . reads

1183−parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

1184−parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

1185−parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns

1186−parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

1187−parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

1188−parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

1189−parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

1190−parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns

1191−parseArgs ("--color":ns) = ColourREPL True : parseArgs ns

1192−parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns

1193−parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns

1194−parseArgs (n:ns) = Filename n : (parseArgs ns)

1195−

1196helphead =

1119helphead =

1197 [ (["Command"], SpecialHeaderArg, "Purpose"),

1120 [ (["Command"], SpecialHeaderArg, "Purpose"),

1198 ([""], NoArg, "")

1121 ([""], NoArg, "")

src/Pkg/PParser.hs+2−1

@@ -8,6 +8,7 @@ import Idris.Core.TT

8import Idris.REPL

9import Idris.AbsSyntaxTree

10import Idris.ParseHelpers

11+import Idris.CmdOptions

12import Paths_idris

13import Paths_idris

@@ -66,7 +67,7 @@ pClause = do reserved "executable"; lchar '=';

66 <|> do reserved "opts"; lchar '=';

67 <|> do reserved "opts"; lchar '=';

67 opts <- stringLiteral

68 opts <- stringLiteral

68 st <- get

69 st <- get

69− let args = parseArgs (words opts)

70+ let args = pureArgParser (words opts)

70 put (st { idris_opts = args })

71 put (st { idris_opts = args })

71 <|> do reserved "modules"; lchar '=';

72 <|> do reserved "modules"; lchar '=';

72 ms <- sepBy1 (iName []) (lchar ',')

73 ms <- sepBy1 (iName []) (lchar ',')

test/reg029/run+1−1

@@ -3,5 +3,5 @@ idris $@ reg029.idr -o reg029

3unset IDRIS_REG029_NONEXISTENT_VAR

4export IDRIS_REG029_EXISTENT_VAR='exists!'

5./reg029

6−idris $@ reg029.idr --exec

6+idris $@ reg029.idr --execute

7rm -f reg029 *.ibc