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.AbsSyntax

8import Core.TT

9import qualified Idris.Parser as P

10

11import Control.Applicative

12import Control.Monad.State.Strict

13

14import Text.Parser.Combinators

15import Text.Parser.Char(anyChar)

16import Text.Trifecta(Result, parseString)

17import Text.Trifecta.Delta

18

19import Debug.Trace

20import Data.List

21import Data.List.Split(splitOn)

22import Data.Char(toLower)

23import qualified Data.ByteString.UTF8 as UTF8

24

25parseCmd :: IState -> String -> String -> Result Command

26parseCmd i inputname = parseString (evalStateT pCmd i) (Directed (UTF8.fromString inputname) 0 0 0 0)

27

28cmd :: [String] -> P.IdrisParser ()

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

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

31 docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs

32

33pCmd :: P.IdrisParser Command

34pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

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

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

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

38 return (ModImport (toPath f)))

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

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

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

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

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

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

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

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

47 <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

48 <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

49 return (Just x))

50 eof; return (AddProof n))

51 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

52 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

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

54 <|> try (do cmd ["l", "load"]; f <- many anyChar; return (Load f))

55 <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

56 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

57 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

58 <|> try (do cmd ["doc"]; n <- P.fnName; eof; return (DocStr n))

59 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

60 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

61 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

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

63 <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

64 <|> try (do cmd ["i", "info"]; n <- P.fnName; eof; return (Info n))

65 <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

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

67 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

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

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

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

71 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

72 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

73 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

74 <|> do P.whiteSpace; do eof; return NOP

75 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

76

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

78

79pOption :: P.IdrisParser Opt

80pOption = do discard (P.symbol "errorcontext"); return ErrContext

81 <|> do discard (P.symbol "showimplicits"); return ShowImpl

82

83

84colours :: [(String, Color)]

85colours = [ ("black", Black)

86 , ("red", Red)

87 , ("green", Green)

88 , ("yellow", Yellow)

89 , ("blue", Blue)

90 , ("magenta", Magenta)

91 , ("cyan", Cyan)

92 , ("white", White)

93 ]

94

95pColour :: P.IdrisParser Color

96pColour = doColour colours

97 where doColour [] = fail "Unknown colour"

98 doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs

99

100pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

101pColourMod = try (P.symbol "vivid" >> return doVivid)

102 <|> try (P.symbol "dull" >> return doDull)

103 <|> try (P.symbol "underline" >> return doUnderline)

104 <|> try (P.symbol "nounderline" >> return doNoUnderline)

105 <|> try (P.symbol "bold" >> return doBold)

106 <|> try (P.symbol "nobold" >> return doNoBold)

107 <|> try (P.symbol "italic" >> return doItalic)

108 <|> try (P.symbol "noitalic" >> return doNoItalic)

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

110 where doVivid i = i { vivid = True }

111 doDull i = i { vivid = False }

112 doUnderline i = i { underline = True }

113 doNoUnderline i = i { underline = False }

114 doBold i = i { bold = True }

115 doNoBold i = i { bold = False }

116 doItalic i = i { italic = True }

117 doNoItalic i = i { italic = False }

118 doSetColour c i = i { colour = c }

119

120

121colourTypes :: [(String, ColourType)]

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

123 enumFromTo minBound maxBound

124

125pColourType :: P.IdrisParser ColourType

126pColourType = doColourType colourTypes

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

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

129 doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts

130

131pSetColourCmd :: P.IdrisParser Command

132pSetColourCmd = (do c <- pColourType

133 let defaultColour = IdrisColour Black True False False False

134 opts <- sepBy pColourMod (P.whiteSpace)

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

136 return $ SetColour c colour)

137 <|> try (P.symbol "on" >> return ColourOn)

138 <|> try (P.symbol "off" >> return ColourOff)