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 Idris.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 = P.runparser pCmd i inputname

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 ["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 ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))

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

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

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

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

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

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

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

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

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

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

52 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

68 upd <- option False (do P.lchar '!'; return True)

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

70 return (CaseSplitAt upd (fromInteger l) n))

71 <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;

72 upd <- option False (do P.lchar '!'; return True)

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

74 return (AddProofClauseFrom upd (fromInteger l) n))

75 <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

76 upd <- option False (do P.lchar '!'; return True)

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

78 return (AddClauseFrom upd (fromInteger l) n))

79 <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;

80 upd <- option False (do P.lchar '!'; return True)

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

82 return (AddMissing upd (fromInteger l) n))

83 <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

84 upd <- option False (do P.lchar '!'; return True)

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

86 return (MakeWith upd (fromInteger l) n))

87 <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

88 upd <- option False (do P.lchar '!'; return True)

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

90 hints <- many P.name

91 return (DoProofSearch upd (fromInteger l) n hints))

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

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

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

95 return (Just x))

96 eof; return (AddProof n))

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

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

99 <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

100 <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

101 <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))

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

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

104

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

106

107pOption :: P.IdrisParser Opt

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

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

110 <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

111 <|> do discard (P.symbol "autosolve"); return AutoSolve

112

113pConsoleWidth :: P.IdrisParser ConsoleWidth

114pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

115 <|> do discard (P.symbol "infinite"); return InfinitelyWide

116 <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

117

118colours :: [(String, Maybe Color)]

119colours = [ ("black", Just Black)

120 , ("red", Just Red)

121 , ("green", Just Green)

122 , ("yellow", Just Yellow)

123 , ("blue", Just Blue)

124 , ("magenta", Just Magenta)

125 , ("cyan", Just Cyan)

126 , ("white", Just White)

127 , ("default", Nothing)

128 ]

129

130pColour :: P.IdrisParser (Maybe Color)

131pColour = doColour colours

132 where doColour [] = fail "Unknown colour"

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

134

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

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

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

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

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

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

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

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

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

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

145 where doVivid i = i { vivid = True }

146 doDull i = i { vivid = False }

147 doUnderline i = i { underline = True }

148 doNoUnderline i = i { underline = False }

149 doBold i = i { bold = True }

150 doNoBold i = i { bold = False }

151 doItalic i = i { italic = True }

152 doNoItalic i = i { italic = False }

153 doSetColour c i = i { colour = c }

154

155

156colourTypes :: [(String, ColourType)]

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

158 enumFromTo minBound maxBound

159

160pColourType :: P.IdrisParser ColourType

161pColourType = doColourType colourTypes

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

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

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

165

166pSetColourCmd :: P.IdrisParser Command

167pSetColourCmd = (do c <- pColourType

168 let defaultColour = IdrisColour Nothing True False False False

169 opts <- sepBy pColourMod (P.whiteSpace)

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

171 return $ SetColour c colour)

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

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