mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
unify help and completion of REPL - previously they were not in sync, now it is one lookup table
This commit is contained in:
parent
9841e2a841
commit
2297270b80
@ -3,10 +3,12 @@ Thanks to the following for their help and contributions:
|
||||
Ozgur Akgun
|
||||
Nicola Botta
|
||||
Edwin Brady
|
||||
David Raymond Christiansen
|
||||
Jason Dagit
|
||||
Cezar Ionescu
|
||||
Irene Knapp
|
||||
Mathnerd314
|
||||
Hannes Mehnert
|
||||
Mekeor Melire
|
||||
Melissa Mozifian
|
||||
Dominic Mulligan
|
||||
@ -20,4 +22,3 @@ Dirk Ullrich
|
||||
Leif Warner
|
||||
Daniel Waterworth
|
||||
Jonas Westerlund
|
||||
David Raymond Christiansen
|
||||
|
@ -77,7 +77,7 @@ Executable idris
|
||||
Core.CaseTree, Core.Constraints,
|
||||
|
||||
Idris.AbsSyntax, Idris.AbsSyntaxTree,
|
||||
Idris.Parser, Idris.REPL,
|
||||
Idris.Parser, Idris.Help, Idris.REPL,
|
||||
Idris.REPLParser, Idris.ElabDecls, Idris.Error,
|
||||
Idris.Delaborate, Idris.Primitives, Idris.Imports,
|
||||
Idris.Compiler, Idris.Prover, Idris.ElabTerm,
|
||||
|
@ -6,6 +6,7 @@ import Core.TT
|
||||
import Core.CoreParser (opChars)
|
||||
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Help
|
||||
|
||||
import Control.Monad.State.Strict
|
||||
|
||||
@ -14,40 +15,11 @@ import Data.Maybe
|
||||
|
||||
import System.Console.Haskeline
|
||||
|
||||
-- TODO: add specific classes of identifiers to complete, fx metavariables
|
||||
-- | A specification of the arguments that REPL commands can take
|
||||
data CmdArg = ExprArg -- ^ The command takes an expression
|
||||
| NameArg -- ^ The command takes a name
|
||||
| FileArg -- ^ The command takes a file
|
||||
| ModuleArg -- ^ The command takes a module name
|
||||
| OptionArg -- ^ The command takes an option
|
||||
| MetaVarArg -- ^ The command takes a metavariable
|
||||
|
||||
-- | Information about how to complete the various commands
|
||||
cmdArgs :: [(String, CmdArg)]
|
||||
cmdArgs = [ (":t", ExprArg)
|
||||
, (":miss", NameArg)
|
||||
, (":missing", NameArg)
|
||||
, (":i", NameArg)
|
||||
, (":info", NameArg)
|
||||
, (":total", NameArg)
|
||||
, (":l", FileArg)
|
||||
, (":load", FileArg)
|
||||
, (":m", ModuleArg) -- NOTE: Argumentless form is a different command
|
||||
, (":p", MetaVarArg)
|
||||
, (":prove", MetaVarArg)
|
||||
, (":a", NameArg)
|
||||
, (":addproof", NameArg)
|
||||
, (":rmproof", NameArg)
|
||||
, (":showproof", NameArg)
|
||||
, (":c", FileArg)
|
||||
, (":compile", FileArg)
|
||||
, (":js", FileArg)
|
||||
, (":javascript", FileArg)
|
||||
, (":set", OptionArg)
|
||||
, (":unset", OptionArg)
|
||||
]
|
||||
commands = map fst cmdArgs
|
||||
fst4 :: (a, b, c, d) -> a
|
||||
fst4 (a, b, c, d) = a
|
||||
|
||||
commands = concatMap fst4 help
|
||||
|
||||
-- | A specification of the arguments that tactics can take
|
||||
data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
|
||||
@ -124,15 +96,22 @@ completeOption = completeWord Nothing " \t" completeOpt
|
||||
isWhitespace :: Char -> Bool
|
||||
isWhitespace = (flip elem) " \t\n"
|
||||
|
||||
lookupInHelp :: String -> Maybe CmdArg
|
||||
lookupInHelp cmd = lookupInHelp' cmd help
|
||||
where lookupInHelp' cmd ((cmds, _, _, arg):xs) | elem cmd cmds = Just arg
|
||||
| otherwise = lookupInHelp' cmd xs
|
||||
lookupInHelp' cmd [] = Nothing
|
||||
|
||||
-- | Get the completion function for a particular command
|
||||
completeCmd :: String -> CompletionFunc Idris
|
||||
completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
|
||||
completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
|
||||
where completeArg FileArg = completeFilename (prev, next)
|
||||
completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
|
||||
completeArg OptionArg = completeOption (prev, next)
|
||||
completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
|
||||
completeArg ExprArg = completeExpr [] (prev, next)
|
||||
completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
|
||||
completeArg NoArg = noCompletion (prev, next)
|
||||
completeCmdName = return $ ("", completeWith commands cmd)
|
||||
|
||||
-- | Complete REPL commands and defined identifiers
|
||||
|
36
src/Idris/Help.hs
Normal file
36
src/Idris/Help.hs
Normal file
@ -0,0 +1,36 @@
|
||||
module Idris.Help (CmdArg(..), help) where
|
||||
|
||||
data CmdArg = ExprArg -- ^ The command takes an expression
|
||||
| NameArg -- ^ The command takes a name
|
||||
| FileArg -- ^ The command takes a file
|
||||
| ModuleArg -- ^ The command takes a module name
|
||||
| OptionArg -- ^ The command takes an option
|
||||
| MetaVarArg -- ^ The command takes a metavariable
|
||||
| NoArg -- ^ No completion yet
|
||||
|
||||
|
||||
help :: [([String], String, String, CmdArg)]
|
||||
help =
|
||||
[ (["<expr>"], "", "Evaluate an expression", NoArg),
|
||||
([":t"], "<expr>", "Check the type of an expression", ExprArg),
|
||||
([":miss", ":missing"], "<name>", "Show missing clauses", NameArg),
|
||||
([":i", ":info"], "<name>", "Display information about a type class", NameArg),
|
||||
([":total"], "<name>", "Check the totality of a name", NameArg),
|
||||
([":r",":reload"], "", "Reload current file", NoArg),
|
||||
([":l",":load"], "<filename>", "Load a new file", FileArg),
|
||||
([":m",":module"], "<module>", "Import an extra module", ModuleArg), -- NOTE: dragons
|
||||
([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL", NoArg),
|
||||
([":m",":metavars"], "", "Show remaining proof obligations (metavariables)", MetaVarArg),
|
||||
([":p",":prove"], "<name>", "Prove a metavariable", MetaVarArg),
|
||||
([":a",":addproof"], "<name>", "Add proof to source file", NameArg),
|
||||
([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),
|
||||
([":showproof"], "<name>", "Show proof", NameArg),
|
||||
([":proofs"], "", "Show available proofs", NoArg),
|
||||
([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),
|
||||
([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),
|
||||
([":exec",":execute"], "", "Compile to an executable and run", NoArg),
|
||||
([":?",":h",":help"], "", "Display this help text", NoArg),
|
||||
([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),
|
||||
([":unset"], "<option>", "Unset an option", OptionArg),
|
||||
([":q",":quit"], "", "Exit the Idris system", NoArg)
|
||||
]
|
@ -16,6 +16,7 @@ import Idris.Primitives
|
||||
import Idris.Coverage
|
||||
import Idris.UnusedArgs
|
||||
import Idris.Docs
|
||||
import Idris.Help
|
||||
import Idris.Completion
|
||||
|
||||
import Paths_idris
|
||||
@ -418,8 +419,9 @@ showTotalN i n = case lookupTotal n (tt_ctxt i) of
|
||||
displayHelp = let vstr = showVersion version in
|
||||
"\nIdris version " ++ vstr ++ "\n" ++
|
||||
"--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
|
||||
concatMap cmdInfo helphead ++
|
||||
concatMap cmdInfo help
|
||||
where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text
|
||||
where cmdInfo (cmds, args, text, _) = " " ++ col 16 12 (showSep " " cmds) args text
|
||||
col c1 c2 l m r =
|
||||
l ++ take (c1 - length l) (repeat ' ') ++
|
||||
m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
|
||||
@ -469,31 +471,9 @@ parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
|
||||
parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
|
||||
parseArgs (n:ns) = Filename n : (parseArgs ns)
|
||||
|
||||
help =
|
||||
[ (["Command"], "Arguments", "Purpose"),
|
||||
([""], "", ""),
|
||||
(["<expr>"], "", "Evaluate an expression"),
|
||||
([":t"], "<expr>", "Check the type of an expression"),
|
||||
([":miss", ":missing"], "<name>", "Show missing clauses"),
|
||||
([":i", ":info"], "<name>", "Display information about a type class"),
|
||||
([":total"], "<name>", "Check the totality of a name"),
|
||||
([":r",":reload"], "", "Reload current file"),
|
||||
([":l",":load"], "<filename>", "Load a new file"),
|
||||
([":m",":module"], "<module>", "Import an extra module"),
|
||||
([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
|
||||
([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
|
||||
([":p",":prove"], "<name>", "Prove a metavariable"),
|
||||
([":a",":addproof"], "<name>", "Add proof to source file"),
|
||||
([":rmproof"], "<name>", "Remove proof from proof stack"),
|
||||
([":showproof"], "<name>", "Show proof"),
|
||||
([":proofs"], "", "Show available proofs"),
|
||||
([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
|
||||
([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),
|
||||
([":exec",":execute"], "", "Compile to an executable and run"),
|
||||
([":?",":h",":help"], "", "Display this help text"),
|
||||
([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),
|
||||
([":unset"], "<option>", "Unset an option"),
|
||||
([":q",":quit"], "", "Exit the Idris system")
|
||||
helphead =
|
||||
[ (["Command"], "Arguments", "Purpose", ""),
|
||||
([""], "", "", "")
|
||||
]
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user