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