git.iko.soy/Idris-dev
on 0a7dcf0 help sign in
Idris-dev/src/Idris/REPL/Parser.hs
539 lines 22 kB history raw
1{-|
2Module : Idris.REPL.Parser
3Description : Parser for the REPL commands.
4License : BSD3
5Maintainer : The Idris Community.
6-}
7module Idris.REPL.Parser (
8 parseCmd
9 , help
10 , allHelp
11 , setOptions
12 ) where
14import Idris.AbsSyntax
15import Idris.Colours
16import Idris.Core.TT
17import Idris.Help
18import Idris.Imports
19import Idris.Options
20import qualified Idris.Parser as IP
21import qualified Idris.Parser.Expr as IP
22import qualified Idris.Parser.Helpers as IP
23import qualified Idris.Parser.Ops as IP
25import Idris.REPL.Commands
27import Control.Applicative
28import Control.Monad.State.Strict
29import Data.Char (isSpace, toLower)
30import Data.List
31import Data.List.Split (splitOn)
32import System.Console.ANSI (Color(..))
33import System.FilePath ((</>))
34import Text.Parser.Char (anyChar, oneOf)
35import Text.Parser.Combinators
37parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)
38parseCmd i inputname = IP.runparser pCmd i inputname . trim
39 where trim = f . f
40 where f = reverse . dropWhile isSpace
42type CommandTable = [ ( [String], CmdArg, String
43 , String -> IP.IdrisParser (Either String Command) ) ]
45setOptions :: [(String, Opt)]
46setOptions = [("errorcontext", ErrContext),
47 ("showimplicits", ShowImpl),
48 ("originalerrors", ShowOrigErr),
49 ("autosolve", AutoSolve),
50 ("nobanner", NoBanner),
51 ("warnreach", WarnReach),
52 ("evaltypes", EvalTypes),
53 ("desugarnats", DesugarNats)]
55help :: [([String], CmdArg, String)]
56help = (["<expr>"], NoArg, "Evaluate an expression") :
57 [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]
59allHelp :: [([String], CmdArg, String)]
60allHelp = [ (map (':' :) names, args, text)
61 | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]
63parserCommandsForHelp :: CommandTable
64parserCommandsForHelp =
65 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
66 , exprArgCmd ["core"] Core "View the core language representation of a term"
67 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"
68 , (["doc"], NameArg, "Show internal documentation", cmd_doc)
69 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"
70 , genArg "namespace" (many anyChar) MakeDoc)
71 , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"
72 , cmd_apropos)
73 , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg
74 , " Search for values by type", cmd_search)
75 , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"
76 , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"
77 , namespaceArgCmd ["browse"] Browse "List the contents of some namespace"
78 , nameArgCmd ["total"] TotCheck "Check the totality of a name"
79 , noArgCmd ["r", "reload"] Reload "Reload current file"
80 , noArgCmd ["w", "watch"] Watch "Watch the current file for changes"
81 , (["l", "load"], FileArg, "Load a new file"
82 , strArg (\f -> Load f Nothing))
83 , (["!"], ShellCommandArg, "Run a shell command", strArg RunShellCommand)
84 , (["cd"], FileArg, "Change working directory"
85 , strArg ChangeDirectory)
86 , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons
87 , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"
88 , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables or holes)"
89 , (["p", "prove"], MetaVarArg, "Prove a metavariable"
90 , nameArg (Prove False))
91 , (["elab"], MetaVarArg, "Build a metavariable using the elaboration shell"
92 , nameArg (Prove True))
93 , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)
94 , (["rmproof"], NameArg, "Remove proof from proof stack"
95 , nameArg RmProof)
96 , (["showproof"], NameArg, "Show proof"
97 , nameArg ShowProof)
98 , noArgCmd ["proofs"] Proofs "Show available proofs"
99 , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"
100 , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)
101 , (["exec", "execute"], OptionalArg ExprArg, "Compile to an executable and run", cmd_execute)
102 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)
103 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)
104 , noArgCmd ["?", "h", "help"] Help "Display this help text"
105 , optArgCmd ["set"] SetOpt $ "Set an option (" ++ optionsList ++ ")"
106 , optArgCmd ["unset"] UnsetOpt "Unset an option"
107 , (["color", "colour"], ColourArg
108 , "Turn REPL colours on or off; set a specific colour"
109 , cmd_colour)
110 , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)
111 , (["printerdepth"], OptionalArg NumberArg, "Set the maximum pretty-printer depth (no arg for infinite)", cmd_printdepth)
112 , noArgCmd ["q", "quit"] Quit "Exit the Idris system"
113 , noArgCmd ["warranty"] Warranty "Displays warranty information"
114 , (["let"], ManyArgs DeclArg
115 , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"
116 , cmd_let)
117 , (["unlet", "undefine"], ManyArgs NameArg
118 , "Remove the listed repl definitions, or all repl definitions if no names given"
119 , cmd_unlet)
120 , nameArgCmd ["printdef"] PrintDef "Show the definition of a function"
121 , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg))
122 , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."
123 , cmd_pprint)
124 , (["verbosity"], NumberArg, "Set verbosity level", cmd_verb)
125 ]
126 where optionsList = intercalate ", " $ map fst setOptions
129parserCommands :: CommandTable
130parserCommands =
131 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"
132 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"
134 , nameArgCmd ["d", "def"] Defn "Display a name's internal definitions"
135 , nameArgCmd ["transinfo"] TransformInfo "Show relevant transformation rules for a name"
136 , nameArgCmd ["di", "dbginfo"] DebugInfo "Show debugging information for a name"
138 , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression"
139 , exprArgCmd ["spec"] Spec "?"
140 , exprArgCmd ["whnf"] WHNF "(Debugging) Show weak head normal form of an expression"
141 , exprArgCmd ["inline"] TestInline "?"
142 , proofArgCmd ["cs", "casesplit"] CaseSplitAt
143 ":cs <line> <name> splits the pattern variable on the line"
144 , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom
145 ":apc <line> <name> adds a pattern-matching proof clause to name on line"
146 , proofArgCmd ["ac", "addclause"] AddClauseFrom
147 ":ac <line> <name> adds a clause for the definition of the name on the line"
148 , proofArgCmd ["am", "addmissing"] AddMissing
149 ":am <line> <name> adds all missing pattern matches for the name on the line"
150 , proofArgCmd ["mw", "makewith"] MakeWith
151 ":mw <line> <name> adds a with clause for the definition of the name on the line"
152 , proofArgCmd ["mc", "makecase"] MakeCase
153 ":mc <line> <name> adds a case block for the definition of the metavariable on the line"
154 , proofArgCmd ["ml", "makelemma"] MakeLemma "?"
155 , (["log"], NumberArg, "Set logging level", cmd_log)
156 , ( ["logcats"]
157 , ManyArgs NameArg
158 , "Set logging categories"
159 , cmd_cats)
160 , (["lto", "loadto"], SeqArgs NumberArg FileArg
161 , "Load file up to line number", cmd_loadto)
162 , (["ps", "proofsearch"], NoArg
163 , ":ps <line> <name> <names> does proof search for name on line, with names as hints"
164 , cmd_proofsearch)
165 , (["ref", "refine"], NoArg
166 , ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"
167 , cmd_refine)
168 , (["debugunify"], SeqArgs ExprArg ExprArg
169 , "(Debugging) Try to unify two expressions", const $ do
170 l <- IP.simpleExpr defaultSyntax
171 r <- IP.simpleExpr defaultSyntax
172 eof
173 return (Right (DebugUnify l r))
174 )
175 ]
177noArgCmd names command doc =
178 (names, NoArg, doc, noArgs command)
179nameArgCmd names command doc =
180 (names, NameArg, doc, fnNameArg command)
181namespaceArgCmd names command doc =
182 (names, NamespaceArg, doc, namespaceArg command)
183exprArgCmd names command doc =
184 (names, ExprArg, doc, exprArg command)
185optArgCmd names command doc =
186 (names, OptionArg, doc, optArg command)
187proofArgCmd names command doc =
188 (names, NoArg, doc, proofArg command)
190pCmd :: IP.IdrisParser (Either String Command)
191pCmd = choice [ do c <- cmd names; parser c
192 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]
193 <|> unrecognized
194 <|> nop
195 <|> eval
196 where nop = do eof; return (Right NOP)
197 unrecognized = do
198 IP.lchar ':'
199 cmd <- many anyChar
200 let cmd' = takeWhile (/=' ') cmd
201 return (Left $ "Unrecognized command: " ++ cmd')
203cmd :: [String] -> IP.IdrisParser String
204cmd xs = try $ do
205 IP.lchar ':'
206 docmd sorted_xs
208 where docmd [] = fail "Could not parse command"
209 docmd (x:xs) = try (IP.reserved x >> return x) <|> docmd xs
211 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
214noArgs :: Command -> String -> IP.IdrisParser (Either String Command)
215noArgs cmd name = do
216 let emptyArgs = do
217 eof
218 return (Right cmd)
220 let failure = return (Left $ ":" ++ name ++ " takes no arguments")
222 emptyArgs <|> failure
224eval :: IP.IdrisParser (Either String Command)
225eval = do
226 t <- IP.fullExpr defaultSyntax
227 return $ Right (Eval t)
229exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)
230exprArg cmd name = do
231 let noArg = do
232 eof
233 return $ Left ("Usage is :" ++ name ++ " <expression>")
235 let justOperator = do
236 (op, fc) <- IP.symbolicOperatorFC
237 eof
238 return $ Right $ cmd (PRef fc [] (sUN op))
240 let properArg = do
241 t <- IP.fullExpr defaultSyntax
242 return $ Right (cmd t)
243 try noArg <|> try justOperator <|> properArg
245genArg :: String -> IP.IdrisParser a -> (a -> Command)
246 -> String -> IP.IdrisParser (Either String Command)
247genArg argName argParser cmd name = do
248 let emptyArgs = do eof; failure
249 oneArg = do arg <- argParser
250 eof
251 return (Right (cmd arg))
252 try emptyArgs <|> oneArg <|> failure
253 where
254 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")
256nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)
257nameArg = genArg "name" $ fst <$> IP.name
258fnNameArg = genArg "functionname" $ fst <$> IP.fnName
260strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)
261strArg = genArg "string" (many anyChar)
263moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)
264moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)
265 where
266 toPath n = foldl1' (</>) $ splitOn "." n
268namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)
269namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)
270 where
271 toNS = splitOn "."
273optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)
274optArg cmd name = do
275 let emptyArgs = do
276 eof
277 return $ Left ("Usage is :" ++ name ++ " <option>")
279 let oneArg = do
280 o <- pOption
281 IP.whiteSpace
282 eof
283 return (Right (cmd o))
285 let failure = return $ Left "Unrecognized setting"
287 try emptyArgs <|> oneArg <|> failure
289 where
290 pOption :: IP.IdrisParser Opt
291 pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions
293proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)
294proofArg cmd name = do
295 upd <- option False $ do
296 IP.lchar '!'
297 return True
298 l <- fst <$> IP.natural
299 n <- fst <$> IP.name;
300 return (Right (cmd upd (fromInteger l) n))
302cmd_doc :: String -> IP.IdrisParser (Either String Command)
303cmd_doc name = do
304 let constant = do
305 c <- fmap fst IP.constant
306 eof
307 return $ Right (DocStr (Right c) FullDocs)
309 let pType = do
310 IP.reserved "Type"
311 eof
312 return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)
314 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name
316 try constant <|> pType <|> fnName
318cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)
319cmd_consolewidth name = do
320 w <- pConsoleWidth
321 return (Right (SetConsoleWidth w))
323 where
324 pConsoleWidth :: IP.IdrisParser ConsoleWidth
325 pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth
326 <|> do discard (IP.symbol "infinite"); return InfinitelyWide
327 <|> do n <- fmap (fromInteger . fst) IP.natural
328 return (ColsWide n)
330cmd_printdepth :: String -> IP.IdrisParser (Either String Command)
331cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)
332 return (Right $ SetPrinterDepth d)
334cmd_execute :: String -> IP.IdrisParser (Either String Command)
335cmd_execute name = do
336 tm <- option maintm (IP.fullExpr defaultSyntax)
337 return (Right (Execute tm))
338 where
339 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])
341cmd_dynamic :: String -> IP.IdrisParser (Either String Command)
342cmd_dynamic name = do
343 let optArg = do l <- many anyChar
344 if (l /= "")
345 then return $ Right (DynamicLink l)
346 else return $ Right ListDynamic
347 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
348 try optArg <|> failure
350cmd_pprint :: String -> IP.IdrisParser (Either String Command)
351cmd_pprint name = do
352 fmt <- ppFormat
353 IP.whiteSpace
354 n <- fmap (fromInteger . fst) IP.natural
355 IP.whiteSpace
356 t <- IP.fullExpr defaultSyntax
357 return (Right (PPrint fmt n t))
359 where
360 ppFormat :: IP.IdrisParser OutputFmt
361 ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)
362 <|> (discard (IP.symbol "latex") >> return LaTeXOutput)
364cmd_compile :: String -> IP.IdrisParser (Either String Command)
365cmd_compile name = do
366 let defaultCodegen = Via IBCFormat "c"
368 let codegenOption :: IP.IdrisParser Codegen
369 codegenOption = do
370 let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode
371 viaCodegen = do x <- fst <$> IP.identifier
372 return (Via IBCFormat (map toLower x))
373 bytecodeCodegen <|> viaCodegen
375 let hasOneArg = do
376 i <- get
377 f <- fst <$> IP.identifier
378 eof
379 return $ Right (Compile defaultCodegen f)
381 let hasTwoArgs = do
382 i <- get
383 codegen <- codegenOption
384 f <- fst <$> IP.identifier
385 eof
386 return $ Right (Compile codegen f)
388 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
389 try hasTwoArgs <|> try hasOneArg <|> failure
391cmd_addproof :: String -> IP.IdrisParser (Either String Command)
392cmd_addproof name = do
393 n <- option Nothing $ do
394 x <- fst <$> IP.name
395 return (Just x)
396 eof
397 return (Right (AddProof n))
399cmd_log :: String -> IP.IdrisParser (Either String Command)
400cmd_log name = do
401 i <- fmap (fromIntegral . fst) IP.natural
402 eof
403 return (Right (LogLvl i))
405cmd_verb :: String -> IP.IdrisParser (Either String Command)
406cmd_verb name = do
407 i <- fmap (fromIntegral . fst) IP.natural
408 eof
409 return (Right (Verbosity i))
411cmd_cats :: String -> IP.IdrisParser (Either String Command)
412cmd_cats name = do
413 cs <- sepBy pLogCats (IP.whiteSpace)
414 eof
415 return $ Right $ LogCategory (concat cs)
416 where
417 badCat = do
418 c <- fst <$> IP.identifier
419 fail $ "Category: " ++ c ++ " is not recognised."
421 pLogCats :: IP.IdrisParser [LogCat]
422 pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))
423 <|> try (elabCats <$ IP.symbol (strLogCat IElab))
424 <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))
425 <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))
426 <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))
427 <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))
428 <|> badCat
430cmd_let :: String -> IP.IdrisParser (Either String Command)
431cmd_let name = do
432 defn <- concat <$> many (IP.decl defaultSyntax)
433 return (Right (NewDefn defn))
435cmd_unlet :: String -> IP.IdrisParser (Either String Command)
436cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)
438cmd_loadto :: String -> IP.IdrisParser (Either String Command)
439cmd_loadto name = do
440 toline <- fmap (fromInteger . fst) IP.natural
441 f <- many anyChar;
442 return (Right (Load f (Just toline)))
444cmd_colour :: String -> IP.IdrisParser (Either String Command)
445cmd_colour name = fmap Right pSetColourCmd
447 where
448 colours :: [(String, Maybe Color)]
449 colours = [ ("black", Just Black)
450 , ("red", Just Red)
451 , ("green", Just Green)
452 , ("yellow", Just Yellow)
453 , ("blue", Just Blue)
454 , ("magenta", Just Magenta)
455 , ("cyan", Just Cyan)
456 , ("white", Just White)
457 , ("default", Nothing)
458 ]
460 pSetColourCmd :: IP.IdrisParser Command
461 pSetColourCmd = (do c <- pColourType
462 let defaultColour = IdrisColour Nothing True False False False
463 opts <- sepBy pColourMod (IP.whiteSpace)
464 let colour = foldr ($) defaultColour $ reverse opts
465 return $ SetColour c colour)
466 <|> try (IP.symbol "on" >> return ColourOn)
467 <|> try (IP.symbol "off" >> return ColourOff)
469 pColour :: IP.IdrisParser (Maybe Color)
470 pColour = doColour colours
471 where doColour [] = fail "Unknown colour"
472 doColour ((s, c):cs) = (try (IP.symbol s) >> return c) <|> doColour cs
474 pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)
475 pColourMod = try (doVivid <$ IP.symbol "vivid")
476 <|> try (doDull <$ IP.symbol "dull")
477 <|> try (doUnderline <$ IP.symbol "underline")
478 <|> try (doNoUnderline <$ IP.symbol "nounderline")
479 <|> try (doBold <$ IP.symbol "bold")
480 <|> try (doNoBold <$ IP.symbol "nobold")
481 <|> try (doItalic <$ IP.symbol "italic")
482 <|> try (doNoItalic <$ IP.symbol "noitalic")
483 <|> try (pColour >>= return . doSetColour)
484 where doVivid i = i { vivid = True }
485 doDull i = i { vivid = False }
486 doUnderline i = i { underline = True }
487 doNoUnderline i = i { underline = False }
488 doBold i = i { bold = True }
489 doNoBold i = i { bold = False }
490 doItalic i = i { italic = True }
491 doNoItalic i = i { italic = False }
492 doSetColour c i = i { colour = c }
494 -- | Generate the colour type names using the default Show instance.
495 colourTypes :: [(String, ColourType)]
496 colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
497 enumFromTo minBound maxBound
499 pColourType :: IP.IdrisParser ColourType
500 pColourType = doColourType colourTypes
501 where doColourType [] = fail $ "Unknown colour category. Options: " ++
502 (concat . intersperse ", " . map fst) colourTypes
503 doColourType ((s,ct):cts) = (try (IP.symbol s) >> return ct) <|> doColourType cts
505idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])
507cmd_apropos :: String -> IP.IdrisParser (Either String Command)
508cmd_apropos = packageBasedCmd (some idChar) Apropos
510packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)
511 -> String -> IP.IdrisParser (Either String Command)
512packageBasedCmd valParser cmd name =
513 try (do IP.lchar '('
514 pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')
515 IP.lchar ')'
516 val <- valParser
517 return (Right (cmd pkgs val)))
518 <|> do val <- valParser
519 return (Right (cmd [] val))
520 where
521 pkg = either fail pure . pkgName =<< IP.packageName
523cmd_search :: String -> IP.IdrisParser (Either String Command)
524cmd_search = packageBasedCmd
525 (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search
527cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)
528cmd_proofsearch name = do
529 upd <- option False (True <$ IP.lchar '!')
530 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name
531 hints <- many (fst <$> IP.fnName)
532 return (Right (DoProofSearch upd True l n hints))
534cmd_refine :: String -> IP.IdrisParser (Either String Command)
535cmd_refine name = do
536 upd <- option False (do IP.lchar '!'; return True)
537 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name
538 hint <- fst <$> IP.fnName
539 return (Right (DoProofSearch upd False l n [hint]))