src/Idris/REPLParser.hs · Idris-dev

git.iko.soy/Idris-dev

on aa8aefd help sign in

Idris-dev/src/Idris/REPLParser.hs

71 lines 3.5 kB history raw

1module Idris.REPLParser(parseCmd) where

3import System.FilePath ((</>))

5import Idris.Parser

6import Idris.AbsSyntax

7import Core.TT

9import Text.ParserCombinators.Parsec

10import Text.ParserCombinators.Parsec.Expr

11import Text.ParserCombinators.Parsec.Language

12import qualified Text.ParserCombinators.Parsec.Token as PTok

14import Debug.Trace

15import Data.List

16import Data.List.Split(splitOn)

18parseCmd i = runParser pCmd i "(input)"

20cmd :: [String] -> IParser ()

21cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

22 where docmd [] = fail "No such command"

23 docmd (x:xs) = try (discard (symbol x)) <|> docmd xs

25pCmd :: IParser Command

26pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

27 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

28 <|> try (do cmd ["r", "reload"]; eof; return Reload)

29 <|> try (do cmd ["m", "module"]; f <- identifier; eof;

30 return (ModImport (toPath f)))

31 <|> try (do cmd ["e", "edit"]; eof; return Edit)

32 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

33 <|> try (do cmd ["ttshell"]; eof; return TTShell)

34 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))

35 <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))

36 <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ToJavaScript f))

37 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

38 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

39 <|> try (do cmd ["proofs"]; eof; return Proofs)

40 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

41 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;

42 return (Just x))

43 eof; return (AddProof n))

44 <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))

45 <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))

46 <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))

47 <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))

48 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

49 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

50 <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))

51 <|> try (do cmd ["d", "def"]; n <- pfName; eof; return (Defn n))

52 <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))

53 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

54 <|> try (do cmd ["u", "universes"]; eof; return Universes)

55 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))

56 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

57 <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))

58 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

59 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

60 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

61 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

62 <|> try (do cmd ["patt"]; t <- pFullExpr defaultSyntax; return (Pattelab t))

63 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

64 <|> do eof; return NOP

66 where toPath n = foldl1 (</>) $ splitOn "." n

68pOption :: IParser Opt

69pOption = do discard (symbol "errorcontext"); return ErrContext

70 <|> do discard (symbol "showimplicits"); return ShowImpl