src/Idris/REPLParser.hs · Idris-dev

1

2module Idris.REPLParser(parseCmd) where

3

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

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

6

7import Idris.Colours

8import Idris.AbsSyntax

9import Idris.Core.TT

10import qualified Idris.Parser as P

11

12import Control.Applicative

13import Control.Monad.State.Strict

14

15import Text.Parser.Combinators

16import Text.Parser.Char(anyChar)

17import Text.Trifecta(Result, parseString)

18import Text.Trifecta.Delta

19

20import Debug.Trace

21import Data.List

22import Data.List.Split(splitOn)

23import Data.Char(toLower)

24import qualified Data.ByteString.UTF8 as UTF8

25

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

27parseCmd i inputname = P.runparser pCmd i inputname

28

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

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

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

32 docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs

33

34pCmd :: P.IdrisParser Command

35

36pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

37 <|> do cmd ["h", "?", "help"]; eof; return Help

38 <|> do cmd ["w", "warranty"]; eof; return Warranty

39 <|> do cmd ["r", "reload"]; eof; return Reload

40 <|> do cmd ["module"]; f <- P.identifier; eof;

41 return (ModImport (toPath f))

42 <|> do cmd ["e", "edit"]; eof; return Edit

43 <|> do cmd ["exec", "execute"]; eof; return Execute

44 <|> do cmd ["c", "compile"]

45 i <- get

46 c <- option (opt_codegen $ idris_options i) codegenOption

47 f <- P.identifier

48 eof

49 return (Compile c f)

50 <|> do cmd ["proofs"]; eof; return Proofs

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

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

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

54 <|> do cmd ["let"]

55 defn <- concat <$> many (P.decl defaultSyntax)

56 return (NewDefn defn)

57 <|> do cmd ["unlet","undefine"]

58 Undefine `fmap` many P.name

59 <|> do cmd ["lto", "loadto"];

60 toline <- P.natural

61 f <- many anyChar;

62 return (Load f (Just (fromInteger toline)))

63 <|> do cmd ["l", "load"]; f <- many anyChar;

64 return (Load f Nothing)

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

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

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

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

69 <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))

70 <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))

71 <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)

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

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

74 <|> do cmd ["u", "universes"]; eof; return Universes

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

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

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

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

79 <|> do cmd ["color", "colour"]; pSetColourCmd

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

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

82 <|> do cmd ["s", "search"]; P.whiteSpace;

83 t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)

84 <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

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

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

87 return (CaseSplitAt upd (fromInteger l) n)

88 <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

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

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

91 return (AddProofClauseFrom upd (fromInteger l) n)

92 <|> do cmd ["ac", "addclause"]; P.whiteSpace;

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

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

95 return (AddClauseFrom upd (fromInteger l) n)

96 <|> do cmd ["am", "addmissing"]; P.whiteSpace;

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

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

99 return (AddMissing upd (fromInteger l) n)

100 <|> do cmd ["mw", "makewith"]; P.whiteSpace;

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

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

103 return (MakeWith upd (fromInteger l) n)

104 <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

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

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

107 return (MakeLemma upd (fromInteger l) n)

108 <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

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

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

111 hints <- many P.fnName

112 return (DoProofSearch upd True (fromInteger l) n hints)

113 <|> do cmd ["ref", "refine"]; P.whiteSpace;

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

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

116 hint <- P.fnName

117 return (DoProofSearch upd False (fromInteger l) n [hint])

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

119 <|> do cmd ["m", "metavars"]; eof; return Metavars

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

121 return (Just x))

122 eof; return (AddProof n)

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

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

125 <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers

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

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

128 <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)

129 <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

130 <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

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

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

133

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

135

136pOption :: P.IdrisParser Opt

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

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

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

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

141 <|> do discard (P.symbol "nobanner") ; return NoBanner

142 <|> do discard (P.symbol "warnreach"); return WarnReach

143

144codegenOption :: P.IdrisParser Codegen

145codegenOption = do discard (P.symbol "javascript"); return ViaJavaScript

146 <|> do discard (P.symbol "node"); return ViaNode

147 <|> do discard (P.symbol "Java"); return ViaJava

148 <|> do discard (P.symbol "llvm"); return ViaLLVM

149 <|> do discard (P.symbol "bytecode"); return Bytecode

150 <|> do discard (P.symbol "C"); return ViaC

151

152pConsoleWidth :: P.IdrisParser ConsoleWidth

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

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

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

156

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

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

159 , ("red", Just Red)

160 , ("green", Just Green)

161 , ("yellow", Just Yellow)

162 , ("blue", Just Blue)

163 , ("magenta", Just Magenta)

164 , ("cyan", Just Cyan)

165 , ("white", Just White)

166 , ("default", Nothing)

167 ]

168

169pColour :: P.IdrisParser (Maybe Color)

170pColour = doColour colours

171 where doColour [] = fail "Unknown colour"

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

173

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

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

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

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

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

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

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

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

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

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

184 where doVivid i = i { vivid = True }

185 doDull i = i { vivid = False }

186 doUnderline i = i { underline = True }

187 doNoUnderline i = i { underline = False }

188 doBold i = i { bold = True }

189 doNoBold i = i { bold = False }

190 doItalic i = i { italic = True }

191 doNoItalic i = i { italic = False }

192 doSetColour c i = i { colour = c }

193

194-- | Generate the colour type names using the default Show instance.

195colourTypes :: [(String, ColourType)]

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

197 enumFromTo minBound maxBound

198

199pColourType :: P.IdrisParser ColourType

200pColourType = doColourType colourTypes

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

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

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

204

205pSetColourCmd :: P.IdrisParser Command

206pSetColourCmd = (do c <- pColourType

207 let defaultColour = IdrisColour Nothing True False False False

208 opts <- sepBy pColourMod (P.whiteSpace)

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

210 return $ SetColour c colour)

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

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