git.iko.soy/Idris-dev
on da0a382 help sign in
Idris-dev/src/Idris/CmdOptions.hs
275 lines 15 kB history raw
1{-|
2Module : Idris.CmdOptions
3Description : A parser for the CmdOptions for the Idris executable.
4License : BSD3
5Maintainer : The Idris Community.
6-}
7{-# LANGUAGE Arrows #-}
8module Idris.CmdOptions
9 (
10 module Idris.CmdOptions
11 , opt
12 , getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc
13 , getPkgREPL, getPkgTest, getPort, getIBCSubDir
14 ) where
16import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,
17 getPkgClean, getPkgMkDoc, getPkgREPL, getPkgTest,
18 getPort, opt)
19import Idris.AbsSyntaxTree
20import Idris.Info (getIdrisVersion)
21-- import Idris.REPL
22import IRTS.CodegenCommon
24import Control.Monad.Trans (lift)
25import Control.Monad.Trans.Except (throwE)
26import Control.Monad.Trans.Reader (ask)
27import Data.Char
28import Data.Maybe
29import Options.Applicative
30import Options.Applicative.Arrows
31import Options.Applicative.Types (ReadM(..))
32import Safe (lastMay)
33import Text.ParserCombinators.ReadP hiding (many, option)
34import qualified Text.PrettyPrint.ANSI.Leijen as PP
36runArgParser :: IO [Opt]
37runArgParser = do opts <- execParser $ info parser
38 (fullDesc
39 <> headerDoc (Just idrisHeader)
40 <> progDescDoc (Just idrisProgDesc)
41 <> footerDoc (Just idrisFooter)
42 )
43 return $ preProcOpts opts
44 where
45 idrisHeader = PP.hsep [PP.text "Idris version", PP.text getIdrisVersion, PP.text ", (C) The Idris Community 2016"]
46 idrisProgDesc = PP.vsep [PP.empty,
47 PP.text "Idris is a general purpose pure functional programming language with dependent",
48 PP.text "types. Dependent types allow types to be predicated on values, meaning that",
49 PP.text "some aspects of a program's behaviour can be specified precisely in the type.",
50 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
51 PP.text "and ML.",
52 PP.empty,
53 PP.vsep $ map (PP.indent 4 . PP.text) [
54 "+ Full dependent types with dependent pattern matching",
55 "+ Simple case expressions, where-clauses, with-rule",
56 "+ Pattern matching let- and lambda-bindings",
57 "+ Overloading via Interfaces (Type class-like), Monad comprehensions",
58 "+ do-notation, idiom brackets",
59 "+ Syntactic conveniences for lists, tuples, dependent pairs",
60 "+ Totality checking",
61 "+ Coinductive types",
62 "+ Indentation significant syntax, Extensible syntax",
63 "+ Tactic based theorem proving (influenced by Coq)",
64 "+ Cumulative universes",
65 "+ Simple Foreign Function Interface",
66 "+ Hugs style interactive environment"
67 ]]
68 idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",
69 PP.text "and project. Thus the tooling provided and resulting programs created",
70 PP.text "should not necessarily be seen as production ready nor for industrial use.",
71 PP.empty,
72 PP.text "More details over Idris can be found online here:",
73 PP.empty,
74 PP.indent 4 (PP.text "http://www.idris-lang.org/")]
76pureArgParser :: [String] -> [Opt]
77pureArgParser args = case getParseResult $ execParserPure (prefs idm) (info parser idm) args of
78 Just opts -> preProcOpts opts
79 Nothing -> []
81parser :: Parser [Opt]
82parser = runA $ proc () -> do
83 flags <- asA parseFlags -< ()
84 files <- asA (many $ argument (fmap Filename str) (metavar "FILES")) -< ()
85 A parseVersion >>> A helper -< (flags ++ files)
87parseFlags :: Parser [Opt]
88parseFlags = many $
89 flag' NoBanner (long "nobanner" <> help "Suppress the banner")
90 <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")
92 -- IDE Mode Specific Flags
93 <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")
94 <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")
96 <|> (Client <$> strOption (long "client"))
98 -- Logging Flags
99 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))
100 <|> (OLogCats <$> option (str >>= parseLogCats)
101 (long "logging-categories"
102 <> metavar "CATS"
103 <> help "Colon separated logging categories. Use --listlogcats to see list."))
105 -- Turn off things
106 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")
107 <|> flag' NoPrelude (long "noprelude" <> help "Do not use the given prelude")
108 <|> flag' NoBuiltins (long "nobuiltins" <> help "Do not use the builtin functions")
110 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")
112 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))
114 -- <|> flag' TypeCase (long "typecase")
115 <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")
116 <|> flag' TypeInType (long "typeintype" <> help "Turn off Universe checking")
117 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")
118 <|> flag' DefaultPartial (long "partial")
119 <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")
120 <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")
121 <|> flag' NoCoverage (long "nocoverage")
122 <|> flag' ErrContext (long "errorcontext")
124 -- Show things
125 <|> flag' ShowAll (long "info" <> help "Display information about installation.")
126 <|> flag' ShowLoggingCats (long "listlogcats" <> help "Display logging categories")
127 <|> flag' ShowLibs (long "link" <> help "Display link flags")
128 <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")
129 <|> flag' ShowLibDir (long "libdir" <> help "Display library directory")
130 <|> flag' ShowDocDir (long "docdir" <> help "Display idrisdoc install directory")
131 <|> flag' ShowIncs (long "include" <> help "Display the includes flags")
133 <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")
135 <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))
136 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))
137 <|> (SourceDir <$> strOption (long "sourcepath" <> help "Add directory to the list of source search paths"))
139 <|> flag' WarnOnly (long "warn")
141 <|> (Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))
142 <|> (Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port"))
144 -- Package commands
145 <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))
146 <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))
147 <|> (PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables"))
148 <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))
149 <|> (PkgDocBuild <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))
150 <|> (PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package"))
151 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))
152 <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))
154 -- Misc options
155 <|> (BCAsm <$> strOption (long "bytecode"))
157 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")
158 <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")
160 <|> (DumpDefun <$> strOption (long "dumpdefuns"))
161 <|> (DumpCases <$> strOption (long "dumpcases"))
163 <|> (UseCodegen . parseCodegen) <$> strOption (long "codegen"
164 <> metavar "TARGET"
165 <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris")
167 <|> ((UseCodegen . Via JSONFormat) <$> strOption (long "portable-codegen"
168 <> metavar "TARGET"
169 <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))
171 <|> (CodegenArgs <$> strOption (long "cg-opt"
172 <> metavar "ARG"
173 <> help "Arguments to pass to code generator"))
175 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))
177 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")
178 <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))
180 <|> ((Extension . getExt) <$> strOption (long "extension"
181 <> short 'X'
182 <> metavar "EXT"
183 <> help "Turn on language extension (TypeProviders or ErrorReflection)"))
185 -- Optimisation Levels
186 <|> flag' (OptLevel 3) (long "O3")
187 <|> flag' (OptLevel 2) (long "O2")
188 <|> flag' (OptLevel 1) (long "O1")
189 <|> flag' (OptLevel 0) (long "O0")
191 <|> flag' (AddOpt PETransform) (long "partial-eval")
192 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")
194 <|> (OptLevel <$> option auto (short 'O' <> long "level"))
196 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple."))
197 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "If supported the codegen will target the named CPU e.g. corei7 or cortex-m3"))
199 -- Colour Options
200 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")
201 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")
203 <|> (UseConsoleWidth <$> option (str >>= parseConsoleWidth) (long "consolewidth" <> metavar "WIDTH" <> help "Select console width: auto, infinite, nat"))
205 <|> flag' DumpHighlights (long "highlight" <> help "Emit source code highlighting")
207 <|> flag' NoElimDeprecationWarnings (long "no-elim-deprecation-warnings" <> help "Disable deprecation warnings for %elim")
208 <|> flag' NoOldTacticDeprecationWarnings (long "no-tactic-deprecation-warnings" <> help "Disable deprecation warnings for the old tactic sublanguage")
210 where
211 getExt :: String -> LanguageExt
212 getExt s = fromMaybe (error ("Unknown extension " ++ s)) (maybeRead s)
213 maybeRead :: String -> Maybe LanguageExt
214 maybeRead = fmap fst . listToMaybe . reads
215 portReader :: ReadM REPLPort
216 portReader =
217 ((ListenPort . fromIntegral) <$> auto) <|>
218 (ReadM $ do opt <- ask
219 if map toLower opt == "none"
220 then return $ DontListen
221 else lift $ throwE $ ErrorMsg $
222 "got " <> opt <> " expected port number or \"none\"")
224parseVersion :: Parser (a -> a)
225parseVersion = infoOption getIdrisVersion (short 'v' <> long "version" <> help "Print version information")
227preProcOpts :: [Opt] -> [Opt]
228preProcOpts (NoBuiltins : xs) = NoBuiltins : NoPrelude : preProcOpts xs
229preProcOpts (Output s : xs) = Output s : NoREPL : preProcOpts xs
230preProcOpts (BCAsm s : xs) = BCAsm s : NoREPL : preProcOpts xs
231preProcOpts (x:xs) = x : preProcOpts xs
232preProcOpts [] = []
234parseCodegen :: String -> Codegen
235parseCodegen "bytecode" = Bytecode
236parseCodegen cg = Via IBCFormat (map toLower cg)
238parseLogCats :: Monad m => String -> m [LogCat]
239parseLogCats s =
240 case lastMay (readP_to_S doParse s) of
241 Just (xs, _) -> return xs
242 _ -> fail "Incorrect categories specified"
243 where
244 doParse :: ReadP [LogCat]
245 doParse = do
246 cs <- sepBy1 parseLogCat (char ':')
247 eof
248 return (concat cs)
250 parseLogCat :: ReadP [LogCat]
251 parseLogCat = (string (strLogCat IParse) *> return parserCats)
252 <|> (string (strLogCat IElab) *> return elabCats)
253 <|> (string (strLogCat ICodeGen) *> return codegenCats)
254 <|> (string (strLogCat ICoverage) *> return [ICoverage])
255 <|> (string (strLogCat IIBC) *> return [IIBC])
256 <|> (string (strLogCat IErasure) *> return [IErasure])
257 <|> parseLogCatBad
259 parseLogCatBad :: ReadP [LogCat]
260 parseLogCatBad = do
261 s <- look
262 fail $ "Category: " ++ s ++ " is not recognised."
264parseConsoleWidth :: Monad m => String -> m ConsoleWidth
265parseConsoleWidth "auto" = return AutomaticWidth
266parseConsoleWidth "infinite" = return InfinitelyWide
267parseConsoleWidth s =
268 case lastMay (readP_to_S integerReader s) of
269 Just (r, _) -> return $ ColsWide r
270 _ -> fail $ "Cannot parse: " ++ s
272integerReader :: ReadP Int
273integerReader = do
274 digits <- many1 $ satisfy isDigit
275 return $ read digits