99be9f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Various cleanup of the REPL, mainly with parsing and completion

99be9f0Ben Sherman12 years ago

src/Idris/Completion.hs+3−5

compare with master

unifiedsplit

@@ -10,6 +10,7 @@ import Idris.Colours

10import Idris.ParseHelpers(opChars)

11import qualified Idris.ParseExpr (constants, tactics)

12import Idris.ParseExpr (TacticArg (..))

13+import Idris.REPLParser (allHelp)

13import Control.Monad.State.Strict

14import Control.Monad.State.Strict

15import Data.List

16import Data.List

@@ -20,10 +21,7 @@ import System.Console.Haskeline

20import System.Console.ANSI (Color)

21import System.Console.ANSI (Color)

23−fst3 :: (a, b, c) -> a

24−fst3 (a, b, c) = a

25−

26−commands = concatMap fst3 (help ++ extraHelp)

24+commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

28tacticArgs :: [(String, Maybe TacticArg)]

26tacticArgs :: [(String, Maybe TacticArg)]

29tacticArgs = [ (name, args) | (names, args, _) <- Idris.ParseExpr.tactics

27tacticArgs = [ (name, args) | (names, args, _) <- Idris.ParseExpr.tactics

@@ -97,7 +95,7 @@ isWhitespace :: Char -> Bool

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

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

99lookupInHelp :: String -> Maybe CmdArg

97lookupInHelp :: String -> Maybe CmdArg

100−lookupInHelp cmd = lookupInHelp' cmd help

98+lookupInHelp cmd = lookupInHelp' cmd allHelp

101 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg

99 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg

102 | otherwise = lookupInHelp' cmd xs

100 | otherwise = lookupInHelp' cmd xs

103 lookupInHelp' cmd [] = Nothing

101 lookupInHelp' cmd [] = Nothing

src/Idris/Help.hs+2−65

@@ -1,4 +1,4 @@

1−module Idris.Help (CmdArg(..), help, extraHelp) where

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

3data CmdArg = ExprArg -- ^ The command takes an expression

4 | NameArg -- ^ The command takes a name

@@ -37,77 +37,14 @@ instance Show CmdArg where

37 show (OptionalArg a) = "[" ++ show a ++ "]"

38 show (SeqArgs a b) = show a ++ " " ++ show b

40−help :: [([String], CmdArg, String)]

41−help =

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

43− ([":t"], ExprArg, "Check the type of an expression"),

44− ([":miss", ":missing"], NameArg, "Show missing clauses"),

45− ([":doc"], NameArg, "Show internal documentation"),

46− ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),

47− ([":apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"),

48− ([":search", ":s"], SeqArgs (OptionalArg PkgArgs) ExprArg, " Search for values by type"),

49− ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

50− ([":callswho", ":cw"], NameArg, "List the callees of some name"),

51− ([":total"], NameArg, "Check the totality of a name"),

52− ([":r",":reload"], NoArg, "Reload current file"),

53− ([":l",":load"], FileArg, "Load a new file"),

54− ([":cd"], FileArg, "Change working directory"),

55− ([":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons

56− ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),

57− ([":m",":metavars"], NoArg, "Show remaining proof obligations (metavariables)"),

58− ([":p",":prove"], MetaVarArg, "Prove a metavariable"),

59− ([":a",":addproof"], NameArg, "Add proof to source file"),

60− ([":rmproof"], NameArg, "Remove proof from proof stack"),

61− ([":showproof"], NameArg, "Show proof"),

62− ([":proofs"], NoArg, "Show available proofs"),

63− ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),

64− ([":c",":compile"], FileArg, "Compile to an executable [codegen] <filename>"),

65− ([":exec",":execute"], NoArg, "Compile to an executable and run"),

66− ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),

67− ([":dynamic"], NoArg, "List dynamically loaded C libraries"),

68− ([":?",":h",":help"], NoArg, "Display this help text"),

69− ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

70− ([":unset"], OptionArg, "Unset an option"),

71− ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

72− ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

73− ([":q",":quit"], NoArg, "Exit the Idris system"),

74− ([":w", ":warranty"], NoArg, "Displays warranty information"),

75− ([":let"], ManyArgs DeclArg, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"),

76− ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given"),

77− ([":printdef"], NameArg, "Show the definition of a function"),

78− ([":pp", ":pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg)), "Pretty prints an Idris function in either LaTeX or HTML and for a specified width.")

79− ]

80−

81-- | Use these for completion, but don't show them in :help

40-- | Use these for completion, but don't show them in :help

82extraHelp ::[([String], CmdArg, String)]

41extraHelp ::[([String], CmdArg, String)]

83extraHelp =

42extraHelp =

84− [ ([":casesplit", ":cs"], NoArg, ":cs <line> <name> splits the pattern variable on the line")

85− , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")

43+ [ ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")

86− , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")

87 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")

44 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")

88− , ([":addmissing", ":am"], NoArg, ":am <line> <name> adds all missing pattern matches for the name on the line")

89 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")

45 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")

90− , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")

91 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

46 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

92− , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")

93 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

47 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

94− , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")

95 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

48 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

96− , ([":refine", ":ref"], NoArg, ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

97 , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

49 , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

98−

99− , ([":u", ":universes"], NoArg, "Display universe constraints")

100− , ([":errorhandlers"], NoArg, "List registered error handlers")

101− , ([":d", ":def"], NameArg, "Display a name's internal definitions")

102− , ([":transinfo"], NameArg, "Show relevant transformation rules for a name")

103− , ([":di", ":dbginfo"], NameArg, "Show debugging information for a name")

104− , ([":spec"], ExprArg, "?")

105− , ([":hnf"], ExprArg, "?")

106− , ([":inline"], ExprArg, "?")

107−

108− , ([":ml", ":makelemma"], NoArg, "?")

109−

110− , ([":log"], NumberArg, "Set logging verbosity level")

111− , ([":lto", ":loadto"], SeqArgs NumberArg FileArg, "Load file up to line number")

112− , ([":debugunify"], SeqArgs ExprArg ExprArg, "(Debugging) Try to unify two expressions")

113 ]

50 ]

src/Idris/Parser.hs+3−3

@@ -1198,13 +1198,13 @@ parseProg syn fname input mrk

1198 return (ds, i')

1199

1200{- | Load idris module and show error if something wrong happens -}

1201−loadModule :: FilePath -> Idris String

1201+loadModule :: FilePath -> Idris (Maybe String)

1202loadModule f

1203− = idrisCatch (loadModule' f)

1203+ = idrisCatch (fmap Just (loadModule' f))

1204 (\e -> do setErrSpan (getErrSpan e)

1205 ist <- getIState

1206 iWarn (getErrSpan e) $ pprintErr ist e

1207− return "")

1207+ return Nothing)

1208

1209{- | Load idris module -}

1210loadModule' :: FilePath -> Idris String

src/Idris/REPL.hs+2−2

@@ -14,13 +14,13 @@ import Idris.Error

14import Idris.ErrReverse

15import Idris.Delaborate

16import Idris.Docstrings (Docstring, overview, renderDocstring)

17+import Idris.Help

17import Idris.IdrisDoc

18import Idris.IdrisDoc

18import Idris.Prover

19import Idris.Prover

19import Idris.Parser hiding (indent)

20import Idris.Parser hiding (indent)

20import Idris.Primitives

21import Idris.Primitives

21import Idris.Coverage

22import Idris.Coverage

22import Idris.Docs hiding (Doc)

23import Idris.Docs hiding (Doc)

23−import Idris.Help

24import Idris.Completion

25import qualified Idris.IdeSlave as IdeSlave

26import Idris.Chaser

@@ -633,7 +633,7 @@ processInput cmd orig inputs

633 Success (Right (ModImport f)) ->

634 do clearErr

635 fmod <- loadModule f

636− return (Just (inputs ++ [fmod]))

636+ return (Just (inputs ++ maybe [] (:[]) fmod))

637 Success (Right Edit) -> do -- takeMVar stvar

638 edit fn orig

639 return (Just inputs)

src/Idris/REPLParser.hs+180−153

@@ -1,5 +1,5 @@

2−module Idris.REPLParser(parseCmd) where

2+module Idris.REPLParser (parseCmd, help, allHelp) where

4import System.FilePath ((</>))

5import System.Console.ANSI (Color(..))

@@ -7,6 +7,7 @@ import System.Console.ANSI (Color(..))

7import Idris.Colours

8import Idris.AbsSyntax

9import Idris.Core.TT

10+import Idris.Help

10import qualified Idris.Parser as P

11import qualified Idris.Parser as P

12import Control.Applicative

13import Control.Applicative

@@ -26,82 +27,135 @@ import qualified Data.ByteString.UTF8 as UTF8

26parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace

28parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace

30+type CommandTable = [ ( [String], CmdArg, String

31+ , String -> P.IdrisParser (Either String Command) ) ]

32+

33+help :: [([String], CmdArg, String)]

34+help = (["<expr>"], NoArg, "Evaluate an expression") :

35+ [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

36+

37+allHelp :: [([String], CmdArg, String)]

38+allHelp = [ (map (':' :) names, args, text)

39+ | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]

40+

41+parserCommandsForHelp :: CommandTable

42+parserCommandsForHelp =

43+ [ exprArgCmd ["t", "type"] Check "Check the type of an expression"

44+ , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

45+ , (["doc"], NameArg, "Show internal documentation", cmd_doc)

46+ , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

47+ , genArg "namespace" (many anyChar) MakeDoc)

48+ , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

49+ , cmd_apropos)

50+ , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

51+ , " Search for values by type", cmd_search)

52+ , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"

53+ , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"

54+ , nameArgCmd ["total"] TotCheck "Check the totality of a name"

55+ , noArgCmd ["r", "reload"] Reload "Reload current file"

56+ , (["l", "load"], FileArg, "Load a new file"

57+ , strArg (\f -> Load f Nothing))

58+ , (["cd"], FileArg, "Change working directory"

59+ , strArg ChangeDirectory)

60+ , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons

61+ , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"

62+ , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables)"

63+ , (["p", "prove"], MetaVarArg, "Prove a metavariable"

64+ , nameArg Prove)

65+ , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)

66+ , (["rmproof"], NameArg, "Remove proof from proof stack"

67+ , nameArg RmProof)

68+ , (["showproof"], NameArg, "Show proof"

69+ , nameArg ShowProof)

70+ , noArgCmd ["proofs"] Proofs "Show available proofs"

71+ , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"

72+ , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)

73+ , noArgCmd ["exec", "execute"] Execute "Compile to an executable and run"

74+ , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

75+ , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

76+ , noArgCmd ["?", "h", "help"] Help "Display this help text"

77+ , optArgCmd ["set"] SetOpt "Set an option (errorcontext, showimplicits)"

78+ , optArgCmd ["unset"] UnsetOpt "Unset an option"

79+ , (["color", "colour"], ColourArg

80+ , "Turn REPL colours on or off; set a specific colour"

81+ , cmd_colour)

82+ , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)

83+ , noArgCmd ["q", "quit"] Quit "Exit the Idris system"

84+ , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"

85+ , (["let"], ManyArgs DeclArg

86+ , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"

87+ , cmd_let)

88+ , (["unlet", "undefine"], ManyArgs NameArg

89+ , "Remove the listed repl definitions, or all repl definitions if no names given"

90+ , cmd_unlet)

91+ , nameArgCmd ["printdef"] PrintDef "Show the definition of a function"

92+ , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg))

93+ , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

94+ , cmd_pprint)

95+ ]

96+

97+parserCommands =

98+ [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

99+ , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"

100+

101+ , nameArgCmd ["d", "def"] Defn "Display a name's internal definitions"

102+ , nameArgCmd ["transinfo"] TransformInfo "Show relevant transformation rules for a name"

103+ , nameArgCmd ["di", "dbginfo"] DebugInfo "Show debugging information for a name"

104+

105+ , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression"

106+ , exprArgCmd ["spec"] Spec "?"

107+ , exprArgCmd ["hnf"] HNF "?"

108+ , exprArgCmd ["inline"] TestInline "?"

109+ , proofArgCmd ["cs", "casesplit"] CaseSplitAt

110+ ":cs <line> <name> splits the pattern variable on the line"

111+ , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom

112+ ":apc <line> <name> adds a pattern-matching proof clause to name on line"

113+ , proofArgCmd ["ac", "addclause"] AddClauseFrom

114+ ":ac <line> <name> adds a clause for the definition of the name on the line"

115+ , proofArgCmd ["am", "addmissing"] AddMissing

116+ ":am <line> <name> adds all missing pattern matches for the name on the line"

117+ , proofArgCmd ["mw", "makewith"] MakeWith

118+ ":mw <line> <name> adds a with clause for the definition of the name on the line"

119+ , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

120+ , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

121+ , (["lto", "loadto"], SeqArgs NumberArg FileArg

122+ , "Load file up to line number", cmd_loadto)

123+ , (["ps", "proofsearch"], NoArg

124+ , ":ps <line> <name> <names> does proof search for name on line, with names as hints"

125+ , cmd_proofsearch)

126+ , (["ref", "refine"], NoArg

127+ , ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"

128+ , cmd_refine)

129+ , (["debugunify"], SeqArgs ExprArg ExprArg

130+ , "(Debugging) Try to unify two expressions", const $ do

131+ l <- P.simpleExpr defaultSyntax

132+ r <- P.simpleExpr defaultSyntax

133+ eof

134+ return (Right (DebugUnify l r))

135+ )

136+ ]

137+

138+noArgCmd names command doc =

139+ (names, NoArg, doc, noArgs command)

140+nameArgCmd names command doc =

141+ (names, NameArg, doc, fnNameArg command)

142+exprArgCmd names command doc =

143+ (names, ExprArg, doc, exprArg command)

144+metavarArgCmd names command doc =

145+ (names, MetaVarArg, doc, fnNameArg command)

146+optArgCmd names command doc =

147+ (names, OptionArg, doc, optArg command)

148+proofArgCmd names command doc =

149+ (names, NoArg, doc, proofArg command)

150+

29pCmd :: P.IdrisParser (Either String Command)

151pCmd :: P.IdrisParser (Either String Command)

30−pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit

152+pCmd = choice [ do c <- cmd names; parser c

31− , do c <- cmd ["h", "?", "help"]; noArgs c Help

153+ | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

32− , do c <- cmd ["w", "warranty"]; noArgs c Warranty

33− , do c <- cmd ["r", "reload"]; noArgs c Reload

34− , do c <- cmd ["exec", "execute"]; noArgs c Execute

35− , do c <- cmd ["proofs"]; noArgs c Proofs

36− , do c <- cmd ["u", "universes"]; noArgs c Universes

37− , do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers

38− , do c <- cmd ["m", "metavars"]; noArgs c Metavars

39− , do c <- cmd ["e", "edit"]; noArgs c Edit

40−

41− , do c <- cmd ["d", "def"]; fnNameArg c Defn

42− , do c <- cmd ["total"]; fnNameArg c TotCheck

43− , do c <- cmd ["printdef"]; fnNameArg c PrintDef

44− , do c <- cmd ["transinfo"]; fnNameArg c TransformInfo

45− , do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls

46− , do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho

47− , do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo

48− , do c <- cmd ["miss", "missing"]; fnNameArg c Missing

49−

50− , do c <- cmd ["t", "type"]; exprArg c Check

51− , do c <- cmd ["x"]; exprArg c ExecVal

52− , do c <- cmd ["patt"]; exprArg c Pattelab

53− , do c <- cmd ["spec"]; exprArg c Spec

54− , do c <- cmd ["hnf"]; exprArg c HNF

55− , do c <- cmd ["inline"]; exprArg c TestInline

56−

57− , do c <- cmd ["rmproof"]; nameArg c RmProof

58− , do c <- cmd ["showproof"]; nameArg c ShowProof

59− , do c <- cmd ["p", "prove"]; nameArg c Prove

60−

61− , do c <- cmd ["set"]; optArg c SetOpt

62− , do c <- cmd ["unset"]; optArg c UnsetOpt

63−

64− , do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)

65− , do c <- cmd ["cd"]; strArg c ChangeDirectory

66− , do c <- cmd ["apropos"]; cmd_apropos c

67− , do c <- cmd ["mkdoc"]; strArg c MakeDoc

68−

69− , do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt

70− , do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom

71− , do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom

72− , do c <- cmd ["am", "addmissing"]; proofArg c AddMissing

73− , do c <- cmd ["mw", "makewith"]; proofArg c MakeWith

74− , do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma

75−

76− , do c <- cmd ["pp", "pprint"]; cmd_pprint c

77− , do c <- cmd ["doc"]; cmd_doc c

78− , do c <- cmd ["dynamic"]; cmd_dynamic c

79− , do c <- cmd ["consolewidth"]; cmd_consolewidth c

80− , do c <- cmd ["module"]; cmd_module c

81− , do c <- cmd ["c", "compile"]; cmd_compile c

82− , do c <- cmd ["a", "addproof"]; cmd_addproof c

83− , do c <- cmd ["log"]; cmd_log c

84− , do c <- cmd ["let"]; cmd_let c

85− , do c <- cmd ["unlet","undefine"]; cmd_unlet c

86− , do c <- cmd ["lto", "loadto"]; cmd_loadto c

87− , do c <- cmd ["color", "colour"]; cmd_colour c

88− , do c <- cmd ["s", "search"]; cmd_search c

89− , do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c

90− , do c <- cmd ["ref", "refine"]; cmd_refine c

91−

92− , do c <- cmd ["debugunify"];

93− P.whiteSpace

94− l <- P.simpleExpr defaultSyntax

95− r <- P.simpleExpr defaultSyntax

96− eof

97− return (Right (DebugUnify l r))

98−

99− , unrecognized

154+ <|> unrecognized

100− , nop

155+ <|> nop

101− ]

102− <|> eval

156+ <|> eval

103− where nop = do P.whiteSpace; eof; return (Right NOP)

157+ where nop = do eof; return (Right NOP)

104− eval = exprArg "" Eval

158+ eval = exprArg Eval ""

105 unrecognized = do

159 unrecognized = do

106 P.lchar ':'

160 P.lchar ':'

107 cmd <- many anyChar

161 cmd <- many anyChar

@@ -119,20 +173,18 @@ cmd xs = try $ do

119 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

173 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

120

174

121

175

122−noArgs :: String -> Command -> P.IdrisParser (Either String Command)

176+noArgs :: Command -> String -> P.IdrisParser (Either String Command)

123−noArgs name cmd = do

177+noArgs cmd name = do

124 let emptyArgs = do

178 let emptyArgs = do

125− P.whiteSpace

126 eof

179 eof

127 return (Right cmd)

180 return (Right cmd)

128

181

129 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

182 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

130

183

131− try emptyArgs <|> failure

184+ emptyArgs <|> failure

132

185

133−exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)

186+exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

134−exprArg name cmd = do

187+exprArg cmd name = do

135− P.whiteSpace

136 let noArg = do

188 let noArg = do

137 eof

189 eof

138 return $ Left ("Usage is :" ++ name ++ " <expression>")

190 return $ Left ("Usage is :" ++ name ++ " <expression>")

@@ -143,51 +195,45 @@ exprArg name cmd = do

143 try noArg <|> properArg

195 try noArg <|> properArg

144

196

145

197

198+

146−fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)

199+genArg :: String -> P.IdrisParser a -> (a -> Command)

147−fnNameArg name cmd = do

148− P.whiteSpace

149− let emptyArgs = do eof

150− return $ Left ("Usage is :" ++ name ++ " <functionname>")

151− oneArg = do n <- P.fnName

152− eof

153− return (Right (cmd n))

154− badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")

155− try emptyArgs <|> try oneArg <|> badArg

156−

157−nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)

200+ -> String -> P.IdrisParser (Either String Command)

158−nameArg name cmd = do

201+genArg argName argParser cmd name = do

159− P.whiteSpace

160− let emptyArgs = do eof

202+ let emptyArgs = do eof; failure

161− return $ Left ("Usage is :" ++ name ++ " <functionname>")

162− oneArg = do n <- P.name

203+ oneArg = do arg <- argParser

163 eof

204 eof

164− return (Right (cmd n))

205+ return (Right (cmd arg))

206+ try emptyArgs <|> oneArg <|> failure

207+ where

165− badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")

208+ failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

166− try emptyArgs <|> try oneArg <|> badArg

167

209

168−strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)

210+nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

169−strArg name cmd = do

211+nameArg = genArg "name" P.name

170− n <- many anyChar

212+fnNameArg = genArg "functionname" P.fnName

171− eof

172− return (Right (cmd n))

173

213

214+strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

215+strArg = genArg "string" (many anyChar)

216+

217+moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

218+moduleArg = genArg "module" (fmap toPath P.identifier)

219+ where

220+ toPath n = foldl1' (</>) $ splitOn "." n

221+

174−optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)

222+optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

175−optArg name cmd = do

223+optArg cmd name = do

176 let emptyArgs = do

224 let emptyArgs = do

177 eof

225 eof

178 return $ Left ("Usage is :" ++ name ++ " <option>")

226 return $ Left ("Usage is :" ++ name ++ " <option>")

179

227

180 let oneArg = do

228 let oneArg = do

181− P.whiteSpace

182 o <- pOption

229 o <- pOption

183 P.whiteSpace

230 P.whiteSpace

184 eof

231 eof

185 return (Right (cmd o))

232 return (Right (cmd o))

186

233

187− let failure = do

188− return $ Left "Unrecognized setting"

234+ let failure = return $ Left "Unrecognized setting"

189

235

190− try emptyArgs <|> try oneArg <|> failure

236+ try emptyArgs <|> oneArg <|> failure

191

237

192 where

238 where

193 pOption :: P.IdrisParser Opt

239 pOption :: P.IdrisParser Opt

@@ -198,9 +244,8 @@ optArg name cmd = do

198 <|> do discard (P.symbol "nobanner") ; return NoBanner

244 <|> do discard (P.symbol "nobanner") ; return NoBanner

199 <|> do discard (P.symbol "warnreach"); return WarnReach

245 <|> do discard (P.symbol "warnreach"); return WarnReach

200

246

201−proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)

247+proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

202−proofArg name cmd = do

248+proofArg cmd name = do

203− P.whiteSpace

204 upd <- option False $ do

249 upd <- option False $ do

205 P.lchar '!'

250 P.lchar '!'

206 return True

251 return True

@@ -215,7 +260,7 @@ cmd_doc name = do

215 eof

260 eof

216 return $ Right (DocStr (Right c))

261 return $ Right (DocStr (Right c))

217

262

218− let fnName = fnNameArg name (\n -> DocStr (Left n))

263+ let fnName = fnNameArg (\n -> DocStr (Left n)) name

219

264

220 try constant <|> fnName

265 try constant <|> fnName

221

266

@@ -232,7 +277,7 @@ cmd_consolewidth name = do

232

277

233cmd_dynamic :: String -> P.IdrisParser (Either String Command)

278cmd_dynamic :: String -> P.IdrisParser (Either String Command)

234cmd_dynamic name = do

279cmd_dynamic name = do

235− let emptyArgs = noArgs name ListDynamic

280+ let emptyArgs = noArgs ListDynamic name

236

281

237 let oneArg = do l <- many anyChar

282 let oneArg = do l <- many anyChar

238 return $ Right (DynamicLink l)

283 return $ Right (DynamicLink l)

@@ -243,7 +288,6 @@ cmd_dynamic name = do

243

288

244cmd_pprint :: String -> P.IdrisParser (Either String Command)

289cmd_pprint :: String -> P.IdrisParser (Either String Command)

245cmd_pprint name = do

290cmd_pprint name = do

246− P.whiteSpace

247 fmt <- ppFormat

291 fmt <- ppFormat

248 P.whiteSpace

292 P.whiteSpace

249 n <- fmap fromInteger P.natural

293 n <- fmap fromInteger P.natural

@@ -257,13 +301,6 @@ cmd_pprint name = do

257 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

301 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

258

302

259

303

260−cmd_module :: String -> P.IdrisParser (Either String Command)

261−cmd_module name = do

262− f <- P.identifier

263− eof;

264− return (Right (ModImport (toPath f)))

265− where

266− toPath n = foldl1' (</>) $ splitOn "." n

267

304

268cmd_compile :: String -> P.IdrisParser (Either String Command)

305cmd_compile :: String -> P.IdrisParser (Either String Command)

269cmd_compile name = do

306cmd_compile name = do

@@ -312,8 +349,7 @@ cmd_let name = do

312 return (Right (NewDefn defn))

349 return (Right (NewDefn defn))

313

350

314cmd_unlet :: String -> P.IdrisParser (Either String Command)

351cmd_unlet :: String -> P.IdrisParser (Either String Command)

315−cmd_unlet name = do

316− (Right . Undefine) `fmap` many P.name

352+cmd_unlet name = (Right . Undefine) `fmap` many P.name

317

353

318cmd_loadto :: String -> P.IdrisParser (Either String Command)

354cmd_loadto :: String -> P.IdrisParser (Either String Command)

319cmd_loadto name = do

355cmd_loadto name = do

@@ -322,8 +358,7 @@ cmd_loadto name = do

322 return (Right (Load f (Just (fromInteger toline))))

358 return (Right (Load f (Just (fromInteger toline))))

323

359

324cmd_colour :: String -> P.IdrisParser (Either String Command)

360cmd_colour :: String -> P.IdrisParser (Either String Command)

325−cmd_colour name = do

361+cmd_colour name = fmap Right pSetColourCmd

326− pSetColourCmd >>= return . Right

327

362

328 where

363 where

329 colours :: [(String, Maybe Color)]

364 colours :: [(String, Maybe Color)]

@@ -386,32 +421,25 @@ cmd_colour name = do

386idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

421idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

387

422

388cmd_apropos :: String -> P.IdrisParser (Either String Command)

423cmd_apropos :: String -> P.IdrisParser (Either String Command)

389−cmd_apropos name =

424+cmd_apropos = packageBasedCmd (some idChar) Apropos

390− try (do P.whiteSpace

425+

426+packageBasedCmd :: P.IdrisParser a -> ([String] -> a -> Command)

427+ -> String -> P.IdrisParser (Either String Command)

428+packageBasedCmd valParser cmd name = do

429+ pkgs <- option [] . try $ do

391− P.lchar '('

430+ P.lchar '('

392− pkgs <- sepBy (some idChar) (P.lchar ',')

431+ pks <- sepBy (some idChar) (P.lchar ',')

393− P.lchar ')'

432+ P.lchar ')'

394− nm <- some idChar

433+ return pks

395− return (Right (Apropos pkgs nm)))

434+ val <- valParser

396− <|> do P.whiteSpace;

397− nm <- some idChar

398− return (Right (Apropos [] nm))

435+ return (Right (cmd pkgs val))

399

436

400cmd_search :: String -> P.IdrisParser (Either String Command)

437cmd_search :: String -> P.IdrisParser (Either String Command)

401−cmd_search name =

438+cmd_search = packageBasedCmd

402− try (do P.whiteSpace

403− P.lchar '('

404− pkgs <- sepBy (some idChar) (P.lchar ',')

405− P.lchar ')'

406− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

439+ (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search

407− return (Right (Search pkgs t)))

408− <|> do P.whiteSpace;

409− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

410− return (Right (Search [] t))

411

440

412cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

441cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

413cmd_proofsearch name = do

442cmd_proofsearch name = do

414− P.whiteSpace

415 upd <- option False (do P.lchar '!'; return True)

443 upd <- option False (do P.lchar '!'; return True)

416 l <- P.natural; n <- P.name;

444 l <- P.natural; n <- P.name;

417 hints <- many P.fnName

445 hints <- many P.fnName

@@ -419,7 +447,6 @@ cmd_proofsearch name = do

419

447

420cmd_refine :: String -> P.IdrisParser (Either String Command)

448cmd_refine :: String -> P.IdrisParser (Either String Command)

421cmd_refine name = do

449cmd_refine name = do

422− P.whiteSpace

423 upd <- option False (do P.lchar '!'; return True)

450 upd <- option False (do P.lchar '!'; return True)

424 l <- P.natural; n <- P.name;

451 l <- P.natural; n <- P.name;

425 hint <- P.fnName

452 hint <- P.fnName