git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/REPLParser.hs
400 lines 16 kB history raw
2module Idris.REPLParser(parseCmd) where
4import System.FilePath ((</>))
5import System.Console.ANSI (Color(..))
7import Idris.Colours
8import Idris.AbsSyntax
9import Idris.Core.TT
10import qualified Idris.Parser as P
12import Control.Applicative
13import Control.Monad.State.Strict
15import Text.Parser.Combinators
16import Text.Parser.Char(anyChar)
17import Text.Trifecta(Result, parseString)
18import Text.Trifecta.Delta
20import Debug.Trace
21import Data.List
22import Data.List.Split(splitOn)
23import Data.Char(toLower)
24import qualified Data.ByteString.UTF8 as UTF8
26parseCmd :: IState -> String -> String -> Result (Either String Command)
27parseCmd i inputname = P.runparser pCmd i inputname
29pCmd :: P.IdrisParser (Either String Command)
30pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit
31 <|> do c <- cmd ["h", "?", "help"]; noArgs c Help
32 <|> do c <- cmd ["w", "warranty"]; noArgs c Warranty
33 <|> do c <- cmd ["r", "reload"]; noArgs c Reload
34 <|> do c <- cmd ["exec", "execute"]; noArgs c Execute
35 <|> do c <- cmd ["proofs"]; noArgs c Proofs
36 <|> do c <- cmd ["u", "universes"]; noArgs c Universes
37 <|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
38 <|> do c <- cmd ["m", "metavars"]; noArgs c Metavars
39 <|> do c <- cmd ["e", "edit"]; noArgs c Edit
41 <|> do c <- cmd ["d", "def"]; fnNameArg c Defn
42 <|> do c <- cmd ["total"]; fnNameArg c TotCheck
43 <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef
44 <|> do c <- cmd ["transinfo"]; fnNameArg c TransformInfo
45 <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
46 <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
47 <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
48 <|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing
50 <|> do c <- cmd ["t", "type"]; exprArg c Check
51 <|> do c <- cmd ["x"]; exprArg c ExecVal
52 <|> do c <- cmd ["patt"]; exprArg c Pattelab
53 <|> do c <- cmd ["spec"]; exprArg c Spec
54 <|> do c <- cmd ["hnf"]; exprArg c HNF
55 <|> do c <- cmd ["inline"]; exprArg c TestInline
57 <|> do c <- cmd ["rmproof"]; nameArg c RmProof
58 <|> do c <- cmd ["showproof"]; nameArg c ShowProof
59 <|> do c <- cmd ["p", "prove"]; nameArg c Prove
61 <|> do c <- cmd ["set"]; optArg c SetOpt
62 <|> do c <- cmd ["unset"]; optArg c UnsetOpt
64 <|> do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
65 <|> do c <- cmd ["cd"]; strArg c ChangeDirectory
66 <|> do c <- cmd ["apropos"]; strArg c Apropos
67 <|> do c <- cmd ["mkdoc"]; strArg c MakeDoc
69 <|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
70 <|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
71 <|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
72 <|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
73 <|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
74 <|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
76 <|> do c <- cmd ["pp", "pprint"]; cmd_pprint c
77 <|> do c <- cmd ["doc"]; cmd_doc c
78 <|> do c <- cmd ["dynamic"]; cmd_dynamic c
79 <|> do c <- cmd ["consolewidth"]; cmd_consolewidth c
80 <|> do c <- cmd ["module"]; cmd_module c
81 <|> do c <- cmd ["c", "compile"]; cmd_compile c
82 <|> do c <- cmd ["a", "addproof"]; cmd_addproof c
83 <|> do c <- cmd ["log"]; cmd_log c
84 <|> do c <- cmd ["let"]; cmd_let c
85 <|> do c <- cmd ["unlet","undefine"]; cmd_unlet c
86 <|> do c <- cmd ["lto", "loadto"]; cmd_loadto c
87 <|> do c <- cmd ["color", "colour"]; cmd_colour c
88 <|> do c <- cmd ["s", "search"]; cmd_search c
89 <|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
90 <|> do c <- cmd ["ref", "refine"]; cmd_refine c
92 <|> unrecognized
93 <|> nop
94 <|> eval
96 where nop = do P.whiteSpace; eof; return (Right NOP)
97 eval = exprArg "" Eval
98 unrecognized = do
99 P.lchar ':'
100 cmd <- many anyChar
101 let cmd' = takeWhile (/=' ') cmd
102 return (Left $ "Unrecognized command: " ++ cmd')
104cmd :: [String] -> P.IdrisParser String
105cmd xs = try $ do
106 P.lchar ':'
107 docmd sorted_xs
109 where docmd [] = fail "Could not parse command"
110 docmd (x:xs) = try (P.reserved x >> return x) <|> docmd xs
112 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
115noArgs :: String -> Command -> P.IdrisParser (Either String Command)
116noArgs name cmd = do
117 let emptyArgs = do
118 P.whiteSpace
119 eof
120 return (Right cmd)
122 let failure = return (Left $ ":" ++ name ++ " takes no arguments")
124 try emptyArgs <|> failure
126exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)
127exprArg name cmd = do
128 P.whiteSpace
129 let noArg = do
130 eof
131 return $ Left ("Usage is :" ++ name ++ " <expression>")
133 let properArg = do
134 t <- P.fullExpr defaultSyntax
135 return $ Right (cmd t)
136 try noArg <|> properArg
139fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
140fnNameArg name cmd = do
141 P.whiteSpace
142 let emptyArgs = do eof
143 return $ Left ("Usage is :" ++ name ++ " <functionname>")
144 oneArg = do n <- P.fnName
145 eof
146 return (Right (cmd n))
147 badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
148 try emptyArgs <|> try oneArg <|> badArg
150nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
151nameArg name cmd = do
152 P.whiteSpace
153 let emptyArgs = do eof
154 return $ Left ("Usage is :" ++ name ++ " <functionname>")
155 oneArg = do n <- P.name
156 eof
157 return (Right (cmd n))
158 badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
159 try emptyArgs <|> try oneArg <|> badArg
161strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)
162strArg name cmd = do
163 n <- many anyChar
164 eof
165 return (Right (cmd n))
167optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)
168optArg name cmd = do
169 let emptyArgs = do
170 eof
171 return $ Left ("Usage is :" ++ name ++ " <option>")
173 let oneArg = do
174 P.whiteSpace
175 o <- pOption
176 P.whiteSpace
177 eof
178 return (Right (cmd o))
180 let failure = do
181 return $ Left "Unrecognized setting"
183 try emptyArgs <|> try oneArg <|> failure
185 where
186 pOption :: P.IdrisParser Opt
187 pOption = do discard (P.symbol "errorcontext"); return ErrContext
188 <|> do discard (P.symbol "showimplicits"); return ShowImpl
189 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
190 <|> do discard (P.symbol "autosolve"); return AutoSolve
191 <|> do discard (P.symbol "nobanner") ; return NoBanner
192 <|> do discard (P.symbol "warnreach"); return WarnReach
194proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)
195proofArg name cmd = do
196 P.whiteSpace
197 upd <- option False $ do
198 P.lchar '!'
199 return True
200 l <- P.natural
201 n <- P.name;
202 return (Right (cmd upd (fromInteger l) n))
204cmd_doc :: String -> P.IdrisParser (Either String Command)
205cmd_doc name = do
206 let constant = do
207 c <- P.constant
208 eof
209 return $ Right (DocStr (Right c))
211 let fnName = fnNameArg name (\n -> DocStr (Left n))
213 try constant <|> fnName
215cmd_consolewidth :: String -> P.IdrisParser (Either String Command)
216cmd_consolewidth name = do
217 w <- pConsoleWidth
218 return (Right (SetConsoleWidth w))
220 where
221 pConsoleWidth :: P.IdrisParser ConsoleWidth
222 pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
223 <|> do discard (P.symbol "infinite"); return InfinitelyWide
224 <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
226cmd_dynamic :: String -> P.IdrisParser (Either String Command)
227cmd_dynamic name = do
228 let emptyArgs = noArgs name ListDynamic
230 let oneArg = do l <- many anyChar
231 return $ Right (DynamicLink l)
233 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
235 try emptyArgs <|> try oneArg <|> failure
237cmd_pprint :: String -> P.IdrisParser (Either String Command)
238cmd_pprint name = do
239 P.whiteSpace
240 fmt <- ppFormat
241 P.whiteSpace
242 n <- fmap fromInteger P.natural
243 P.whiteSpace
244 t <- P.fullExpr defaultSyntax
245 return (Right (PPrint fmt n t))
247 where
248 ppFormat :: P.IdrisParser OutputFmt
249 ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
250 <|> (discard (P.symbol "latex") >> return LaTeXOutput)
253cmd_module :: String -> P.IdrisParser (Either String Command)
254cmd_module name = do
255 f <- P.identifier
256 eof;
257 return (Right (ModImport (toPath f)))
258 where
259 toPath n = foldl1' (</>) $ splitOn "." n
261cmd_compile :: String -> P.IdrisParser (Either String Command)
262cmd_compile name = do
263 let defaultCodegen = Via "c"
265 let codegenOption :: P.IdrisParser Codegen
266 codegenOption = do
267 let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
268 viaCodegen = do x <- P.identifier
269 return (Via (map toLower x))
270 bytecodeCodegen <|> viaCodegen
272 let hasOneArg = do
273 i <- get
274 f <- P.identifier
275 eof
276 return $ Right (Compile defaultCodegen f)
278 let hasTwoArgs = do
279 i <- get
280 codegen <- codegenOption
281 f <- P.identifier
282 eof
283 return $ Right (Compile codegen f)
285 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
286 try hasTwoArgs <|> try hasOneArg <|> failure
288cmd_addproof :: String -> P.IdrisParser (Either String Command)
289cmd_addproof name = do
290 n <- option Nothing $ do
291 x <- P.name;
292 return (Just x)
293 eof
294 return (Right (AddProof n))
296cmd_log :: String -> P.IdrisParser (Either String Command)
297cmd_log name = do
298 i <- P.natural
299 eof
300 return (Right (LogLvl (fromIntegral i)))
302cmd_let :: String -> P.IdrisParser (Either String Command)
303cmd_let name = do
304 defn <- concat <$> many (P.decl defaultSyntax)
305 return (Right (NewDefn defn))
307cmd_unlet :: String -> P.IdrisParser (Either String Command)
308cmd_unlet name = do
309 (Right . Undefine) `fmap` many P.name
311cmd_loadto :: String -> P.IdrisParser (Either String Command)
312cmd_loadto name = do
313 toline <- P.natural
314 f <- many anyChar;
315 return (Right (Load f (Just (fromInteger toline))))
317cmd_colour :: String -> P.IdrisParser (Either String Command)
318cmd_colour name = do
319 pSetColourCmd >>= return . Right
321 where
322 colours :: [(String, Maybe Color)]
323 colours = [ ("black", Just Black)
324 , ("red", Just Red)
325 , ("green", Just Green)
326 , ("yellow", Just Yellow)
327 , ("blue", Just Blue)
328 , ("magenta", Just Magenta)
329 , ("cyan", Just Cyan)
330 , ("white", Just White)
331 , ("default", Nothing)
332 ]
334 pSetColourCmd :: P.IdrisParser Command
335 pSetColourCmd = (do c <- pColourType
336 let defaultColour = IdrisColour Nothing True False False False
337 opts <- sepBy pColourMod (P.whiteSpace)
338 let colour = foldr ($) defaultColour $ reverse opts
339 return $ SetColour c colour)
340 <|> try (P.symbol "on" >> return ColourOn)
341 <|> try (P.symbol "off" >> return ColourOff)
343 pColour :: P.IdrisParser (Maybe Color)
344 pColour = doColour colours
345 where doColour [] = fail "Unknown colour"
346 doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
348 pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
349 pColourMod = try (P.symbol "vivid" >> return doVivid)
350 <|> try (P.symbol "dull" >> return doDull)
351 <|> try (P.symbol "underline" >> return doUnderline)
352 <|> try (P.symbol "nounderline" >> return doNoUnderline)
353 <|> try (P.symbol "bold" >> return doBold)
354 <|> try (P.symbol "nobold" >> return doNoBold)
355 <|> try (P.symbol "italic" >> return doItalic)
356 <|> try (P.symbol "noitalic" >> return doNoItalic)
357 <|> try (pColour >>= return . doSetColour)
358 where doVivid i = i { vivid = True }
359 doDull i = i { vivid = False }
360 doUnderline i = i { underline = True }
361 doNoUnderline i = i { underline = False }
362 doBold i = i { bold = True }
363 doNoBold i = i { bold = False }
364 doItalic i = i { italic = True }
365 doNoItalic i = i { italic = False }
366 doSetColour c i = i { colour = c }
368 -- | Generate the colour type names using the default Show instance.
369 colourTypes :: [(String, ColourType)]
370 colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
371 enumFromTo minBound maxBound
373 pColourType :: P.IdrisParser ColourType
374 pColourType = doColourType colourTypes
375 where doColourType [] = fail $ "Unknown colour category. Options: " ++
376 (concat . intersperse ", " . map fst) colourTypes
377 doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
380cmd_search :: String -> P.IdrisParser (Either String Command)
381cmd_search name = do
382 P.whiteSpace;
383 t <- P.typeExpr (defaultSyntax { implicitAllowed = True })
384 return (Right (Search t))
386cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
387cmd_proofsearch name = do
388 P.whiteSpace
389 upd <- option False (do P.lchar '!'; return True)
390 l <- P.natural; n <- P.name;
391 hints <- many P.fnName
392 return (Right (DoProofSearch upd True (fromInteger l) n hints))
394cmd_refine :: String -> P.IdrisParser (Either String Command)
395cmd_refine name = do
396 P.whiteSpace
397 upd <- option False (do P.lchar '!'; return True)
398 l <- P.natural; n <- P.name;
399 hint <- P.fnName
400 return (Right (DoProofSearch upd False (fromInteger l) n [hint]))