git.iko.soy/Idris-dev
on f8a6746 help sign in
Idris-dev/src/Idris/Help.hs
94 lines 6.1 kB history raw
1module Idris.Help (CmdArg(..), help, extraHelp) where
3data CmdArg = ExprArg -- ^ The command takes an expression
4 | NameArg -- ^ The command takes a name
5 | FileArg -- ^ The command takes a file
6 | ModuleArg -- ^ The command takes a module name
7 | NumberArg -- ^ The command takes a number
8 | NamespaceArg -- ^ The command takes a namespace name
9 | OptionArg -- ^ The command takes an option
10 | MetaVarArg -- ^ The command takes a metavariable
11 | ColourArg -- ^ The command is the colour-setting command
12 | NoArg -- ^ No completion (yet!?)
13 | SpecialHeaderArg -- ^ do not use
14 | ConsoleWidthArg -- ^ The width of the console
15 | DeclArg -- ^ An Idris declaration, as might be contained in a file
16 | ManyArgs CmdArg -- ^ Zero or more of one kind of argument
17 | OptionalArg CmdArg -- ^ Zero or one of one kind of argument
18 | SeqArgs CmdArg CmdArg -- ^ One kind of argument followed by another
20instance Show CmdArg where
21 show ExprArg = "<expr>"
22 show NameArg = "<name>"
23 show FileArg = "<filename>"
24 show ModuleArg = "<module>"
25 show NumberArg = "<number>"
26 show NamespaceArg = "<namespace>"
27 show OptionArg = "<option>"
28 show MetaVarArg = "<metavar>"
29 show ColourArg = "<option>"
30 show NoArg = ""
31 show SpecialHeaderArg = "Arguments"
32 show ConsoleWidthArg = "auto|infinite|<number>"
33 show DeclArg = "<top-level declaration>"
34 show (ManyArgs a) = "(" ++ show a ++ ")..."
35 show (OptionalArg a) = "[" ++ show a ++ "]"
36 show (SeqArgs a b) = show a ++ " " ++ show b
38help :: [([String], CmdArg, String)]
39help =
40 [ (["<expr>"], NoArg, "Evaluate an expression"),
41 ([":t"], ExprArg, "Check the type of an expression"),
42 ([":miss", ":missing"], NameArg, "Show missing clauses"),
43 ([":doc"], NameArg, "Show internal documentation"),
44 ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),
45 ([":apropos"], NoArg, "Search names, types, and documentation"),
46 ([":search", ":s"], ExprArg, "Search for values by type"),
47 ([":whocalls", ":wc"], NameArg, "List the callers of some name"),
48 ([":callswho", ":cw"], NameArg, "List the callees of some name"),
49 ([":total"], NameArg, "Check the totality of a name"),
50 ([":r",":reload"], NoArg, "Reload current file"),
51 ([":l",":load"], FileArg, "Load a new file"),
52 ([":cd"], FileArg, "Change working directory"),
53 ([":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
54 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),
55 ([":m",":metavars"], NoArg, "Show remaining proof obligations (metavariables)"),
56 ([":p",":prove"], MetaVarArg, "Prove a metavariable"),
57 ([":a",":addproof"], NameArg, "Add proof to source file"),
58 ([":rmproof"], NameArg, "Remove proof from proof stack"),
59 ([":showproof"], NameArg, "Show proof"),
60 ([":proofs"], NoArg, "Show available proofs"),
61 ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),
62 ([":c",":compile"], FileArg, "Compile to an executable [codegen] <filename>"),
63 ([":exec",":execute"], NoArg, "Compile to an executable and run"),
64 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),
65 ([":dynamic"], NoArg, "List dynamically loaded C libraries"),
66 ([":?",":h",":help"], NoArg, "Display this help text"),
67 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),
68 ([":unset"], OptionArg, "Unset an option"),
69 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),
70 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),
71 ([":q",":quit"], NoArg, "Exit the Idris system"),
72 ([":w", ":warranty"], NoArg, "Displays warranty information"),
73 ([":let"], ManyArgs DeclArg, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"),
74 ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given"),
75 ([":printdef"], NameArg, "Show the definition of a function"),
76 ([":pp", ":pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg)), "Pretty prints an Idris function in either LaTeX or HTML and for a specified width.")
77 ]
79-- | Use these for completion, but don't show them in :help
80extraHelp ::[([String], CmdArg, String)]
81extraHelp =
82 [ ([":casesplit", ":cs"], NoArg, ":cs <line> <name> splits the pattern variable on the line")
83 , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")
84 , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")
85 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")
86 , ([":addmissing", ":am"], NoArg, ":am <line> <name> adds all missing pattern matches for the name on the line")
87 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")
88 , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")
89 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")
90 , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")
91 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")
92 , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")
93 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")
94 ]