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