2297270 · Idris-dev · git.iko.soy

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

2297270Hannes Mehnert14 years ago

CONTRIBUTORS+2−1

compare with master

unifiedsplit

@@ -3,10 +3,12 @@ Thanks to the following for their help and contributions:

3Ozgur Akgun

4Nicola Botta

5Edwin Brady

6+David Raymond Christiansen

6Jason Dagit

7Jason Dagit

7Cezar Ionescu

8Cezar Ionescu

8Irene Knapp

9Irene Knapp

9Mathnerd314

10Mathnerd314

11+Hannes Mehnert

10Mekeor Melire

12Mekeor Melire

11Melissa Mozifian

13Melissa Mozifian

12Dominic Mulligan

14Dominic Mulligan

@@ -20,4 +22,3 @@ Dirk Ullrich

20Leif Warner

22Leif Warner

21Daniel Waterworth

23Daniel Waterworth

22Jonas Westerlund

24Jonas Westerlund

23−David Raymond Christiansen

idris.cabal+1−1

@@ -77,7 +77,7 @@ Executable idris

77 Core.CaseTree, Core.Constraints,

79 Idris.AbsSyntax, Idris.AbsSyntaxTree,

80− Idris.Parser, Idris.REPL,

80+ Idris.Parser, Idris.Help, Idris.REPL,

81 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

82 Idris.Delaborate, Idris.Primitives, Idris.Imports,

83 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

src/Idris/Completion.hs+14−35

@@ -6,6 +6,7 @@ import Core.TT

6import Core.CoreParser (opChars)

8import Idris.AbsSyntaxTree

9+import Idris.Help

10import Control.Monad.State.Strict

11import Control.Monad.State.Strict

@@ -14,40 +15,11 @@ import Data.Maybe

15import System.Console.Haskeline

16import System.Console.Haskeline

17−-- TODO: add specific classes of identifiers to complete, fx metavariables

18+

18−-- | A specification of the arguments that REPL commands can take

19+fst4 :: (a, b, c, d) -> a

19−data CmdArg = ExprArg -- ^ The command takes an expression

20+fst4 (a, b, c, d) = a

20− | NameArg -- ^ The command takes a name

21+

21− | FileArg -- ^ The command takes a file

22+commands = concatMap fst4 help

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

52-- | A specification of the arguments that tactics can take

24-- | A specification of the arguments that tactics can take

53data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

25data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

@@ -124,15 +96,22 @@ completeOption = completeWord Nothing " \t" completeOpt

124isWhitespace :: Char -> Bool

96isWhitespace :: Char -> Bool

125isWhitespace = (flip elem) " \t\n"

97isWhitespace = (flip elem) " \t\n"

126

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+

127-- | Get the completion function for a particular command

105-- | Get the completion function for a particular command

128completeCmd :: String -> CompletionFunc Idris

106completeCmd :: 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

130 where completeArg FileArg = completeFilename (prev, next)

108 where completeArg FileArg = completeFilename (prev, next)

131 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

109 completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name

132 completeArg OptionArg = completeOption (prev, next)

110 completeArg OptionArg = completeOption (prev, next)

133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

111 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

134 completeArg ExprArg = completeExpr [] (prev, next)

112 completeArg ExprArg = completeExpr [] (prev, next)

135 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

113 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

114+ completeArg NoArg = noCompletion (prev, next)

136 completeCmdName = return $ ("", completeWith commands cmd)

115 completeCmdName = return $ ("", completeWith commands cmd)

137

116

138-- | Complete REPL commands and defined identifiers

117-- | Complete REPL commands and defined identifiers

src/Idris/Help.hsnew file+36

@@ -0,0 +1,36 @@

1+module Idris.Help (CmdArg(..), help) where

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

16import Idris.Coverage

17import Idris.UnusedArgs

18import Idris.Docs

19+import Idris.Help

19import Idris.Completion

20import Idris.Completion

21import Paths_idris

22import Paths_idris

@@ -418,8 +419,9 @@ showTotalN i n = case lookupTotal n (tt_ctxt i) of

418displayHelp = let vstr = showVersion version in

419displayHelp = let vstr = showVersion version in

419 "\nIdris version " ++ vstr ++ "\n" ++

420 "\nIdris version " ++ vstr ++ "\n" ++

420 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

421 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

422+ concatMap cmdInfo helphead ++

421 concatMap cmdInfo help

423 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

423 col c1 c2 l m r =

425 col c1 c2 l m r =

424 l ++ take (c1 - length l) (repeat ' ') ++

426 l ++ take (c1 - length l) (repeat ' ') ++

425 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

427 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

@@ -469,31 +471,9 @@ parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

469parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

471parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

470parseArgs (n:ns) = Filename n : (parseArgs ns)

472parseArgs (n:ns) = Filename n : (parseArgs ns)

471

473

472−help =

474+helphead =

473− [ (["Command"], "Arguments", "Purpose"),

475+ [ (["Command"], "Arguments", "Purpose", ""),

474− ([""], "", ""),

475− (["<expr>"], "", "Evaluate an expression"),

476+ ([""], "", "", "")

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")

497 ]

477 ]

498

478

499

479