git.iko.soy/Idris-dev
on 96db606 help sign in
Idris-dev/src/Idris/REPLParser.hs
68 lines 3.4 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 ["m", "module"]; f <- identifier; eof;
27 return (ModImport (map dot f)))
28 <|> try (do cmd ["e", "edit"]; eof; return Edit)
29 <|> try (do cmd ["exec", "execute"]; eof; return Execute)
30 <|> try (do cmd ["ttshell"]; eof; return TTShell)
31 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
32 <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
33 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))
34 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
35 <|> try (do cmd ["proofs"]; eof; return Proofs)
36 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
37 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;
38 return (Just x))
39 eof; return (AddProof n))
40 <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
41 <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
42 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
43 <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))
44 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
45 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
46 <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))
47 <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))
48 <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
49 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))
50 <|> try (do cmd ["u", "universes"]; eof; return Universes)
51 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
52 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
53 <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))
54 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
55 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
56 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))
57 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))
58 <|> try (do cmd ["patt"]; t <- pFullExpr defaultSyntax; return (Pattelab t))
59 <|> do t <- pFullExpr defaultSyntax; return (Eval t)
60 <|> do eof; return NOP
62 where dot '.' = '/'
63 dot c = c
65pOption :: IParser Opt
66pOption = do discard (symbol "errorcontext"); return ErrContext
67 <|> do discard (symbol "showimplicits"); return ShowImpl