module Idris.Help (CmdArg(..), extraHelp) where
data CmdArg = ExprArg
| NameArg
| FileArg
| ShellCommandArg
| ModuleArg
| PkgArgs
| NumberArg
| NamespaceArg
| OptionArg
| MetaVarArg
| ColourArg
| NoArg
|
| ConsoleWidthArg
| DeclArg
| ManyArgs CmdArg
| OptionalArg CmdArg
| SeqArgs CmdArg CmdArg
instance Show CmdArg where
show :: CmdArg -> String
show CmdArg
ExprArg = String
"<expr>"
show CmdArg
NameArg = String
"<name>"
show CmdArg
FileArg = String
"<filename>"
show CmdArg
ShellCommandArg = String
"<command>"
show CmdArg
ModuleArg = String
"<module>"
show CmdArg
PkgArgs = String
"<package list>"
show CmdArg
NumberArg = String
"<number>"
show CmdArg
NamespaceArg = String
"<namespace>"
show CmdArg
OptionArg = String
"<option>"
show CmdArg
MetaVarArg = String
"<hole>"
show CmdArg
ColourArg = String
"<option>"
show CmdArg
NoArg = String
""
show CmdArg
SpecialHeaderArg = String
"Arguments"
show CmdArg
ConsoleWidthArg = String
"auto|infinite|<number>"
show CmdArg
DeclArg = String
"<top-level declaration>"
show (ManyArgs CmdArg
a) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CmdArg -> String
forall a. Show a => a -> String
show CmdArg
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")..."
show (OptionalArg CmdArg
a) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CmdArg -> String
forall a. Show a => a -> String
show CmdArg
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
show (SeqArgs CmdArg
a CmdArg
b) = CmdArg -> String
forall a. Show a => a -> String
show CmdArg
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CmdArg -> String
forall a. Show a => a -> String
show CmdArg
b
extraHelp ::[([String], CmdArg, String)]
=
[ ([String
":casesplit!", String
":cs!"], CmdArg
NoArg, String
":cs! <line> <name> destructively splits the pattern variable on the line")
, ([String
":addclause!", String
":ac!"], CmdArg
NoArg, String
":ac! <line> <name> destructively adds a clause for the definition of the name on the line")
, ([String
":addmissing!", String
":am!"], CmdArg
NoArg, String
":am! <line> <name> destructively adds all missing pattern matches for the name on the line")
, ([String
":makewith!", String
":mw!"], CmdArg
NoArg, String
":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")
, ([String
":proofsearch!", String
":ps!"], CmdArg
NoArg, String
":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")
, ([String
":addproofclause!", String
":apc!"], CmdArg
NoArg, String
":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")
, ([String
":refine!", String
":ref!"], CmdArg
NoArg, String
":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing holes for arguments that aren't inferrable")
]