@@ -1,5 +1,5 @@
11
2−module Idris.REPLParser(parseCmd) where
2+module Idris.REPLParser (parseCmd, help, allHelp) where
33
44import System.FilePath ((</>))
55import System.Console.ANSI (Color(..))
@@ -7,6 +7,7 @@ import System.Console.ANSI (Color(..))
77import Idris.Colours
88import Idris.AbsSyntax
99import Idris.Core.TT
10+import Idris.Help
1011import qualified Idris.Parser as P
1112
1213import Control.Applicative
@@ -26,82 +27,135 @@ import qualified Data.ByteString.UTF8 as UTF8
2627parseCmd :: IState -> String -> String -> Result (Either String Command)
2728parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace
2829
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+
29151pCmd :: P.IdrisParser (Either String Command)
30−pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit
31− , do c <- cmd ["h", "?", "help"]; noArgs c Help
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
100− , nop
101− ]
102− <|> eval
103− where nop = do P.whiteSpace; eof; return (Right NOP)
104− eval = exprArg "" Eval
152+pCmd = choice [ do c <- cmd names; parser c
153+ | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]
154+ <|> unrecognized
155+ <|> nop
156+ <|> eval
157+ where nop = do eof; return (Right NOP)
158+ eval = exprArg Eval ""
105159 unrecognized = do
106160 P.lchar ':'
107161 cmd <- many anyChar
@@ -119,20 +173,18 @@ cmd xs = try $ do
119173 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
120174
121175
122−noArgs :: String -> Command -> P.IdrisParser (Either String Command)
123−noArgs name cmd = do
176+noArgs :: Command -> String -> P.IdrisParser (Either String Command)
177+noArgs cmd name = do
124178 let emptyArgs = do
125− P.whiteSpace
126179 eof
127180 return (Right cmd)
128181
129182 let failure = return (Left $ ":" ++ name ++ " takes no arguments")
130183
131− try emptyArgs <|> failure
184+ emptyArgs <|> failure
132185
133−exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)
134−exprArg name cmd = do
135− P.whiteSpace
186+exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)
187+exprArg cmd name = do
136188 let noArg = do
137189 eof
138190 return $ Left ("Usage is :" ++ name ++ " <expression>")
@@ -143,51 +195,45 @@ exprArg name cmd = do
143195 try noArg <|> properArg
144196
145197
146−fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String 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)
158−nameArg name cmd = do
159− P.whiteSpace
160− let emptyArgs = do eof
161− return $ Left ("Usage is :" ++ name ++ " <functionname>")
162− oneArg = do n <- P.name
198+
199+genArg :: String -> P.IdrisParser a -> (a -> Command)
200+ -> String -> P.IdrisParser (Either String Command)
201+genArg argName argParser cmd name = do
202+ let emptyArgs = do eof; failure
203+ oneArg = do arg <- argParser
163204 eof
164− return (Right (cmd n))
165− badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
166− try emptyArgs <|> try oneArg <|> badArg
205+ return (Right (cmd arg))
206+ try emptyArgs <|> oneArg <|> failure
207+ where
208+ failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")
167209
168−strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)
169−strArg name cmd = do
170− n <- many anyChar
171− eof
172− return (Right (cmd n))
210+nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)
211+nameArg = genArg "name" P.name
212+fnNameArg = genArg "functionname" P.fnName
173213
174−optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)
175−optArg name cmd = do
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+
222+optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)
223+optArg cmd name = do
176224 let emptyArgs = do
177225 eof
178226 return $ Left ("Usage is :" ++ name ++ " <option>")
179227
180228 let oneArg = do
181− P.whiteSpace
182229 o <- pOption
183230 P.whiteSpace
184231 eof
185232 return (Right (cmd o))
186233
187− let failure = do
188− return $ Left "Unrecognized setting"
234+ let failure = return $ Left "Unrecognized setting"
189235
190− try emptyArgs <|> try oneArg <|> failure
236+ try emptyArgs <|> oneArg <|> failure
191237
192238 where
193239 pOption :: P.IdrisParser Opt
@@ -198,9 +244,8 @@ optArg name cmd = do
198244 <|> do discard (P.symbol "nobanner") ; return NoBanner
199245 <|> do discard (P.symbol "warnreach"); return WarnReach
200246
201−proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)
202−proofArg name cmd = do
203− P.whiteSpace
247+proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)
248+proofArg cmd name = do
204249 upd <- option False $ do
205250 P.lchar '!'
206251 return True
@@ -215,7 +260,7 @@ cmd_doc name = do
215260 eof
216261 return $ Right (DocStr (Right c))
217262
218− let fnName = fnNameArg name (\n -> DocStr (Left n))
263+ let fnName = fnNameArg (\n -> DocStr (Left n)) name
219264
220265 try constant <|> fnName
221266
@@ -232,7 +277,7 @@ cmd_consolewidth name = do
232277
233278cmd_dynamic :: String -> P.IdrisParser (Either String Command)
234279cmd_dynamic name = do
235− let emptyArgs = noArgs name ListDynamic
280+ let emptyArgs = noArgs ListDynamic name
236281
237282 let oneArg = do l <- many anyChar
238283 return $ Right (DynamicLink l)
@@ -243,7 +288,6 @@ cmd_dynamic name = do
243288
244289cmd_pprint :: String -> P.IdrisParser (Either String Command)
245290cmd_pprint name = do
246− P.whiteSpace
247291 fmt <- ppFormat
248292 P.whiteSpace
249293 n <- fmap fromInteger P.natural
@@ -257,13 +301,6 @@ cmd_pprint name = do
257301 <|> (discard (P.symbol "latex") >> return LaTeXOutput)
258302
259303
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
267304
268305cmd_compile :: String -> P.IdrisParser (Either String Command)
269306cmd_compile name = do
@@ -312,8 +349,7 @@ cmd_let name = do
312349 return (Right (NewDefn defn))
313350
314351cmd_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
317353
318354cmd_loadto :: String -> P.IdrisParser (Either String Command)
319355cmd_loadto name = do
@@ -322,8 +358,7 @@ cmd_loadto name = do
322358 return (Right (Load f (Just (fromInteger toline))))
323359
324360cmd_colour :: String -> P.IdrisParser (Either String Command)
325−cmd_colour name = do
326− pSetColourCmd >>= return . Right
361+cmd_colour name = fmap Right pSetColourCmd
327362
328363 where
329364 colours :: [(String, Maybe Color)]
@@ -386,32 +421,25 @@ cmd_colour name = do
386421idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])
387422
388423cmd_apropos :: String -> P.IdrisParser (Either String Command)
389−cmd_apropos name =
390− try (do P.whiteSpace
391− P.lchar '('
392− pkgs <- sepBy (some idChar) (P.lchar ',')
393− P.lchar ')'
394− nm <- some idChar
395− return (Right (Apropos pkgs nm)))
396− <|> do P.whiteSpace;
397− nm <- some idChar
398− return (Right (Apropos [] nm))
424+cmd_apropos = packageBasedCmd (some idChar) Apropos
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
430+ P.lchar '('
431+ pks <- sepBy (some idChar) (P.lchar ',')
432+ P.lchar ')'
433+ return pks
434+ val <- valParser
435+ return (Right (cmd pkgs val))
399436
400437cmd_search :: String -> P.IdrisParser (Either String Command)
401−cmd_search name =
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 })
407− return (Right (Search pkgs t)))
408− <|> do P.whiteSpace;
409− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })
410− return (Right (Search [] t))
438+cmd_search = packageBasedCmd
439+ (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search
411440
412441cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
413442cmd_proofsearch name = do
414− P.whiteSpace
415443 upd <- option False (do P.lchar '!'; return True)
416444 l <- P.natural; n <- P.name;
417445 hints <- many P.fnName
@@ -419,7 +447,6 @@ cmd_proofsearch name = do
419447
420448cmd_refine :: String -> P.IdrisParser (Either String Command)
421449cmd_refine name = do
422− P.whiteSpace
423450 upd <- option False (do P.lchar '!'; return True)
424451 l <- P.natural; n <- P.name;
425452 hint <- P.fnName