src/Idris/REPLParser.hs · Idris-dev

1module Idris.REPLParser(parseCmd) where

2

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

4import System.Console.ANSI (Color(..))

5

6import Idris.Colours

7import Idris.Parser

8import Idris.AbsSyntax

9import Core.TT

10

11import Text.ParserCombinators.Parsec

12import Text.ParserCombinators.Parsec.Expr

13import Text.ParserCombinators.Parsec.Language

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

15

16import Debug.Trace

17import Data.List

18import Data.List.Split(splitOn)

19import Data.Char(toLower)

20

21parseCmd :: IState -> String -> String -> Either ParseError Command

22parseCmd i inputname = runParser pCmd i inputname

23

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

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

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

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

28

29pCmd :: IParser Command

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

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

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

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

34 return (ModImport (toPath f)))

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

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

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

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

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

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

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

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

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

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

45 return (Just x))

46 eof; return (AddProof n))

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

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

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

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

51 <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))

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

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

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

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

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

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

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

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

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

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

62 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

63 <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))

64 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

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

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

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

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

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

70 <|> do whiteSpace; do eof; return NOP

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

72

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

74

75pOption :: IParser Opt

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

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

78

79

80colours :: [(String, Color)]

81colours = [ ("black", Black)

82 , ("red", Red)

83 , ("green", Green)

84 , ("yellow", Yellow)

85 , ("blue", Blue)

86 , ("magenta", Magenta)

87 , ("cyan", Cyan)

88 , ("white", White)

89 ]

90

91pColour :: IParser Color

92pColour = doColour colours

93 where doColour [] = fail "Unknown colour"

94 doColour ((s, c):cs) = (try (symbol s) >> return c) <|> doColour cs

95

96pColourMod :: IParser (IdrisColour -> IdrisColour)

97pColourMod = try (symbol "vivid" >> return doVivid)

98 <|> try (symbol "dull" >> return doDull)

99 <|> try (symbol "underline" >> return doUnderline)

100 <|> try (symbol "nounderline" >> return doNoUnderline)

101 <|> try (symbol "bold" >> return doBold)

102 <|> try (symbol "nobold" >> return doNoBold)

103 <|> try (pColour >>= return . doSetColour)

104 where doVivid i = i { vivid = True }

105 doDull i = i { vivid = False }

106 doUnderline i = i { underline = True }

107 doNoUnderline i = i { underline = False }

108 doBold i = i { bold = True }

109 doNoBold i = i { bold = False }

110 doSetColour c i = i { colour = c }

111

112

113colourTypes :: [(String, ColourType)]

114colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

115 enumFromTo minBound maxBound

116

117pColourType :: IParser ColourType

118pColourType = doColourType colourTypes

119 where doColourType [] = fail $ "Unknown colour category. Options: " ++

120 (concat . intersperse ", " . map fst) colourTypes

121 doColourType ((s,ct):cts) = (try (symbol s) >> return ct) <|> doColourType cts

122

123pSetColourCmd :: IParser Command

124pSetColourCmd = (do c <- pColourType

125 let defaultColour = IdrisColour Black True False False

126 opts <- sepBy pColourMod spaces

127 let colour = foldr ($) defaultColour $ reverse opts

128 return $ SetColour c colour)

129 <|> try (symbol "on" >> return ColourOn)

130 <|> try (symbol "off" >> return ColourOff)