aad7688 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Megaparsec prep (#4164)

aad7688Jason Felice9 years ago

src/Idris/Core/TT.hs−9

compare with master

unifiedsplit

@@ -1141,15 +1141,6 @@ isInjective (Bind _ (Pi _ _ _ _) sc) = True

1141isInjective (App _ f a) = isInjective f

1142isInjective _ = False

1143

1144−-- | Count the number of instances of a de Bruijn index in a term

1145−vinstances :: Int -> TT n -> Int

1146−vinstances i (V x) | i == x = 1

1147−vinstances i (App _ f a) = vinstances i f + vinstances i a

1148−vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

1149− where instancesB (Let c t v) = vinstances i v

1150− instancesB _ = 0

1151−vinstances i t = 0

1152−

1153-- | Replace the outermost (index 0) de Bruijn variable with the given term

1144-- | Replace the outermost (index 0) de Bruijn variable with the given term

1154instantiate :: TT n -> TT n -> TT n

1145instantiate :: TT n -> TT n -> TT n

1155instantiate e = subst 0 where

1146instantiate e = subst 0 where

src/Idris/IdeMode.hs+17−18

@@ -25,8 +25,8 @@ import qualified Data.Text as T

25import Numeric

26import System.IO

27import Text.Printf

28−import Text.Trifecta hiding (Err)

28+import qualified Text.Trifecta as P

29−import Text.Trifecta.Delta

29+import qualified Text.Trifecta.Delta as P

31getNChar :: Handle -> Int -> String -> IO (String)

32getNChar _ 0 s = return (reverse s)

@@ -205,28 +205,27 @@ escape = concatMap escapeChar

205 escapeChar '"' = "\\\""

206 escapeChar c = [c]

207

208−pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))

208+pSExp = SexpList <$> P.between (P.char '(') (P.char ')') (pSExp `P.sepBy` (P.char ' '))

209− return (SexpList xs)

210 <|> atom

209 <|> atom

211

210

212−atom = do string "nil"; return (SexpList [])

211+atom = SexpList [] <$ P.string "nil"

213− <|> do char ':'; x <- atomC; return x

212+ <|> P.char ':' *> atomC

214− <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

213+ <|> StringAtom <$> P.between (P.char '"') (P.char '"') (P.many quotedChar)

215− <|> do ints <- some digit

214+ <|> do ints <- some P.digit

216 case readDec ints of

215 case readDec ints of

217 ((num, ""):_) -> return (IntegerAtom (toInteger num))

216 ((num, ""):_) -> return (IntegerAtom (toInteger num))

218 _ -> return (StringAtom ints)

217 _ -> return (StringAtom ints)

219

218

220−atomC = do string "True"; return (BoolAtom True)

219+atomC = BoolAtom True <$ P.string "True"

221− <|> do string "False"; return (BoolAtom False)

220+ <|> BoolAtom False <$ P.string "False"

222− <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)

221+ <|> SymbolAtom <$> many (P.noneOf " \n\t\r\"()")

223

222

224−quotedChar = try (string "\\\\" >> return '\\')

223+quotedChar = P.try ('\\' <$ P.string "\\\\")

225− <|> try (string "\\\"" >> return '"')

224+ <|> P.try ('"' <$ P.string "\\\"")

226− <|> noneOf "\""

225+ <|> P.noneOf "\""

227

226

228−parseSExp :: String -> Result SExp

227+parseSExp :: String -> P.Result SExp

229−parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

228+parseSExp = P.parseString pSExp (P.Directed (UTF8.fromString "(unknown)") 0 0 0 0)

230

229

231data Opt = ShowImpl | ErrContext deriving Show

230data Opt = ShowImpl | ErrContext deriving Show

232

231

@@ -324,8 +323,8 @@ parseMessage x = case receiveString x of

324receiveString :: String -> Either Err SExp

323receiveString :: String -> Either Err SExp

325receiveString x =

324receiveString x =

326 case parseSExp x of

325 case parseSExp x of

327− Failure _ -> Left . Msg $ "parse failure"

326+ P.Failure _ -> Left . Msg $ "parse failure"

328− Success r -> Right r

327+ P.Success r -> Right r

329

328

330convSExp :: SExpable a => String -> a -> Integer -> String

329convSExp :: SExpable a => String -> a -> Integer -> String

331convSExp pre s id =

330convSExp pre s id =

src/Idris/Main.hs+18−19

@@ -47,7 +47,6 @@ import System.Exit

47import System.FilePath

48import System.IO

49import System.IO.CodePage (withCP65001)

50−import Text.Trifecta.Result (ErrInfo(..), Result(..))

52-- | How to run Idris programs.

51-- | How to run Idris programs.

53runMain :: Idris () -> IO ()

52runMain :: Idris () -> IO ()

@@ -196,9 +195,9 @@ idrisMain opts =

196 mapM_ (\str -> do ist <- getIState

195 mapM_ (\str -> do ist <- getIState

197 c <- colourise

196 c <- colourise

198 case parseExpr ist str of

197 case parseExpr ist str of

199− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

198+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

200− runIO $ exitWith (ExitFailure 1)

199+ runIO $ exitWith (ExitFailure 1)

201− Success e -> process "" (Eval e))

200+ Right e -> process "" (Eval e))

202 exprs

201 exprs

203 runIO exitSuccess

202 runIO exitSuccess

204

203

@@ -273,12 +272,12 @@ execScript :: String -> Idris ()

273execScript expr = do i <- getIState

272execScript expr = do i <- getIState

274 c <- colourise

273 c <- colourise

275 case parseExpr i expr of

274 case parseExpr i expr of

276− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

275+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

277− runIO $ exitWith (ExitFailure 1)

276+ runIO $ exitWith (ExitFailure 1)

278− Success term -> do ctxt <- getContext

277+ Right term -> do ctxt <- getContext

279− (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

278+ (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

280− res <- execute tm

279+ res <- execute tm

281− runIO $ exitSuccess

280+ runIO $ exitSuccess

282

281

283-- | Run the initialisation script

282-- | Run the initialisation script

284initScript :: Idris ()

283initScript :: Idris ()

@@ -300,12 +299,12 @@ initScript = do script <- runIO $ getIdrisInitScript

300 runInit h

299 runInit h

301 processLine i cmd input clr =

300 processLine i cmd input clr =

302 case parseCmd i input cmd of

301 case parseCmd i input cmd of

303− Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)

302+ Left err -> runIO . print . fixColour clr . parseErrorDoc $ err

304− Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

303+ Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

305− Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

304+ Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

306− Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

305+ Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

307− Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

306+ Right (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

308− Success (Right Proofs) -> proofs i

307+ Right (Right Proofs) -> proofs i

309− Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

308+ Right (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

310− Success (Right cmd ) -> process [] cmd

309+ Right (Right cmd ) -> process [] cmd

311− Success (Left err) -> runIO $ print err

310+ Right (Left err) -> runIO $ print err

src/Idris/Package/Parser.hs+58−152

@@ -11,7 +11,9 @@ module Idris.Package.Parser where

11import Idris.CmdOptions

12import Idris.Imports

13import Idris.Package.Common

14−import Idris.Parser.Helpers hiding (stringLiteral)

14+import Idris.Parser.Helpers (MonadicParsing, eol, iName, identifier, isEol,

15+ lchar, packageName, parseErrorDoc, reserved,

16+ runparser, someSpace')

16import Control.Applicative

18import Control.Applicative

17import Control.Monad.State.Strict

19import Control.Monad.State.Strict

@@ -20,30 +22,27 @@ import System.Directory (doesFileExist)

20import System.Exit

22import System.Exit

21import System.FilePath (isValid, takeExtension, takeFileName)

23import System.FilePath (isValid, takeExtension, takeFileName)

22import qualified Text.PrettyPrint.ANSI.Leijen as PP

24import qualified Text.PrettyPrint.ANSI.Leijen as PP

23−import Text.Trifecta hiding (char, charLiteral, natural, span, string, symbol,

25+import Text.Trifecta ((<?>))

24− whiteSpace)

26+import qualified Text.Trifecta as P

26−type PParser = StateT PkgDesc IdrisInnerParser

28+type PParser = StateT PkgDesc P.Parser

27−

28−instance HasLastTokenSpan PParser where

29− getLastTokenSpan = return Nothing

31#if MIN_VERSION_base(4,9,0)

30#if MIN_VERSION_base(4,9,0)

32−instance {-# OVERLAPPING #-} DeltaParsing PParser where

31+instance {-# OVERLAPPING #-} P.DeltaParsing PParser where

33− line = lift line

32+ line = lift P.line

34 {-# INLINE line #-}

33 {-# INLINE line #-}

35− position = lift position

34+ position = lift P.position

36 {-# INLINE position #-}

35 {-# INLINE position #-}

37− slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

36+ slicedWith f (StateT m) = StateT $ \s -> P.slicedWith (\(a,s') b -> (f a b, s')) $ m s

38 {-# INLINE slicedWith #-}

37 {-# INLINE slicedWith #-}

39− rend = lift rend

38+ rend = lift P.rend

40 {-# INLINE rend #-}

39 {-# INLINE rend #-}

41− restOfLine = lift restOfLine

40+ restOfLine = lift P.restOfLine

42 {-# INLINE restOfLine #-}

41 {-# INLINE restOfLine #-}

43#endif

42#endif

45−instance {-# OVERLAPPING #-} TokenParsing PParser where

44+instance {-# OVERLAPPING #-} P.TokenParsing PParser where

46− someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

45+ someSpace = someSpace'

49parseDesc :: FilePath -> IO PkgDesc

48parseDesc :: FilePath -> IO PkgDesc

@@ -56,8 +55,8 @@ parseDesc fp = do

56 then do

55 then do

57 p <- readFile fp

56 p <- readFile fp

58 case runparser pPkg defaultPkg fp p of

57 case runparser pPkg defaultPkg fp p of

59− Failure (ErrInfo err _) -> fail (show $ PP.plain err)

58+ Left err -> fail (show $ PP.plain $ parseErrorDoc err)

60− Success x -> return x

59+ Right x -> return x

61 else do

60 else do

62 putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]

61 putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]

63 exitWith (ExitFailure 1)

62 exitWith (ExitFailure 1)

@@ -66,12 +65,11 @@ pPkg :: PParser PkgDesc

66pPkg = do

65pPkg = do

67 reserved "package"

66 reserved "package"

68 p <- pPkgName

67 p <- pPkgName

69− someSpace

68+ someSpace'

70− st <- get

71− put (st { pkgname = p })

69+ modify $ \st -> st { pkgname = p }

72 some pClause

70 some pClause

73 st <- get

71 st <- get

74− eof

72+ P.eof

75 return st

73 return st

77pPkgName :: PParser PkgName

75pPkgName :: PParser PkgName

@@ -80,18 +78,16 @@ pPkgName = (either fail pure . pkgName =<< packageName) <?> "PkgName"

80-- | Parses a filename.

78-- | Parses a filename.

81-- |

79-- |

82-- | Treated for now as an identifier or a double-quoted string.

80-- | Treated for now as an identifier or a double-quoted string.

83−filename :: (MonadicParsing m, HasLastTokenSpan m) => m String

81+filename :: (MonadicParsing m) => m String

84filename = (do

82filename = (do

85− filename <- token $

86− -- Treat a double-quoted string as a filename to support spaces.

83+ -- Treat a double-quoted string as a filename to support spaces.

87− -- This also moves away from tying filenames to identifiers, so

84+ -- This also moves away from tying filenames to identifiers, so

88− -- it will also accept hyphens

85+ -- it will also accept hyphens

89− -- (https://github.com/idris-lang/Idris-dev/issues/2721)

86+ -- (https://github.com/idris-lang/Idris-dev/issues/2721)

90− stringLiteral

87+ filename <- P.stringLiteral <* someSpace'

91− <|>

92− -- Through at least version 0.9.19.1, IPKG executable values were

88+ -- Through at least version 0.9.19.1, IPKG executable values were

93− -- possibly namespaced identifiers, like foo.bar.baz.

89+ -- possibly namespaced identifiers, like foo.bar.baz.

94− show <$> fst <$> iName []

90+ <|> show . fst <$> iName []

95 case filenameErrorMessage filename of

91 case filenameErrorMessage filename of

96 Just errorMessage -> fail errorMessage

92 Just errorMessage -> fail errorMessage

97 Nothing -> return filename)

93 Nothing -> return filename)

@@ -119,126 +115,36 @@ filename = (do

119 checkThat (path == takeFileName path)

115 checkThat (path == takeFileName path)

120 "filename must contain no directory component"

116 "filename must contain no directory component"

121

117

118+textUntilEol :: MonadicParsing m => m String

119+textUntilEol = many (P.satisfy (not . isEol)) <* eol <* someSpace'

120+

121+clause :: String -> PParser a -> (PkgDesc -> a -> PkgDesc) -> PParser ()

122+clause name p f = do value <- reserved name *> lchar '=' *> p <* someSpace'

123+ modify $ \st -> f st value

124+

125+commaSep :: MonadicParsing m => m a -> m [a]

126+commaSep p = P.sepBy1 p (lchar ',')

122

127

123pClause :: PParser ()

128pClause :: PParser ()

124−pClause = do reserved "executable"; lchar '=';

129+pClause = clause "executable" filename (\st v -> st { execout = Just v })

125− exec <- filename

126− st <- get

127− put (st { execout = Just exec })

128−

129− <|> do reserved "main"; lchar '=';

130− main <- fst <$> iName []

131− st <- get

132− put (st { idris_main = Just main })

130+ <|> clause "main" (fst <$> iName []) (\st v -> st { idris_main = Just v })

133−

134− <|> do reserved "sourcedir"; lchar '=';

135− src <- fst <$> identifier

131+ <|> clause "sourcedir" (fst <$> identifier) (\st v -> st { sourcedir = v })

136− st <- get

137− put (st { sourcedir = src })

138−

139− <|> do reserved "opts"; lchar '=';

140− opts <- stringLiteral

141− st <- get

142− let args = pureArgParser (words opts)

143− put (st { idris_opts = args ++ idris_opts st })

132+ <|> clause "opts" (pureArgParser . words <$> P.stringLiteral) (\st v -> st { idris_opts = v ++ idris_opts st })

144−

145− <|> do reserved "pkgs"; lchar '=';

146− ps <- sepBy1 (pPkgName <* someSpace) (lchar ',')

133+ <|> clause "pkgs" (commaSep (pPkgName <* someSpace')) (\st ps ->

147− st <- get

148 let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps

134 let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps

149−

150− put (st { pkgdeps = ps `union` (pkgdeps st)

135+ in st { pkgdeps = ps `union` pkgdeps st

151− , idris_opts = pkgs ++ idris_opts st})

136+ , idris_opts = pkgs ++ idris_opts st })

152−

153− <|> do reserved "modules"; lchar '=';

154− ms <- sepBy1 (fst <$> iName []) (lchar ',')

155− st <- get

156− put (st { modules = modules st ++ ms })

137+ <|> clause "modules" (commaSep (fst <$> iName [])) (\st v -> st { modules = modules st ++ v })

157−

158− <|> do reserved "libs"; lchar '=';

159− ls <- sepBy1 (fst <$> identifier) (lchar ',')

160− st <- get

161− put (st { libdeps = libdeps st ++ ls })

138+ <|> clause "libs" (commaSep (fst <$> identifier)) (\st v -> st { libdeps = libdeps st ++ v })

162−

139+ <|> clause "objs" (commaSep (fst <$> identifier)) (\st v -> st { objs = objs st ++ v })

163− <|> do reserved "objs"; lchar '=';

164− ls <- sepBy1 (fst <$> identifier) (lchar ',')

165− st <- get

166− put (st { objs = objs st ++ ls })

167−

168− <|> do reserved "makefile"; lchar '=';

169− mk <- fst <$> iName []

170− st <- get

171− put (st { makefile = Just (show mk) })

140+ <|> clause "makefile" (fst <$> iName []) (\st v -> st { makefile = Just (show v) })

172−

173− <|> do reserved "tests"; lchar '=';

174− ts <- sepBy1 (fst <$> iName []) (lchar ',')

175− st <- get

176− put st { idris_tests = idris_tests st ++ ts }

141+ <|> clause "tests" (commaSep (fst <$> iName [])) (\st v -> st { idris_tests = idris_tests st ++ v })

177−

178− <|> do reserved "version"

179− lchar '='

180− vStr <- many (satisfy (not . isEol))

181− eol

182− someSpace

183− st <- get

184− put st {pkgversion = Just vStr}

142+ <|> clause "version" textUntilEol (\st v -> st { pkgversion = Just v })

185−

186− <|> do reserved "readme"

187− lchar '='

188− rme <- many (satisfy (not . isEol))

189− eol

190− someSpace

191− st <- get

192− put (st { pkgreadme = Just rme })

143+ <|> clause "readme" textUntilEol (\st v -> st { pkgreadme = Just v })

193−

194− <|> do reserved "license"

195− lchar '='

196− lStr <- many (satisfy (not . isEol))

197− eol

198− st <- get

199− put st {pkglicense = Just lStr}

144+ <|> clause "license" textUntilEol (\st v -> st { pkglicense = Just v })

200−

201− <|> do reserved "homepage"

202− lchar '='

203− www <- many (satisfy (not . isEol))

204− eol

205− someSpace

206− st <- get

207− put st {pkghomepage = Just www}

145+ <|> clause "homepage" textUntilEol (\st v -> st { pkghomepage = Just v })

208−

209− <|> do reserved "sourceloc"

210− lchar '='

211− srcpage <- many (satisfy (not . isEol))

212− eol

213− someSpace

214− st <- get

215− put st {pkgsourceloc = Just srcpage}

146+ <|> clause "sourceloc" textUntilEol (\st v -> st { pkgsourceloc = Just v })

216−

217− <|> do reserved "bugtracker"

218− lchar '='

219− src <- many (satisfy (not . isEol))

220− eol

221− someSpace

222− st <- get

223− put st {pkgbugtracker = Just src}

147+ <|> clause "bugtracker" textUntilEol (\st v -> st { pkgbugtracker = Just v })

224−

225− <|> do reserved "brief"

226− lchar '='

227− brief <- stringLiteral

228− st <- get

229− someSpace

230− put st {pkgbrief = Just brief}

148+ <|> clause "brief" P.stringLiteral (\st v -> st { pkgbrief = Just v })

231−

232− <|> do reserved "author"; lchar '=';

233− author <- many (satisfy (not . isEol))

234− eol

235− someSpace

236− st <- get

237− put st {pkgauthor = Just author}

149+ <|> clause "author" textUntilEol (\st v -> st { pkgauthor = Just v })

238−

239− <|> do reserved "maintainer"; lchar '=';

240− maintainer <- many (satisfy (not . isEol))

241− eol

242− someSpace

243− st <- get

244− put st {pkgmaintainer = Just maintainer}

150+ <|> clause "maintainer" textUntilEol (\st v -> st { pkgmaintainer = Just v })

src/Idris/Parser.hs+180−203

@@ -14,7 +14,7 @@ Maintainer : The Idris Community.

15module Idris.Parser(IdrisParser(..), ImportInfo(..), addReplSyntax, clearParserWarnings,

16 decl, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,

17− runparser) where

17+ runparser, ParseError, parseErrorDoc) where

19import Idris.AbsSyntax hiding (namespace, params)

20import Idris.Core.Evaluate

@@ -36,7 +36,7 @@ import Idris.Parser.Ops

36import Idris.Termination

37import Idris.Unlit

39−import qualified Util.Pretty as P

39+import qualified Util.Pretty

40import Util.System (readSource)

42import Prelude hiding (pi)

@@ -57,11 +57,10 @@ import Data.Ord

57import qualified Data.Text as T

58import qualified System.Directory as Dir (makeAbsolute)

59import System.FilePath

60−import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

61−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

60+import qualified Text.PrettyPrint.ANSI.Leijen as PP

62−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

61+import Text.Trifecta ((<?>))

63− stringLiteral, symbol, whiteSpace)

62+import qualified Text.Trifecta as P

64−import Text.Trifecta.Delta

63+import qualified Text.Trifecta.Delta as P

66{-

65{-

67@

66@

@@ -84,17 +83,17 @@ import Text.Trifecta.Delta

84@

83@

85-}

84-}

86moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

85moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

87−moduleHeader = try (do docs <- optional docComment

86+moduleHeader = P.try (do docs <- optional docComment

88− noArgs docs

87+ noArgs docs

89− reservedHL "module"

88+ reservedHL "module"

90− (i, ifc) <- identifier

89+ (i, ifc) <- identifier

91− option ';' (lchar ';')

90+ P.option ';' (lchar ';')

92− let modName = moduleName i

91+ let modName = moduleName i

93− return (fmap fst docs,

92+ return (fmap fst docs,

94− modName,

93+ modName,

95− [(ifc, AnnNamespace (map T.pack modName) Nothing)]))

94+ [(ifc, AnnNamespace (map T.pack modName) Nothing)]))

96− <|> try (do lchar '%'; reserved "unqualified"

95+ <|> P.try (do lchar '%'; reserved "unqualified"

97− return (Nothing, [], []))

96+ return (Nothing, [], []))

98 <|> return (Nothing, moduleName "Main", [])

97 <|> return (Nothing, moduleName "Main", [])

99 where moduleName x = case span (/='.') x of

98 where moduleName x = case span (/='.') x of

100 (x, "") -> [x]

99 (x, "") -> [x]

@@ -119,12 +118,11 @@ data ImportInfo = ImportInfo { import_reexport :: Bool

119import_ :: IdrisParser ImportInfo

118import_ :: IdrisParser ImportInfo

120import_ = do fc <- getFC

119import_ = do fc <- getFC

121 reservedHL "import"

120 reservedHL "import"

122− reexport <- option False (do reservedHL "public"

121+ reexport <- P.option False (True <$ reservedHL "public")

123− return True)

124 (id, idfc) <- identifier

122 (id, idfc) <- identifier

125 newName <- optional (do reservedHL "as"

123 newName <- optional (do reservedHL "as"

126 identifier)

124 identifier)

127− option ';' (lchar ';')

125+ P.option ';' (lchar ';')

128 return $ ImportInfo reexport (toPath id)

126 return $ ImportInfo reexport (toPath id)

129 (fmap (\(n, fc) -> (toPath n, fc)) newName)

127 (fmap (\(n, fc) -> (toPath n, fc)) newName)

130 (map T.pack $ ns id) fc idfc

128 (map T.pack $ ns id) fc idfc

@@ -143,7 +141,7 @@ prog syn = do whiteSpace

143 decls <- many (decl syn)

141 decls <- many (decl syn)

144 let c = concat decls

142 let c = concat decls

145 case maxline syn of

143 case maxline syn of

146− Nothing -> do notOpenBraces; eof

144+ Nothing -> do notOpenBraces; P.eof

147 _ -> return ()

145 _ -> return ()

148 ist <- get

146 ist <- get

149 fc <- getFC

147 fc <- getFC

@@ -172,7 +170,7 @@ Decl ::=

172@

170@

173-}

171-}

174decl :: SyntaxInfo -> IdrisParser [PDecl]

172decl :: SyntaxInfo -> IdrisParser [PDecl]

175−decl syn = try (externalDecl syn)

173+decl syn = P.try (externalDecl syn)

176 <|> internalDecl syn

174 <|> internalDecl syn

177 <?> "declaration"

175 <?> "declaration"

178

176

@@ -195,13 +193,13 @@ internalDecl syn

195 if continue then

193 if continue then

196 do notEndBlock

194 do notEndBlock

197 declBody continue

195 declBody continue

198− else try (do notEndBlock

196+ else P.try (do notEndBlock

199− declBody continue)

197+ declBody continue)

200 <|> fail "End of readable input"

198 <|> fail "End of readable input"

201 where declBody :: Bool -> IdrisParser [PDecl]

199 where declBody :: Bool -> IdrisParser [PDecl]

202 declBody b =

200 declBody b =

203− try (implementation True syn)

201+ P.try (implementation True syn)

204− <|> try (openInterface syn)

202+ <|> P.try (openInterface syn)

205 <|> declBody' b

203 <|> declBody' b

206 <|> using_ syn

204 <|> using_ syn

207 <|> params syn

205 <|> params syn

@@ -276,9 +274,9 @@ declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

276declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

274declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

277 -> IdrisParser [PDecl]

275 -> IdrisParser [PDecl]

278declExtension syn ns rules =

276declExtension syn ns rules =

279− choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

277+ P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

280 case head rs of -- can never be []

278 case head rs of -- can never be []

281− DeclRule (symb:_) _ -> try $ do

279+ DeclRule (symb:_) _ -> P.try $ do

282 n <- extSymbol symb

280 n <- extSymbol symb

283 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

281 declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

284 -- If we have more than one Rule in this bucket, our grammar is

282 -- If we have more than one Rule in this bucket, our grammar is

@@ -427,28 +425,28 @@ SyntaxSym ::= '[' Name_t ']'

427-}

425-}

428syntaxRule :: SyntaxInfo -> IdrisParser Syntax

426syntaxRule :: SyntaxInfo -> IdrisParser Syntax

429syntaxRule syn

427syntaxRule syn

430− = do sty <- try (do

428+ = do sty <- P.try (do

431 pushIndent

429 pushIndent

432− sty <- option AnySyntax

430+ sty <- P.option AnySyntax

433− (do reservedHL "term"; return TermSyntax

431+ (TermSyntax <$ reservedHL "term"

434− <|> do reservedHL "pattern"; return PatternSyntax)

432+ <|> PatternSyntax <$ reservedHL "pattern")

435 reservedHL "syntax"

433 reservedHL "syntax"

436 return sty)

434 return sty)

437 syms <- some syntaxSym

435 syms <- some syntaxSym

438− when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

436+ when (all isExpr syms) $ P.unexpected "missing keywords in syntax rule"

439 let ns = mapMaybe getName syms

437 let ns = mapMaybe getName syms

440 when (length ns /= length (nub ns))

438 when (length ns /= length (nub ns))

441− $ unexpected "repeated variable in syntax rule"

439+ $ P.unexpected "repeated variable in syntax rule"

442 lchar '='

440 lchar '='

443 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

441 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

444 terminator

442 terminator

445 return (Rule (mkSimple syms) tm sty)

443 return (Rule (mkSimple syms) tm sty)

446 <|> do reservedHL "decl"; reservedHL "syntax"

444 <|> do reservedHL "decl"; reservedHL "syntax"

447 syms <- some syntaxSym

445 syms <- some syntaxSym

448− when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

446+ when (all isExpr syms) $ P.unexpected "missing keywords in syntax rule"

449 let ns = mapMaybe getName syms

447 let ns = mapMaybe getName syms

450 when (length ns /= length (nub ns))

448 when (length ns /= length (nub ns))

451− $ unexpected "repeated variable in syntax rule"

449+ $ P.unexpected "repeated variable in syntax rule"

452 lchar '='

450 lchar '='

453 openBlock

451 openBlock

454 dec <- some (decl syn)

452 dec <- some (decl syn)

@@ -544,10 +542,10 @@ SyntaxSym ::= '[' Name_t ']'

544@

542@

545 -}

543 -}

546syntaxSym :: IdrisParser SSymbol

544syntaxSym :: IdrisParser SSymbol

547−syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'

545+syntaxSym = P.try (do lchar '['; n <- fst <$> name; lchar ']'

548− return (Expr n))

546+ return (Expr n))

549− <|> try (do lchar '{'; n <- fst <$> name; lchar '}'

547+ <|> P.try (do lchar '{'; n <- fst <$> name; lchar '}'

550− return (Binding n))

548+ return (Binding n))

551 <|> do n <- fst <$> iName []

549 <|> do n <- fst <$> iName []

552 return (Keyword n)

550 return (Keyword n)

553 <|> do sym <- fmap fst stringLiteral

551 <|> do sym <- fmap fst stringLiteral

@@ -561,11 +559,11 @@ syntaxSym = try (do lchar '['; n <- fst <$> name; lchar ']'

561@

559@

562-}

560-}

563fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

561fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

564−fnDecl syn = try (do notEndBlock

562+fnDecl syn = P.try (do notEndBlock

565− d <- fnDecl' syn

563+ d <- fnDecl' syn

566− i <- get

564+ i <- get

567− let d' = fmap (desugar syn i) d

565+ let d' = fmap (desugar syn i) d

568− return [d']) <?> "function declaration"

566+ return [d']) <?> "function declaration"

569

567

570{-| Parses a function declaration

568{-| Parses a function declaration

571

569

@@ -580,7 +578,7 @@ fnDecl syn = try (do notEndBlock

580-}

578-}

581fnDecl' :: SyntaxInfo -> IdrisParser PDecl

579fnDecl' :: SyntaxInfo -> IdrisParser PDecl

582fnDecl' syn = checkDeclFixity $

580fnDecl' syn = checkDeclFixity $

583− do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

581+ do (doc, argDocs, fc, opts', n, nfc, acc) <- P.try (do

584 pushIndent

582 pushIndent

585 (doc, argDocs) <- docstring syn

583 (doc, argDocs) <- docstring syn

586 (opts, acc) <- fnOpts

584 (opts, acc) <- fnOpts

@@ -658,41 +656,32 @@ NameTimesList ::=

658-}

656-}

659fnOpt :: IdrisParser FnOpt

657fnOpt :: IdrisParser FnOpt

660fnOpt = do reservedHL "total"; return TotalFn

658fnOpt = do reservedHL "total"; return TotalFn

661− <|> do reservedHL "partial"; return PartialFn

659+ <|> PartialFn <$ reservedHL "partial"

662− <|> do reservedHL "covering"; return CoveringFn

660+ <|> CoveringFn <$ reservedHL "covering"

663− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

661+ <|> do P.try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

664− return $ CExport c

662+ return $ CExport c

665− <|> do try (lchar '%' *> reserved "no_implicit");

663+ <|> NoImplicit <$ P.try (lchar '%' *> reserved "no_implicit")

666− return NoImplicit

667− <|> do try (lchar '%' *> reserved "inline");

664+ <|> Inlinable <$ P.try (lchar '%' *> reserved "inline")

668− return Inlinable

665+ <|> StaticFn <$ P.try (lchar '%' *> reserved "static")

669− <|> do try (lchar '%' *> reserved "static");

670− return StaticFn

671− <|> do try (lchar '%' *> reserved "assert_total");

666+ <|> do P.try (lchar '%' *> reserved "assert_total");

672 fc <- getFC

667 fc <- getFC

673 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")

668 parserWarning fc Nothing (Msg "%assert_total is deprecated. Use the 'assert_total' function instead.")

674 return AssertTotal

669 return AssertTotal

675− <|> do try (lchar '%' *> reserved "error_handler");

670+ <|> ErrorHandler <$ P.try (lchar '%' *> reserved "error_handler")

676− return ErrorHandler

677− <|> do try (lchar '%' *> reserved "error_reverse");

671+ <|> ErrorReverse <$ P.try (lchar '%' *> reserved "error_reverse")

678− return ErrorReverse

679− <|> do try (lchar '%' *> reserved "error_reduce");

672+ <|> ErrorReduce <$ P.try (lchar '%' *> reserved "error_reduce")

680− return ErrorReduce

681− <|> do try (lchar '%' *> reserved "reflection");

682− return Reflection

683− <|> do try (lchar '%' *> reserved "hint");

673+ <|> Reflection <$ P.try (lchar '%' *> reserved "reflection")

684− return AutoHint

685− <|> do try (lchar '%' *> reserved "overlapping");

674+ <|> AutoHint <$ P.try (lchar '%' *> reserved "hint")

686− return OverlappingDictionary

675+ <|> OverlappingDictionary <$ P.try (lchar '%' *> reserved "overlapping")

687 <|> do lchar '%'; reserved "specialise";

676 <|> do lchar '%'; reserved "specialise";

688− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';

677+ lchar '['; ns <- P.sepBy nameTimes (lchar ','); lchar ']';

689 return $ Specialise ns

678 return $ Specialise ns

690− <|> do reservedHL "implicit"; return Implicit

679+ <|> Implicit <$ reservedHL "implicit"

691 <?> "function modifier"

680 <?> "function modifier"

692 where nameTimes :: IdrisParser (Name, Maybe Int)

681 where nameTimes :: IdrisParser (Name, Maybe Int)

693 nameTimes = do n <- fst <$> fnName

682 nameTimes = do n <- fst <$> fnName

694− t <- option Nothing (do reds <- fmap fst natural

683+ t <- P.option Nothing (do reds <- fmap fst natural

695− return (Just (fromInteger reds)))

684+ return (Just (fromInteger reds)))

696 return (n, t)

685 return (n, t)

697

686

698{-| Parses a postulate

687{-| Parses a postulate

@@ -705,10 +694,10 @@ Postulate ::=

705-}

694-}

706postulate :: SyntaxInfo -> IdrisParser PDecl

695postulate :: SyntaxInfo -> IdrisParser PDecl

707postulate syn = do (doc, ext)

696postulate syn = do (doc, ext)

708− <- try $ do (doc, _) <- docstring syn

697+ <- P.try $ do (doc, _) <- docstring syn

709− pushIndent

698+ pushIndent

710− ext <- ppostDecl

699+ ext <- ppostDecl

711− return (doc, ext)

700+ return (doc, ext)

712 ist <- get

701 ist <- get

713 (opts, acc) <- fnOpts

702 (opts, acc) <- fnOpts

714 (n_in, nfc) <- fnName

703 (n_in, nfc) <- fnName

@@ -768,7 +757,7 @@ openInterface syn =

768 do reservedHL "using"

757 do reservedHL "using"

769 reservedHL "implementation"

758 reservedHL "implementation"

770 fc <- getFC

759 fc <- getFC

771− ns <- sepBy1 fnName (lchar ',')

760+ ns <- P.sepBy1 fnName (lchar ',')

772

761

773 openBlock

762 openBlock

774 ds <- many (decl syn)

763 ds <- many (decl syn)

@@ -848,14 +837,14 @@ InterfaceBlock ::=

848interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

837interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

849interfaceBlock syn = do reservedHL "where"

838interfaceBlock syn = do reservedHL "where"

850 openBlock

839 openBlock

851− (cn, cd) <- option (Nothing, emptyDocstring) $

840+ (cn, cd) <- P.option (Nothing, emptyDocstring) $

852− try (do (doc, _) <- option noDocs docComment

841+ P.try (do (doc, _) <- P.option noDocs docComment

853− n <- constructor

842+ n <- constructor

854− return (Just n, doc))

843+ return (Just n, doc))

855 ist <- get

844 ist <- get

856 let cd' = annotate syn ist cd

845 let cd' = annotate syn ist cd

857

846

858− ds <- many (notEndBlock >> try (implementation True syn)

847+ ds <- many (notEndBlock >> P.try (implementation True syn)

859 <|> do x <- data_ syn

848 <|> do x <- data_ syn

860 return [x]

849 return [x]

861 <|> fnDecl syn)

850 <|> fnDecl syn)

@@ -886,24 +875,24 @@ Interface ::=

886-}

875-}

887interface_ :: SyntaxInfo -> IdrisParser [PDecl]

876interface_ :: SyntaxInfo -> IdrisParser [PDecl]

888interface_ syn = do (doc, argDocs, acc)

877interface_ syn = do (doc, argDocs, acc)

889− <- try (do (doc, argDocs) <- docstring syn

878+ <- P.try (do (doc, argDocs) <- docstring syn

890− acc <- accessibility

879+ acc <- accessibility

891− interfaceKeyword

880+ interfaceKeyword

892− return (doc, argDocs, acc))

881+ return (doc, argDocs, acc))

893 fc <- getFC

882 fc <- getFC

894 cons <- constraintList syn

883 cons <- constraintList syn

895 let cons' = [(c, ty) | (_, c, _, ty) <- cons]

884 let cons' = [(c, ty) | (_, c, _, ty) <- cons]

896 (n_in, nfc) <- fnName

885 (n_in, nfc) <- fnName

897 let n = expandNS syn n_in

886 let n = expandNS syn n_in

898 cs <- many carg

887 cs <- many carg

899− fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

888+ fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

900− (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)

889+ (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)

901 accData acc n (concatMap declared ds)

890 accData acc n (concatMap declared ds)

902 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]

891 return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]

903 <?> "interface declaration"

892 <?> "interface declaration"

904 where

893 where

905 fundeps :: IdrisParser [(Name, FC)]

894 fundeps :: IdrisParser [(Name, FC)]

906− fundeps = do lchar '|'; sepBy name (lchar ',')

895+ fundeps = do lchar '|'; P.sepBy name (lchar ',')

907

896

908 interfaceKeyword :: IdrisParser ()

897 interfaceKeyword :: IdrisParser ()

909 interfaceKeyword = reservedHL "interface"

898 interfaceKeyword = reservedHL "interface"

@@ -964,7 +953,7 @@ implementation kwopt syn

964

953

965 implementationUsing :: IdrisParser [Name]

954 implementationUsing :: IdrisParser [Name]

966 implementationUsing = do reservedHL "using"

955 implementationUsing = do reservedHL "using"

967− ns <- sepBy1 fnName (lchar ',')

956+ ns <- P.sepBy1 fnName (lchar ',')

968 return (map fst ns)

957 return (map fst ns)

969 <|> return []

958 <|> return []

970

959

@@ -972,7 +961,7 @@ implementation kwopt syn

972docstring :: SyntaxInfo

961docstring :: SyntaxInfo

973 -> IdrisParser (Docstring (Either Err PTerm),

962 -> IdrisParser (Docstring (Either Err PTerm),

974 [(Name,Docstring (Either Err PTerm))])

963 [(Name,Docstring (Either Err PTerm))])

975−docstring syn = do (doc, argDocs) <- option noDocs docComment

964+docstring syn = do (doc, argDocs) <- P.option noDocs docComment

976 ist <- get

965 ist <- get

977 let doc' = annotCode (tryFullExpr syn ist) doc

966 let doc' = annotCode (tryFullExpr syn ist) doc

978 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

967 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

@@ -1005,8 +994,8 @@ NameList ::=

1005-}

994-}

1006usingDeclList :: SyntaxInfo -> IdrisParser [Using]

995usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1007usingDeclList syn

996usingDeclList syn

1008− = try (sepBy1 (usingDecl syn) (lchar ','))

997+ = P.try (P.sepBy1 (usingDecl syn) (lchar ','))

1009− <|> do ns <- sepBy1 (fst <$> name) (lchar ',')

998+ <|> do ns <- P.sepBy1 (fst <$> name) (lchar ',')

1010 lchar ':'

999 lchar ':'

1011 t <- typeExpr (disallowImp syn)

1000 t <- typeExpr (disallowImp syn)

1012 return (map (\x -> UImplicit x t) ns)

1001 return (map (\x -> UImplicit x t) ns)

@@ -1022,10 +1011,10 @@ UsingDecl ::=

1022@

1011@

1023-}

1012-}

1024usingDecl :: SyntaxInfo -> IdrisParser Using

1013usingDecl :: SyntaxInfo -> IdrisParser Using

1025−usingDecl syn = try (do x <- fst <$> fnName

1014+usingDecl syn = P.try (do x <- fst <$> fnName

1026− lchar ':'

1015+ lchar ':'

1027− t <- typeExpr (disallowImp syn)

1016+ t <- typeExpr (disallowImp syn)

1028− return (UImplicit x t))

1017+ return (UImplicit x t))

1029 <|> do c <- fst <$> fnName

1018 <|> do c <- fst <$> fnName

1030 xs <- many (fst <$> fnName)

1019 xs <- many (fst <$> fnName)

1031 return (UConstraint c xs)

1020 return (UConstraint c xs)

@@ -1068,7 +1057,7 @@ ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

1068-}

1057-}

1069argExpr :: SyntaxInfo -> IdrisParser PTerm

1058argExpr :: SyntaxInfo -> IdrisParser PTerm

1070argExpr syn = let syn' = syn { inPattern = True } in

1059argExpr syn = let syn' = syn { inPattern = True } in

1071− try (hsimpleExpr syn') <|> simpleExternalExpr syn'

1060+ P.try (hsimpleExpr syn') <|> simpleExternalExpr syn'

1072 <?> "argument expression"

1061 <?> "argument expression"

1073

1062

1074{-| Parse a right hand side of a function

1063{-| Parse a right hand side of a function

@@ -1090,8 +1079,8 @@ rhs syn n = do lchar '='

1090 expr syn

1079 expr syn

1091 <|> do symbol "?=";

1080 <|> do symbol "?=";

1092 fc <- getFC

1081 fc <- getFC

1093− name <- option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";

1082+ name <- P.option n' (do symbol "{"; n <- fst <$> fnName; symbol "}";

1094− return n)

1083+ return n)

1095 r <- expr syn

1084 r <- expr syn

1096 return (addLet fc name r)

1085 return (addLet fc name r)

1097 <|> impossible

1086 <|> impossible

@@ -1135,7 +1124,7 @@ WhereOrTerminator ::= WhereBlock | Terminator;

1135-}

1124-}

1136clause :: SyntaxInfo -> IdrisParser PClause

1125clause :: SyntaxInfo -> IdrisParser PClause

1137clause syn

1126clause syn

1138− = do wargs <- try (do pushIndent; some (wExpr syn))

1127+ = do wargs <- P.try (do pushIndent; some (wExpr syn))

1139 fc <- getFC

1128 fc <- getFC

1140 ist <- get

1129 ist <- get

1141 n <- case lastParse ist of

1130 n <- case lastParse ist of

@@ -1143,11 +1132,8 @@ clause syn

1143 Nothing -> fail "Invalid clause"

1132 Nothing -> fail "Invalid clause"

1144 (do r <- rhs syn n

1133 (do r <- rhs syn n

1145 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1134 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1146− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1135+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1147− popIndent

1148− return x,

1149− do terminator

1136+ <|> ([], []) <$ terminator

1150− return ([], [])]

1151 return $ PClauseR fc wargs r wheres) <|> (do

1137 return $ PClauseR fc wargs r wheres) <|> (do

1152 popIndent

1138 popIndent

1153 reservedHL "with"

1139 reservedHL "with"

@@ -1158,19 +1144,16 @@ clause syn

1158 let withs = concat ds

1144 let withs = concat ds

1159 closeBlock

1145 closeBlock

1160 return $ PWithR fc wargs wval pn withs)

1146 return $ PWithR fc wargs wval pn withs)

1161− <|> do ty <- try (do pushIndent

1147+ <|> do ty <- P.try (do pushIndent

1162− ty <- simpleExpr syn

1148+ ty <- simpleExpr syn

1163− symbol "<=="

1149+ symbol "<=="

1164− return ty)

1150+ return ty)

1165 fc <- getFC

1151 fc <- getFC

1166 n_in <- fst <$> fnName; let n = expandNS syn n_in

1152 n_in <- fst <$> fnName; let n = expandNS syn n_in

1167 r <- rhs syn n

1153 r <- rhs syn n

1168 let wsyn = syn { syn_namespace = [] }

1154 let wsyn = syn { syn_namespace = [] }

1169− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1155+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1170− popIndent

1171− return x,

1172− do terminator

1156+ <|> ([], []) <$ terminator

1173− return ([], [])]

1174 let capp = PLet fc RigW (sMN 0 "match") NoFC

1157 let capp = PLet fc RigW (sMN 0 "match") NoFC

1175 ty

1158 ty

1176 (PMatchApp fc n)

1159 (PMatchApp fc n)

@@ -1178,7 +1161,7 @@ clause syn

1178 ist <- get

1161 ist <- get

1179 put (ist { lastParse = Just n })

1162 put (ist { lastParse = Just n })

1180 return $ PClause fc n capp [] r wheres

1163 return $ PClause fc n capp [] r wheres

1181− <|> do (l, op, nfc) <- try (do

1164+ <|> do (l, op, nfc) <- P.try (do

1182 pushIndent

1165 pushIndent

1183 l <- argExpr syn

1166 l <- argExpr syn

1184 (op, nfc) <- symbolicOperatorFC

1167 (op, nfc) <- symbolicOperatorFC

@@ -1191,11 +1174,8 @@ clause syn

1191 wargs <- many (wExpr syn)

1174 wargs <- many (wExpr syn)

1192 (do rs <- rhs syn n

1175 (do rs <- rhs syn n

1193 let wsyn = syn { syn_namespace = [] }

1176 let wsyn = syn { syn_namespace = [] }

1194− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1177+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1195− popIndent

1196− return x,

1197− do terminator

1178+ <|> ([], []) <$ terminator

1198− return ([], [])]

1199 ist <- get

1179 ist <- get

1200 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

1180 let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

1201 put (ist { lastParse = Just n })

1181 put (ist { lastParse = Just n })

@@ -1215,18 +1195,15 @@ clause syn

1215 <|> do pushIndent

1195 <|> do pushIndent

1216 (n_in, nfc) <- fnName; let n = expandNS syn n_in

1196 (n_in, nfc) <- fnName; let n = expandNS syn n_in

1217 fc <- getFC

1197 fc <- getFC

1218− args <- many (try (implicitArg (syn { inPattern = True } ))

1198+ args <- many (P.try (implicitArg (syn { inPattern = True } ))

1219− <|> try (constraintArg (syn { inPattern = True }))

1199+ <|> P.try (constraintArg (syn { inPattern = True }))

1220 <|> (fmap pexp (argExpr syn)))

1200 <|> (fmap pexp (argExpr syn)))

1221 wargs <- many (wExpr syn)

1201 wargs <- many (wExpr syn)

1222 let capp = PApp fc (PRef nfc [nfc] n) args

1202 let capp = PApp fc (PRef nfc [nfc] n) args

1223 (do r <- rhs syn n

1203 (do r <- rhs syn n

1224 let wsyn = syn { syn_namespace = [] }

1204 let wsyn = syn { syn_namespace = [] }

1225− (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1205+ (wheres, nmap) <- whereBlock n wsyn <* popIndent

1226− popIndent

1227− return x,

1228− do terminator

1206+ <|> ([], []) <$ terminator

1229− return ([], [])]

1230 ist <- get

1207 ist <- get

1231 put (ist { lastParse = Just n })

1208 put (ist { lastParse = Just n })

1232 return $ PClause fc n capp wargs r wheres) <|> (do

1209 return $ PClause fc n capp wargs r wheres) <|> (do

@@ -1243,9 +1220,9 @@ clause syn

1243 return $ PWith fc n capp wargs wval pn withs)

1220 return $ PWith fc n capp wargs wval pn withs)

1244 <?> "function clause"

1221 <?> "function clause"

1245 where

1222 where

1246− optProof = option Nothing (do reservedHL "proof"

1223+ optProof = P.option Nothing (do reservedHL "proof"

1247− n <- fnName

1224+ n <- fnName

1248− return (Just n))

1225+ return (Just n))

1249

1226

1250 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause

1227 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause

1251 fillLHS n capp owargs (PClauseR fc wargs v ws)

1228 fillLHS n capp owargs (PClauseR fc wargs v ws)

@@ -1336,74 +1313,74 @@ Directive' ::= 'lib' CodeGen String_t

1336@

1313@

1337-}

1314-}

1338directive :: SyntaxInfo -> IdrisParser [PDecl]

1315directive :: SyntaxInfo -> IdrisParser [PDecl]

1339−directive syn = do try (lchar '%' *> reserved "lib")

1316+directive syn = do P.try (lchar '%' *> reserved "lib")

1340 cgn <- codegen_

1317 cgn <- codegen_

1341 lib <- fmap fst stringLiteral

1318 lib <- fmap fst stringLiteral

1342 return [PDirective (DLib cgn lib)]

1319 return [PDirective (DLib cgn lib)]

1343− <|> do try (lchar '%' *> reserved "link")

1320+ <|> do P.try (lchar '%' *> reserved "link")

1344 cgn <- codegen_; obj <- fst <$> stringLiteral

1321 cgn <- codegen_; obj <- fst <$> stringLiteral

1345 return [PDirective (DLink cgn obj)]

1322 return [PDirective (DLink cgn obj)]

1346− <|> do try (lchar '%' *> reserved "flag")

1323+ <|> do P.try (lchar '%' *> reserved "flag")

1347 cgn <- codegen_; flag <- fst <$> stringLiteral

1324 cgn <- codegen_; flag <- fst <$> stringLiteral

1348 return [PDirective (DFlag cgn flag)]

1325 return [PDirective (DFlag cgn flag)]

1349− <|> do try (lchar '%' *> reserved "include")

1326+ <|> do P.try (lchar '%' *> reserved "include")

1350 cgn <- codegen_

1327 cgn <- codegen_

1351 hdr <- fst <$> stringLiteral

1328 hdr <- fst <$> stringLiteral

1352 return [PDirective (DInclude cgn hdr)]

1329 return [PDirective (DInclude cgn hdr)]

1353− <|> do try (lchar '%' *> reserved "hide"); n <- fst <$> fnName

1330+ <|> do P.try (lchar '%' *> reserved "hide"); n <- fst <$> fnName

1354 return [PDirective (DHide n)]

1331 return [PDirective (DHide n)]

1355− <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

1332+ <|> do P.try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []

1356 return [PDirective (DFreeze n)]

1333 return [PDirective (DFreeze n)]

1357− <|> do try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []

1334+ <|> do P.try (lchar '%' *> reserved "thaw"); n <- fst <$> iName []

1358 return [PDirective (DThaw n)]

1335 return [PDirective (DThaw n)]

1359 -- injectivity assertins are intended for debugging purposes

1336 -- injectivity assertins are intended for debugging purposes

1360 -- only, and won't be documented/could be removed at any point

1337 -- only, and won't be documented/could be removed at any point

1361− <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

1338+ <|> do P.try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName

1362 return [PDirective (DInjective n)]

1339 return [PDirective (DInjective n)]

1363 -- Assert totality of something after definition. This is

1340 -- Assert totality of something after definition. This is

1364 -- here as a debugging aid, so commented out...

1341 -- here as a debugging aid, so commented out...

1365−-- <|> do try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName

1342+-- <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName

1366-- return [PDirective (DSetTotal n)]

1343-- return [PDirective (DSetTotal n)]

1367− <|> do try (lchar '%' *> reserved "access")

1344+ <|> do P.try (lchar '%' *> reserved "access")

1368 acc <- accessibility

1345 acc <- accessibility

1369 ist <- get

1346 ist <- get

1370 put ist { default_access = acc }

1347 put ist { default_access = acc }

1371 return [PDirective (DAccess acc)]

1348 return [PDirective (DAccess acc)]

1372− <|> do try (lchar '%' *> reserved "default"); tot <- totality

1349+ <|> do P.try (lchar '%' *> reserved "default"); tot <- totality

1373 i <- get

1350 i <- get

1374 put (i { default_total = tot } )

1351 put (i { default_total = tot } )

1375 return [PDirective (DDefault tot)]

1352 return [PDirective (DDefault tot)]

1376− <|> do try (lchar '%' *> reserved "logging")

1353+ <|> do P.try (lchar '%' *> reserved "logging")

1377 i <- fst <$> natural

1354 i <- fst <$> natural

1378 return [PDirective (DLogging i)]

1355 return [PDirective (DLogging i)]

1379− <|> do try (lchar '%' *> reserved "dynamic")

1356+ <|> do P.try (lchar '%' *> reserved "dynamic")

1380− libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')

1357+ libs <- P.sepBy1 (fmap fst stringLiteral) (lchar ',')

1381 return [PDirective (DDynamicLibs libs)]

1358 return [PDirective (DDynamicLibs libs)]

1382− <|> do try (lchar '%' *> reserved "name")

1359+ <|> do P.try (lchar '%' *> reserved "name")

1383 (ty, tyFC) <- fnName

1360 (ty, tyFC) <- fnName

1384− ns <- sepBy1 name (lchar ',')

1361+ ns <- P.sepBy1 name (lchar ',')

1385 return [PDirective (DNameHint ty tyFC ns)]

1362 return [PDirective (DNameHint ty tyFC ns)]

1386− <|> do try (lchar '%' *> reserved "error_handlers")

1363+ <|> do P.try (lchar '%' *> reserved "error_handlers")

1387 (fn, nfc) <- fnName

1364 (fn, nfc) <- fnName

1388 (arg, afc) <- fnName

1365 (arg, afc) <- fnName

1389− ns <- sepBy1 name (lchar ',')

1366+ ns <- P.sepBy1 name (lchar ',')

1390 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]

1367 return [PDirective (DErrorHandlers fn nfc arg afc ns) ]

1391− <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

1368+ <|> do P.try (lchar '%' *> reserved "language"); ext <- pLangExt;

1392 return [PDirective (DLanguage ext)]

1369 return [PDirective (DLanguage ext)]

1393− <|> do try (lchar '%' *> reserved "deprecate")

1370+ <|> do P.try (lchar '%' *> reserved "deprecate")

1394 n <- fst <$> fnName

1371 n <- fst <$> fnName

1395− alt <- option "" (fst <$> stringLiteral)

1372+ alt <- P.option "" (fst <$> stringLiteral)

1396 return [PDirective (DDeprecate n alt)]

1373 return [PDirective (DDeprecate n alt)]

1397− <|> do try (lchar '%' *> reserved "fragile")

1374+ <|> do P.try (lchar '%' *> reserved "fragile")

1398 n <- fst <$> fnName

1375 n <- fst <$> fnName

1399− alt <- option "" (fst <$> stringLiteral)

1376+ alt <- P.option "" (fst <$> stringLiteral)

1400 return [PDirective (DFragile n alt)]

1377 return [PDirective (DFragile n alt)]

1401 <|> do fc <- getFC

1378 <|> do fc <- getFC

1402− try (lchar '%' *> reserved "used")

1379+ P.try (lchar '%' *> reserved "used")

1403 fn <- fst <$> fnName

1380 fn <- fst <$> fnName

1404 arg <- fst <$> iName []

1381 arg <- fst <$> iName []

1405 return [PDirective (DUsed fc fn arg)]

1382 return [PDirective (DUsed fc fn arg)]

1406− <|> do try (lchar '%' *> reserved "auto_implicits")

1383+ <|> do P.try (lchar '%' *> reserved "auto_implicits")

1407 b <- on_off

1384 b <- on_off

1408 return [PDirective (DAutoImplicits b)]

1385 return [PDirective (DAutoImplicits b)]

1409 <?> "directive"

1386 <?> "directive"

@@ -1440,12 +1417,12 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1440@

1417@

1441 -}

1418 -}

1442provider :: SyntaxInfo -> IdrisParser [PDecl]

1419provider :: SyntaxInfo -> IdrisParser [PDecl]

1443−provider syn = do doc <- try (do (doc, _) <- docstring syn

1420+provider syn = do doc <- P.try (do (doc, _) <- docstring syn

1444− fc1 <- getFC

1421+ fc1 <- getFC

1445− lchar '%'

1422+ lchar '%'

1446− fc2 <- reservedFC "provide"

1423+ fc2 <- reservedFC "provide"

1447− highlightP (spanFC fc1 fc2) AnnKeyword

1424+ highlightP (spanFC fc1 fc2) AnnKeyword

1448− return doc)

1425+ return doc)

1449 provideTerm doc <|> providePostulate doc

1426 provideTerm doc <|> providePostulate doc

1450 <?> "type provider"

1427 <?> "type provider"

1451 where provideTerm doc =

1428 where provideTerm doc =

@@ -1469,7 +1446,7 @@ Transform ::= '%' 'transform' Expr '==>' Expr

1469@

1446@

1470-}

1447-}

1471transform :: SyntaxInfo -> IdrisParser [PDecl]

1448transform :: SyntaxInfo -> IdrisParser [PDecl]

1472−transform syn = do try (lchar '%' *> reserved "transform")

1449+transform syn = do P.try (lchar '%' *> reserved "transform")

1473 -- leave it unchecked, until we work out what this should

1450 -- leave it unchecked, until we work out what this should

1474 -- actually mean...

1451 -- actually mean...

1475-- safety <- option True (do reserved "unsafe"

1452-- safety <- option True (do reserved "unsafe"

@@ -1489,10 +1466,10 @@ RunElabDecl ::= '%' 'runElab' Expr

1489-}

1466-}

1490runElabDecl :: SyntaxInfo -> IdrisParser PDecl

1467runElabDecl :: SyntaxInfo -> IdrisParser PDecl

1491runElabDecl syn =

1468runElabDecl syn =

1492− do kwFC <- try (do fc <- getFC

1469+ do kwFC <- P.try (do fc <- getFC

1493− lchar '%'

1470+ lchar '%'

1494− fc' <- reservedFC "runElab"

1471+ fc' <- reservedFC "runElab"

1495− return (spanFC fc fc'))

1472+ return (spanFC fc fc'))

1496 script <- expr syn <?> "elaborator script"

1473 script <- expr syn <?> "elaborator script"

1497 highlightP kwFC AnnKeyword

1474 highlightP kwFC AnnKeyword

1498 return $ PRunElabDecl kwFC script (syn_namespace syn)

1475 return $ PRunElabDecl kwFC script (syn_namespace syn)

@@ -1500,20 +1477,20 @@ runElabDecl syn =

1500

1477

1501{- * Loading and parsing -}

1478{- * Loading and parsing -}

1502{-| Parses an expression from input -}

1479{-| Parses an expression from input -}

1503−parseExpr :: IState -> String -> Result PTerm

1480+parseExpr :: IState -> String -> Either ParseError PTerm

1504parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1481parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1505

1482

1506{-| Parses a constant form input -}

1483{-| Parses a constant form input -}

1507−parseConst :: IState -> String -> Result Const

1484+parseConst :: IState -> String -> Either ParseError Const

1508parseConst st = runparser (fmap fst constant) st "(input)"

1485parseConst st = runparser (fmap fst constant) st "(input)"

1509

1486

1510{-| Parses a tactic from input -}

1487{-| Parses a tactic from input -}

1511−parseTactic :: IState -> String -> Result PTactic

1488+parseTactic :: IState -> String -> Either ParseError PTactic

1512parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1489parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1513

1490

1514{-| Parses a do-step from input (used in the elab shell) -}

1491{-| Parses a do-step from input (used in the elab shell) -}

1515−parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

1492+parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)

1516−parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left elabShellCmd) ist "(input)"

1493+parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"

1517 where elabShellCmd = char ':' >>

1494 where elabShellCmd = char ':' >>

1518 (reserved "qed" >> pure EQED ) <|>

1495 (reserved "qed" >> pure EQED ) <|>

1519 (reserved "abandon" >> pure EAbandon ) <|>

1496 (reserved "abandon" >> pure EAbandon ) <|>

@@ -1525,7 +1502,7 @@ parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left

1525 (expressionTactic ["search"] ESearch ) <|>

1502 (expressionTactic ["search"] ESearch ) <|>

1526 (do reserved "doc"

1503 (do reserved "doc"

1527 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1504 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1528− eof

1505+ P.eof

1529 return (EDocStr doc))

1506 return (EDocStr doc))

1530 <?> "elab command"

1507 <?> "elab command"

1531 expressionTactic cmds tactic =

1508 expressionTactic cmds tactic =

@@ -1536,26 +1513,26 @@ parseElabShellStep ist = runparser (fmap Right (do_ defaultSyntax) <|> fmap Left

1536 spaced parser = indentGt *> parser

1513 spaced parser = indentGt *> parser

1537

1514

1538-- | Parse module header and imports

1515-- | Parse module header and imports

1539−parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

1516+parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe P.Delta)

1540parseImports fname input

1517parseImports fname input

1541 = do i <- getIState

1518 = do i <- getIState

1542− case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

1519+ case P.parseString (evalStateT imports i) (P.Directed (UTF8.fromString fname) 0 0 0 0) input of

1543− Failure (ErrInfo err _) -> ifail $ show err

1520+ P.Failure (P.ErrInfo err _) -> ifail $ show err

1544− Success (x, annots, i) ->

1521+ P.Success (x, annots, i) ->

1545 do putIState i

1522 do putIState i

1546 fname' <- runIO $ Dir.makeAbsolute fname

1523 fname' <- runIO $ Dir.makeAbsolute fname

1547 sendHighlighting $ addPath annots fname'

1524 sendHighlighting $ addPath annots fname'

1548 return x

1525 return x

1549 where imports :: IdrisParser ((Maybe (Docstring ()), [String],

1526 where imports :: IdrisParser ((Maybe (Docstring ()), [String],

1550 [ImportInfo],

1527 [ImportInfo],

1551− Maybe Delta),

1528+ Maybe P.Delta),

1552 [(FC, OutputAnnotation)], IState)

1529 [(FC, OutputAnnotation)], IState)

1553 imports = do optional shebang

1530 imports = do optional shebang

1554 whiteSpace

1531 whiteSpace

1555 (mdoc, mname, annots) <- moduleHeader

1532 (mdoc, mname, annots) <- moduleHeader

1556 ps_exp <- many import_

1533 ps_exp <- many import_

1557− mrk <- mark

1534+ mrk <- P.mark

1558− isEof <- lookAheadMatches eof

1535+ isEof <- lookAheadMatches P.eof

1559 let mrk' = if isEof

1536 let mrk' = if isEof

1560 then Nothing

1537 then Nothing

1561 else Just mrk

1538 else Just mrk

@@ -1572,11 +1549,11 @@ parseImports fname input

1572 addPath (annot:annots) path = annot : addPath annots path

1549 addPath (annot:annots) path = annot : addPath annots path

1573

1550

1574 shebang :: IdrisParser ()

1551 shebang :: IdrisParser ()

1575− shebang = string "#!" *> many (satisfy $ not . isEol) *> eol *> pure ()

1552+ shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

1576

1553

1577-- | There should be a better way of doing this...

1554-- | There should be a better way of doing this...

1578−findFC :: Doc -> (FC, String)

1555+findFC :: PP.Doc -> (FC, String)

1579−findFC x = let s = show (plain x) in findFC' s

1556+findFC x = let s = show (PP.plain x) in findFC' s

1580 where findFC' s = case span (/= ':') s of

1557 where findFC' s = case span (/= ':') s of

1581 -- Horrid kludge to prevent crashes on Windows

1558 -- Horrid kludge to prevent crashes on Windows

1582 (prefix, ':':'\\':rest) ->

1559 (prefix, ':':'\\':rest) ->

@@ -1590,36 +1567,36 @@ findFC x = let s = show (plain x) in findFC' s

1590 (FC failname pos pos, msg)

1567 (FC failname pos pos, msg)

1591

1568

1592-- | Check if the coloring matches the options and corrects if necessary

1569-- | Check if the coloring matches the options and corrects if necessary

1593−fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1570+fixColour :: Bool -> PP.Doc -> PP.Doc

1594−fixColour False doc = ANSI.plain doc

1571+fixColour False doc = PP.plain doc

1595fixColour True doc = doc

1572fixColour True doc = doc

1596

1573

1597-- | A program is a list of declarations, possibly with associated

1574-- | A program is a list of declarations, possibly with associated

1598-- documentation strings.

1575-- documentation strings.

1599−parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

1576+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe P.Delta ->

1600 Idris [PDecl]

1577 Idris [PDecl]

1601parseProg syn fname input mrk

1578parseProg syn fname input mrk

1602 = do i <- getIState

1579 = do i <- getIState

1603 case runparser mainProg i fname input of

1580 case runparser mainProg i fname input of

1604− Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta

1581+ Left err -> do -- FIXME: Get error location from trifecta

1605− -- this can't be the solution!

1582+ -- this can't be the solution!

1606− -- Issue #1575 on the issue tracker.

1583+ -- Issue #1575 on the issue tracker.

1607− -- https://github.com/idris-lang/Idris-dev/issues/1575

1584+ -- https://github.com/idris-lang/Idris-dev/issues/1575

1608− let (fc, msg) = findFC doc

1585+ let (fc, msg) = findFC $ parseErrorDoc err

1609− i <- getIState

1586+ i <- getIState

1610− case idris_outputmode i of

1587+ case idris_outputmode i of

1611− RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1588+ RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

1612− IdeMode n h -> iWarn fc (P.text msg)

1589+ IdeMode n h -> iWarn fc (Util.Pretty.text msg)

1613− putIState (i { errSpan = Just fc })

1590+ putIState (i { errSpan = Just fc })

1614− return []

1591+ return []

1615− Success (x, i) -> do putIState i

1592+ Right (x, i) -> do putIState i

1616− reportParserWarnings

1593+ reportParserWarnings

1617− return $ collect x

1594+ return $ collect x

1618 where mainProg :: IdrisParser ([PDecl], IState)

1595 where mainProg :: IdrisParser ([PDecl], IState)

1619 mainProg = case mrk of

1596 mainProg = case mrk of

1620 Nothing -> do i <- get; return ([], i)

1597 Nothing -> do i <- get; return ([], i)

1621 Just mrk -> do

1598 Just mrk -> do

1622− release mrk

1599+ P.release mrk

1623 ds <- prog syn

1600 ds <- prog syn

1624 i' <- get

1601 i' <- get

1625 return (ds, i')

1602 return (ds, i')

src/Idris/Parser/Data.hs+28−28

@@ -22,16 +22,16 @@ import Control.Applicative

22import Control.Monad.State.Strict

23import Data.List

24import Data.Maybe

25−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

25+import Text.Trifecta ((<?>))

26− stringLiteral, symbol, whiteSpace)

26+import qualified Text.Trifecta as P

28{- | Parses a record type declaration

29Record ::=

30 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

31-}

32record :: SyntaxInfo -> IdrisParser PDecl

33−record syn = do (doc, paramDocs, acc, opts) <- try (do

33+record syn = do (doc, paramDocs, acc, opts) <- P.try (do

34− (doc, paramDocs) <- option noDocs docComment

34+ (doc, paramDocs) <- P.option noDocs docComment

35 ist <- get

36 let doc' = annotCode (tryFullExpr syn ist) doc

37 paramDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

@@ -45,7 +45,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

45 let tyn = expandNS syn tyn_in

46 let rsyn = syn { syn_namespace = show (nsroot tyn) :

47 syn_namespace syn }

48− params <- manyTill (recordParameter rsyn) (reservedHL "where")

48+ params <- P.manyTill (recordParameter rsyn) (reservedHL "where")

49 (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn

50 let fnames = map (expandNS rsyn) (mapMaybe getName fields)

51 case cname of

@@ -62,8 +62,8 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

62 ist <- get

63 fc <- getFC

65− (constructorName, constructorDoc) <- option (Nothing, emptyDocstring)

65+ (constructorName, constructorDoc) <- P.option (Nothing, emptyDocstring)

66− (do (doc, _) <- option noDocs docComment

66+ (do (doc, _) <- P.option noDocs docComment

67 n <- constructor

68 return (Just n, doc))

@@ -170,8 +170,8 @@ SimpleConstructorList ::=

170-}

171data_ :: SyntaxInfo -> IdrisParser PDecl

172data_ syn = checkDeclFixity $

173− do (doc, argDocs, acc, dataOpts) <- try (do

173+ do (doc, argDocs, acc, dataOpts) <- P.try (do

174− (doc, argDocs) <- option noDocs docComment

174+ (doc, argDocs) <- P.option noDocs docComment

175 pushIndent

176 acc <- accessibility

177 elim <- dataOpts []

@@ -184,10 +184,10 @@ data_ syn = checkDeclFixity $

184 return (doc', argDocs', acc, dataOpts))

185 fc <- getFC

186 (tyn_in, nfc) <- fnName

187− (do try (lchar ':')

187+ (do P.try (lchar ':')

188 ty <- typeExpr (allowImp syn)

189 let tyn = expandNS syn tyn_in

190− d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

190+ d <- P.option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

191 reservedHL "where"

192 cons <- indentedBlock (constructor syn)

193 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

@@ -199,19 +199,19 @@ data_ syn = checkDeclFixity $

199 return x)

200 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

201 let tyn = expandNS syn tyn_in

202− d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

202+ d <- P.option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

203− try (lchar '=') <|> do reservedHL "where"

203+ P.try (lchar '=') <|> do reservedHL "where"

204− let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

204+ let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

205− let n = show tyn_in ++ " "

205+ let n = show tyn_in ++ " "

206− let s = kw ++ n

206+ let s = kw ++ n

207− let as = unwords (map show args) ++ " "

207+ let as = unwords (map show args) ++ " "

208− let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

208+ let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

209− let ss = concat (intersperse " -> " $ map (const "Type") args)

209+ let ss = concat (intersperse " -> " $ map (const "Type") args)

210− let fix1 = s ++ as ++ " = ..."

210+ let fix1 = s ++ as ++ " = ..."

211− let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

211+ let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

212− let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

212+ let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

213− fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

213+ fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

214− cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

214+ cons <- P.sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")

215 let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

216 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

217 do let cty = bindArgs cargs conty

@@ -238,12 +238,12 @@ data_ syn = checkDeclFixity $

238-}

239constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])

240constructor syn

241− = do (doc, argDocs) <- option noDocs docComment

241+ = do (doc, argDocs) <- P.option noDocs docComment

242 (cn_in, nfc) <- fnName; fc <- getFC

243 let cn = expandNS syn cn_in

244 lchar ':'

245− fs <- option [] (do lchar '%'; reserved "erase"

245+ fs <- P.option [] (do lchar '%'; reserved "erase"

246− sepBy1 (fst <$> name) (lchar ','))

246+ P.sepBy1 (fst <$> name) (lchar ','))

247 ty <- typeExpr (allowImp syn)

248 ist <- get

249 let doc' = annotCode (tryFullExpr syn ist) doc

@@ -258,7 +258,7 @@ constructor syn

258-}

259simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])

260simpleConstructor syn

261− = do (doc, _) <- option noDocs (try docComment)

261+ = do (doc, _) <- P.option noDocs (P.try docComment)

262 ist <- get

263 let doc' = annotCode (tryFullExpr syn ist) doc

264 (cn_in, nfc) <- fnName

src/Idris/Parser/Expr.hs+152−155

@@ -19,14 +19,15 @@ import Idris.Parser.Ops

19import Prelude hiding (pi)

21import Control.Applicative

22+import Control.Arrow (left)

22import Control.Monad

23import Control.Monad

23import Control.Monad.State.Strict

24import Control.Monad.State.Strict

24import Data.Function (on)

25import Data.Function (on)

25import Data.List

26import Data.List

26import Data.Maybe

27import Data.Maybe

27import Text.Parser.Expression

28import Text.Parser.Expression

28−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

29+import Text.Trifecta ((<?>))

29− stringLiteral, symbol, whiteSpace)

30+import qualified Text.Trifecta as P

31-- | Allow implicit type declarations

32-- | Allow implicit type declarations

32allowImp :: SyntaxInfo -> SyntaxInfo

33allowImp :: SyntaxInfo -> SyntaxInfo

@@ -53,15 +54,12 @@ allowConstr syn = syn { constraintAllowed = True }

53 -}

54 -}

54fullExpr :: SyntaxInfo -> IdrisParser PTerm

55fullExpr :: SyntaxInfo -> IdrisParser PTerm

55fullExpr syn = do x <- expr syn

56fullExpr syn = do x <- expr syn

56− eof

57+ P.eof

57 i <- get

58 i <- get

58 return $ debindApp syn (desugar syn i x)

59 return $ debindApp syn (desugar syn i x)

60tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

61tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

61−tryFullExpr syn st input =

62+tryFullExpr syn st = left (Msg . show . parseErrorDoc) . runparser (fullExpr syn) st ""

62− case runparser (fullExpr syn) st "" input of

63− Success tm -> Right tm

64− Failure e -> Left (Msg (show e))

66{- | Parses an expression

64{- | Parses an expression

67@

65@

@@ -89,7 +87,7 @@ Expr' ::= "External (User-defined) Syntax"

89@

87@

90 -}

88 -}

91expr' :: SyntaxInfo -> IdrisParser PTerm

89expr' :: SyntaxInfo -> IdrisParser PTerm

92−expr' syn = try (externalExpr syn)

90+expr' syn = P.try (externalExpr syn)

93 <|> internalExpr syn

91 <|> internalExpr syn

94 <?> "expression"

92 <?> "expression"

@@ -140,9 +138,9 @@ data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting in

140

138

141extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

139extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

142extension syn ns rules =

140extension syn ns rules =

143− choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

141+ P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

144 case head rs of -- can never be []

142 case head rs of -- can never be []

145− Rule (symb:_) _ _ -> try $ do

143+ Rule (symb:_) _ _ -> P.try $ do

146 n <- extensionSymbol symb

144 n <- extensionSymbol symb

147 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

145 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

148 -- If we have more than one Rule in this bucket, our grammar is

146 -- If we have more than one Rule in this bucket, our grammar is

@@ -397,8 +395,8 @@ SimpleExpr ::=

397-}

395-}

398simpleExpr :: SyntaxInfo -> IdrisParser PTerm

396simpleExpr :: SyntaxInfo -> IdrisParser PTerm

399simpleExpr syn =

397simpleExpr syn =

400− try (simpleExternalExpr syn)

398+ P.try (simpleExternalExpr syn)

401− <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

399+ <|> do (x, FC f (l, c) end) <- P.try (lchar '?' *> name)

402 return (PMetavar (FC f (l, c-1) end) x)

400 return (PMetavar (FC f (l, c-1) end) x)

403 <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)

401 <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)

404 <|> do lchar '%'; fc <- getFC; reserved "instance"

402 <|> do lchar '%'; fc <- getFC; reserved "instance"

@@ -407,7 +405,7 @@ simpleExpr syn =

407 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

405 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

408 <|> proofExpr syn

406 <|> proofExpr syn

409 <|> tacticsExpr syn

407 <|> tacticsExpr syn

410− <|> try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)

408+ <|> P.try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)

411 <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes

409 <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes

412 <|> PType <$> reservedFC "Type"

410 <|> PType <$> reservedFC "Type"

413 <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType

411 <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType

@@ -420,11 +418,11 @@ simpleExpr syn =

420 [pexp (PConstant NoFC (Str (show str)))])

418 [pexp (PConstant NoFC (Str (show str)))])

421 <|> do (x, fc) <- fnName

419 <|> do (x, fc) <- fnName

422 if inPattern syn

420 if inPattern syn

423− then option (PRef fc [fc] x)

421+ then P.option (PRef fc [fc] x)

424− (do reservedOp "@"

422+ (do reservedOp "@"

425− s <- simpleExpr syn

423+ s <- simpleExpr syn

426− fcIn <- getFC

424+ fcIn <- getFC

427− return (PAs fcIn x s))

425+ return (PAs fcIn x s))

428 else return (PRef fc [fc] x)

426 else return (PRef fc [fc] x)

429 <|> idiom syn

427 <|> idiom syn

430 <|> listExpr syn

428 <|> listExpr syn

@@ -467,22 +465,22 @@ bracketed' open syn =

467 do (FC f start (l, c)) <- getFC

465 do (FC f start (l, c)) <- getFC

468 lchar ')'

466 lchar ')'

469 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

467 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

470− <|> try (dependentPair TypeOrTerm [] open syn)

468+ <|> P.try (dependentPair TypeOrTerm [] open syn)

471− <|> try (do (opName, fc) <- operatorName

469+ <|> P.try (do (opName, fc) <- operatorName

472− guardNotPrefix opName

470+ guardNotPrefix opName

473−

471+

474− e <- expr syn

472+ e <- expr syn

475− lchar ')'

473+ lchar ')'

476− return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

474+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

477− (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

475+ (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

478− pexp e]))

476+ pexp e]))

479− <|> try (simpleExpr syn >>= \l ->

477+ <|> P.try (simpleExpr syn >>= \l ->

480− try (do (opName, _) <- operatorName

478+ P.try (do (opName, _) <- operatorName

481− lchar ')'

479+ lchar ')'

482− fc <- getFC

480+ fc <- getFC

483− return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

481+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

484− (PApp fc (PRef fc [] opName) [pexp l,

482+ (PApp fc (PRef fc [] opName) [pexp l,

485− pexp (PRef fc [] (sMN 1000 "ARG"))]))

483+ pexp (PRef fc [] (sMN 1000 "ARG"))]))

486 <|> bracketedExpr syn open l)

484 <|> bracketedExpr syn open l)

487 <|> do l <- expr (allowConstr syn)

485 <|> do l <- expr (allowConstr syn)

488 bracketedExpr (allowConstr syn) open l

486 bracketedExpr (allowConstr syn) open l

@@ -510,14 +508,14 @@ dependentPair pun prev openFC syn =

510 IsTerm -> exprPart False

508 IsTerm -> exprPart False

511 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False

509 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False

512 where nametypePart = do

510 where nametypePart = do

513− (ln, lnfc, colonFC) <- try $ do

511+ (ln, lnfc, colonFC) <- P.try $ do

514 (ln, lnfc) <- name

512 (ln, lnfc) <- name

515 colonFC <- lcharFC ':'

513 colonFC <- lcharFC ':'

516 return (ln, lnfc, colonFC)

514 return (ln, lnfc, colonFC)

517 lty <- expr' syn

515 lty <- expr' syn

518 starsFC <- reservedOpFC "**"

516 starsFC <- reservedOpFC "**"

519 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn

517 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn

520− namePart = try $ do

518+ namePart = P.try $ do

521 (ln, lnfc) <- name

519 (ln, lnfc) <- name

522 starsFC <- reservedOpFC "**"

520 starsFC <- reservedOpFC "**"

523 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn

521 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn

@@ -590,7 +588,7 @@ modifyConst syn fc x = x

590@

588@

591-}

589-}

592alt :: SyntaxInfo -> IdrisParser PTerm

590alt :: SyntaxInfo -> IdrisParser PTerm

593−alt syn = do symbol "(|"; alts <- sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"

591+alt syn = do symbol "(|"; alts <- P.sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"

594 return (PAlternative [] FirstSuccess alts)

592 return (PAlternative [] FirstSuccess alts)

595

593

596{- | Parses a possibly hidden simple expression

594{- | Parses a possibly hidden simple expression

@@ -615,7 +613,7 @@ UnifyLog ::=

615 ;

613 ;

616-}

614-}

617unifyLog :: SyntaxInfo -> IdrisParser PTerm

615unifyLog :: SyntaxInfo -> IdrisParser PTerm

618−unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")

616+unifyLog syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "unifyLog")

619 tm <- simpleExpr syn

617 tm <- simpleExpr syn

620 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

618 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

621 return (PUnifyLog tm)

619 return (PUnifyLog tm)

@@ -627,7 +625,7 @@ RunTactics ::=

627 ;

625 ;

628-}

626-}

629runElab :: SyntaxInfo -> IdrisParser PTerm

627runElab :: SyntaxInfo -> IdrisParser PTerm

630−runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")

628+runElab syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "runElab")

631 fc <- getFC

629 fc <- getFC

632 tm <- simpleExpr syn

630 tm <- simpleExpr syn

633 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

631 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

@@ -641,7 +639,7 @@ Disamb ::=

641-}

639-}

642disamb :: SyntaxInfo -> IdrisParser PTerm

640disamb :: SyntaxInfo -> IdrisParser PTerm

643disamb syn = do kw <- reservedFC "with"

641disamb syn = do kw <- reservedFC "with"

644− ns <- sepBy1 (fst <$> name) (lchar ',')

642+ ns <- P.sepBy1 (fst <$> name) (lchar ',')

645 tm <- expr' syn

643 tm <- expr' syn

646 highlightP kw AnnKeyword

644 highlightP kw AnnKeyword

647 return (PDisamb (map tons ns) tm)

645 return (PDisamb (map tons ns) tm)

@@ -656,7 +654,7 @@ NoImplicits ::=

656@

654@

657-}

655-}

658noImplicits :: SyntaxInfo -> IdrisParser PTerm

656noImplicits :: SyntaxInfo -> IdrisParser PTerm

659−noImplicits syn = do try (lchar '%' *> reserved "noImplicits")

657+noImplicits syn = do P.try (lchar '%' *> reserved "noImplicits")

660 tm <- simpleExpr syn

658 tm <- simpleExpr syn

661 return (PNoImplicits tm)

659 return (PNoImplicits tm)

662 <?> "no implicits expression"

660 <?> "no implicits expression"

@@ -675,7 +673,7 @@ MatchApp ::=

675-}

673-}

676app :: SyntaxInfo -> IdrisParser PTerm

674app :: SyntaxInfo -> IdrisParser PTerm

677app syn = do f <- simpleExpr syn

675app syn = do f <- simpleExpr syn

678− (do try $ reservedOp "<=="

676+ (do P.try $ reservedOp "<=="

679 fc <- getFC

677 fc <- getFC

680 ff <- fst <$> fnName

678 ff <- fst <$> fnName

681 return (PLet fc RigW (sMN 0 "match") NoFC

679 return (PLet fc RigW (sMN 0 "match") NoFC

@@ -737,8 +735,8 @@ implicitArg :: SyntaxInfo -> IdrisParser PArg

737implicitArg syn = do lchar '{'

735implicitArg syn = do lchar '{'

738 (n, nfc) <- name

736 (n, nfc) <- name

739 fc <- getFC

737 fc <- getFC

740− v <- option (PRef nfc [nfc] n) (do lchar '='

738+ v <- P.option (PRef nfc [nfc] n) (do lchar '='

741− expr syn)

739+ expr syn)

742 lchar '}'

740 lchar '}'

743 return (pimp n v True)

741 return (pimp n v True)

744 <?> "implicit function argument"

742 <?> "implicit function argument"

@@ -800,8 +798,8 @@ unquote syn = do guard (syn_in_quasiquote syn > 0)

800-}

798-}

801namequote :: SyntaxInfo -> IdrisParser PTerm

799namequote :: SyntaxInfo -> IdrisParser PTerm

802namequote syn = do (startFC, res) <-

800namequote syn = do (startFC, res) <-

803− try (do fc <- symbolFC "`{{"

801+ P.try (do fc <- symbolFC "`{{"

804− return (fc, False)) <|>

802+ return (fc, False)) <|>

805 (do fc <- symbolFC "`{"

803 (do fc <- symbolFC "`{"

806 return (fc, True))

804 return (fc, True))

807 (n, nfc) <- fnName

805 (n, nfc) <- fnName

@@ -871,11 +869,10 @@ recordType syn =

871 <?> "field setter"

869 <?> "field setter"

872

870

873 fieldGet :: IdrisParser [Name]

871 fieldGet :: IdrisParser [Name]

874− fieldGet = sepBy1 (fst <$> fnName) (symbol "->")

872+ fieldGet = P.sepBy1 (fst <$> fnName) (symbol "->")

875

873

876 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])

874 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])

877− fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')

875+ fieldGetOrSet = P.try (Left <$> P.sepBy1 fieldSet (lchar ','))

878− return (Left fs))

879 <|> do f <- fieldGet

876 <|> do f <- fieldGet

880 return (Right f)

877 return (Right f)

881

878

@@ -942,15 +939,15 @@ LambdaTail ::=

942-}

939-}

943lambda :: SyntaxInfo -> IdrisParser PTerm

940lambda :: SyntaxInfo -> IdrisParser PTerm

944lambda syn = do lchar '\\' <?> "lambda expression"

941lambda syn = do lchar '\\' <?> "lambda expression"

945− ((do xt <- try $ tyOptDeclList (disallowImp syn)

942+ ((do xt <- P.try $ tyOptDeclList (disallowImp syn)

946 fc <- getFC

943 fc <- getFC

947 sc <- lambdaTail

944 sc <- lambdaTail

948 return (bindList (\r -> PLam fc) xt sc))

945 return (bindList (\r -> PLam fc) xt sc))

949 <|>

946 <|>

950− (do ps <- sepBy (do fc <- getFC

947+ (do ps <- P.sepBy (do fc <- getFC

951− e <- simpleExpr (disallowImp (syn { inPattern = True }))

948+ e <- simpleExpr (disallowImp (syn { inPattern = True }))

952− return (fc, e))

949+ return (fc, e))

953− (lchar ',')

950+ (lchar ',')

954 sc <- lambdaTail

951 sc <- lambdaTail

955 return (pmList (zip [0..] ps) sc)))

952 return (pmList (zip [0..] ps) sc)))

956 <?> "lambda expression"

953 <?> "lambda expression"

@@ -996,11 +993,11 @@ TypeSig' ::=

996@

993@

997 -}

994 -}

998let_ :: SyntaxInfo -> IdrisParser PTerm

995let_ :: SyntaxInfo -> IdrisParser PTerm

999−let_ syn = try (do kw <- reservedFC "let"

996+let_ syn = P.try (do kw <- reservedFC "let"

1000− ls <- indentedBlock (let_binding syn)

997+ ls <- indentedBlock (let_binding syn)

1001− kw' <- reservedFC "in"; sc <- expr syn

998+ kw' <- reservedFC "in"; sc <- expr syn

1002− highlightP kw AnnKeyword; highlightP kw' AnnKeyword

999+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1003− return (buildLets ls sc))

1000+ return (buildLets ls sc))

1004 <?> "let binding"

1001 <?> "let binding"

1005 where buildLets [] sc = sc

1002 where buildLets [] sc = sc

1006 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

1003 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

@@ -1010,11 +1007,11 @@ let_ syn = try (do kw <- reservedFC "let"

1010

1007

1011let_binding syn = do fc <- getFC;

1008let_binding syn = do fc <- getFC;

1012 pat <- expr' (syn { inPattern = True })

1009 pat <- expr' (syn { inPattern = True })

1013− ty <- option Placeholder (do lchar ':'; expr' syn)

1010+ ty <- P.option Placeholder (do lchar ':'; expr' syn)

1014 lchar '='

1011 lchar '='

1015 v <- expr (syn { withAppAllowed = isVar pat })

1012 v <- expr (syn { withAppAllowed = isVar pat })

1016− ts <- option [] (do lchar '|'

1013+ ts <- P.option [] (do lchar '|'

1017− sepBy1 (do_alt syn) (lchar '|'))

1014+ P.sepBy1 (do_alt syn) (lchar '|'))

1018 return (fc,pat,ty,v,ts)

1015 return (fc,pat,ty,v,ts)

1019 where isVar (PRef _ _ _) = True

1016 where isVar (PRef _ _ _) = True

1020 isVar _ = False

1017 isVar _ = False

@@ -1079,7 +1076,7 @@ bindsymbol opts st syn

1079 return (Exp opts st False RigW)

1076 return (Exp opts st False RigW)

1080

1077

1081explicitPi opts st syn

1078explicitPi opts st syn

1082− = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1079+ = do xt <- P.try (lchar '(' *> typeDeclList syn <* lchar ')')

1083 binder <- bindsymbol opts st syn

1080 binder <- bindsymbol opts st syn

1084 sc <- expr (allowConstr syn)

1081 sc <- expr (allowConstr syn)

1085 return (bindList (\r -> PPi (binder { pcount = r })) xt sc)

1082 return (bindList (\r -> PPi (binder { pcount = r })) xt sc)

@@ -1147,9 +1144,9 @@ unboundPiNoConstraint opts st syn = do

1147 x <- opExpr syn

1144 x <- opExpr syn

1148 (do binder <- bindsymbol opts st syn

1145 (do binder <- bindsymbol opts st syn

1149 sc <- expr syn

1146 sc <- expr syn

1150− notFollowedBy $ reservedOp "=>"

1147+ P.notFollowedBy $ reservedOp "=>"

1151 return (PPi binder (sUN "__pi_arg") NoFC x sc))

1148 return (PPi binder (sUN "__pi_arg") NoFC x sc))

1152− <|> do notFollowedBy $ reservedOp "=>"

1149+ <|> do P.notFollowedBy $ reservedOp "=>"

1153 return x

1150 return x

1154

1151

1155

1152

@@ -1158,10 +1155,10 @@ pi syn =

1158 do opts <- piOpts syn

1155 do opts <- piOpts syn

1159 st <- static

1156 st <- static

1160 explicitPi opts st syn

1157 explicitPi opts st syn

1161− <|> try (do lchar '{'; implicitPi opts st syn)

1158+ <|> P.try (do lchar '{'; implicitPi opts st syn)

1162 <|> if constraintAllowed syn

1159 <|> if constraintAllowed syn

1163− then try (unboundPiNoConstraint opts st syn)

1160+ then P.try (unboundPiNoConstraint opts st syn)

1164− <|> constraintPi opts st syn

1161+ <|> constraintPi opts st syn

1165 else unboundPi opts st syn

1162 else unboundPi opts st syn

1166 <?> "dependent type signature"

1163 <?> "dependent type signature"

1167

1164

@@ -1186,22 +1183,22 @@ ConstraintList ::=

1186@

1183@

1187-}

1184-}

1188constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1185constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1189−constraintList syn = try (constraintList1 syn)

1186+constraintList syn = P.try (constraintList1 syn)

1190 <|> return []

1187 <|> return []

1191

1188

1192constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1189constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1193−constraintList1 syn = try (do lchar '('

1190+constraintList1 syn = P.try (do lchar '('

1194− tys <- sepBy1 nexpr (lchar ',')

1191+ tys <- P.sepBy1 nexpr (lchar ',')

1195− lchar ')'

1192+ lchar ')'

1196− reservedOp "=>"

1193+ reservedOp "=>"

1197− return tys)

1194+ return tys)

1198− <|> try (do t <- opExpr (disallowImp syn)

1195+ <|> P.try (do t <- opExpr (disallowImp syn)

1199− reservedOp "=>"

1196+ reservedOp "=>"

1200− return [(RigW, defname, NoFC, t)])

1197+ return [(RigW, defname, NoFC, t)])

1201 <?> "type constraint list"

1198 <?> "type constraint list"

1202− where nexpr = try (do (n, fc) <- name; lchar ':'

1199+ where nexpr = P.try (do (n, fc) <- name; lchar ':'

1203− e <- expr (disallowImp syn)

1200+ e <- expr (disallowImp syn)

1204− return (RigW, n, fc, e))

1201+ return (RigW, n, fc, e))

1205 <|> do e <- expr (disallowImp syn)

1202 <|> do e <- expr (disallowImp syn)

1206 return (RigW, defname, NoFC, e)

1203 return (RigW, defname, NoFC, e)

1207 defname = sMN 0 "constraint"

1204 defname = sMN 0 "constraint"

@@ -1222,13 +1219,13 @@ FunctionSignatureList ::=

1222@

1219@

1223-}

1220-}

1224typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1221typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1225−typeDeclList syn = try (sepBy1 (do rig <- option RigW rigCount

1222+typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount

1226− (x, xfc) <- fnName

1223+ (x, xfc) <- fnName

1227− lchar ':'

1224+ lchar ':'

1228− t <- typeExpr (disallowImp syn)

1225+ t <- typeExpr (disallowImp syn)

1229− return (rig, x, xfc, t))

1226+ return (rig, x, xfc, t))

1230− (lchar ','))

1227+ (lchar ','))

1231− <|> do ns <- sepBy1 name (lchar ',')

1228+ <|> do ns <- P.sepBy1 name (lchar ',')

1232 lchar ':'

1229 lchar ':'

1233 t <- typeExpr (disallowImp syn)

1230 t <- typeExpr (disallowImp syn)

1234 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)

1231 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)

@@ -1250,11 +1247,11 @@ NameOrPlaceHolder ::= Name | '_';

1250@

1247@

1251-}

1248-}

1252tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1249tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1253−tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1250+tyOptDeclList syn = P.sepBy1 (do (x, fc) <- nameOrPlaceholder

1254− t <- option Placeholder (do lchar ':'

1251+ t <- P.option Placeholder (do lchar ':'

1255− expr syn)

1252+ expr syn)

1256− return (RigW, x, fc, t))

1253+ return (RigW, x, fc, t))

1257− (lchar ',')

1254+ (lchar ',')

1258 <?> "type declaration list"

1255 <?> "type declaration list"

1259 where nameOrPlaceholder :: IdrisParser (Name, FC)

1256 where nameOrPlaceholder :: IdrisParser (Name, FC)

1260 nameOrPlaceholder = fnName

1257 nameOrPlaceholder = fnName

@@ -1286,12 +1283,12 @@ ExprList ::=

1286listExpr :: SyntaxInfo -> IdrisParser PTerm

1283listExpr :: SyntaxInfo -> IdrisParser PTerm

1287listExpr syn = do (FC f (l, c) _) <- getFC

1284listExpr syn = do (FC f (l, c) _) <- getFC

1288 lchar '['; fc <- getFC;

1285 lchar '['; fc <- getFC;

1289− (try . token $ do (char ']' <?> "end of list expression")

1286+ (P.try . P.token $ do (char ']' <?> "end of list expression")

1290− (FC _ _ (l', c')) <- getFC

1287+ (FC _ _ (l', c')) <- getFC

1291− return (mkNil (FC f (l, c) (l', c'))))

1288+ return (mkNil (FC f (l, c) (l', c'))))

1292 <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"

1289 <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"

1293− (do try (lchar '|') <?> "list comprehension"

1290+ (do P.try (lchar '|') <?> "list comprehension"

1294− qs <- sepBy1 (do_ syn) (lchar ',')

1291+ qs <- P.sepBy1 (do_ syn) (lchar ',')

1295 lchar ']'

1292 lchar ']'

1296 return (PDoBlock (map addGuard qs ++

1293 return (PDoBlock (map addGuard qs ++

1297 [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))

1294 [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))

@@ -1350,53 +1347,53 @@ Do ::=

1350-}

1347-}

1351do_ :: SyntaxInfo -> IdrisParser PDo

1348do_ :: SyntaxInfo -> IdrisParser PDo

1352do_ syn

1349do_ syn

1353− = try (do kw <- reservedFC "let"

1350+ = P.try (do kw <- reservedFC "let"

1354− (i, ifc) <- name

1351+ (i, ifc) <- name

1355− ty <- option Placeholder (do lchar ':'

1352+ ty <- P.option Placeholder (do lchar ':'

1356− expr' syn)

1353+ expr' syn)

1357− reservedOp "="

1354+ reservedOp "="

1358− fc <- getFC

1355+ fc <- getFC

1359− e <- expr syn

1356+ e <- expr syn

1360− highlightP kw AnnKeyword

1357+ highlightP kw AnnKeyword

1361− return (DoLet fc RigW i ifc ty e))

1358+ return (DoLet fc RigW i ifc ty e))

1362− <|> try (do kw <- reservedFC "let"

1359+ <|> P.try (do kw <- reservedFC "let"

1363− i <- expr' syn

1360+ i <- expr' syn

1364− reservedOp "="

1361+ reservedOp "="

1365− fc <- getFC

1362+ fc <- getFC

1366− sc <- expr syn

1363+ sc <- expr syn

1367− highlightP kw AnnKeyword

1364+ highlightP kw AnnKeyword

1368− return (DoLetP fc i sc))

1365+ return (DoLetP fc i sc))

1369− <|> try (do kw <- reservedFC "rewrite"

1366+ <|> P.try (do kw <- reservedFC "rewrite"

1370− fc <- getFC

1367+ fc <- getFC

1371− sc <- expr syn

1368+ sc <- expr syn

1372− highlightP kw AnnKeyword

1369+ highlightP kw AnnKeyword

1373− return (DoRewrite fc sc))

1370+ return (DoRewrite fc sc))

1374− <|> try (do (i, ifc) <- name

1371+ <|> P.try (do (i, ifc) <- name

1375− symbol "<-"

1372+ symbol "<-"

1376− fc <- getFC

1373+ fc <- getFC

1377− e <- expr (syn { withAppAllowed = False });

1374+ e <- expr (syn { withAppAllowed = False });

1378− option (DoBind fc i ifc e)

1375+ P.option (DoBind fc i ifc e)

1379− (do lchar '|'

1376+ (do lchar '|'

1380− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1377+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1381− return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1378+ return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1382− <|> try (do i <- expr' syn

1379+ <|> P.try (do i <- expr' syn

1383− symbol "<-"

1380+ symbol "<-"

1384− fc <- getFC

1381+ fc <- getFC

1385− e <- expr (syn { withAppAllowed = False });

1382+ e <- expr (syn { withAppAllowed = False });

1386− option (DoBindP fc i e [])

1383+ P.option (DoBindP fc i e [])

1387− (do lchar '|'

1384+ (do lchar '|'

1388− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1385+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1389− return (DoBindP fc i e ts)))

1386+ return (DoBindP fc i e ts)))

1390 <|> do e <- expr syn

1387 <|> do e <- expr syn

1391 fc <- getFC

1388 fc <- getFC

1392 return (DoExp fc e)

1389 return (DoExp fc e)

1393 <?> "do block expression"

1390 <?> "do block expression"

1394

1391

1395do_alt syn = do l <- expr' syn

1392do_alt syn = do l <- expr' syn

1396− option (Placeholder, l)

1393+ P.option (Placeholder, l)

1397− (do symbol "=>"

1394+ (do symbol "=>"

1398− r <- expr' syn

1395+ r <- expr' syn

1399− return (l, r))

1396+ return (l, r))

1400

1397

1401{- | Parses an expression in idiom brackets

1398{- | Parses an expression in idiom brackets

1402@

1399@

@@ -1451,14 +1448,14 @@ constants =

1451

1448

1452-- | Parse a constant and its source span

1449-- | Parse a constant and its source span

1453constant :: IdrisParser (Idris.Core.TT.Const, FC)

1450constant :: IdrisParser (Idris.Core.TT.Const, FC)

1454−constant = choice [ do fc <- reservedFC name; return (ty, fc)

1451+constant = P.choice [ do fc <- reservedFC name; return (ty, fc)

1455− | (name, ty) <- constants

1452+ | (name, ty) <- constants

1456− ]

1453+ ]

1457− <|> do (f, fc) <- try float; return (Fl f, fc)

1454+ <|> do (f, fc) <- P.try float; return (Fl f, fc)

1458 <|> do (i, fc) <- natural; return (BI i, fc)

1455 <|> do (i, fc) <- natural; return (BI i, fc)

1459 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1456 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1460 <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1457 <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1461− <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1458+ <|> do (c, fc) <- P.try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1462 <?> "constant or literal"

1459 <?> "constant or literal"

1463

1460

1464{- | Parses a verbatim multi-line string literal (triple-quoted)

1461{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1470,11 +1467,11 @@ VerbatimString_t ::=

1470@

1467@

1471 -}

1468 -}

1472verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1469verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1473−verbatimStringLiteral = token $ do (FC f start _) <- getFC

1470+verbatimStringLiteral = P.token $ do (FC f start _) <- getFC

1474− try $ string "\"\"\""

1471+ P.try $ string "\"\"\""

1475− str <- manyTill anyChar $ try (string "\"\"\"")

1472+ str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1476− (FC _ _ end) <- getFC

1473+ (FC _ _ end) <- getFC

1477− return (str, FC f start end)

1474+ return (str, FC f start end)

1478

1475

1479{- | Parses a static modifier

1476{- | Parses a static modifier

1480

1477

@@ -1545,7 +1542,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

1545tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1542tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1546tactics =

1543tactics =

1547 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1544 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1548− do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1545+ do ns <- P.sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1549 , noArgs ["intros"] Intros

1546 , noArgs ["intros"] Intros

1550 , noArgs ["unfocus"] Unfocus

1547 , noArgs ["unfocus"] Unfocus

1551 , (["refine"], Just ExprTArg, const $

1548 , (["refine"], Just ExprTArg, const $

@@ -1593,7 +1590,7 @@ tactics =

1593 , noArgs ["trivial"] Trivial

1590 , noArgs ["trivial"] Trivial

1594 , noArgs ["unify"] DoUnify

1591 , noArgs ["unify"] DoUnify

1595 , (["search"], Nothing, const $

1592 , (["search"], Nothing, const $

1596− do depth <- option 10 $ fst <$> natural

1593+ do depth <- P.option 10 $ fst <$> natural

1597 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1594 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1598 , noArgs ["implementation"] TCImplementation

1595 , noArgs ["implementation"] TCImplementation

1599 , noArgs ["solve"] Solve

1596 , noArgs ["solve"] Solve

@@ -1614,7 +1611,7 @@ tactics =

1614 , ([":doc"], Just ExprTArg, const $

1611 , ([":doc"], Just ExprTArg, const $

1615 do whiteSpace

1612 do whiteSpace

1616 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1613 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)

1617− eof

1614+ P.eof

1618 return (TDocStr doc))

1615 return (TDocStr doc))

1619 ]

1616 ]

1620 where

1617 where

@@ -1630,12 +1627,12 @@ tactics =

1630

1627

1631

1628

1632tactic :: SyntaxInfo -> IdrisParser PTactic

1629tactic :: SyntaxInfo -> IdrisParser PTactic

1633−tactic syn = choice [ do choice (map reserved names); parser syn

1630+tactic syn = P.choice [ do P.choice (map reserved names); parser syn

1634− | (names, _, parser) <- tactics ]

1631+ | (names, _, parser) <- tactics ]

1635 <|> do lchar '{'

1632 <|> do lchar '{'

1636 t <- tactic syn;

1633 t <- tactic syn;

1637 lchar ';';

1634 lchar ';';

1638− ts <- sepBy1 (tactic syn) (lchar ';')

1635+ ts <- P.sepBy1 (tactic syn) (lchar ';')

1639 lchar '}'

1636 lchar '}'

1640 return $ TSeq t (mergeSeq ts)

1637 return $ TSeq t (mergeSeq ts)

1641 <|> ((lchar ':' >> empty) <?> "prover command")

1638 <|> ((lchar ':' >> empty) <?> "prover command")

@@ -1648,5 +1645,5 @@ tactic syn = choice [ do choice (map reserved names); parser syn

1648-- | Parses a tactic as a whole

1645-- | Parses a tactic as a whole

1649fullTactic :: SyntaxInfo -> IdrisParser PTactic

1646fullTactic :: SyntaxInfo -> IdrisParser PTactic

1650fullTactic syn = do t <- tactic syn

1647fullTactic syn = do t <- tactic syn

1651− eof

1648+ P.eof

1652 return t

1649 return t

src/Idris/Parser/Helpers.hs+108−107

@@ -34,36 +34,33 @@ import System.FilePath

34import qualified Text.Parser.Char as Chr

35import Text.Parser.LookAhead

36import qualified Text.Parser.Token as Tok

37−import qualified Text.Parser.Token.Highlight as Hi

37+import qualified Text.PrettyPrint.ANSI.Leijen as PP

38−import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

38+import Text.Trifecta ((<?>))

39− stringLiteral, symbol, whiteSpace)

39+import qualified Text.Trifecta as P

40−import Text.Trifecta.Delta

40+import qualified Text.Trifecta.Delta as P

42-- | Idris parser with state used during parsing

43−type IdrisParser = StateT IState IdrisInnerParser

43+type IdrisParser = StateT IState P.Parser

44−

45−newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

46− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

47−

48−deriving instance Parsing IdrisInnerParser

50#if MIN_VERSION_base(4,9,0)

45#if MIN_VERSION_base(4,9,0)

51−instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

46+instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where

52− line = lift line

47+ line = lift P.line

53 {-# INLINE line #-}

48 {-# INLINE line #-}

54− position = lift position

49+ position = lift P.position

55 {-# INLINE position #-}

50 {-# INLINE position #-}

56− slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

51+ slicedWith f (StateT m) = StateT $ \s -> P.slicedWith (\(a,s') b -> (f a b, s')) $ m s

57 {-# INLINE slicedWith #-}

52 {-# INLINE slicedWith #-}

58− rend = lift rend

53+ rend = lift P.rend

59 {-# INLINE rend #-}

54 {-# INLINE rend #-}

60− restOfLine = lift restOfLine

55+ restOfLine = lift P.restOfLine

61 {-# INLINE restOfLine #-}

56 {-# INLINE restOfLine #-}

62−

63#endif

57#endif

59+someSpace' :: MonadicParsing m => m ()

60+someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

61+

65−instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

62+instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where

66− someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

63+ someSpace = someSpace'

67 token p = do s <- get

64 token p = do s <- get

68 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

65 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

69 -- See Issue #1594

66 -- See Issue #1594

@@ -72,8 +69,9 @@ instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

72 whiteSpace

69 whiteSpace

73 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

70 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

74 return r

71 return r

72+

75-- | Generalized monadic parsing constraint type

73-- | Generalized monadic parsing constraint type

76−type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

74+type MonadicParsing m = (P.DeltaParsing m, LookAheadParsing m, Monad m)

78class HasLastTokenSpan m where

76class HasLastTokenSpan m where

79 getLastTokenSpan :: m (Maybe FC)

77 getLastTokenSpan :: m (Maybe FC)

@@ -81,11 +79,15 @@ class HasLastTokenSpan m where

81instance HasLastTokenSpan IdrisParser where

79instance HasLastTokenSpan IdrisParser where

82 getLastTokenSpan = lastTokenSpan <$> get

80 getLastTokenSpan = lastTokenSpan <$> get

82+newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }

83+

84-- | Helper to run Idris inner parser based stateT parsers

85−runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res

85+runparser :: StateT st P.Parser res -> st -> String -> String -> Either ParseError res

86−runparser p i inputname =

86+runparser p i inputname s =

87− parseString (runInnerParser (evalStateT p i))

87+ case P.parseString (evalStateT p i)

88− (Directed (UTF8.fromString inputname) 0 0 0 0)

88+ (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of

89+ P.Failure (P.ErrInfo doc _) -> Left (ParseError doc)

90+ P.Success value -> Right value

90highlightP :: FC -> OutputAnnotation -> IdrisParser ()

92highlightP :: FC -> OutputAnnotation -> IdrisParser ()

91highlightP fc annot = do ist <- get

93highlightP fc annot = do ist <- get

@@ -125,7 +127,7 @@ parserWarning fc warnOpt warnErr = do

125

127

126-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

128-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

127simpleWhiteSpace :: MonadicParsing m => m ()

129simpleWhiteSpace :: MonadicParsing m => m ()

128−simpleWhiteSpace = satisfy isSpace *> pure ()

130+simpleWhiteSpace = () <$ P.satisfy isSpace

129

131

130-- | Checks if a charcter is end of line

132-- | Checks if a charcter is end of line

131isEol :: Char -> Bool

133isEol :: Char -> Bool

@@ -134,7 +136,7 @@ isEol _ = False

134

136

135-- | A parser that succeeds at the end of the line

137-- | A parser that succeeds at the end of the line

136eol :: MonadicParsing m => m ()

138eol :: MonadicParsing m => m ()

137−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

139+eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

138

140

139{- | Consumes a single-line comment

141{- | Consumes a single-line comment

140

142

@@ -144,7 +146,7 @@ eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

144 -}

146 -}

145singleLineComment :: MonadicParsing m => m ()

147singleLineComment :: MonadicParsing m => m ()

146singleLineComment = (string "--" *>

148singleLineComment = (string "--" *>

147− many (satisfy (not . isEol)) *>

149+ many (P.satisfy (not . isEol)) *>

148 eol *> pure ())

150 eol *> pure ())

149 <?> ""

151 <?> ""

150

152

@@ -166,15 +168,15 @@ singleLineComment = (string "--" *>

166@

168@

167-}

169-}

168multiLineComment :: MonadicParsing m => m ()

170multiLineComment :: MonadicParsing m => m ()

169−multiLineComment = try (string "{-" *> (string "-}") *> pure ())

171+multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())

170 <|> string "{-" *> inCommentChars

172 <|> string "{-" *> inCommentChars

171 <?> ""

173 <?> ""

172 where inCommentChars :: MonadicParsing m => m ()

174 where inCommentChars :: MonadicParsing m => m ()

173 inCommentChars = string "-}" *> pure ()

175 inCommentChars = string "-}" *> pure ()

174− <|> try (multiLineComment) *> inCommentChars

176+ <|> P.try (multiLineComment) *> inCommentChars

175− <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

177+ <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars

176− <|> skipSome (noneOf startEnd) *> inCommentChars

178+ <|> P.skipSome (P.noneOf startEnd) *> inCommentChars

177− <|> oneOf startEnd *> inCommentChars

179+ <|> P.oneOf startEnd *> inCommentChars

178 <?> "end of comment"

180 <?> "end of comment"

179 startEnd :: String

181 startEnd :: String

180 startEnd = "{}-"

182 startEnd = "{}-"

@@ -197,23 +199,23 @@ docComment = do dc <- pushIndent *> docCommentLine

197 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

199 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

198

200

199 where docCommentLine :: MonadicParsing m => m String

201 where docCommentLine :: MonadicParsing m => m String

200− docCommentLine = try (do string "|||"

202+ docCommentLine = P.try (do string "|||"

201− many (satisfy (==' '))

203+ many (P.satisfy (==' '))

202− contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

204+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

203− res <- many (satisfy (not . isEol))

205+ res <- many (P.satisfy (not . isEol))

204− return $ first:res)

206+ return $ first:res)

205− eol ; someSpace

207+ eol ; someSpace'

206− return contents)-- ++ concat rest))

208+ return contents)

207 <?> ""

209 <?> ""

208

210

209 argDocCommentLine = do string "|||"

211 argDocCommentLine = do string "|||"

210− many (satisfy isSpace)

212+ many (P.satisfy isSpace)

211 char '@'

213 char '@'

212− many (satisfy isSpace)

214+ many (P.satisfy isSpace)

213 n <- fst <$> name

215 n <- fst <$> name

214− many (satisfy isSpace)

216+ many (P.satisfy isSpace)

215− docs <- many (satisfy (not . isEol))

217+ docs <- many (P.satisfy (not . isEol))

216− eol ; someSpace

218+ eol ; someSpace'

217 return (n, docs)

219 return (n, docs)

218

220

219-- | Parses some white space

221-- | Parses some white space

@@ -250,23 +252,22 @@ float = do f <- Tok.double

250

252

251{- * Symbols, identifiers, names and operators -}

253{- * Symbols, identifiers, names and operators -}

252

254

253−

255+reservedIdentifiers :: HS.HashSet String

254−-- | Idris Style for parsing identifiers/reserved keywords

256+reservedIdentifiers = HS.fromList

255−idrisStyle :: MonadicParsing m => IdentifierStyle m

257+ [ "Type"

256−idrisStyle = IdentifierStyle {

258+ , "abstract", "case", "class", "codata", "constructor", "corecord", "data"

257− _styleName = "Idris"

259+ , "do", "dsl", "else", "export", "if", "implementation", "implicit"

258− , _styleStart = satisfy isAlpha <|> oneOf "_"

259− , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

260− , _styleReserved = HS.fromList

261− ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",

262− "import", "impossible", "case", "of", "total", "partial", "mutual",

263− "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",

260+ , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"

264− "proof", "postulate", "using", "namespace", "class", "instance",

265− "interface", "implementation", "parameters", "public", "private",

261+ , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"

266− "export", "abstract", "implicit", "quoteGoal", "constructor", "if",

262+ , "postulate", "private", "proof", "public", "quoteGoal", "record"

267− "then", "else"]

263+ , "rewrite", "syntax", "then", "total", "using", "where", "with"

268− , _styleHighlight = Hi.Identifier

264+ ]

269− , _styleReservedHighlight = Hi.ReservedIdentifier }

265+

266+identifierOrReserved :: MonadicParsing m => m String

267+identifierOrReserved = P.token $ P.try $ do

268+ c <- P.satisfy isAlpha <|> P.oneOf "_"

269+ cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")

270+ return $ c : cs

270

271

271char :: MonadicParsing m => Char -> m Char

272char :: MonadicParsing m => Char -> m Char

272char = Chr.char

273char = Chr.char

@@ -276,26 +277,28 @@ string = Chr.string

276

277

277-- | Parses a character as a token

278-- | Parses a character as a token

278lchar :: MonadicParsing m => Char -> m Char

279lchar :: MonadicParsing m => Char -> m Char

279−lchar = token . char

280+lchar = P.token . P.char

280

281

281-- | Parses a character as a token, returning the source span of the character

282-- | Parses a character as a token, returning the source span of the character

282lcharFC :: MonadicParsing m => Char -> m FC

283lcharFC :: MonadicParsing m => Char -> m FC

283lcharFC ch = do (FC file (l, c) _) <- getFC

284lcharFC ch = do (FC file (l, c) _) <- getFC

284− _ <- token (char ch)

285+ _ <- P.token (char ch)

285 return $ FC file (l, c) (l, c+1)

286 return $ FC file (l, c) (l, c+1)

286

287

287-- | Parses string as a token

288-- | Parses string as a token

288−symbol :: MonadicParsing m => String -> m String

289+symbol :: MonadicParsing m => String -> m ()

289−symbol = Tok.symbol

290+symbol = void . Tok.symbol

290

291

291symbolFC :: MonadicParsing m => String -> m FC

292symbolFC :: MonadicParsing m => String -> m FC

292symbolFC str = do (FC file (l, c) _) <- getFC

293symbolFC str = do (FC file (l, c) _) <- getFC

293− Tok.symbol str

294+ symbol str

294 return $ FC file (l, c) (l, c + length str)

295 return $ FC file (l, c) (l, c + length str)

295

296

296-- | Parses a reserved identifier

297-- | Parses a reserved identifier

297reserved :: MonadicParsing m => String -> m ()

298reserved :: MonadicParsing m => String -> m ()

298−reserved = Tok.reserve idrisStyle

299+reserved name = P.token $ P.try $ do

300+ P.string name

301+ P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

299

302

300-- | Parses a reserved identifier, computing its span. Assumes that

303-- | Parses a reserved identifier, computing its span. Assumes that

301-- reserved identifiers never contain line breaks.

304-- reserved identifiers never contain line breaks.

@@ -311,9 +314,9 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

311-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

314-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

312-- | Parses a reserved operator

315-- | Parses a reserved operator

313reservedOp :: MonadicParsing m => String -> m ()

316reservedOp :: MonadicParsing m => String -> m ()

314−reservedOp name = token $ try $

317+reservedOp name = P.token $ P.try $

315 do string name

318 do string name

316− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

319+ P.notFollowedBy operatorLetter <?> ("end of " ++ show name)

317

320

318reservedOpFC :: MonadicParsing m => String -> m FC

321reservedOpFC :: MonadicParsing m => String -> m FC

319reservedOpFC name = do (FC f (l, c) _) <- getFC

322reservedOpFC name = do (FC f (l, c) _) <- getFC

@@ -322,27 +325,25 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC

322

325

323-- | Parses an identifier as a token

326-- | Parses an identifier as a token

324identifier :: (MonadicParsing m) => m (String, FC)

327identifier :: (MonadicParsing m) => m (String, FC)

325−identifier = try(do (i, fc) <-

328+identifier = P.try $ do

326− token $ do (FC f (l, c) _) <- getFC

329+ (FC f (l, c) _) <- getFC

327− i <- Tok.ident idrisStyle

330+ ident <- identifierOrReserved

331+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident

332+ when (ident == "_") $ P.unexpected "wildcard"

328− return (i, FC f (l, c) (l, c + length i))

333+ return (ident, FC f (l, c) (l, c + length ident))

329− when (i == "_") $ unexpected "wildcard"

330− return (i, fc))

331

334

332-- | Parses an identifier with possible namespace as a name

335-- | Parses an identifier with possible namespace as a name

333−iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

336+iName :: (MonadicParsing m) => [String] -> m (Name, FC)

334−iName bad = do (n, fc) <- maybeWithNS identifier False bad

337+iName bad = maybeWithNS identifier False bad <?> "name"

335− return (n, fc)

336− <?> "name"

337

338

338-- | Parses an string possibly prefixed by a namespace

339-- | Parses an string possibly prefixed by a namespace

339−maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

340+maybeWithNS :: (MonadicParsing m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

340maybeWithNS parser ascend bad = do

341maybeWithNS parser ascend bad = do

341 fc <- getFC

342 fc <- getFC

342− i <- option "" (lookAhead (fst <$> identifier))

343+ i <- P.option "" (lookAhead (fst <$> identifier))

343− when (i `elem` bad) $ unexpected "reserved identifier"

344+ when (i `elem` bad) $ P.unexpected "reserved identifier"

344 let transf = if ascend then id else reverse

345 let transf = if ascend then id else reverse

345− (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))

346+ (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))

346 return (mkName (x, xs), fc)

347 return (mkName (x, xs), fc)

347 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

348 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

348 parserNoNS parser = do startFC <- getFC

349 parserNoNS parser = do startFC <- getFC

@@ -354,7 +355,7 @@ maybeWithNS parser ascend bad = do

354 lchar '.'; (x, nameFC) <- parser

355 lchar '.'; (x, nameFC) <- parser

355 return (x, xs, spanFC startFC nameFC)

356 return (x, xs, spanFC startFC nameFC)

356 parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

357 parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

357− parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

358+ parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

358

359

359-- | Parses a name

360-- | Parses a name

360name :: IdrisParser (Name, FC)

361name :: IdrisParser (Name, FC)

@@ -393,11 +394,11 @@ opChars :: String

393opChars = ":!#$%&*+./<=>?@\\^|-~"

394opChars = ":!#$%&*+./<=>?@\\^|-~"

394

395

395operatorLetter :: MonadicParsing m => m Char

396operatorLetter :: MonadicParsing m => m Char

396−operatorLetter = oneOf opChars

397+operatorLetter = P.oneOf opChars

397

398

398-- | Parse a package name

399-- | Parse a package name

399packageName :: MonadicParsing m => m String

400packageName :: MonadicParsing m => m String

400−packageName = (:) <$> oneOf firstChars <*> many (oneOf remChars)

401+packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)

401 where firstChars = ['a'..'z'] ++ ['A'..'Z']

402 where firstChars = ['a'..'z'] ++ ['A'..'Z']

402 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

403 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

403

404

@@ -409,7 +410,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%

409

410

410-- | Parses an operator

411-- | Parses an operator

411symbolicOperator :: MonadicParsing m => m String

412symbolicOperator :: MonadicParsing m => m String

412−symbolicOperator = do op <- token . some $ operatorLetter

413+symbolicOperator = do op <- P.token . some $ operatorLetter

413 when (op `elem` (invalidOperators ++ commentMarkers)) $

414 when (op `elem` (invalidOperators ++ commentMarkers)) $

414 fail $ op ++ " is not a valid operator"

415 fail $ op ++ " is not a valid operator"

415 return op

416 return op

@@ -422,24 +423,24 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC

422

423

423{- * Position helpers -}

424{- * Position helpers -}

424{- | Get filename from position (returns "(interactive)" when no source file is given) -}

425{- | Get filename from position (returns "(interactive)" when no source file is given) -}

425−fileName :: Delta -> String

426+fileName :: P.Delta -> String

426−fileName (Directed fn _ _ _ _) = UTF8.toString fn

427+fileName (P.Directed fn _ _ _ _) = UTF8.toString fn

427−fileName _ = "(interactive)"

428+fileName _ = "(interactive)"

428

429

429{- | Get line number from position -}

430{- | Get line number from position -}

430−lineNum :: Delta -> Int

431+lineNum :: P.Delta -> Int

431−lineNum (Lines l _ _ _) = fromIntegral l + 1

432+lineNum (P.Lines l _ _ _) = fromIntegral l + 1

432−lineNum (Directed _ l _ _ _) = fromIntegral l + 1

433+lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1

433lineNum _ = 0

434lineNum _ = 0

434

435

435{- | Get column number from position -}

436{- | Get column number from position -}

436−columnNum :: Delta -> Int

437+columnNum :: P.Delta -> Int

437−columnNum pos = fromIntegral (column pos) + 1

438+columnNum pos = fromIntegral (P.column pos) + 1

438

439

440

440{- | Get file position as FC -}

441{- | Get file position as FC -}

441getFC :: MonadicParsing m => m FC

442getFC :: MonadicParsing m => m FC

442−getFC = do s <- position

443+getFC = do s <- P.position

443 let (dir, file) = splitFileName (fileName s)

444 let (dir, file) = splitFileName (fileName s)

444 let f = if dir == addTrailingPathSeparator "." then file else fileName s

445 let f = if dir == addTrailingPathSeparator "." then file else fileName s

445 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

446 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

@@ -456,15 +457,15 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

456{- | @commaSeparated p@ parses one or more occurences of `p`,

457{- | @commaSeparated p@ parses one or more occurences of `p`,

457 separated by commas and optional whitespace. -}

458 separated by commas and optional whitespace. -}

458commaSeparated :: MonadicParsing m => m a -> m [a]

459commaSeparated :: MonadicParsing m => m a -> m [a]

459−commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)

460+commaSeparated p = p `P.sepBy1` (P.spaces >> P.char ',' >> P.spaces)

460

461

461{- * Layout helpers -}

462{- * Layout helpers -}

462

463

463-- | Push indentation to stack

464-- | Push indentation to stack

464pushIndent :: IdrisParser ()

465pushIndent :: IdrisParser ()

465−pushIndent = do pos <- position

466+pushIndent = do pos <- P.position

466 ist <- get

467 ist <- get

467− put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })

468+ put (ist { indent_stack = (fromIntegral (P.column pos) + 1) : indent_stack ist })

468

469

469-- | Pops indentation from stack

470-- | Pops indentation from stack

470popIndent :: IdrisParser ()

471popIndent :: IdrisParser ()

@@ -476,7 +477,7 @@ popIndent = do ist <- get

476

477

477-- | Gets current indentation

478-- | Gets current indentation

478indent :: IdrisParser Int

479indent :: IdrisParser Int

479−indent = liftM ((+1) . fromIntegral . column) position

480+indent = liftM ((+1) . fromIntegral . P.column) P.position

480

481

481-- | Gets last indentation

482-- | Gets last indentation

482lastIndent :: IdrisParser Int

483lastIndent :: IdrisParser Int

@@ -544,7 +545,7 @@ openBlock = do lchar '{'

544closeBlock :: IdrisParser ()

545closeBlock :: IdrisParser ()

545closeBlock = do ist <- get

546closeBlock = do ist <- get

546 bs <- case brace_stack ist of

547 bs <- case brace_stack ist of

547− [] -> eof >> return []

548+ [] -> [] <$ P.eof

548 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

549 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

549 Just lvl : xs -> (do i <- indent

550 Just lvl : xs -> (do i <- indent

550 isParen <- lookAheadMatches (char ')')

551 isParen <- lookAheadMatches (char ')')

@@ -553,7 +554,7 @@ closeBlock = do ist <- get

553 then fail "not end of block"

554 then fail "not end of block"

554 else return xs)

555 else return xs)

555 <|> (do notOpenBraces

556 <|> (do notOpenBraces

556− eof

557+ P.eof

557 return [])

558 return [])

558 put (ist { brace_stack = bs })

559 put (ist { brace_stack = bs })

559

560

@@ -562,19 +563,19 @@ terminator :: IdrisParser ()

562terminator = do lchar ';'; popIndent

563terminator = do lchar ';'; popIndent

563 <|> do c <- indent; l <- lastIndent

564 <|> do c <- indent; l <- lastIndent

564 if c <= l then popIndent else fail "not a terminator"

565 if c <= l then popIndent else fail "not a terminator"

565− <|> do isParen <- lookAheadMatches (oneOf ")}")

566+ <|> do isParen <- lookAheadMatches (P.oneOf ")}")

566 if isParen then popIndent else fail "not a terminator"

567 if isParen then popIndent else fail "not a terminator"

567− <|> lookAhead eof

568+ <|> lookAhead P.eof

568

569

569-- | Parses and keeps a terminator

570-- | Parses and keeps a terminator

570keepTerminator :: IdrisParser ()

571keepTerminator :: IdrisParser ()

571−keepTerminator = do lchar ';'; return ()

572+keepTerminator = () <$ lchar ';'

572 <|> do c <- indent; l <- lastIndent

573 <|> do c <- indent; l <- lastIndent

573 unless (c <= l) $ fail "not a terminator"

574 unless (c <= l) $ fail "not a terminator"

574− <|> do isParen <- lookAheadMatches (oneOf ")}|")

575+ <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

575 isIn <- lookAheadMatches (reserved "in")

576 isIn <- lookAheadMatches (reserved "in")

576 unless (isIn || isParen) $ fail "not a terminator"

577 unless (isIn || isParen) $ fail "not a terminator"

577− <|> lookAhead eof

578+ <|> lookAhead P.eof

578

579

579-- | Checks if application expression does not end

580-- | Checks if application expression does not end

580notEndApp :: IdrisParser ()

581notEndApp :: IdrisParser ()

src/Idris/Parser/Ops.hs+11−11

@@ -22,8 +22,8 @@ import Control.Monad.State.Strict

22import Data.Char (isAlpha)

23import Data.List

24import Text.Parser.Expression

25−import Text.Trifecta hiding (char, charLiteral, natural, span, string,

25+import Text.Trifecta ((<?>))

26− stringLiteral, symbol, whiteSpace)

26+import qualified Text.Trifecta as P

28-- | Creates table for fixity declarations to build expression parser

29-- using pre-build and user-defined operator/fixity declarations

@@ -49,8 +49,8 @@ table fixes

49 noFixityOperator :: Operator IdrisParser PTerm

50 noFixityOperator = flip Infix AssocNone $ do

51 indentGt

52− op <- try symbolicOperator

52+ op <- P.try symbolicOperator

53− unexpected $ "Operator without known fixity: " ++ op

53+ P.unexpected $ "Operator without known fixity: " ++ op

55 -- | Calculates table for fixity declarations

56 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

@@ -71,7 +71,7 @@ table fixes

72 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

73 binary name assoc f

74− | isBacktick name = flip Infix assoc $ try $ do

74+ | isBacktick name = flip Infix assoc $ P.try $ do

75 (n, fc) <- backtickOperator

76 guard $ show (nsroot n) == name

77 return $ f fc n

@@ -96,7 +96,7 @@ table fixes

96@

97-}

98backtickOperator :: IdrisParser (Name, FC)

99−backtickOperator = between (indentGt *> lchar '`') (indentGt *> lchar '`') name

99+backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name

100

101{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

102

@@ -123,9 +123,9 @@ operatorName = first sUN <$> symbolicOperatorFC

123

124-}

125operatorFront :: IdrisParser (Name, FC)

126−operatorFront = try (do (FC f (l, c) _) <- getFC

126+operatorFront = P.try (do (FC f (l, c) _) <- getFC

127− op <- lchar '(' *> reservedOp "=" <* lchar ')'

127+ op <- lchar '(' *> reservedOp "=" <* lchar ')'

128− return (eqTy, FC f (l, c) (l, c+3)))

128+ return (eqTy, FC f (l, c) (l, c+3)))

129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

130 op <- lchar '(' *> symbolicOperator

131 (FC _ _ (l', c')) <- getFC

@@ -139,7 +139,7 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

139@

140-}

141fnName :: IdrisParser (Name, FC)

142−fnName = try operatorFront <|> name <?> "function name"

142+fnName = P.try operatorFront <|> name <?> "function name"

143

144{- | Parses a fixity declaration

145@

@@ -151,7 +151,7 @@ Fixity ::=

151fixity :: IdrisParser PDecl

152fixity = do pushIndent

153 f <- fixityType; i <- fst <$> natural;

154− ops <- sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

154+ ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

155 terminator

156 let prec = fromInteger i

157 istate <- get

src/Idris/Prover.hs+23−24

@@ -43,7 +43,6 @@ import Control.Monad.State.Strict

43import System.Console.Haskeline

44import System.Console.Haskeline.History

45import System.IO (Handle, hPutStrLn, stdin, stdout)

46−import Text.Trifecta.Result (ErrInfo(..), Result(..))

48-- | Launch the proof shell

47-- | Launch the proof shell

49prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

48prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

@@ -312,15 +311,15 @@ elabloop info fn d prompt prf e prev h env

312

311

313 -- if we're abandoning, it has to be outside the scope of the catch

312 -- if we're abandoning, it has to be outside the scope of the catch

314 case cmd of

313 case cmd of

315− Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

314+ Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

316 _ -> return ()

315 _ -> return ()

317

316

318 (d, prev', st, done, prf', env', res) <-

317 (d, prev', st, done, prf', env', res) <-

319 idrisCatch

318 idrisCatch

320 (case cmd of

319 (case cmd of

321− Failure (ErrInfo err _) ->

320+ Left err ->

322− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

321+ return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)

323− Success (Left cmd') ->

322+ Right (Left cmd') ->

324 case cmd' of

323 case cmd' of

325 EQED -> do hs <- lifte e get_holes

324 EQED -> do hs <- lifte e get_holes

326 unless (null hs) $ ifail "Incomplete proof"

325 unless (null hs) $ ifail "Incomplete proof"

@@ -345,7 +344,7 @@ elabloop info fn d prompt prf e prev h env

345 return (d', prev, st', done, prf', env, go)

344 return (d', prev, st', done, prf', env, go)

346 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

345 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

347 return (d', prev, st', done, prf', env, go)

346 return (d', prev, st', done, prf', env, go)

348− Success (Right cmd') ->

347+ Right (Right cmd') ->

349 case cmd' of

348 case cmd' of

350 DoLetP {} -> ifail "Pattern-matching let not supported here"

349 DoLetP {} -> ifail "Pattern-matching let not supported here"

351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

350 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

@@ -430,27 +429,27 @@ ploop fn d prompt prf e h

430 Nothing -> do iPrintError ""; ifail "Abandoned"

429 Nothing -> do iPrintError ""; ifail "Abandoned"

431 Just input -> return (parseTactic i input, input)

430 Just input -> return (parseTactic i input, input)

432 case cmd of

431 case cmd of

433− Success Abandon -> do iPrintError ""; ifail "Abandoned"

432+ Right Abandon -> do iPrintError ""; ifail "Abandoned"

434 _ -> return ()

433 _ -> return ()

435 (d, st, done, prf', res) <- idrisCatch

434 (d, st, done, prf', res) <- idrisCatch

436 (case cmd of

435 (case cmd of

437− Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

436+ Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

438− Success Undo -> do (_, st) <- elabStep e loadState

437+ Right Undo -> do (_, st) <- elabStep e loadState

439− return (True, st, False, init prf, Right $ iPrintResult "")

438+ return (True, st, False, init prf, Right $ iPrintResult "")

440− Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

439+ Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

441− Success ProofTerm -> do tm <- lifte e get_term

440+ Right ProofTerm -> do tm <- lifte e get_term

442− iputStrLn $ "TT: " ++ show tm ++ "\n"

441+ iputStrLn $ "TT: " ++ show tm ++ "\n"

443− return (False, e, False, prf, Right $ iPrintResult "")

442+ return (False, e, False, prf, Right $ iPrintResult "")

444− Success Qed -> do hs <- lifte e get_holes

443+ Right Qed -> do hs <- lifte e get_holes

445− unless (null hs) $ ifail "Incomplete proof"

444+ unless (null hs) $ ifail "Incomplete proof"

446− iputStrLn "Proof completed!"

445+ iputStrLn "Proof completed!"

447− return (False, e, True, prf, Right $ iPrintResult "")

446+ return (False, e, True, prf, Right $ iPrintResult "")

448− Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

447+ Right (TCheck (PRef _ _ n)) -> checkNameType e prf n

449− Success (TCheck t) -> checkType e prf t

448+ Right (TCheck t) -> checkType e prf t

450− Success (TEval t) -> evalTerm e prf t

449+ Right (TEval t) -> evalTerm e prf t

451− Success (TDocStr x) -> docStr e prf x

450+ Right (TDocStr x) -> docStr e prf x

452− Success (TSearch t) -> search e prf t

451+ Right (TSearch t) -> search e prf t

453− Success tac ->

452+ Right tac ->

454 do (_, e) <- elabStep e saveState

453 do (_, e) <- elabStep e saveState

455 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

454 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

456 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

455 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

src/Idris/REPL.hs+22−26

@@ -93,7 +93,6 @@ import System.FSNotify (watchDir, withManager)

93import System.FSNotify.Devel (allEvents, doAllEvents)

94import System.IO

95import System.Process

96−import Text.Trifecta.Result (ErrInfo(..), Result(..))

97import Util.DynamicLinker

96import Util.DynamicLinker

98import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

97import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

99import Util.Pretty hiding ((</>))

98import Util.Pretty hiding ((</>))

@@ -177,9 +176,9 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

177 IO (IState, FilePath)

176 IO (IState, FilePath)

178processNetCmd orig i h fn cmd

177processNetCmd orig i h fn cmd

179 = do res <- case parseCmd i "(net)" cmd of

178 = do res <- case parseCmd i "(net)" cmd of

180− Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))

179+ Left err -> return (Left (Msg " invalid command"))

181− Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

180+ Right (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182− Success (Left err) -> return (Left (Msg err))

181+ Right (Left err) -> return (Left (Msg err))

183 case res of

182 case res of

184 Right x -> return x

183 Right x -> return x

185 Left err -> do hPutStrLn h (show err)

184 Left err -> do hPutStrLn h (show err)

@@ -295,8 +294,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

295 do c <- colourise

294 do c <- colourise

296 i <- getIState

295 i <- getIState

297 case parseCmd i "(input)" cmd of

296 case parseCmd i "(input)" cmd of

298− Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)

297+ Left err -> iPrintError . show . fixColour False . parseErrorDoc $ err

299− Success (Right (Prove mode n')) ->

298+ Right (Right (Prove mode n')) ->

300 idrisCatch

299 idrisCatch

301 (do process fn (Prove mode n')

300 (do process fn (Prove mode n')

302 isetPrompt (mkPrompt mods)

301 isetPrompt (mkPrompt mods)

@@ -315,10 +314,10 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

315 IdeMode.convSExp "abandon-proof" "Abandoned" n

314 IdeMode.convSExp "abandon-proof" "Abandoned" n

316 _ -> return ()

315 _ -> return ()

317 iRenderError $ pprintErr ist e)

316 iRenderError $ pprintErr ist e)

318− Success (Right cmd) -> idrisCatch

317+ Right (Right cmd) -> idrisCatch

319 (idemodeProcess fn cmd)

318 (idemodeProcess fn cmd)

320 (\e -> getIState >>= iRenderError . flip pprintErr e)

319 (\e -> getIState >>= iRenderError . flip pprintErr e)

321− Success (Left err) -> iPrintError err

320+ Right (Left err) -> iPrintError err

322runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

321runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

323 do (unused, compls) <- replCompletion (reverse str, "")

322 do (unused, compls) <- replCompletion (reverse str, "")

324 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

323 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

@@ -353,8 +352,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

353 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

352 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

354runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

353runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

355 case parseConst orig name of

354 case parseConst orig name of

356− Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

355+ Right c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357− Failure _ ->

356+ Left _ ->

358 case splitName name of

357 case splitName name of

359 Left err -> iPrintError err

358 Left err -> iPrintError err

360 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

359 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

@@ -727,11 +726,10 @@ processInput cmd orig inputs efile

727 let fn = fromMaybe "" (listToMaybe inputs)

726 let fn = fromMaybe "" (listToMaybe inputs)

728 c <- colourise

727 c <- colourise

729 case parseCmd i "(input)" cmd of

728 case parseCmd i "(input)" cmd of

730− Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

729+ Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)

731− return (Just inputs)

732− Success (Right Reload) ->

730+ Right (Right Reload) ->

733 reload orig inputs

731 reload orig inputs

734− Success (Right Watch) ->

732+ Right (Right Watch) ->

735 if null inputs then

733 if null inputs then

736 do iputStrLn "No loaded files to watch."

734 do iputStrLn "No loaded files to watch."

737 return (Just inputs)

735 return (Just inputs)

@@ -739,7 +737,7 @@ processInput cmd orig inputs efile

739 do iputStrLn efile

737 do iputStrLn efile

740 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

738 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

741 watch orig inputs

739 watch orig inputs

742− Success (Right (Load f toline)) ->

740+ Right (Right (Load f toline)) ->

743 -- The $!! here prevents a space leak on reloading.

741 -- The $!! here prevents a space leak on reloading.

744 -- This isn't a solution - but it's a temporary stopgap.

742 -- This isn't a solution - but it's a temporary stopgap.

745 -- See issue #2386

743 -- See issue #2386

@@ -749,22 +747,20 @@ processInput cmd orig inputs efile

749 clearErr

747 clearErr

750 mod <- loadInputs [f] toline

748 mod <- loadInputs [f] toline

751 return (Just mod)

749 return (Just mod)

752− Success (Right (ModImport f)) ->

750+ Right (Right (ModImport f)) ->

753 do clearErr

751 do clearErr

754 fmod <- loadModule f (IBC_REPL True)

752 fmod <- loadModule f (IBC_REPL True)

755 return (Just (inputs ++ maybe [] (:[]) fmod))

753 return (Just (inputs ++ maybe [] (:[]) fmod))

756− Success (Right Edit) -> do -- takeMVar stvar

754+ Right (Right Edit) -> do -- takeMVar stvar

757 edit efile orig

755 edit efile orig

758 return (Just inputs)

756 return (Just inputs)

759− Success (Right Proofs) -> do proofs orig

757+ Right (Right Proofs) -> Just inputs <$ proofs orig

760− return (Just inputs)

761− Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")

758+ Right (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye")

762− return Nothing

763− Success (Right cmd ) -> do idrisCatch (process fn cmd)

759+ Right (Right cmd ) -> do idrisCatch (process fn cmd)

764− (\e -> do msg <- showErr e ; iputStrLn msg)

760+ (\e -> do msg <- showErr e ; iputStrLn msg)

765− return (Just inputs)

766− Success (Left err) -> do runIO $ putStrLn err

767 return (Just inputs)

761 return (Just inputs)

762+ Right (Left err) -> do runIO $ putStrLn err

763+ return (Just inputs)

768

764

769resolveProof :: Name -> Idris Name

765resolveProof :: Name -> Idris Name

770resolveProof n'

766resolveProof n'

@@ -1429,7 +1425,7 @@ process fn (Browse ns) =

1429process fn (MakeDoc s) =

1425process fn (MakeDoc s) =

1430 do istate <- getIState

1426 do istate <- getIState

1431 let names = words s

1427 let names = words s

1432− parse n | Success x <- runparser (fmap fst name) istate fn n = Right x

1428+ parse n | Right x <- runparser (fmap fst name) istate fn n = Right x

1433 parse n = Left n

1429 parse n = Left n

1434 (bad, nss) = partitionEithers $ map parse names

1430 (bad, nss) = partitionEithers $ map parse names

1435 cd <- runIO getCurrentDirectory

1431 cd <- runIO getCurrentDirectory

src/Idris/REPL/Parser.hs+124−125

@@ -17,10 +17,10 @@ import Idris.Core.TT

17import Idris.Help

18import Idris.Imports

19import Idris.Options

20−import qualified Idris.Parser as P

20+import qualified Idris.Parser as IP

21−import qualified Idris.Parser.Expr as P

21+import qualified Idris.Parser.Expr as IP

22−import qualified Idris.Parser.Helpers as P

22+import qualified Idris.Parser.Helpers as IP

23−import qualified Idris.Parser.Ops as P

23+import qualified Idris.Parser.Ops as IP

25import Idris.REPL.Commands

@@ -33,15 +33,14 @@ import System.Console.ANSI (Color(..))

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

34import Text.Parser.Char (anyChar, oneOf)

35import Text.Parser.Combinators

36−import Text.Trifecta (Result)

38−parseCmd :: IState -> String -> String -> Result (Either String Command)

37+parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

39−parseCmd i inputname = P.runparser pCmd i inputname . trim

38+parseCmd i inputname = IP.runparser pCmd i inputname . trim

40 where trim = f . f

39 where trim = f . f

41 where f = reverse . dropWhile isSpace

40 where f = reverse . dropWhile isSpace

43type CommandTable = [ ( [String], CmdArg, String

42type CommandTable = [ ( [String], CmdArg, String

44− , String -> P.IdrisParser (Either String Command) ) ]

43+ , String -> IP.IdrisParser (Either String Command) ) ]

46setOptions :: [(String, Opt)]

45setOptions :: [(String, Opt)]

47setOptions = [("errorcontext", ErrContext),

46setOptions = [("errorcontext", ErrContext),

@@ -168,8 +167,8 @@ parserCommands =

168 , cmd_refine)

167 , cmd_refine)

169 , (["debugunify"], SeqArgs ExprArg ExprArg

168 , (["debugunify"], SeqArgs ExprArg ExprArg

170 , "(Debugging) Try to unify two expressions", const $ do

169 , "(Debugging) Try to unify two expressions", const $ do

171− l <- P.simpleExpr defaultSyntax

170+ l <- IP.simpleExpr defaultSyntax

172− r <- P.simpleExpr defaultSyntax

171+ r <- IP.simpleExpr defaultSyntax

173 eof

172 eof

174 return (Right (DebugUnify l r))

173 return (Right (DebugUnify l r))

175 )

174 )

@@ -188,7 +187,7 @@ optArgCmd names command doc =

188proofArgCmd names command doc =

187proofArgCmd names command doc =

189 (names, NoArg, doc, proofArg command)

188 (names, NoArg, doc, proofArg command)

190

189

191−pCmd :: P.IdrisParser (Either String Command)

190+pCmd :: IP.IdrisParser (Either String Command)

192pCmd = choice [ do c <- cmd names; parser c

191pCmd = choice [ do c <- cmd names; parser c

193 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

192 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

194 <|> unrecognized

193 <|> unrecognized

@@ -196,23 +195,23 @@ pCmd = choice [ do c <- cmd names; parser c

196 <|> eval

195 <|> eval

197 where nop = do eof; return (Right NOP)

196 where nop = do eof; return (Right NOP)

198 unrecognized = do

197 unrecognized = do

199− P.lchar ':'

198+ IP.lchar ':'

200 cmd <- many anyChar

199 cmd <- many anyChar

201 let cmd' = takeWhile (/=' ') cmd

200 let cmd' = takeWhile (/=' ') cmd

202 return (Left $ "Unrecognized command: " ++ cmd')

201 return (Left $ "Unrecognized command: " ++ cmd')

203

202

204−cmd :: [String] -> P.IdrisParser String

203+cmd :: [String] -> IP.IdrisParser String

205cmd xs = try $ do

204cmd xs = try $ do

206− P.lchar ':'

205+ IP.lchar ':'

207 docmd sorted_xs

206 docmd sorted_xs

208

207

209 where docmd [] = fail "Could not parse command"

208 where docmd [] = fail "Could not parse command"

210− docmd (x:xs) = try (P.reserved x >> return x) <|> docmd xs

209+ docmd (x:xs) = try (IP.reserved x >> return x) <|> docmd xs

211

210

212 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

211 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

213

212

214

213

215−noArgs :: Command -> String -> P.IdrisParser (Either String Command)

214+noArgs :: Command -> String -> IP.IdrisParser (Either String Command)

216noArgs cmd name = do

215noArgs cmd name = do

217 let emptyArgs = do

216 let emptyArgs = do

218 eof

217 eof

@@ -222,29 +221,29 @@ noArgs cmd name = do

222

221

223 emptyArgs <|> failure

222 emptyArgs <|> failure

224

223

225−eval :: P.IdrisParser (Either String Command)

224+eval :: IP.IdrisParser (Either String Command)

226eval = do

225eval = do

227− t <- P.fullExpr defaultSyntax

226+ t <- IP.fullExpr defaultSyntax

228 return $ Right (Eval t)

227 return $ Right (Eval t)

229

228

230−exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

229+exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)

231exprArg cmd name = do

230exprArg cmd name = do

232 let noArg = do

231 let noArg = do

233 eof

232 eof

234 return $ Left ("Usage is :" ++ name ++ " <expression>")

233 return $ Left ("Usage is :" ++ name ++ " <expression>")

235

234

236 let justOperator = do

235 let justOperator = do

237− (op, fc) <- P.symbolicOperatorFC

236+ (op, fc) <- IP.symbolicOperatorFC

238 eof

237 eof

239 return $ Right $ cmd (PRef fc [] (sUN op))

238 return $ Right $ cmd (PRef fc [] (sUN op))

240

239

241 let properArg = do

240 let properArg = do

242− t <- P.fullExpr defaultSyntax

241+ t <- IP.fullExpr defaultSyntax

243 return $ Right (cmd t)

242 return $ Right (cmd t)

244 try noArg <|> try justOperator <|> properArg

243 try noArg <|> try justOperator <|> properArg

245

244

246−genArg :: String -> P.IdrisParser a -> (a -> Command)

245+genArg :: String -> IP.IdrisParser a -> (a -> Command)

247− -> String -> P.IdrisParser (Either String Command)

246+ -> String -> IP.IdrisParser (Either String Command)

248genArg argName argParser cmd name = do

247genArg argName argParser cmd name = do

249 let emptyArgs = do eof; failure

248 let emptyArgs = do eof; failure

250 oneArg = do arg <- argParser

249 oneArg = do arg <- argParser

@@ -254,24 +253,24 @@ genArg argName argParser cmd name = do

254 where

253 where

255 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

254 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

256

255

257−nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

256+nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)

258−nameArg = genArg "name" $ fst <$> P.name

257+nameArg = genArg "name" $ fst <$> IP.name

259−fnNameArg = genArg "functionname" $ fst <$> P.fnName

258+fnNameArg = genArg "functionname" $ fst <$> IP.fnName

260

259

261−strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

260+strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

262strArg = genArg "string" (many anyChar)

261strArg = genArg "string" (many anyChar)

263

262

264−moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

263+moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

265−moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

264+moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)

266 where

265 where

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

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

268

267

269−namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

268+namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)

270−namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

269+namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

271 where

270 where

272 toNS = splitOn "."

271 toNS = splitOn "."

273

272

274−optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

273+optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)

275optArg cmd name = do

274optArg cmd name = do

276 let emptyArgs = do

275 let emptyArgs = do

277 eof

276 eof

@@ -279,7 +278,7 @@ optArg cmd name = do

279

278

280 let oneArg = do

279 let oneArg = do

281 o <- pOption

280 o <- pOption

282− P.whiteSpace

281+ IP.whiteSpace

283 eof

282 eof

284 return (Right (cmd o))

283 return (Right (cmd o))

285

284

@@ -288,58 +287,58 @@ optArg cmd name = do

288 try emptyArgs <|> oneArg <|> failure

287 try emptyArgs <|> oneArg <|> failure

289

288

290 where

289 where

291− pOption :: P.IdrisParser Opt

290+ pOption :: IP.IdrisParser Opt

292− pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

291+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions

293

292

294−proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

293+proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)

295proofArg cmd name = do

294proofArg cmd name = do

296 upd <- option False $ do

295 upd <- option False $ do

297− P.lchar '!'

296+ IP.lchar '!'

298 return True

297 return True

299− l <- fst <$> P.natural

298+ l <- fst <$> IP.natural

300− n <- fst <$> P.name;

299+ n <- fst <$> IP.name;

301 return (Right (cmd upd (fromInteger l) n))

300 return (Right (cmd upd (fromInteger l) n))

302

301

303−cmd_doc :: String -> P.IdrisParser (Either String Command)

302+cmd_doc :: String -> IP.IdrisParser (Either String Command)

304cmd_doc name = do

303cmd_doc name = do

305 let constant = do

304 let constant = do

306− c <- fmap fst P.constant

305+ c <- fmap fst IP.constant

307 eof

306 eof

308 return $ Right (DocStr (Right c) FullDocs)

307 return $ Right (DocStr (Right c) FullDocs)

309

308

310 let pType = do

309 let pType = do

311− P.reserved "Type"

310+ IP.reserved "Type"

312 eof

311 eof

313− return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

312+ return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)

314

313

315 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

314 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

316

315

317 try constant <|> pType <|> fnName

316 try constant <|> pType <|> fnName

318

317

319−cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

318+cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)

320cmd_consolewidth name = do

319cmd_consolewidth name = do

321 w <- pConsoleWidth

320 w <- pConsoleWidth

322 return (Right (SetConsoleWidth w))

321 return (Right (SetConsoleWidth w))

323

322

324 where

323 where

325− pConsoleWidth :: P.IdrisParser ConsoleWidth

324+ pConsoleWidth :: IP.IdrisParser ConsoleWidth

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

325+ pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth

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

326+ <|> do discard (IP.symbol "infinite"); return InfinitelyWide

328− <|> do n <- fmap (fromInteger . fst) P.natural

327+ <|> do n <- fmap (fromInteger . fst) IP.natural

329 return (ColsWide n)

328 return (ColsWide n)

330

329

331−cmd_printdepth :: String -> P.IdrisParser (Either String Command)

330+cmd_printdepth :: String -> IP.IdrisParser (Either String Command)

332−cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)

331+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

333 return (Right $ SetPrinterDepth d)

332 return (Right $ SetPrinterDepth d)

334

333

335−cmd_execute :: String -> P.IdrisParser (Either String Command)

334+cmd_execute :: String -> IP.IdrisParser (Either String Command)

336cmd_execute name = do

335cmd_execute name = do

337− tm <- option maintm (P.fullExpr defaultSyntax)

336+ tm <- option maintm (IP.fullExpr defaultSyntax)

338 return (Right (Execute tm))

337 return (Right (Execute tm))

339 where

338 where

340 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

339 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

341

340

342−cmd_dynamic :: String -> P.IdrisParser (Either String Command)

341+cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

343cmd_dynamic name = do

342cmd_dynamic name = do

344 let optArg = do l <- many anyChar

343 let optArg = do l <- many anyChar

345 if (l /= "")

344 if (l /= "")

@@ -348,101 +347,101 @@ cmd_dynamic name = do

348 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

347 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349 try optArg <|> failure

348 try optArg <|> failure

350

349

351−cmd_pprint :: String -> P.IdrisParser (Either String Command)

350+cmd_pprint :: String -> IP.IdrisParser (Either String Command)

352cmd_pprint name = do

351cmd_pprint name = do

353 fmt <- ppFormat

352 fmt <- ppFormat

354− P.whiteSpace

353+ IP.whiteSpace

355− n <- fmap (fromInteger . fst) P.natural

354+ n <- fmap (fromInteger . fst) IP.natural

356− P.whiteSpace

355+ IP.whiteSpace

357− t <- P.fullExpr defaultSyntax

356+ t <- IP.fullExpr defaultSyntax

358 return (Right (PPrint fmt n t))

357 return (Right (PPrint fmt n t))

359

358

360 where

359 where

361− ppFormat :: P.IdrisParser OutputFmt

360+ ppFormat :: IP.IdrisParser OutputFmt

362− ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

361+ ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)

363− <|> (discard (P.symbol "latex") >> return LaTeXOutput)

362+ <|> (discard (IP.symbol "latex") >> return LaTeXOutput)

364

363

365−cmd_compile :: String -> P.IdrisParser (Either String Command)

364+cmd_compile :: String -> IP.IdrisParser (Either String Command)

366cmd_compile name = do

365cmd_compile name = do

367 let defaultCodegen = Via IBCFormat "c"

366 let defaultCodegen = Via IBCFormat "c"

368

367

369− let codegenOption :: P.IdrisParser Codegen

368+ let codegenOption :: IP.IdrisParser Codegen

370 codegenOption = do

369 codegenOption = do

371− let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

370+ let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode

372− viaCodegen = do x <- fst <$> P.identifier

371+ viaCodegen = do x <- fst <$> IP.identifier

373 return (Via IBCFormat (map toLower x))

372 return (Via IBCFormat (map toLower x))

374 bytecodeCodegen <|> viaCodegen

373 bytecodeCodegen <|> viaCodegen

375

374

376 let hasOneArg = do

375 let hasOneArg = do

377 i <- get

376 i <- get

378− f <- fst <$> P.identifier

377+ f <- fst <$> IP.identifier

379 eof

378 eof

380 return $ Right (Compile defaultCodegen f)

379 return $ Right (Compile defaultCodegen f)

381

380

382 let hasTwoArgs = do

381 let hasTwoArgs = do

383 i <- get

382 i <- get

384 codegen <- codegenOption

383 codegen <- codegenOption

385− f <- fst <$> P.identifier

384+ f <- fst <$> IP.identifier

386 eof

385 eof

387 return $ Right (Compile codegen f)

386 return $ Right (Compile codegen f)

388

387

389 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

388 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

390 try hasTwoArgs <|> try hasOneArg <|> failure

389 try hasTwoArgs <|> try hasOneArg <|> failure

391

390

392−cmd_addproof :: String -> P.IdrisParser (Either String Command)

391+cmd_addproof :: String -> IP.IdrisParser (Either String Command)

393cmd_addproof name = do

392cmd_addproof name = do

394 n <- option Nothing $ do

393 n <- option Nothing $ do

395− x <- fst <$> P.name

394+ x <- fst <$> IP.name

396 return (Just x)

395 return (Just x)

397 eof

396 eof

398 return (Right (AddProof n))

397 return (Right (AddProof n))

399

398

400−cmd_log :: String -> P.IdrisParser (Either String Command)

399+cmd_log :: String -> IP.IdrisParser (Either String Command)

401cmd_log name = do

400cmd_log name = do

402− i <- fmap (fromIntegral . fst) P.natural

401+ i <- fmap (fromIntegral . fst) IP.natural

403 eof

402 eof

404 return (Right (LogLvl i))

403 return (Right (LogLvl i))

405

404

406−cmd_verb :: String -> P.IdrisParser (Either String Command)

405+cmd_verb :: String -> IP.IdrisParser (Either String Command)

407cmd_verb name = do

406cmd_verb name = do

408− i <- fmap (fromIntegral . fst) P.natural

407+ i <- fmap (fromIntegral . fst) IP.natural

409 eof

408 eof

410 return (Right (Verbosity i))

409 return (Right (Verbosity i))

411

410

412−cmd_cats :: String -> P.IdrisParser (Either String Command)

411+cmd_cats :: String -> IP.IdrisParser (Either String Command)

413cmd_cats name = do

412cmd_cats name = do

414− cs <- sepBy pLogCats (P.whiteSpace)

413+ cs <- sepBy pLogCats (IP.whiteSpace)

415 eof

414 eof

416 return $ Right $ LogCategory (concat cs)

415 return $ Right $ LogCategory (concat cs)

417 where

416 where

418 badCat = do

417 badCat = do

419− c <- fst <$> P.identifier

418+ c <- fst <$> IP.identifier

420 fail $ "Category: " ++ c ++ " is not recognised."

419 fail $ "Category: " ++ c ++ " is not recognised."

421

420

422− pLogCats :: P.IdrisParser [LogCat]

421+ pLogCats :: IP.IdrisParser [LogCat]

423− pLogCats = try (P.symbol (strLogCat IParse) >> return parserCats)

422+ pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))

424− <|> try (P.symbol (strLogCat IElab) >> return elabCats)

423+ <|> try (elabCats <$ IP.symbol (strLogCat IElab))

425− <|> try (P.symbol (strLogCat ICodeGen) >> return codegenCats)

424+ <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

426− <|> try (P.symbol (strLogCat ICoverage) >> return [ICoverage])

425+ <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

427− <|> try (P.symbol (strLogCat IIBC) >> return [IIBC])

426+ <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))

428− <|> try (P.symbol (strLogCat IErasure) >> return [IErasure])

427+ <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))

429 <|> badCat

428 <|> badCat

430

429

431−cmd_let :: String -> P.IdrisParser (Either String Command)

430+cmd_let :: String -> IP.IdrisParser (Either String Command)

432cmd_let name = do

431cmd_let name = do

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

432+ defn <- concat <$> many (IP.decl defaultSyntax)

434 return (Right (NewDefn defn))

433 return (Right (NewDefn defn))

435

434

436−cmd_unlet :: String -> P.IdrisParser (Either String Command)

435+cmd_unlet :: String -> IP.IdrisParser (Either String Command)

437−cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> P.name)

436+cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)

438

437

439−cmd_loadto :: String -> P.IdrisParser (Either String Command)

438+cmd_loadto :: String -> IP.IdrisParser (Either String Command)

440cmd_loadto name = do

439cmd_loadto name = do

441− toline <- fmap (fromInteger . fst) P.natural

440+ toline <- fmap (fromInteger . fst) IP.natural

442 f <- many anyChar;

441 f <- many anyChar;

443 return (Right (Load f (Just toline)))

442 return (Right (Load f (Just toline)))

444

443

445−cmd_colour :: String -> P.IdrisParser (Either String Command)

444+cmd_colour :: String -> IP.IdrisParser (Either String Command)

446cmd_colour name = fmap Right pSetColourCmd

445cmd_colour name = fmap Right pSetColourCmd

447

446

448 where

447 where

@@ -458,29 +457,29 @@ cmd_colour name = fmap Right pSetColourCmd

458 , ("default", Nothing)

457 , ("default", Nothing)

459 ]

458 ]

460

459

461− pSetColourCmd :: P.IdrisParser Command

460+ pSetColourCmd :: IP.IdrisParser Command

462 pSetColourCmd = (do c <- pColourType

461 pSetColourCmd = (do c <- pColourType

463 let defaultColour = IdrisColour Nothing True False False False

462 let defaultColour = IdrisColour Nothing True False False False

464− opts <- sepBy pColourMod (P.whiteSpace)

463+ opts <- sepBy pColourMod (IP.whiteSpace)

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

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

466 return $ SetColour c colour)

465 return $ SetColour c colour)

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

466+ <|> try (IP.symbol "on" >> return ColourOn)

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

467+ <|> try (IP.symbol "off" >> return ColourOff)

469

468

470− pColour :: P.IdrisParser (Maybe Color)

469+ pColour :: IP.IdrisParser (Maybe Color)

471 pColour = doColour colours

470 pColour = doColour colours

472 where doColour [] = fail "Unknown colour"

471 where doColour [] = fail "Unknown colour"

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

472+ doColour ((s, c):cs) = (try (IP.symbol s) >> return c) <|> doColour cs

474−

473+

475− pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

474+ pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)

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

475+ pColourMod = try (doVivid <$ IP.symbol "vivid")

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

476+ <|> try (doDull <$ IP.symbol "dull")

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

477+ <|> try (doUnderline <$ IP.symbol "underline")

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

478+ <|> try (doNoUnderline <$ IP.symbol "nounderline")

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

479+ <|> try (doBold <$ IP.symbol "bold")

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

480+ <|> try (doNoBold <$ IP.symbol "nobold")

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

481+ <|> try (doItalic <$ IP.symbol "italic")

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

482+ <|> try (doNoItalic <$ IP.symbol "noitalic")

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

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

485 where doVivid i = i { vivid = True }

484 where doVivid i = i { vivid = True }

486 doDull i = i { vivid = False }

485 doDull i = i { vivid = False }

@@ -497,44 +496,44 @@ cmd_colour name = fmap Right pSetColourCmd

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

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

498 enumFromTo minBound maxBound

497 enumFromTo minBound maxBound

499

498

500− pColourType :: P.IdrisParser ColourType

499+ pColourType :: IP.IdrisParser ColourType

501 pColourType = doColourType colourTypes

500 pColourType = doColourType colourTypes

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

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

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

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

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

503+ doColourType ((s,ct):cts) = (try (IP.symbol s) >> return ct) <|> doColourType cts

505

504

506idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

505idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507

506

508−cmd_apropos :: String -> P.IdrisParser (Either String Command)

507+cmd_apropos :: String -> IP.IdrisParser (Either String Command)

509cmd_apropos = packageBasedCmd (some idChar) Apropos

508cmd_apropos = packageBasedCmd (some idChar) Apropos

510

509

511−packageBasedCmd :: P.IdrisParser a -> ([PkgName] -> a -> Command)

510+packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)

512− -> String -> P.IdrisParser (Either String Command)

511+ -> String -> IP.IdrisParser (Either String Command)

513packageBasedCmd valParser cmd name =

512packageBasedCmd valParser cmd name =

514− try (do P.lchar '('

513+ try (do IP.lchar '('

515− pkgs <- sepBy (pkg <* P.whiteSpace) (P.lchar ',')

514+ pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

516− P.lchar ')'

515+ IP.lchar ')'

517 val <- valParser

516 val <- valParser

518 return (Right (cmd pkgs val)))

517 return (Right (cmd pkgs val)))

519 <|> do val <- valParser

518 <|> do val <- valParser

520 return (Right (cmd [] val))

519 return (Right (cmd [] val))

521 where

520 where

522− pkg = either fail pure . pkgName =<< P.packageName

521+ pkg = either fail pure . pkgName =<< IP.packageName

523

522

524−cmd_search :: String -> P.IdrisParser (Either String Command)

523+cmd_search :: String -> IP.IdrisParser (Either String Command)

525cmd_search = packageBasedCmd

524cmd_search = packageBasedCmd

526− (P.fullExpr (defaultSyntax { implicitAllowed = True })) Search

525+ (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search

527

526

528−cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

527+cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)

529cmd_proofsearch name = do

528cmd_proofsearch name = do

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

529+ upd <- option False (True <$ IP.lchar '!')

531− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

530+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

532− hints <- many (fst <$> P.fnName)

531+ hints <- many (fst <$> IP.fnName)

533 return (Right (DoProofSearch upd True l n hints))

532 return (Right (DoProofSearch upd True l n hints))

534

533

535−cmd_refine :: String -> P.IdrisParser (Either String Command)

534+cmd_refine :: String -> IP.IdrisParser (Either String Command)

536cmd_refine name = do

535cmd_refine name = do

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

536+ upd <- option False (do IP.lchar '!'; return True)

538− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

537+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

539− hint <- fst <$> P.fnName

538+ hint <- fst <$> IP.fnName

540 return (Right (DoProofSearch upd False l n [hint]))

539 return (Right (DoProofSearch upd False l n [hint]))