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