git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Idris/REPLParser.hs
43 lines 1.9 kB history raw
1module Idris.REPLParser(parseCmd) where
3import Idris.Parser
4import Idris.AbsSyntax
5import Core.TT
7import Text.ParserCombinators.Parsec
8import Text.ParserCombinators.Parsec.Expr
9import Text.ParserCombinators.Parsec.Language
10import qualified Text.ParserCombinators.Parsec.Token as PTok
12import Debug.Trace
13import Data.List
15parseCmd i = runParser pCmd i "(input)"
17cmd :: [String] -> IParser ()
18cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
19 where docmd [] = fail "No such command"
20 docmd (x:xs) = try (discard (symbol x)) <|> docmd xs
22pCmd :: IParser Command
23pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
24 <|> try (do cmd ["h", "?", "help"]; eof; return Help)
25 <|> try (do cmd ["r", "reload"]; eof; return Reload)
26 <|> try (do cmd ["e", "edit"]; eof; return Edit)
27 <|> try (do cmd ["exec", "execute"]; eof; return Execute)
28 <|> try (do cmd ["ttshell"]; eof; return TTShell)
29 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))
30 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
31 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
32 <|> try (do cmd ["a", "addproof"]; eof; return AddProof)
33 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
34 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
35 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
36 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))
37 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))
38 <|> try (do cmd ["u", "universes"]; eof; return Universes)
39 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
40 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))
41 <|> do t <- pFullExpr defaultSyntax; return (Eval t)
42 <|> do eof; return NOP