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