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 (P.runInnerParser (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 ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

73 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

74 l <- P.natural; n <- P.name;

75 return (CaseSplitAt (fromInteger l) n))

76 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

77 n <- P.name;

78 t <- P.fullExpr defaultSyntax;

79 return (CaseSplit n t))

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

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

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

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

84

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

86

87pOption :: P.IdrisParser Opt

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

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

90

91

92colours :: [(String, Color)]

93colours = [ ("black", Black)

94 , ("red", Red)

95 , ("green", Green)

96 , ("yellow", Yellow)

97 , ("blue", Blue)

98 , ("magenta", Magenta)

99 , ("cyan", Cyan)

100 , ("white", White)

101 ]

102

103pColour :: P.IdrisParser Color

104pColour = doColour colours

105 where doColour [] = fail "Unknown colour"

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

107

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

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

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

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

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

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

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

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

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

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

118 where doVivid i = i { vivid = True }

119 doDull i = i { vivid = False }

120 doUnderline i = i { underline = True }

121 doNoUnderline i = i { underline = False }

122 doBold i = i { bold = True }

123 doNoBold i = i { bold = False }

124 doItalic i = i { italic = True }

125 doNoItalic i = i { italic = False }

126 doSetColour c i = i { colour = c }

127

128

129colourTypes :: [(String, ColourType)]

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

131 enumFromTo minBound maxBound

132

133pColourType :: P.IdrisParser ColourType

134pColourType = doColourType colourTypes

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

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

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

138

139pSetColourCmd :: P.IdrisParser Command

140pSetColourCmd = (do c <- pColourType

141 let defaultColour = IdrisColour Black True False False False

142 opts <- sepBy pColourMod (P.whiteSpace)

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

144 return $ SetColour c colour)

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

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