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