Permalink
Browse files

unify help and completion of REPL - previously they were not in sync,…

… now it is one lookup table
  • Loading branch information...
1 parent 9841e2a commit 2297270b80d11c86b8a9867295589a90cd49cec8 @hannesm hannesm committed Mar 13, 2013
Showing with 59 additions and 63 deletions.
  1. +2 −1 CONTRIBUTORS
  2. +1 −1 idris.cabal
  3. +14 −35 src/Idris/Completion.hs
  4. +36 −0 src/Idris/Help.hs
  5. +6 −26 src/Idris/REPL.hs
View
@@ -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
View
@@ -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,
View
@@ -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
View
@@ -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)
+ ]
View
@@ -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", ""),
+ ([""], "", "", "")
]

0 comments on commit 2297270

Please sign in to comment.