src/Idris/CmdOptions.hs · Idris-dev

1{-# LANGUAGE Arrows #-}

2module Idris.CmdOptions where

3

4import Idris.AbsSyntaxTree

5import Idris.REPL

6

7import IRTS.CodegenCommon

8

9import Options.Applicative

10import Options.Applicative.Arrows

11import Data.Char

12import Data.Maybe

13

14import Text.ParserCombinators.ReadP hiding (many, option)

15

16import Safe (lastMay)

17

18

19

20import qualified Text.PrettyPrint.ANSI.Leijen as PP

21

22runArgParser :: IO [Opt]

23runArgParser = do opts <- execParser $ info parser

24 (fullDesc

25 <> headerDoc (Just idrisHeader)

26 <> progDescDoc (Just idrisProgDesc)

27 <> footerDoc (Just idrisFooter)

28 )

29 return $ preProcOpts opts []

30 where

31 idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]

32 idrisProgDesc = PP.vsep [PP.empty,

33 PP.text "Idris is a general purpose pure functional programming language with dependent",

34 PP.text "types. Dependent types allow types to be predicated on values, meaning that",

35 PP.text "some aspects of a program's behaviour can be specified precisely in the type.",

36 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",

37 PP.text "and ML.",

38 PP.empty,

39 PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [

40 "+ Full dependent types with dependent pattern matching",

41 "+ where clauses, with rule, simple case expressions",

42 "+ pattern matching let and lambda bindings",

43 "+ Type classes, monad comprehensions",

44 "+ do notation, idiom brackets",

45 "+ syntactic conveniences for lists, tuples, dependent pairs",

46 "+ Totality checking",

47 "+ Coinductive types",

48 "+ Indentation significant syntax, extensible syntax",

49 "+ Tactic based theorem proving (influenced by Coq)",

50 "+ Cumulative universes",

51 "+ Simple foreign function interface (to C)",

52 "+ Hugs style interactive environment"

53 ]]

54 idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",

55 PP.text "and project. Thus the tooling provided and resulting programs created",

56 PP.text "should not necessarily be seen as production ready nor for industrial use.",

57 PP.empty,

58 PP.text "More details over Idris can be found online here:",

59 PP.empty,

60 PP.indent 4 (PP.text "http://www.idris-lang.org/")]

65pureArgParser :: [String] -> [Opt]

66pureArgParser args = case getParseResult $ execParserPure (prefs idm) (info parser idm) args of

67 Just opts -> preProcOpts opts []

68 Nothing -> []

69

70parser :: Parser [Opt]

71parser = runA $ proc () -> do

72 flags <- asA parseFlags -< ()

73 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()

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

75

76

77parseFlags :: Parser [Opt]

78parseFlags = many $

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

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

81 -- IDE Mode Specific Flags

82 <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")

83 <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")

84 <|> flag' Idemode (long "ideslave" <> help "Deprecated version of --ide-mode") -- TODO: Remove in v0.9.18

85 <|> flag' IdemodeSocket (long "ideslave-socket" <> help "Deprecated version of --ide-mode-socket") -- TODO: Remove in v0.9.18

86 <|> (Client <$> strOption (long "client"))

87 -- Logging Flags

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

89 <|> (OLogCats <$> option (str >>= parseLogCats)

90 (long "logging-categories"

91 <> metavar "CATS"

92 <> help "Colon separated logging categories. Use --listlogcats to see list."))

93

94 -- Turn off Certain libraries.

95 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

96 <|> flag' NoPrelude (long "noprelude" <> help "Do not use the given prelude")

97 <|> flag' NoBuiltins (long "nobuiltins" <> help "Do not use the builtin functions")

98 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

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

100 -- <|> flag' TypeCase (long "typecase")

101 <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

102 <|> flag' TypeInType (long "typeintype" <> help "Turn off Universe checking")

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

104 <|> flag' DefaultPartial (long "partial")

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

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

107 <|> flag' NoCoverage (long "nocoverage")

108 <|> flag' ErrContext (long "errorcontext")

109 -- Show things

110 <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")

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

112 <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

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

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

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

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

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

118 <|> flag' WarnOnly (long "warn")

119 <|> (Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))

120 <|> (Port <$> strOption (long "port" <> metavar "PORT" <> help "REPL TCP port"))

121 -- Package commands

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

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

124 <|> (PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables"))

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

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

127 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

128 <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

129 -- Misc options

130 <|> (BCAsm <$> strOption (long "bytecode"))

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

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

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

134 <|> (DumpDefun <$> strOption (long "dumpdefuns"))

135 <|> (DumpCases <$> strOption (long "dumpcases"))

136 <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))

137 <|> (CodegenArgs <$> strOption (long "cg-opt" <> metavar "ARG" <> help "Arguments to pass to code generator"))

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

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

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

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

142 -- Optimisation Levels

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

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

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

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

147 <|> flag' (AddOpt PETransform) (long "partial-eval")

148 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

149 <|> (OptLevel <$> option auto (short 'O' <> long "level"))

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

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

152 -- Colour Options

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

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

155

156 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))

157 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")

158 <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")

159 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")

160

161 where

162 getExt s = case maybeRead s of

163 Just ext -> ext

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

165 maybeRead = fmap fst . listToMaybe . reads

166

167parseVersion :: Parser (a -> a)

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

169

170preProcOpts :: [Opt] -> [Opt] -> [Opt]

171preProcOpts [] ys = ys