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