@@ -10,10 +10,50 @@ import Options.Applicative
10import Options.Applicative.Arrows
10import Options.Applicative.Arrows
11import Data.Maybe
11import Data.Maybe
13+import qualified Text.PrettyPrint.ANSI.Leijen as PP
13runArgParser :: IO [Opt]
15runArgParser :: IO [Opt]
14−runArgParser = do opts <- execParser $ info parser $
16+runArgParser = do opts <- execParser $ info parser
15− header ("Idris version " ++ ver ++ ", (C) The Idris Community 2014")
17+ (fullDesc
18+ <> headerDoc (Just idrisHeader)
19+ <> progDescDoc (Just idrisProgDesc)
20+ <> footerDoc (Just idrisFooter)
16 return $ preProcOpts opts []
22 return $ preProcOpts opts []
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",
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"
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.",
51+ PP.text "More details over Idris can be found online here:",
53+ PP.indent 4 (PP.text "http://www.idris-lang.org/")]
18pureArgParser :: [String] -> [Opt]
58pureArgParser :: [String] -> [Opt]
19pureArgParser args = case execParserMaybe (info parser idm) args of
59pureArgParser args = case execParserMaybe (info parser idm) args of