git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/CmdOptions.hs
150 lines 8.9 kB history raw
1{-# LANGUAGE Arrows #-}
2module Idris.CmdOptions where
4import Idris.AbsSyntaxTree
5import Idris.REPL
7import IRTS.CodegenCommon
9import Options.Applicative
10import Options.Applicative.Arrows
11import Data.Maybe
13import qualified Text.PrettyPrint.ANSI.Leijen as PP
15runArgParser :: IO [Opt]
16runArgParser = do opts <- execParser $ info parser
17 (fullDesc
18 <> headerDoc (Just idrisHeader)
19 <> progDescDoc (Just idrisProgDesc)
20 <> footerDoc (Just idrisFooter)
21 )
22 return $ preProcOpts opts []
23 where
24 idrisHeader = PP.hsep [PP.text "Idris version", PP.text ver, PP.text ", (C) The Idris Community 2014"]
25 idrisProgDesc = PP.vsep [PP.text "Idris is a general purpose pure functional programming language with dependent",
26 PP.text "types. Dependent types allow types to be predicated on values, meaning that",
27 PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",
28 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
29 PP.text "and ML.",
30 PP.empty,
31 PP.vsep $ map (\x -> PP.indent 4 (PP.text x)) [
32 "+ Full dependent types with dependent pattern matching",
33 "+ where clauses, with rule, simple case expressions",
34 "+ pattern matching let and lambda bindings",
35 "+ Type classes, monad comprehensions",
36 "+ do notation, idiom brackets",
37 "+ syntactic conveniences for lists, tuples, dependent pairs",
38 "+ Totality checking",
39 "+ Coinductive types",
40 "+ Indentation significant syntax, extensible syntax",
41 "+ Tactic based theorem proving (influenced by Coq)",
42 "+ Cumulative universes",
43 "+ Simple foreign function interface (to C)",
44 "+ Hugs style interactive environment"
45 ],
46 PP.empty]
47 idrisFooter = PP.vsep [PP.text "It is important to note that Idris is first and foremost a research tool",
48 PP.text "and project. Thus the tooling provided and resulting programs created",
49 PP.text "should not necessarily be seen as production ready nor for industrial use.",
50 PP.empty,
51 PP.text "More details over Idris can be found online here:",
52 PP.empty,
53 PP.indent 4 (PP.text "http://www.idris-lang.org/")]
58pureArgParser :: [String] -> [Opt]
59pureArgParser args = case execParserMaybe (info parser idm) args of
60 Just opts -> preProcOpts opts []
61 Nothing -> []
63parser :: Parser [Opt]
64parser = runA $ proc () -> do
65 flags <- asA parseFlags -< ()
66 files <- asA (many $ argument ((fmap . fmap) Filename str) (metavar "FILES")) -< ()
67 A parseVersion >>> A helper -< (flags ++ files)
69parseFlags :: Parser [Opt]
70parseFlags = many $
71 flag' NoBanner (long "nobanner" <> help "Suppress the banner")
72 <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")
73 <|> flag' Ideslave (long "ideslave")
74 <|> flag' IdeslaveSocket (long "ideslave-socket")
75 <|> (Client <$> strOption (long "client"))
76 <|> (OLogging <$> option (long "log" <> metavar "LEVEL" <> help "Debugging log level"))
77 <|> flag' NoBasePkgs (long "nobasepkgs")
78 <|> flag' NoPrelude (long "noprelude")
79 <|> flag' NoBuiltins (long "nobuiltins")
80 <|> flag' NoREPL (long "check")
81 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))
82 <|> flag' TypeCase (long "typecase")
83 <|> flag' TypeInType (long "typeintype")
84 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")
85 <|> flag' DefaultPartial (long "partial")
86 <|> flag' WarnPartial (long "warnpartial" <> help "Warn about undeclared partial functions")
87 <|> flag' WarnReach (long "warnreach" <> help "Warn about reachable but inaccessible arguments")
88 <|> flag' NoCoverage (long "nocoverage")
89 <|> flag' ErrContext (long "errorcontext")
90 <|> flag' ShowLibs (long "link" <> help "Display link flags")
91 <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")
92 <|> flag' ShowIncs (long "include" <> help "Display the includes flags")
93 <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")
94 <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))
95 <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))
96 <|> flag' WarnOnly (long "warn")
97 <|> (Pkg <$> strOption (short 'p' <> long "package"))
98 -- Package commands
99 <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))
100 <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))
101 <|> (PkgREPL <$> strOption (long "repl"))
102 <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))
103 <|> (PkgMkDoc <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))
104 <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))
105 <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))
106 -- Misc options
107 <|> (BCAsm <$> strOption (long "bytecode"))
108 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")
109 <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")
110 <|> flag' (OutputTy MavenProject) (long "mvn" <> help "Create a maven project (for Java codegen)")
111 <|> (DumpDefun <$> strOption (long "dumpdefuns"))
112 <|> (DumpCases <$> strOption (long "dumpcases"))
113 <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen" <> metavar "TARGET" <> help "Select code generator: C, Java, bytecode"))
114 <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))
115 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")
116 <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))
117 <|> ((\s -> Extension $ getExt s) <$> strOption (long "extension" <> short 'X' <> metavar "EXT" <> help "Turn on langage extension (TypeProviders or ErrorReflection)"))
118 <|> flag' (OptLevel 3) (long "O3")
119 <|> flag' (OptLevel 2) (long "O2")
120 <|> flag' (OptLevel 1) (long "O1")
121 <|> flag' (OptLevel 0) (long "O0")
122 <|> (OptLevel <$> option (short 'O' <> long "level"))
123 <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "Select target triple (for llvm codegen)"))
124 <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "Select target CPU e.g. corei7 or cortex-m3 (for LLVM codegen)"))
125 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")
126 <|> flag' (ColourREPL False) (long "nocolour" <> long "nocolor" <> help "Disable coloured output")
127 where
128 getExt s = case maybeRead s of
129 Just ext -> ext
130 Nothing -> error ("Unknown extension " ++ s)
131 maybeRead = fmap fst . listToMaybe . reads
133parseVersion :: Parser (a -> a)
134parseVersion = infoOption ver (short 'v' <> long "version" <> help "Print version information")
136preProcOpts :: [Opt] -> [Opt] -> [Opt]
137preProcOpts [] ys = ys
138preProcOpts (NoBuiltins:xs) ys = NoBuiltins : NoPrelude : preProcOpts xs ys
139preProcOpts (Output s:xs) ys = Output s : NoREPL : preProcOpts xs ys
140preProcOpts (BCAsm s:xs) ys = BCAsm s : NoREPL : preProcOpts xs ys
141preProcOpts (x:xs) ys = preProcOpts xs (x:ys)
143parseCodegen :: String -> Codegen
144parseCodegen "C" = ViaC
145parseCodegen "Java" = ViaJava
146parseCodegen "bytecode" = Bytecode
147parseCodegen "javascript" = ViaJavaScript
148parseCodegen "node" = ViaNode
149parseCodegen "llvm" = ViaLLVM
150parseCodegen _ = error "unknown codegen" -- FIXME: partial function