git.iko.soy/Idris-dev
on master help sign in
unify help and completion of REPL - previously they were not in sync, now it is one lookup table
commit2297270b80d11c86b8a9867295589a90cd49cec8 authorHannes Mehnert <hannes@mehnert.org> dateWed 13 Mar 2013, 15:24 (14 years ago) parent9841e2a
5 files changed+59−63
compare with master
unifiedsplit
CONTRIBUTORS+2−1 idris.cabal+1−1 src/Idris/Completion.hs+14−35 src/Idris/Help.hs+36 src/Idris/REPL.hs+6−26
CONTRIBUTORS+2−1
@@ -3,10 +3,12 @@ Thanks to the following for their help and contributions:
33Ozgur Akgun
44Nicola Botta
55Edwin Brady
6+David Raymond Christiansen
67Jason Dagit
78Cezar Ionescu
89Irene Knapp
910Mathnerd314
11+Hannes Mehnert
1012Mekeor Melire
1113Melissa Mozifian
1214Dominic Mulligan
@@ -20,4 +22,3 @@ Dirk Ullrich
2022Leif Warner
2123Daniel Waterworth
2224Jonas Westerlund
23−David Raymond Christiansen
idris.cabal+1−1
@@ -77,7 +77,7 @@ Executable idris
7777 Core.CaseTree, Core.Constraints,
7878
7979 Idris.AbsSyntax, Idris.AbsSyntaxTree,
80− Idris.Parser, Idris.REPL,
80+ Idris.Parser, Idris.Help, Idris.REPL,
8181 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
8282 Idris.Delaborate, Idris.Primitives, Idris.Imports,
8383 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
src/Idris/Completion.hs+14−35
@@ -6,6 +6,7 @@ import Core.TT
66import Core.CoreParser (opChars)
77
88import Idris.AbsSyntaxTree
9+import Idris.Help
910
1011import Control.Monad.State.Strict
1112
@@ -14,40 +15,11 @@ import Data.Maybe
1415
1516import System.Console.Haskeline
1617
17−-- TODO: add specific classes of identifiers to complete, fx metavariables
18−-- | A specification of the arguments that REPL commands can take
19−data CmdArg = ExprArg -- ^ The command takes an expression
20− | NameArg -- ^ The command takes a name
21− | FileArg -- ^ The command takes a file
22− | ModuleArg -- ^ The command takes a module name
23− | OptionArg -- ^ The command takes an option
24− | MetaVarArg -- ^ The command takes a metavariable
25−
26−-- | Information about how to complete the various commands
27−cmdArgs :: [(String, CmdArg)]
28−cmdArgs = [ (":t", ExprArg)
29− , (":miss", NameArg)
30− , (":missing", NameArg)
31− , (":i", NameArg)
32− , (":info", NameArg)
33− , (":total", NameArg)
34− , (":l", FileArg)
35− , (":load", FileArg)
36− , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
37− , (":p", MetaVarArg)
38− , (":prove", MetaVarArg)
39− , (":a", NameArg)
40− , (":addproof", NameArg)
41− , (":rmproof", NameArg)
42− , (":showproof", NameArg)
43− , (":c", FileArg)
44− , (":compile", FileArg)
45− , (":js", FileArg)
46− , (":javascript", FileArg)
47− , (":set", OptionArg)
48− , (":unset", OptionArg)
49− ]
50−commands = map fst cmdArgs
18+
19+fst4 :: (a, b, c, d) -> a
20+fst4 (a, b, c, d) = a
21+
22+commands = concatMap fst4 help
5123
5224-- | A specification of the arguments that tactics can take
5325data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
@@ -124,15 +96,22 @@ completeOption = completeWord Nothing " \t" completeOpt
12496isWhitespace :: Char -> Bool
12597isWhitespace = (flip elem) " \t\n"
12698
99+lookupInHelp :: String -> Maybe CmdArg
100+lookupInHelp cmd = lookupInHelp' cmd help
101+ where lookupInHelp' cmd ((cmds, _, _, arg):xs) | elem cmd cmds = Just arg
102+ | otherwise = lookupInHelp' cmd xs
103+ lookupInHelp' cmd [] = Nothing
104+
127105-- | Get the completion function for a particular command
128106completeCmd :: String -> CompletionFunc Idris
129−completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
107+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
130108 where completeArg FileArg = completeFilename (prev, next)
131109 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
132110 completeArg OptionArg = completeOption (prev, next)
133111 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
134112 completeArg ExprArg = completeExpr [] (prev, next)
135113 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
114+ completeArg NoArg = noCompletion (prev, next)
136115 completeCmdName = return $ ("", completeWith commands cmd)
137116
138117-- | Complete REPL commands and defined identifiers
src/Idris/Help.hsnew file+36
@@ -0,0 +1,36 @@
1+module Idris.Help (CmdArg(..), help) where
2+
3+data 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+ | OptionArg -- ^ The command takes an option
8+ | MetaVarArg -- ^ The command takes a metavariable
9+ | NoArg -- ^ No completion yet
10+
11+
12+help :: [([String], String, String, CmdArg)]
13+help =
14+ [ (["<expr>"], "", "Evaluate an expression", NoArg),
15+ ([":t"], "<expr>", "Check the type of an expression", ExprArg),
16+ ([":miss", ":missing"], "<name>", "Show missing clauses", NameArg),
17+ ([":i", ":info"], "<name>", "Display information about a type class", NameArg),
18+ ([":total"], "<name>", "Check the totality of a name", NameArg),
19+ ([":r",":reload"], "", "Reload current file", NoArg),
20+ ([":l",":load"], "<filename>", "Load a new file", FileArg),
21+ ([":m",":module"], "<module>", "Import an extra module", ModuleArg), -- NOTE: dragons
22+ ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL", NoArg),
23+ ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)", MetaVarArg),
24+ ([":p",":prove"], "<name>", "Prove a metavariable", MetaVarArg),
25+ ([":a",":addproof"], "<name>", "Add proof to source file", NameArg),
26+ ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),
27+ ([":showproof"], "<name>", "Show proof", NameArg),
28+ ([":proofs"], "", "Show available proofs", NoArg),
29+ ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),
30+ ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),
31+ ([":exec",":execute"], "", "Compile to an executable and run", NoArg),
32+ ([":?",":h",":help"], "", "Display this help text", NoArg),
33+ ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),
34+ ([":unset"], "<option>", "Unset an option", OptionArg),
35+ ([":q",":quit"], "", "Exit the Idris system", NoArg)
36+ ]
src/Idris/REPL.hs+6−26
@@ -16,6 +16,7 @@ import Idris.Primitives
1616import Idris.Coverage
1717import Idris.UnusedArgs
1818import Idris.Docs
19+import Idris.Help
1920import Idris.Completion
2021
2122import Paths_idris
@@ -418,8 +419,9 @@ showTotalN i n = case lookupTotal n (tt_ctxt i) of
418419displayHelp = let vstr = showVersion version in
419420 "\nIdris version " ++ vstr ++ "\n" ++
420421 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
422+ concatMap cmdInfo helphead ++
421423 concatMap cmdInfo help
422− where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text
424+ where cmdInfo (cmds, args, text, _) = " " ++ col 16 12 (showSep " " cmds) args text
423425 col c1 c2 l m r =
424426 l ++ take (c1 - length l) (repeat ' ') ++
425427 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
@@ -469,31 +471,9 @@ parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)
469471parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)
470472parseArgs (n:ns) = Filename n : (parseArgs ns)
471473
472−help =
473− [ (["Command"], "Arguments", "Purpose"),
474− ([""], "", ""),
475− (["<expr>"], "", "Evaluate an expression"),
476− ([":t"], "<expr>", "Check the type of an expression"),
477− ([":miss", ":missing"], "<name>", "Show missing clauses"),
478− ([":i", ":info"], "<name>", "Display information about a type class"),
479− ([":total"], "<name>", "Check the totality of a name"),
480− ([":r",":reload"], "", "Reload current file"),
481− ([":l",":load"], "<filename>", "Load a new file"),
482− ([":m",":module"], "<module>", "Import an extra module"),
483− ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
484− ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
485− ([":p",":prove"], "<name>", "Prove a metavariable"),
486− ([":a",":addproof"], "<name>", "Add proof to source file"),
487− ([":rmproof"], "<name>", "Remove proof from proof stack"),
488− ([":showproof"], "<name>", "Show proof"),
489− ([":proofs"], "", "Show available proofs"),
490− ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
491− ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),
492− ([":exec",":execute"], "", "Compile to an executable and run"),
493− ([":?",":h",":help"], "", "Display this help text"),
494− ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),
495− ([":unset"], "<option>", "Unset an option"),
496− ([":q",":quit"], "", "Exit the Idris system")
474+helphead =
475+ [ (["Command"], "Arguments", "Purpose", ""),
476+ ([""], "", "", "")
497477 ]
498478
499479