forked from idris-lang/Idris-dev
-
Notifications
You must be signed in to change notification settings - Fork 0
/
REPLParser.hs
57 lines (49 loc) · 2.72 KB
/
REPLParser.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
module Idris.REPLParser(parseCmd) where
import Idris.Parser
import Idris.AbsSyntax
import Core.TT
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as PTok
import Debug.Trace
import Data.List
parseCmd i = runParser pCmd i "(input)"
cmd :: [String] -> IParser ()
cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
where docmd [] = fail "No such command"
docmd (x:xs) = try (discard (symbol x)) <|> docmd xs
pCmd :: IParser Command
pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
<|> try (do cmd ["h", "?", "help"]; eof; return Help)
<|> try (do cmd ["r", "reload"]; eof; return Reload)
<|> try (do cmd ["e", "edit"]; eof; return Edit)
<|> try (do cmd ["exec", "execute"]; eof; return Execute)
<|> try (do cmd ["ttshell"]; eof; return TTShell)
<|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
<|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
<|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))
<|> try (do cmd ["m", "metavars"]; eof; return Metavars)
<|> try (do cmd ["proofs"]; eof; return Proofs)
<|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
<|> try (do cmd ["a", "addproof"]; n <- pName; eof; return (AddProof n))
<|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
<|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
<|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
<|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
<|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
<|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))
<|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
<|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))
<|> try (do cmd ["u", "universes"]; eof; return Universes)
<|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
<|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
<|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
<|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
<|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))
<|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))
<|> do t <- pFullExpr defaultSyntax; return (Eval t)
<|> do eof; return NOP
pOption :: IParser Opt
pOption = do discard (symbol "errorcontext"); return ErrContext
<|> do discard (symbol "showimplicits"); return ShowImpl