{-|
Module      : Idris.Help
Description : Utilities to aid with the REPL's HELP system.

License     : BSD3
Maintainer  : The Idris Community.
-}

module Idris.Help (CmdArg(..), extraHelp) where

data CmdArg = ExprArg               -- ^ The command takes an expression
            | NameArg               -- ^ The command takes a name
            | FileArg               -- ^ The command takes a file
            | ShellCommandArg       -- ^ The command takes a shell command name
            | ModuleArg             -- ^ The command takes a module name
            | PkgArgs               -- ^ The command takes a list of package names
            | NumberArg             -- ^ The command takes a number
            | NamespaceArg          -- ^ The command takes a namespace name
            | OptionArg             -- ^ The command takes an option
            | MetaVarArg            -- ^ The command takes a metavariable
            | ColourArg             -- ^ The command is the colour-setting command
            | NoArg                 -- ^ No completion (yet!?)
            | SpecialHeaderArg      -- ^ do not use
            | ConsoleWidthArg       -- ^ The width of the console
            | DeclArg               -- ^ An Idris declaration, as might be contained in a file
            | ManyArgs CmdArg       -- ^ Zero or more of one kind of argument
            | OptionalArg CmdArg    -- ^ Zero or one of one kind of argument
            | SeqArgs CmdArg CmdArg -- ^ One kind of argument followed by another

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

-- | Use these for completion, but don't show them in :help
extraHelp ::[([String], CmdArg, String)]
extraHelp :: [([String], CmdArg, String)]
extraHelp =
    [ ([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")
    ]