aad7688 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Megaparsec prep (#4164)

* Import Trifecta qualified as P * Return parse results using Either * Introduce ParseError type alias * Make ParseError a newtype * Reexport parseErrorDoc from Idris.Parser * Remove unused Core.TT.vinstances * identifiers & reserved without Text.Parsers.Token * Simplify symbol parsing * Explicitly import parser helpers * Extract textUntilEol * Refactor package parser somewhat * Move someSpace * Use modify * Remove unused parsing typeclasses * Implement our own someSpace * Remove a use of P.token * Don't need a newtype for inner parser * Run stylish

commitaad768891f4c52cd1aaf9b58bd9b67f009af7622 authorJason Felice <jason.m.felice@gmail.com> dateMon 30 Oct 2017, 14:32 (9 years ago) parent44a3f9c

12 files changed+741−877

compare with master

unifiedsplit

src/Idris/Core/TT.hs−9 src/Idris/IdeMode.hs+17−18 src/Idris/Main.hs+18−19 src/Idris/Package/Parser.hs+58−152 src/Idris/Parser.hs+180−203 src/Idris/Parser/Data.hs+28−28 src/Idris/Parser/Expr.hs+152−155 src/Idris/Parser/Helpers.hs+108−107 src/Idris/Parser/Ops.hs+11−11 src/Idris/Prover.hs+23−24 src/Idris/REPL.hs+22−26 src/Idris/REPL/Parser.hs+124−125

src/Idris/Core/TT.hs−9

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

11411141isInjective (App _ f a) = isInjective f

11421142isInjective _ = False

11431143

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−

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

11541145instantiate :: TT n -> TT n -> TT n

11551146instantiate e = subst 0 where

src/Idris/IdeMode.hs+17−18

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

2525import Numeric

2626import System.IO

2727import Text.Printf

28−import Text.Trifecta hiding (Err)

29−import Text.Trifecta.Delta

28+import qualified Text.Trifecta as P

29+import qualified Text.Trifecta.Delta as P

3030

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

3232getNChar _ 0 s = return (reverse s)

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

205205 escapeChar '"' = "\\\""

206206 escapeChar c = [c]

207207

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

209− return (SexpList xs)

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

210209 <|> atom

211210

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

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

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

215− <|> do ints <- some digit

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

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

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

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

216215 case readDec ints of

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

218217 _ -> return (StringAtom ints)

219218

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

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

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

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

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

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

223222

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

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

226− <|> noneOf "\""

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

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

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

227226

228−parseSExp :: String -> Result SExp

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

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

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

230229

231230data Opt = ShowImpl | ErrContext deriving Show

232231

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

324323receiveString :: String -> Either Err SExp

325324receiveString x =

326325 case parseSExp x of

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

328− Success r -> Right r

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

327+ P.Success r -> Right r

329328

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

331330convSExp pre s id =

src/Idris/Main.hs+18−19

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

4747import System.FilePath

4848import System.IO

4949import System.IO.CodePage (withCP65001)

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

5150

5251-- | How to run Idris programs.

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

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

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

197196 c <- colourise

198197 case parseExpr ist str of

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

200− runIO $ exitWith (ExitFailure 1)

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

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

199+ runIO $ exitWith (ExitFailure 1)

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

202201 exprs

203202 runIO exitSuccess

204203

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

273272execScript expr = do i <- getIState

274273 c <- colourise

275274 case parseExpr i expr of

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

277− runIO $ exitWith (ExitFailure 1)

278− Success term -> do ctxt <- getContext

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

280− res <- execute tm

281− runIO $ exitSuccess

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

276+ runIO $ exitWith (ExitFailure 1)

277+ Right term -> do ctxt <- getContext

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

279+ res <- execute tm

280+ runIO $ exitSuccess

282281

283282-- | Run the initialisation script

284283initScript :: Idris ()

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

300299 runInit h

301300 processLine i cmd input clr =

302301 case parseCmd i input cmd of

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

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

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

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

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

308− Success (Right Proofs) -> proofs i

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

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

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

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

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

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

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

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

307+ Right (Right Proofs) -> proofs i

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

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

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

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

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

1111import Idris.CmdOptions

1212import Idris.Imports

1313import 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')

1517

1618import Control.Applicative

1719import Control.Monad.State.Strict

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

2022import System.Exit

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

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

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

24− whiteSpace)

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

26+import qualified Text.Trifecta as P

2527

26−type PParser = StateT PkgDesc IdrisInnerParser

27−

28−instance HasLastTokenSpan PParser where

29− getLastTokenSpan = return Nothing

28+type PParser = StateT PkgDesc P.Parser

3029

3130#if MIN_VERSION_base(4,9,0)

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

33− line = lift line

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

32+ line = lift P.line

3433 {-# INLINE line #-}

35− position = lift position

34+ position = lift P.position

3635 {-# 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

3837 {-# INLINE slicedWith #-}

39− rend = lift rend

38+ rend = lift P.rend

4039 {-# INLINE rend #-}

41− restOfLine = lift restOfLine

40+ restOfLine = lift P.restOfLine

4241 {-# INLINE restOfLine #-}

4342#endif

4443

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

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

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

45+ someSpace = someSpace'

4746

4847

4948parseDesc :: FilePath -> IO PkgDesc

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

5655 then do

5756 p <- readFile fp

5857 case runparser pPkg defaultPkg fp p of

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

60− Success x -> return x

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

59+ Right x -> return x

6160 else do

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

6362 exitWith (ExitFailure 1)

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

6665pPkg = do

6766 reserved "package"

6867 p <- pPkgName

69− someSpace

70− st <- get

71− put (st { pkgname = p })

68+ someSpace'

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

7270 some pClause

7371 st <- get

74− eof

72+ P.eof

7573 return st

7674

7775pPkgName :: PParser PkgName

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

8078-- | Parses a filename.

8179-- |

8280-- | 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

8482filename = (do

85− filename <- token $

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

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

88− -- it will also accept hyphens

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

90− stringLiteral

91− <|>

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

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

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

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

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

85+ -- it will also accept hyphens

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

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

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

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

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

9591 case filenameErrorMessage filename of

9692 Just errorMessage -> fail errorMessage

9793 Nothing -> return filename)

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

119115 checkThat (path == takeFileName path)

120116 "filename must contain no directory component"

121117

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 ',')

122127

123128pClause :: PParser ()

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

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 })

133−

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

135− src <- fst <$> identifier

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 })

144−

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

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

147− st <- get

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

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

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

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

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

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

149−

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

151− , 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 })

157−

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

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

160− st <- get

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

162−

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) })

172−

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

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

175− st <- get

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

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}

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 })

193−

194− <|> do reserved "license"

195− lchar '='

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

197− eol

198− st <- get

199− put st {pkglicense = Just lStr}

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}

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}

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}

224−

225− <|> do reserved "brief"

226− lchar '='

227− brief <- stringLiteral

228− st <- get

229− someSpace

230− put st {pkgbrief = Just brief}

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}

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}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Parser.hs+180−203

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

1414

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

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

17− runparser) where

17+ runparser, ParseError, parseErrorDoc) where

1818

1919import Idris.AbsSyntax hiding (namespace, params)

2020import Idris.Core.Evaluate

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

3636import Idris.Termination

3737import Idris.Unlit

3838

39−import qualified Util.Pretty as P

39+import qualified Util.Pretty

4040import Util.System (readSource)

4141

4242import Prelude hiding (pi)

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

5757import qualified Data.Text as T

5858import qualified System.Directory as Dir (makeAbsolute)

5959import System.FilePath

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

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

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

63− stringLiteral, symbol, whiteSpace)

64−import Text.Trifecta.Delta

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

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

62+import qualified Text.Trifecta as P

63+import qualified Text.Trifecta.Delta as P

6564

6665{-

6766@

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

8483@

8584-}

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

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

88− noArgs docs

89− reservedHL "module"

90− (i, ifc) <- identifier

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

92− let modName = moduleName i

93− return (fmap fst docs,

94− modName,

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

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

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

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

87+ noArgs docs

88+ reservedHL "module"

89+ (i, ifc) <- identifier

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

91+ let modName = moduleName i

92+ return (fmap fst docs,

93+ modName,

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

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

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

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

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

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

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

119118import_ :: IdrisParser ImportInfo

120119import_ = do fc <- getFC

121120 reservedHL "import"

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

123− return True)

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

124122 (id, idfc) <- identifier

125123 newName <- optional (do reservedHL "as"

126124 identifier)

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

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

128126 return $ ImportInfo reexport (toPath id)

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

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

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

143141 decls <- many (decl syn)

144142 let c = concat decls

145143 case maxline syn of

146− Nothing -> do notOpenBraces; eof

144+ Nothing -> do notOpenBraces; P.eof

147145 _ -> return ()

148146 ist <- get

149147 fc <- getFC

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

172170@

173171-}

174172decl :: SyntaxInfo -> IdrisParser [PDecl]

175−decl syn = try (externalDecl syn)

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

176174 <|> internalDecl syn

177175 <?> "declaration"

178176

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

195193 if continue then

196194 do notEndBlock

197195 declBody continue

198− else try (do notEndBlock

199− declBody continue)

196+ else P.try (do notEndBlock

197+ declBody continue)

200198 <|> fail "End of readable input"

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

202200 declBody b =

203− try (implementation True syn)

204− <|> try (openInterface syn)

201+ P.try (implementation True syn)

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

205203 <|> declBody' b

206204 <|> using_ syn

207205 <|> params syn

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

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

277275 -> IdrisParser [PDecl]

278276declExtension syn ns rules =

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

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

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

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

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

282280 n <- extSymbol symb

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

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

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

427425-}

428426syntaxRule :: SyntaxInfo -> IdrisParser Syntax

429427syntaxRule syn

430− = do sty <- try (do

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

431429 pushIndent

432− sty <- option AnySyntax

433− (do reservedHL "term"; return TermSyntax

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

430+ sty <- P.option AnySyntax

431+ (TermSyntax <$ reservedHL "term"

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

435433 reservedHL "syntax"

436434 return sty)

437435 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"

439437 let ns = mapMaybe getName syms

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

441− $ unexpected "repeated variable in syntax rule"

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

442440 lchar '='

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

444442 terminator

445443 return (Rule (mkSimple syms) tm sty)

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

447445 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"

449447 let ns = mapMaybe getName syms

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

451− $ unexpected "repeated variable in syntax rule"

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

452450 lchar '='

453451 openBlock

454452 dec <- some (decl syn)

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

544542@

545543 -}

546544syntaxSym :: IdrisParser SSymbol

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

548− return (Expr n))

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

550− return (Binding n))

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

546+ return (Expr n))

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

548+ return (Binding n))

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

552550 return (Keyword n)

553551 <|> do sym <- fmap fst stringLiteral

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

561559@

562560-}

563561fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

564−fnDecl syn = try (do notEndBlock

565− d <- fnDecl' syn

566− i <- get

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

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

562+fnDecl syn = P.try (do notEndBlock

563+ d <- fnDecl' syn

564+ i <- get

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

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

569567

570568{-| Parses a function declaration

571569

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

580578-}

581579fnDecl' :: SyntaxInfo -> IdrisParser PDecl

582580fnDecl' 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

584582 pushIndent

585583 (doc, argDocs) <- docstring syn

586584 (opts, acc) <- fnOpts

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

658656-}

659657fnOpt :: IdrisParser FnOpt

660658fnOpt = do reservedHL "total"; return TotalFn

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

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

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

664− return $ CExport c

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

666− return NoImplicit

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

668− return Inlinable

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

670− return StaticFn

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

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

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

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

662+ return $ CExport c

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

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

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

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

672667 fc <- getFC

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

674669 return AssertTotal

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

676− return ErrorHandler

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

678− return ErrorReverse

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

680− return ErrorReduce

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

682− return Reflection

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

684− return AutoHint

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

686− return OverlappingDictionary

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

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

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

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

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

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

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

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

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

689678 return $ Specialise ns

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

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

691680 <?> "function modifier"

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

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

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

695− return (Just (fromInteger reds)))

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

684+ return (Just (fromInteger reds)))

696685 return (n, t)

697686

698687{-| Parses a postulate

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

705694-}

706695postulate :: SyntaxInfo -> IdrisParser PDecl

707696postulate syn = do (doc, ext)

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

709− pushIndent

710− ext <- ppostDecl

711− return (doc, ext)

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

698+ pushIndent

699+ ext <- ppostDecl

700+ return (doc, ext)

712701 ist <- get

713702 (opts, acc) <- fnOpts

714703 (n_in, nfc) <- fnName

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

768757 do reservedHL "using"

769758 reservedHL "implementation"

770759 fc <- getFC

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

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

772761

773762 openBlock

774763 ds <- many (decl syn)

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

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

849838interfaceBlock syn = do reservedHL "where"

850839 openBlock

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

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

853− n <- constructor

854− return (Just n, doc))

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

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

842+ n <- constructor

843+ return (Just n, doc))

855844 ist <- get

856845 let cd' = annotate syn ist cd

857846

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

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

859848 <|> do x <- data_ syn

860849 return [x]

861850 <|> fnDecl syn)

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

886875-}

887876interface_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

890− acc <- accessibility

891− interfaceKeyword

892− return (doc, argDocs, acc))

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

879+ acc <- accessibility

880+ interfaceKeyword

881+ return (doc, argDocs, acc))

893882 fc <- getFC

894883 cons <- constraintList syn

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

896885 (n_in, nfc) <- fnName

897886 let n = expandNS syn n_in

898887 cs <- many carg

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

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

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

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

901890 accData acc n (concatMap declared ds)

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

903892 <?> "interface declaration"

904893 where

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

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

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

907896

908897 interfaceKeyword :: IdrisParser ()

909898 interfaceKeyword = reservedHL "interface"

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

964953

965954 implementationUsing :: IdrisParser [Name]

966955 implementationUsing = do reservedHL "using"

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

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

968957 return (map fst ns)

969958 <|> return []

970959

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

972961docstring :: SyntaxInfo

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

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

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

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

976965 ist <- get

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

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

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

1005994-}

1006995usingDeclList :: SyntaxInfo -> IdrisParser [Using]

1007996usingDeclList syn

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

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

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

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

1010999 lchar ':'

10111000 t <- typeExpr (disallowImp syn)

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

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

10221011@

10231012-}

10241013usingDecl :: SyntaxInfo -> IdrisParser Using

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

1026− lchar ':'

1027− t <- typeExpr (disallowImp syn)

1028− return (UImplicit x t))

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

1015+ lchar ':'

1016+ t <- typeExpr (disallowImp syn)

1017+ return (UImplicit x t))

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

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

10311020 return (UConstraint c xs)

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

10681057-}

10691058argExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

10721061 <?> "argument expression"

10731062

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

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

10901079 expr syn

10911080 <|> do symbol "?=";

10921081 fc <- getFC

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

1094− return n)

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

1083+ return n)

10951084 r <- expr syn

10961085 return (addLet fc name r)

10971086 <|> impossible

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

11351124-}

11361125clause :: SyntaxInfo -> IdrisParser PClause

11371126clause syn

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

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

11391128 fc <- getFC

11401129 ist <- get

11411130 n <- case lastParse ist of

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

11431132 Nothing -> fail "Invalid clause"

11441133 (do r <- rhs syn n

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

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

1147− popIndent

1148− return x,

1149− do terminator

1150− return ([], [])]

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

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

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

11521138 popIndent

11531139 reservedHL "with"

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

11581144 let withs = concat ds

11591145 closeBlock

11601146 return $ PWithR fc wargs wval pn withs)

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

1162− ty <- simpleExpr syn

1163− symbol "<=="

1164− return ty)

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

1148+ ty <- simpleExpr syn

1149+ symbol "<=="

1150+ return ty)

11651151 fc <- getFC

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

11671153 r <- rhs syn n

11681154 let wsyn = syn { syn_namespace = [] }

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

1170− popIndent

1171− return x,

1172− do terminator

1173− return ([], [])]

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

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

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

11751158 ty

11761159 (PMatchApp fc n)

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

11781161 ist <- get

11791162 put (ist { lastParse = Just n })

11801163 return $ PClause fc n capp [] r wheres

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

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

11821165 pushIndent

11831166 l <- argExpr syn

11841167 (op, nfc) <- symbolicOperatorFC

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

11911174 wargs <- many (wExpr syn)

11921175 (do rs <- rhs syn n

11931176 let wsyn = syn { syn_namespace = [] }

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

1195− popIndent

1196− return x,

1197− do terminator

1198− return ([], [])]

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

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

11991179 ist <- get

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

12011181 put (ist { lastParse = Just n })

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

12151195 <|> do pushIndent

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

12171197 fc <- getFC

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

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

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

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

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

12211201 wargs <- many (wExpr syn)

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

12231203 (do r <- rhs syn n

12241204 let wsyn = syn { syn_namespace = [] }

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

1226− popIndent

1227− return x,

1228− do terminator

1229− return ([], [])]

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

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

12301207 ist <- get

12311208 put (ist { lastParse = Just n })

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

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

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

12441221 <?> "function clause"

12451222 where

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

1247− n <- fnName

1248− return (Just n))

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

1224+ n <- fnName

1225+ return (Just n))

12491226

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

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

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

13361313@

13371314-}

13381315directive :: SyntaxInfo -> IdrisParser [PDecl]

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

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

13401317 cgn <- codegen_

13411318 lib <- fmap fst stringLiteral

13421319 return [PDirective (DLib cgn lib)]

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

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

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

13451322 return [PDirective (DLink cgn obj)]

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

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

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

13481325 return [PDirective (DFlag cgn flag)]

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

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

13501327 cgn <- codegen_

13511328 hdr <- fst <$> stringLiteral

13521329 return [PDirective (DInclude cgn hdr)]

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

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

13541331 return [PDirective (DHide n)]

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

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

13561333 return [PDirective (DFreeze n)]

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

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

13581335 return [PDirective (DThaw n)]

13591336 -- injectivity assertins are intended for debugging purposes

13601337 -- 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

13621339 return [PDirective (DInjective n)]

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

13641341 -- 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

13661343-- return [PDirective (DSetTotal n)]

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

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

13681345 acc <- accessibility

13691346 ist <- get

13701347 put ist { default_access = acc }

13711348 return [PDirective (DAccess acc)]

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

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

13731350 i <- get

13741351 put (i { default_total = tot } )

13751352 return [PDirective (DDefault tot)]

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

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

13771354 i <- fst <$> natural

13781355 return [PDirective (DLogging i)]

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

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

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

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

13811358 return [PDirective (DDynamicLibs libs)]

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

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

13831360 (ty, tyFC) <- fnName

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

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

13851362 return [PDirective (DNameHint ty tyFC ns)]

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

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

13871364 (fn, nfc) <- fnName

13881365 (arg, afc) <- fnName

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

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

13901367 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;

13921369 return [PDirective (DLanguage ext)]

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

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

13941371 n <- fst <$> fnName

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

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

13961373 return [PDirective (DDeprecate n alt)]

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

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

13981375 n <- fst <$> fnName

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

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

14001377 return [PDirective (DFragile n alt)]

14011378 <|> do fc <- getFC

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

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

14031380 fn <- fst <$> fnName

14041381 arg <- fst <$> iName []

14051382 return [PDirective (DUsed fc fn arg)]

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

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

14071384 b <- on_off

14081385 return [PDirective (DAutoImplicits b)]

14091386 <?> "directive"

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

14401417@

14411418 -}

14421419provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1444− fc1 <- getFC

1445− lchar '%'

1446− fc2 <- reservedFC "provide"

1447− highlightP (spanFC fc1 fc2) AnnKeyword

1448− return doc)

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

1421+ fc1 <- getFC

1422+ lchar '%'

1423+ fc2 <- reservedFC "provide"

1424+ highlightP (spanFC fc1 fc2) AnnKeyword

1425+ return doc)

14491426 provideTerm doc <|> providePostulate doc

14501427 <?> "type provider"

14511428 where provideTerm doc =

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

14691446@

14701447-}

14711448transform :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

14741451 -- actually mean...

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

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

14891466-}

14901467runElabDecl :: SyntaxInfo -> IdrisParser PDecl

14911468runElabDecl syn =

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

1493− lchar '%'

1494− fc' <- reservedFC "runElab"

1495− return (spanFC fc fc'))

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

1470+ lchar '%'

1471+ fc' <- reservedFC "runElab"

1472+ return (spanFC fc fc'))

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

14971474 highlightP kwFC AnnKeyword

14981475 return $ PRunElabDecl kwFC script (syn_namespace syn)

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

15001477

15011478{- * Loading and parsing -}

15021479{-| Parses an expression from input -}

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

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

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

15051482

15061483{-| Parses a constant form input -}

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

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

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

15091486

15101487{-| Parses a tactic from input -}

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

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

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

15131490

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

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

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

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

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

15171494 where elabShellCmd = char ':' >>

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

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

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

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

15261503 (do reserved "doc"

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

1528− eof

1505+ P.eof

15291506 return (EDocStr doc))

15301507 <?> "elab command"

15311508 expressionTactic cmds tactic =

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

15361513 spaced parser = indentGt *> parser

15371514

15381515-- | 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)

15401517parseImports fname input

15411518 = do i <- getIState

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

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

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

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

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

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

15451522 do putIState i

15461523 fname' <- runIO $ Dir.makeAbsolute fname

15471524 sendHighlighting $ addPath annots fname'

15481525 return x

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

15501527 [ImportInfo],

1551− Maybe Delta),

1528+ Maybe P.Delta),

15521529 [(FC, OutputAnnotation)], IState)

15531530 imports = do optional shebang

15541531 whiteSpace

15551532 (mdoc, mname, annots) <- moduleHeader

15561533 ps_exp <- many import_

1557− mrk <- mark

1558− isEof <- lookAheadMatches eof

1534+ mrk <- P.mark

1535+ isEof <- lookAheadMatches P.eof

15591536 let mrk' = if isEof

15601537 then Nothing

15611538 else Just mrk

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

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

15731550

15741551 shebang :: IdrisParser ()

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

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

15761553

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

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

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

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

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

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

15811558 -- Horrid kludge to prevent crashes on Windows

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

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

15901567 (FC failname pos pos, msg)

15911568

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

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

1594−fixColour False doc = ANSI.plain doc

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

1571+fixColour False doc = PP.plain doc

15951572fixColour True doc = doc

15961573

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

15981575-- documentation strings.

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

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

16001577 Idris [PDecl]

16011578parseProg syn fname input mrk

16021579 = do i <- getIState

16031580 case runparser mainProg i fname input of

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

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

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

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

1608− let (fc, msg) = findFC doc

1609− i <- getIState

1610− case idris_outputmode i of

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

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

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

1614− return []

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

1616− reportParserWarnings

1617− return $ collect x

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

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

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

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

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

1586+ i <- getIState

1587+ case idris_outputmode i of

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

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

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

1591+ return []

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

1593+ reportParserWarnings

1594+ return $ collect x

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

16191596 mainProg = case mrk of

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

16211598 Just mrk -> do

1622− release mrk

1599+ P.release mrk

16231600 ds <- prog syn

16241601 i' <- get

16251602 return (ds, i')

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

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

2222import Control.Monad.State.Strict

2323import Data.List

2424import Data.Maybe

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

26− stringLiteral, symbol, whiteSpace)

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

26+import qualified Text.Trifecta as P

2727

2828{- | Parses a record type declaration

2929Record ::=

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

3131-}

3232record :: SyntaxInfo -> IdrisParser PDecl

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

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

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

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

3535 ist <- get

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

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

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

4545 let tyn = expandNS syn tyn_in

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

4747 syn_namespace syn }

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

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

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

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

5151 case cname of

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

6262 ist <- get

6363 fc <- getFC

6464

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

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

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

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

6767 n <- constructor

6868 return (Just n, doc))

6969

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

170170-}

171171data_ :: SyntaxInfo -> IdrisParser PDecl

172172data_ syn = checkDeclFixity $

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

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

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

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

175175 pushIndent

176176 acc <- accessibility

177177 elim <- dataOpts []

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

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

185185 fc <- getFC

186186 (tyn_in, nfc) <- fnName

187− (do try (lchar ':')

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

188188 ty <- typeExpr (allowImp syn)

189189 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

191191 reservedHL "where"

192192 cons <- indentedBlock (constructor syn)

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

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

199199 return x)

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

201201 let tyn = expandNS syn tyn_in

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

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

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

205− let n = show tyn_in ++ " "

206− let s = kw ++ n

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

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

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

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

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

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

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

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

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

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 "

205+ let n = show tyn_in ++ " "

206+ let s = kw ++ n

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

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

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

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

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

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

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

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

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

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

217217 do let cty = bindArgs cargs conty

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

238238-}

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

240240constructor syn

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

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

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

243243 let cn = expandNS syn cn_in

244244 lchar ':'

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

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

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

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

247247 ty <- typeExpr (allowImp syn)

248248 ist <- get

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

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

258258-}

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

260260simpleConstructor syn

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

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

262262 ist <- get

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

264264 (cn_in, nfc) <- fnName

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

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

1919import Prelude hiding (pi)

2020

2121import Control.Applicative

22+import Control.Arrow (left)

2223import Control.Monad

2324import Control.Monad.State.Strict

2425import Data.Function (on)

2526import Data.List

2627import Data.Maybe

2728import Text.Parser.Expression

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

29− stringLiteral, symbol, whiteSpace)

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

30+import qualified Text.Trifecta as P

3031

3132-- | Allow implicit type declarations

3233allowImp :: SyntaxInfo -> SyntaxInfo

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

5354 -}

5455fullExpr :: SyntaxInfo -> IdrisParser PTerm

5556fullExpr syn = do x <- expr syn

56− eof

57+ P.eof

5758 i <- get

5859 return $ debindApp syn (desugar syn i x)

5960

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

61−tryFullExpr syn st input =

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

63− Success tm -> Right tm

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

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

6563

6664{- | Parses an expression

6765@

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

8987@

9088 -}

9189expr' :: SyntaxInfo -> IdrisParser PTerm

92−expr' syn = try (externalExpr syn)

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

9391 <|> internalExpr syn

9492 <?> "expression"

9593

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

140138

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

142140extension syn ns rules =

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

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

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

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

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

146144 n <- extensionSymbol symb

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

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

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

397395-}

398396simpleExpr :: SyntaxInfo -> IdrisParser PTerm

399397simpleExpr syn =

400− try (simpleExternalExpr syn)

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

398+ P.try (simpleExternalExpr syn)

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

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

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

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

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

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

408406 <|> proofExpr syn

409407 <|> tacticsExpr syn

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

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

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

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

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

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

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

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

422420 if inPattern syn

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

424− (do reservedOp "@"

425− s <- simpleExpr syn

426− fcIn <- getFC

427− return (PAs fcIn x s))

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

422+ (do reservedOp "@"

423+ s <- simpleExpr syn

424+ fcIn <- getFC

425+ return (PAs fcIn x s))

428426 else return (PRef fc [fc] x)

429427 <|> idiom syn

430428 <|> listExpr syn

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

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

468466 lchar ')'

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

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

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

472− guardNotPrefix opName

473−

474− e <- expr syn

475− lchar ')'

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

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

478− pexp e]))

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

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

481− lchar ')'

482− fc <- getFC

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

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

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

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

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

470+ guardNotPrefix opName

471+

472+ e <- expr syn

473+ lchar ')'

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

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

476+ pexp e]))

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

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

479+ lchar ')'

480+ fc <- getFC

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

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

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

486484 <|> bracketedExpr syn open l)

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

488486 bracketedExpr (allowConstr syn) open l

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

510508 IsTerm -> exprPart False

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

512510 where nametypePart = do

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

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

514512 (ln, lnfc) <- name

515513 colonFC <- lcharFC ':'

516514 return (ln, lnfc, colonFC)

517515 lty <- expr' syn

518516 starsFC <- reservedOpFC "**"

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

520− namePart = try $ do

518+ namePart = P.try $ do

521519 (ln, lnfc) <- name

522520 starsFC <- reservedOpFC "**"

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

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

590588@

591589-}

592590alt :: 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 "|)"

594592 return (PAlternative [] FirstSuccess alts)

595593

596594{- | Parses a possibly hidden simple expression

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

615613 ;

616614-}

617615unifyLog :: 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")

619617 tm <- simpleExpr syn

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

621619 return (PUnifyLog tm)

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

627625 ;

628626-}

629627runElab :: 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")

631629 fc <- getFC

632630 tm <- simpleExpr syn

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

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

641639-}

642640disamb :: SyntaxInfo -> IdrisParser PTerm

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

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

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

645643 tm <- expr' syn

646644 highlightP kw AnnKeyword

647645 return (PDisamb (map tons ns) tm)

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

656654@

657655-}

658656noImplicits :: SyntaxInfo -> IdrisParser PTerm

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

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

660658 tm <- simpleExpr syn

661659 return (PNoImplicits tm)

662660 <?> "no implicits expression"

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

675673-}

676674app :: SyntaxInfo -> IdrisParser PTerm

677675app syn = do f <- simpleExpr syn

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

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

679677 fc <- getFC

680678 ff <- fst <$> fnName

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

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

737735implicitArg syn = do lchar '{'

738736 (n, nfc) <- name

739737 fc <- getFC

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

741− expr syn)

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

739+ expr syn)

742740 lchar '}'

743741 return (pimp n v True)

744742 <?> "implicit function argument"

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

800798-}

801799namequote :: SyntaxInfo -> IdrisParser PTerm

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

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

804− return (fc, False)) <|>

801+ P.try (do fc <- symbolFC "`{{"

802+ return (fc, False)) <|>

805803 (do fc <- symbolFC "`{"

806804 return (fc, True))

807805 (n, nfc) <- fnName

@@ -871,11 +869,10 @@ recordType syn =

871869 <?> "field setter"

872870

873871 fieldGet :: IdrisParser [Name]

874− fieldGet = sepBy1 (fst <$> fnName) (symbol "->")

872+ fieldGet = P.sepBy1 (fst <$> fnName) (symbol "->")

875873

876874 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])

877− fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')

878− return (Left fs))

875+ fieldGetOrSet = P.try (Left <$> P.sepBy1 fieldSet (lchar ','))

879876 <|> do f <- fieldGet

880877 return (Right f)

881878

@@ -942,15 +939,15 @@ LambdaTail ::=

942939-}

943940lambda :: SyntaxInfo -> IdrisParser PTerm

944941lambda syn = do lchar '\\' <?> "lambda expression"

945− ((do xt <- try $ tyOptDeclList (disallowImp syn)

942+ ((do xt <- P.try $ tyOptDeclList (disallowImp syn)

946943 fc <- getFC

947944 sc <- lambdaTail

948945 return (bindList (\r -> PLam fc) xt sc))

949946 <|>

950− (do ps <- sepBy (do fc <- getFC

951− e <- simpleExpr (disallowImp (syn { inPattern = True }))

952− return (fc, e))

953− (lchar ',')

947+ (do ps <- P.sepBy (do fc <- getFC

948+ e <- simpleExpr (disallowImp (syn { inPattern = True }))

949+ return (fc, e))

950+ (lchar ',')

954951 sc <- lambdaTail

955952 return (pmList (zip [0..] ps) sc)))

956953 <?> "lambda expression"

@@ -996,11 +993,11 @@ TypeSig' ::=

996993@

997994 -}

998995let_ :: SyntaxInfo -> IdrisParser PTerm

999−let_ syn = try (do kw <- reservedFC "let"

1000− ls <- indentedBlock (let_binding syn)

1001− kw' <- reservedFC "in"; sc <- expr syn

1002− highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1003− return (buildLets ls sc))

996+let_ syn = P.try (do kw <- reservedFC "let"

997+ ls <- indentedBlock (let_binding syn)

998+ kw' <- reservedFC "in"; sc <- expr syn

999+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword

1000+ return (buildLets ls sc))

10041001 <?> "let binding"

10051002 where buildLets [] sc = sc

10061003 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

@@ -1010,11 +1007,11 @@ let_ syn = try (do kw <- reservedFC "let"

10101007

10111008let_binding syn = do fc <- getFC;

10121009 pat <- expr' (syn { inPattern = True })

1013− ty <- option Placeholder (do lchar ':'; expr' syn)

1010+ ty <- P.option Placeholder (do lchar ':'; expr' syn)

10141011 lchar '='

10151012 v <- expr (syn { withAppAllowed = isVar pat })

1016− ts <- option [] (do lchar '|'

1017− sepBy1 (do_alt syn) (lchar '|'))

1013+ ts <- P.option [] (do lchar '|'

1014+ P.sepBy1 (do_alt syn) (lchar '|'))

10181015 return (fc,pat,ty,v,ts)

10191016 where isVar (PRef _ _ _) = True

10201017 isVar _ = False

@@ -1079,7 +1076,7 @@ bindsymbol opts st syn

10791076 return (Exp opts st False RigW)

10801077

10811078explicitPi opts st syn

1082− = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

1079+ = do xt <- P.try (lchar '(' *> typeDeclList syn <* lchar ')')

10831080 binder <- bindsymbol opts st syn

10841081 sc <- expr (allowConstr syn)

10851082 return (bindList (\r -> PPi (binder { pcount = r })) xt sc)

@@ -1147,9 +1144,9 @@ unboundPiNoConstraint opts st syn = do

11471144 x <- opExpr syn

11481145 (do binder <- bindsymbol opts st syn

11491146 sc <- expr syn

1150− notFollowedBy $ reservedOp "=>"

1147+ P.notFollowedBy $ reservedOp "=>"

11511148 return (PPi binder (sUN "__pi_arg") NoFC x sc))

1152− <|> do notFollowedBy $ reservedOp "=>"

1149+ <|> do P.notFollowedBy $ reservedOp "=>"

11531150 return x

11541151

11551152

@@ -1158,10 +1155,10 @@ pi syn =

11581155 do opts <- piOpts syn

11591156 st <- static

11601157 explicitPi opts st syn

1161− <|> try (do lchar '{'; implicitPi opts st syn)

1158+ <|> P.try (do lchar '{'; implicitPi opts st syn)

11621159 <|> if constraintAllowed syn

1163− then try (unboundPiNoConstraint opts st syn)

1164− <|> constraintPi opts st syn

1160+ then P.try (unboundPiNoConstraint opts st syn)

1161+ <|> constraintPi opts st syn

11651162 else unboundPi opts st syn

11661163 <?> "dependent type signature"

11671164

@@ -1186,22 +1183,22 @@ ConstraintList ::=

11861183@

11871184-}

11881185constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1189−constraintList syn = try (constraintList1 syn)

1186+constraintList syn = P.try (constraintList1 syn)

11901187 <|> return []

11911188

11921189constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1193−constraintList1 syn = try (do lchar '('

1194− tys <- sepBy1 nexpr (lchar ',')

1195− lchar ')'

1196− reservedOp "=>"

1197− return tys)

1198− <|> try (do t <- opExpr (disallowImp syn)

1199− reservedOp "=>"

1200− return [(RigW, defname, NoFC, t)])

1190+constraintList1 syn = P.try (do lchar '('

1191+ tys <- P.sepBy1 nexpr (lchar ',')

1192+ lchar ')'

1193+ reservedOp "=>"

1194+ return tys)

1195+ <|> P.try (do t <- opExpr (disallowImp syn)

1196+ reservedOp "=>"

1197+ return [(RigW, defname, NoFC, t)])

12011198 <?> "type constraint list"

1202− where nexpr = try (do (n, fc) <- name; lchar ':'

1203− e <- expr (disallowImp syn)

1204− return (RigW, n, fc, e))

1199+ where nexpr = P.try (do (n, fc) <- name; lchar ':'

1200+ e <- expr (disallowImp syn)

1201+ return (RigW, n, fc, e))

12051202 <|> do e <- expr (disallowImp syn)

12061203 return (RigW, defname, NoFC, e)

12071204 defname = sMN 0 "constraint"

@@ -1222,13 +1219,13 @@ FunctionSignatureList ::=

12221219@

12231220-}

12241221typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1225−typeDeclList syn = try (sepBy1 (do rig <- option RigW rigCount

1226− (x, xfc) <- fnName

1227− lchar ':'

1228− t <- typeExpr (disallowImp syn)

1229− return (rig, x, xfc, t))

1230− (lchar ','))

1231− <|> do ns <- sepBy1 name (lchar ',')

1222+typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount

1223+ (x, xfc) <- fnName

1224+ lchar ':'

1225+ t <- typeExpr (disallowImp syn)

1226+ return (rig, x, xfc, t))

1227+ (lchar ','))

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

12321229 lchar ':'

12331230 t <- typeExpr (disallowImp syn)

12341231 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)

@@ -1250,11 +1247,11 @@ NameOrPlaceHolder ::= Name | '_';

12501247@

12511248-}

12521249tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

1253−tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1254− t <- option Placeholder (do lchar ':'

1255− expr syn)

1256− return (RigW, x, fc, t))

1257− (lchar ',')

1250+tyOptDeclList syn = P.sepBy1 (do (x, fc) <- nameOrPlaceholder

1251+ t <- P.option Placeholder (do lchar ':'

1252+ expr syn)

1253+ return (RigW, x, fc, t))

1254+ (lchar ',')

12581255 <?> "type declaration list"

12591256 where nameOrPlaceholder :: IdrisParser (Name, FC)

12601257 nameOrPlaceholder = fnName

@@ -1286,12 +1283,12 @@ ExprList ::=

12861283listExpr :: SyntaxInfo -> IdrisParser PTerm

12871284listExpr syn = do (FC f (l, c) _) <- getFC

12881285 lchar '['; fc <- getFC;

1289− (try . token $ do (char ']' <?> "end of list expression")

1290− (FC _ _ (l', c')) <- getFC

1291− return (mkNil (FC f (l, c) (l', c'))))

1286+ (P.try . P.token $ do (char ']' <?> "end of list expression")

1287+ (FC _ _ (l', c')) <- getFC

1288+ return (mkNil (FC f (l, c) (l', c'))))

12921289 <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"

1293− (do try (lchar '|') <?> "list comprehension"

1294− qs <- sepBy1 (do_ syn) (lchar ',')

1290+ (do P.try (lchar '|') <?> "list comprehension"

1291+ qs <- P.sepBy1 (do_ syn) (lchar ',')

12951292 lchar ']'

12961293 return (PDoBlock (map addGuard qs ++

12971294 [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))

@@ -1350,53 +1347,53 @@ Do ::=

13501347-}

13511348do_ :: SyntaxInfo -> IdrisParser PDo

13521349do_ syn

1353− = try (do kw <- reservedFC "let"

1354− (i, ifc) <- name

1355− ty <- option Placeholder (do lchar ':'

1356− expr' syn)

1357− reservedOp "="

1358− fc <- getFC

1359− e <- expr syn

1360− highlightP kw AnnKeyword

1361− return (DoLet fc RigW i ifc ty e))

1362− <|> try (do kw <- reservedFC "let"

1363− i <- expr' syn

1364− reservedOp "="

1365− fc <- getFC

1366− sc <- expr syn

1367− highlightP kw AnnKeyword

1368− return (DoLetP fc i sc))

1369− <|> try (do kw <- reservedFC "rewrite"

1370− fc <- getFC

1371− sc <- expr syn

1372− highlightP kw AnnKeyword

1373− return (DoRewrite fc sc))

1374− <|> try (do (i, ifc) <- name

1375− symbol "<-"

1376− fc <- getFC

1377− e <- expr (syn { withAppAllowed = False });

1378− option (DoBind fc i ifc e)

1379− (do lchar '|'

1380− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1381− return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1382− <|> try (do i <- expr' syn

1383− symbol "<-"

1384− fc <- getFC

1385− e <- expr (syn { withAppAllowed = False });

1386− option (DoBindP fc i e [])

1387− (do lchar '|'

1388− ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1389− return (DoBindP fc i e ts)))

1350+ = P.try (do kw <- reservedFC "let"

1351+ (i, ifc) <- name

1352+ ty <- P.option Placeholder (do lchar ':'

1353+ expr' syn)

1354+ reservedOp "="

1355+ fc <- getFC

1356+ e <- expr syn

1357+ highlightP kw AnnKeyword

1358+ return (DoLet fc RigW i ifc ty e))

1359+ <|> P.try (do kw <- reservedFC "let"

1360+ i <- expr' syn

1361+ reservedOp "="

1362+ fc <- getFC

1363+ sc <- expr syn

1364+ highlightP kw AnnKeyword

1365+ return (DoLetP fc i sc))

1366+ <|> P.try (do kw <- reservedFC "rewrite"

1367+ fc <- getFC

1368+ sc <- expr syn

1369+ highlightP kw AnnKeyword

1370+ return (DoRewrite fc sc))

1371+ <|> P.try (do (i, ifc) <- name

1372+ symbol "<-"

1373+ fc <- getFC

1374+ e <- expr (syn { withAppAllowed = False });

1375+ P.option (DoBind fc i ifc e)

1376+ (do lchar '|'

1377+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1378+ return (DoBindP fc (PRef ifc [ifc] i) e ts)))

1379+ <|> P.try (do i <- expr' syn

1380+ symbol "<-"

1381+ fc <- getFC

1382+ e <- expr (syn { withAppAllowed = False });

1383+ P.option (DoBindP fc i e [])

1384+ (do lchar '|'

1385+ ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')

1386+ return (DoBindP fc i e ts)))

13901387 <|> do e <- expr syn

13911388 fc <- getFC

13921389 return (DoExp fc e)

13931390 <?> "do block expression"

13941391

13951392do_alt syn = do l <- expr' syn

1396− option (Placeholder, l)

1397− (do symbol "=>"

1398− r <- expr' syn

1399− return (l, r))

1393+ P.option (Placeholder, l)

1394+ (do symbol "=>"

1395+ r <- expr' syn

1396+ return (l, r))

14001397

14011398{- | Parses an expression in idiom brackets

14021399@

@@ -1451,14 +1448,14 @@ constants =

14511448

14521449-- | Parse a constant and its source span

14531450constant :: IdrisParser (Idris.Core.TT.Const, FC)

1454−constant = choice [ do fc <- reservedFC name; return (ty, fc)

1455− | (name, ty) <- constants

1456− ]

1457− <|> do (f, fc) <- try float; return (Fl f, fc)

1451+constant = P.choice [ do fc <- reservedFC name; return (ty, fc)

1452+ | (name, ty) <- constants

1453+ ]

1454+ <|> do (f, fc) <- P.try float; return (Fl f, fc)

14581455 <|> do (i, fc) <- natural; return (BI i, fc)

14591456 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

14601457 <|> 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

14621459 <?> "constant or literal"

14631460

14641461{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1470,11 +1467,11 @@ VerbatimString_t ::=

14701467@

14711468 -}

14721469verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1473−verbatimStringLiteral = token $ do (FC f start _) <- getFC

1474− try $ string "\"\"\""

1475− str <- manyTill anyChar $ try (string "\"\"\"")

1476− (FC _ _ end) <- getFC

1477− return (str, FC f start end)

1470+verbatimStringLiteral = P.token $ do (FC f start _) <- getFC

1471+ P.try $ string "\"\"\""

1472+ str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1473+ (FC _ _ end) <- getFC

1474+ return (str, FC f start end)

14781475

14791476{- | Parses a static modifier

14801477

@@ -1545,7 +1542,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

15451542tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

15461543tactics =

15471544 [ (["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)

15491546 , noArgs ["intros"] Intros

15501547 , noArgs ["unfocus"] Unfocus

15511548 , (["refine"], Just ExprTArg, const $

@@ -1593,7 +1590,7 @@ tactics =

15931590 , noArgs ["trivial"] Trivial

15941591 , noArgs ["unify"] DoUnify

15951592 , (["search"], Nothing, const $

1596− do depth <- option 10 $ fst <$> natural

1593+ do depth <- P.option 10 $ fst <$> natural

15971594 return (ProofSearch True True (fromInteger depth) Nothing [] []))

15981595 , noArgs ["implementation"] TCImplementation

15991596 , noArgs ["solve"] Solve

@@ -1614,7 +1611,7 @@ tactics =

16141611 , ([":doc"], Just ExprTArg, const $

16151612 do whiteSpace

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

1617− eof

1614+ P.eof

16181615 return (TDocStr doc))

16191616 ]

16201617 where

@@ -1630,12 +1627,12 @@ tactics =

16301627

16311628

16321629tactic :: SyntaxInfo -> IdrisParser PTactic

1633−tactic syn = choice [ do choice (map reserved names); parser syn

1634− | (names, _, parser) <- tactics ]

1630+tactic syn = P.choice [ do P.choice (map reserved names); parser syn

1631+ | (names, _, parser) <- tactics ]

16351632 <|> do lchar '{'

16361633 t <- tactic syn;

16371634 lchar ';';

1638− ts <- sepBy1 (tactic syn) (lchar ';')

1635+ ts <- P.sepBy1 (tactic syn) (lchar ';')

16391636 lchar '}'

16401637 return $ TSeq t (mergeSeq ts)

16411638 <|> ((lchar ':' >> empty) <?> "prover command")

@@ -1648,5 +1645,5 @@ tactic syn = choice [ do choice (map reserved names); parser syn

16481645-- | Parses a tactic as a whole

16491646fullTactic :: SyntaxInfo -> IdrisParser PTactic

16501647fullTactic syn = do t <- tactic syn

1651− eof

1648+ P.eof

16521649 return t

src/Idris/Parser/Helpers.hs+108−107

@@ -34,36 +34,33 @@ import System.FilePath

3434import qualified Text.Parser.Char as Chr

3535import Text.Parser.LookAhead

3636import qualified Text.Parser.Token as Tok

37−import qualified Text.Parser.Token.Highlight as Hi

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

39− stringLiteral, symbol, whiteSpace)

40−import Text.Trifecta.Delta

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

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

39+import qualified Text.Trifecta as P

40+import qualified Text.Trifecta.Delta as P

4141

4242-- | Idris parser with state used during parsing

43−type IdrisParser = StateT IState IdrisInnerParser

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

43+type IdrisParser = StateT IState P.Parser

4944

5045#if MIN_VERSION_base(4,9,0)

51−instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

52− line = lift line

46+instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where

47+ line = lift P.line

5348 {-# INLINE line #-}

54− position = lift position

49+ position = lift P.position

5550 {-# 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

5752 {-# INLINE slicedWith #-}

58− rend = lift rend

53+ rend = lift P.rend

5954 {-# INLINE rend #-}

60− restOfLine = lift restOfLine

55+ restOfLine = lift P.restOfLine

6156 {-# INLINE restOfLine #-}

62−

6357#endif

6458

65−instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

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

59+someSpace' :: MonadicParsing m => m ()

60+someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

61+

62+instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where

63+ someSpace = someSpace'

6764 token p = do s <- get

6865 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

6966 -- See Issue #1594

@@ -72,8 +69,9 @@ instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

7269 whiteSpace

7370 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

7471 return r

72+

7573-- | 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)

7775

7876class HasLastTokenSpan m where

7977 getLastTokenSpan :: m (Maybe FC)

@@ -81,11 +79,15 @@ class HasLastTokenSpan m where

8179instance HasLastTokenSpan IdrisParser where

8280 getLastTokenSpan = lastTokenSpan <$> get

8381

82+newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }

83+

8484-- | Helper to run Idris inner parser based stateT parsers

85−runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res

86−runparser p i inputname =

87− parseString (runInnerParser (evalStateT p i))

88− (Directed (UTF8.fromString inputname) 0 0 0 0)

85+runparser :: StateT st P.Parser res -> st -> String -> String -> Either ParseError res

86+runparser p i inputname s =

87+ case P.parseString (evalStateT p i)

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

8991

9092highlightP :: FC -> OutputAnnotation -> IdrisParser ()

9193highlightP fc annot = do ist <- get

@@ -125,7 +127,7 @@ parserWarning fc warnOpt warnErr = do

125127

126128-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

127129simpleWhiteSpace :: MonadicParsing m => m ()

128−simpleWhiteSpace = satisfy isSpace *> pure ()

130+simpleWhiteSpace = () <$ P.satisfy isSpace

129131

130132-- | Checks if a charcter is end of line

131133isEol :: Char -> Bool

@@ -134,7 +136,7 @@ isEol _ = False

134136

135137-- | A parser that succeeds at the end of the line

136138eol :: MonadicParsing m => m ()

137−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

139+eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

138140

139141{- | Consumes a single-line comment

140142

@@ -144,7 +146,7 @@ eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

144146 -}

145147singleLineComment :: MonadicParsing m => m ()

146148singleLineComment = (string "--" *>

147− many (satisfy (not . isEol)) *>

149+ many (P.satisfy (not . isEol)) *>

148150 eol *> pure ())

149151 <?> ""

150152

@@ -166,15 +168,15 @@ singleLineComment = (string "--" *>

166168@

167169-}

168170multiLineComment :: MonadicParsing m => m ()

169−multiLineComment = try (string "{-" *> (string "-}") *> pure ())

171+multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())

170172 <|> string "{-" *> inCommentChars

171173 <?> ""

172174 where inCommentChars :: MonadicParsing m => m ()

173175 inCommentChars = string "-}" *> pure ()

174− <|> try (multiLineComment) *> inCommentChars

175− <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

176− <|> skipSome (noneOf startEnd) *> inCommentChars

177− <|> oneOf startEnd *> inCommentChars

176+ <|> P.try (multiLineComment) *> inCommentChars

177+ <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars

178+ <|> P.skipSome (P.noneOf startEnd) *> inCommentChars

179+ <|> P.oneOf startEnd *> inCommentChars

178180 <?> "end of comment"

179181 startEnd :: String

180182 startEnd = "{}-"

@@ -197,23 +199,23 @@ docComment = do dc <- pushIndent *> docCommentLine

197199 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

198200

199201 where docCommentLine :: MonadicParsing m => m String

200− docCommentLine = try (do string "|||"

201− many (satisfy (==' '))

202− contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

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

204− return $ first:res)

205− eol ; someSpace

206− return contents)-- ++ concat rest))

202+ docCommentLine = P.try (do string "|||"

203+ many (P.satisfy (==' '))

204+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

205+ res <- many (P.satisfy (not . isEol))

206+ return $ first:res)

207+ eol ; someSpace'

208+ return contents)

207209 <?> ""

208210

209211 argDocCommentLine = do string "|||"

210− many (satisfy isSpace)

212+ many (P.satisfy isSpace)

211213 char '@'

212− many (satisfy isSpace)

214+ many (P.satisfy isSpace)

213215 n <- fst <$> name

214− many (satisfy isSpace)

215− docs <- many (satisfy (not . isEol))

216− eol ; someSpace

216+ many (P.satisfy isSpace)

217+ docs <- many (P.satisfy (not . isEol))

218+ eol ; someSpace'

217219 return (n, docs)

218220

219221-- | Parses some white space

@@ -250,23 +252,22 @@ float = do f <- Tok.double

250252

251253{- * Symbols, identifiers, names and operators -}

252254

253−

254−-- | Idris Style for parsing identifiers/reserved keywords

255−idrisStyle :: MonadicParsing m => IdentifierStyle m

256−idrisStyle = IdentifierStyle {

257− _styleName = "Idris"

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",

264− "proof", "postulate", "using", "namespace", "class", "instance",

265− "interface", "implementation", "parameters", "public", "private",

266− "export", "abstract", "implicit", "quoteGoal", "constructor", "if",

267− "then", "else"]

268− , _styleHighlight = Hi.Identifier

269− , _styleReservedHighlight = Hi.ReservedIdentifier }

255+reservedIdentifiers :: HS.HashSet String

256+reservedIdentifiers = HS.fromList

257+ [ "Type"

258+ , "abstract", "case", "class", "codata", "constructor", "corecord", "data"

259+ , "do", "dsl", "else", "export", "if", "implementation", "implicit"

260+ , "import", "impossible", "in", "infix", "infixl", "infixr", "instance"

261+ , "interface", "let", "mutual", "namespace", "of", "parameters", "partial"

262+ , "postulate", "private", "proof", "public", "quoteGoal", "record"

263+ , "rewrite", "syntax", "then", "total", "using", "where", "with"

264+ ]

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

270271

271272char :: MonadicParsing m => Char -> m Char

272273char = Chr.char

@@ -276,26 +277,28 @@ string = Chr.string

276277

277278-- | Parses a character as a token

278279lchar :: MonadicParsing m => Char -> m Char

279−lchar = token . char

280+lchar = P.token . P.char

280281

281282-- | Parses a character as a token, returning the source span of the character

282283lcharFC :: MonadicParsing m => Char -> m FC

283284lcharFC ch = do (FC file (l, c) _) <- getFC

284− _ <- token (char ch)

285+ _ <- P.token (char ch)

285286 return $ FC file (l, c) (l, c+1)

286287

287288-- | Parses string as a token

288−symbol :: MonadicParsing m => String -> m String

289−symbol = Tok.symbol

289+symbol :: MonadicParsing m => String -> m ()

290+symbol = void . Tok.symbol

290291

291292symbolFC :: MonadicParsing m => String -> m FC

292293symbolFC str = do (FC file (l, c) _) <- getFC

293− Tok.symbol str

294+ symbol str

294295 return $ FC file (l, c) (l, c + length str)

295296

296297-- | Parses a reserved identifier

297298reserved :: 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

299302

300303-- | Parses a reserved identifier, computing its span. Assumes that

301304-- reserved identifiers never contain line breaks.

@@ -311,9 +314,9 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

311314-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

312315-- | Parses a reserved operator

313316reservedOp :: MonadicParsing m => String -> m ()

314−reservedOp name = token $ try $

317+reservedOp name = P.token $ P.try $

315318 do string name

316− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

319+ P.notFollowedBy operatorLetter <?> ("end of " ++ show name)

317320

318321reservedOpFC :: MonadicParsing m => String -> m FC

319322reservedOpFC name = do (FC f (l, c) _) <- getFC

@@ -322,27 +325,25 @@ reservedOpFC name = do (FC f (l, c) _) <- getFC

322325

323326-- | Parses an identifier as a token

324327identifier :: (MonadicParsing m) => m (String, FC)

325−identifier = try(do (i, fc) <-

326− token $ do (FC f (l, c) _) <- getFC

327− i <- Tok.ident idrisStyle

328− return (i, FC f (l, c) (l, c + length i))

329− when (i == "_") $ unexpected "wildcard"

330− return (i, fc))

328+identifier = P.try $ do

329+ (FC f (l, c) _) <- getFC

330+ ident <- identifierOrReserved

331+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident

332+ when (ident == "_") $ P.unexpected "wildcard"

333+ return (ident, FC f (l, c) (l, c + length ident))

331334

332335-- | Parses an identifier with possible namespace as a name

333−iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

334−iName bad = do (n, fc) <- maybeWithNS identifier False bad

335− return (n, fc)

336− <?> "name"

336+iName :: (MonadicParsing m) => [String] -> m (Name, FC)

337+iName bad = maybeWithNS identifier False bad <?> "name"

337338

338339-- | 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)

340341maybeWithNS parser ascend bad = do

341342 fc <- getFC

342− i <- option "" (lookAhead (fst <$> identifier))

343− when (i `elem` bad) $ unexpected "reserved identifier"

343+ i <- P.option "" (lookAhead (fst <$> identifier))

344+ when (i `elem` bad) $ P.unexpected "reserved identifier"

344345 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))

346347 return (mkName (x, xs), fc)

347348 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

348349 parserNoNS parser = do startFC <- getFC

@@ -354,7 +355,7 @@ maybeWithNS parser ascend bad = do

354355 lchar '.'; (x, nameFC) <- parser

355356 return (x, xs, spanFC startFC nameFC)

356357 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)]

358359

359360-- | Parses a name

360361name :: IdrisParser (Name, FC)

@@ -393,11 +394,11 @@ opChars :: String

393394opChars = ":!#$%&*+./<=>?@\\^|-~"

394395

395396operatorLetter :: MonadicParsing m => m Char

396−operatorLetter = oneOf opChars

397+operatorLetter = P.oneOf opChars

397398

398399-- | Parse a package name

399400packageName :: MonadicParsing m => m String

400−packageName = (:) <$> oneOf firstChars <*> many (oneOf remChars)

401+packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)

401402 where firstChars = ['a'..'z'] ++ ['A'..'Z']

402403 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

403404

@@ -409,7 +410,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%

409410

410411-- | Parses an operator

411412symbolicOperator :: MonadicParsing m => m String

412−symbolicOperator = do op <- token . some $ operatorLetter

413+symbolicOperator = do op <- P.token . some $ operatorLetter

413414 when (op `elem` (invalidOperators ++ commentMarkers)) $

414415 fail $ op ++ " is not a valid operator"

415416 return op

@@ -422,24 +423,24 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC

422423

423424{- * Position helpers -}

424425{- | Get filename from position (returns "(interactive)" when no source file is given) -}

425−fileName :: Delta -> String

426−fileName (Directed fn _ _ _ _) = UTF8.toString fn

427−fileName _ = "(interactive)"

426+fileName :: P.Delta -> String

427+fileName (P.Directed fn _ _ _ _) = UTF8.toString fn

428+fileName _ = "(interactive)"

428429

429430{- | Get line number from position -}

430−lineNum :: Delta -> Int

431−lineNum (Lines l _ _ _) = fromIntegral l + 1

432−lineNum (Directed _ l _ _ _) = fromIntegral l + 1

431+lineNum :: P.Delta -> Int

432+lineNum (P.Lines l _ _ _) = fromIntegral l + 1

433+lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1

433434lineNum _ = 0

434435

435436{- | Get column number from position -}

436−columnNum :: Delta -> Int

437−columnNum pos = fromIntegral (column pos) + 1

437+columnNum :: P.Delta -> Int

438+columnNum pos = fromIntegral (P.column pos) + 1

438439

439440

440441{- | Get file position as FC -}

441442getFC :: MonadicParsing m => m FC

442−getFC = do s <- position

443+getFC = do s <- P.position

443444 let (dir, file) = splitFileName (fileName s)

444445 let f = if dir == addTrailingPathSeparator "." then file else fileName s

445446 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)

456457{- | @commaSeparated p@ parses one or more occurences of `p`,

457458 separated by commas and optional whitespace. -}

458459commaSeparated :: 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)

460461

461462{- * Layout helpers -}

462463

463464-- | Push indentation to stack

464465pushIndent :: IdrisParser ()

465−pushIndent = do pos <- position

466+pushIndent = do pos <- P.position

466467 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 })

468469

469470-- | Pops indentation from stack

470471popIndent :: IdrisParser ()

@@ -476,7 +477,7 @@ popIndent = do ist <- get

476477

477478-- | Gets current indentation

478479indent :: IdrisParser Int

479−indent = liftM ((+1) . fromIntegral . column) position

480+indent = liftM ((+1) . fromIntegral . P.column) P.position

480481

481482-- | Gets last indentation

482483lastIndent :: IdrisParser Int

@@ -544,7 +545,7 @@ openBlock = do lchar '{'

544545closeBlock :: IdrisParser ()

545546closeBlock = do ist <- get

546547 bs <- case brace_stack ist of

547− [] -> eof >> return []

548+ [] -> [] <$ P.eof

548549 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

549550 Just lvl : xs -> (do i <- indent

550551 isParen <- lookAheadMatches (char ')')

@@ -553,7 +554,7 @@ closeBlock = do ist <- get

553554 then fail "not end of block"

554555 else return xs)

555556 <|> (do notOpenBraces

556− eof

557+ P.eof

557558 return [])

558559 put (ist { brace_stack = bs })

559560

@@ -562,19 +563,19 @@ terminator :: IdrisParser ()

562563terminator = do lchar ';'; popIndent

563564 <|> do c <- indent; l <- lastIndent

564565 if c <= l then popIndent else fail "not a terminator"

565− <|> do isParen <- lookAheadMatches (oneOf ")}")

566+ <|> do isParen <- lookAheadMatches (P.oneOf ")}")

566567 if isParen then popIndent else fail "not a terminator"

567− <|> lookAhead eof

568+ <|> lookAhead P.eof

568569

569570-- | Parses and keeps a terminator

570571keepTerminator :: IdrisParser ()

571−keepTerminator = do lchar ';'; return ()

572+keepTerminator = () <$ lchar ';'

572573 <|> do c <- indent; l <- lastIndent

573574 unless (c <= l) $ fail "not a terminator"

574− <|> do isParen <- lookAheadMatches (oneOf ")}|")

575+ <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

575576 isIn <- lookAheadMatches (reserved "in")

576577 unless (isIn || isParen) $ fail "not a terminator"

577− <|> lookAhead eof

578+ <|> lookAhead P.eof

578579

579580-- | Checks if application expression does not end

580581notEndApp :: IdrisParser ()

src/Idris/Parser/Ops.hs+11−11

@@ -22,8 +22,8 @@ import Control.Monad.State.Strict

2222import Data.Char (isAlpha)

2323import Data.List

2424import Text.Parser.Expression

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

26− stringLiteral, symbol, whiteSpace)

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

26+import qualified Text.Trifecta as P

2727

2828-- | Creates table for fixity declarations to build expression parser

2929-- using pre-build and user-defined operator/fixity declarations

@@ -49,8 +49,8 @@ table fixes

4949 noFixityOperator :: Operator IdrisParser PTerm

5050 noFixityOperator = flip Infix AssocNone $ do

5151 indentGt

52− op <- try symbolicOperator

53− unexpected $ "Operator without known fixity: " ++ op

52+ op <- P.try symbolicOperator

53+ P.unexpected $ "Operator without known fixity: " ++ op

5454

5555 -- | Calculates table for fixity declarations

5656 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

@@ -71,7 +71,7 @@ table fixes

7171

7272 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

7373 binary name assoc f

74− | isBacktick name = flip Infix assoc $ try $ do

74+ | isBacktick name = flip Infix assoc $ P.try $ do

7575 (n, fc) <- backtickOperator

7676 guard $ show (nsroot n) == name

7777 return $ f fc n

@@ -96,7 +96,7 @@ table fixes

9696@

9797-}

9898backtickOperator :: IdrisParser (Name, FC)

99−backtickOperator = between (indentGt *> lchar '`') (indentGt *> lchar '`') name

99+backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name

100100

101101{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

102102

@@ -123,9 +123,9 @@ operatorName = first sUN <$> symbolicOperatorFC

123123

124124-}

125125operatorFront :: IdrisParser (Name, FC)

126−operatorFront = try (do (FC f (l, c) _) <- getFC

127− op <- lchar '(' *> reservedOp "=" <* lchar ')'

128− return (eqTy, FC f (l, c) (l, c+3)))

126+operatorFront = P.try (do (FC f (l, c) _) <- getFC

127+ op <- lchar '(' *> reservedOp "=" <* lchar ')'

128+ return (eqTy, FC f (l, c) (l, c+3)))

129129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC

130130 op <- lchar '(' *> symbolicOperator

131131 (FC _ _ (l', c')) <- getFC

@@ -139,7 +139,7 @@ operatorFront = try (do (FC f (l, c) _) <- getFC

139139@

140140-}

141141fnName :: IdrisParser (Name, FC)

142−fnName = try operatorFront <|> name <?> "function name"

142+fnName = P.try operatorFront <|> name <?> "function name"

143143

144144{- | Parses a fixity declaration

145145@

@@ -151,7 +151,7 @@ Fixity ::=

151151fixity :: IdrisParser PDecl

152152fixity = do pushIndent

153153 f <- fixityType; i <- fst <$> natural;

154− ops <- sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

154+ ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

155155 terminator

156156 let prec = fromInteger i

157157 istate <- get

src/Idris/Prover.hs+23−24

@@ -43,7 +43,6 @@ import Control.Monad.State.Strict

4343import System.Console.Haskeline

4444import System.Console.Haskeline.History

4545import System.IO (Handle, hPutStrLn, stdin, stdout)

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

4746

4847-- | Launch the proof shell

4948prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

@@ -312,15 +311,15 @@ elabloop info fn d prompt prf e prev h env

312311

313312 -- if we're abandoning, it has to be outside the scope of the catch

314313 case cmd of

315− Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

314+ Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

316315 _ -> return ()

317316

318317 (d, prev', st, done, prf', env', res) <-

319318 idrisCatch

320319 (case cmd of

321− Failure (ErrInfo err _) ->

322− return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

323− Success (Left cmd') ->

320+ Left err ->

321+ return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) . parseErrorDoc $ err)

322+ Right (Left cmd') ->

324323 case cmd' of

325324 EQED -> do hs <- lifte e get_holes

326325 unless (null hs) $ ifail "Incomplete proof"

@@ -345,7 +344,7 @@ elabloop info fn d prompt prf e prev h env

345344 return (d', prev, st', done, prf', env, go)

346345 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

347346 return (d', prev, st', done, prf', env, go)

348− Success (Right cmd') ->

347+ Right (Right cmd') ->

349348 case cmd' of

350349 DoLetP {} -> ifail "Pattern-matching let not supported here"

351350 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

@@ -430,27 +429,27 @@ ploop fn d prompt prf e h

430429 Nothing -> do iPrintError ""; ifail "Abandoned"

431430 Just input -> return (parseTactic i input, input)

432431 case cmd of

433− Success Abandon -> do iPrintError ""; ifail "Abandoned"

432+ Right Abandon -> do iPrintError ""; ifail "Abandoned"

434433 _ -> return ()

435434 (d, st, done, prf', res) <- idrisCatch

436435 (case cmd of

437− Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

438− Success Undo -> do (_, st) <- elabStep e loadState

439− return (True, st, False, init prf, Right $ iPrintResult "")

440− Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

441− Success ProofTerm -> do tm <- lifte e get_term

442− iputStrLn $ "TT: " ++ show tm ++ "\n"

443− return (False, e, False, prf, Right $ iPrintResult "")

444− Success Qed -> do hs <- lifte e get_holes

445− unless (null hs) $ ifail "Incomplete proof"

446− iputStrLn "Proof completed!"

447− return (False, e, True, prf, Right $ iPrintResult "")

448− Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

449− Success (TCheck t) -> checkType e prf t

450− Success (TEval t) -> evalTerm e prf t

451− Success (TDocStr x) -> docStr e prf x

452− Success (TSearch t) -> search e prf t

453− Success tac ->

436+ Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

437+ Right Undo -> do (_, st) <- elabStep e loadState

438+ return (True, st, False, init prf, Right $ iPrintResult "")

439+ Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

440+ Right ProofTerm -> do tm <- lifte e get_term

441+ iputStrLn $ "TT: " ++ show tm ++ "\n"

442+ return (False, e, False, prf, Right $ iPrintResult "")

443+ Right Qed -> do hs <- lifte e get_holes

444+ unless (null hs) $ ifail "Incomplete proof"

445+ iputStrLn "Proof completed!"

446+ return (False, e, True, prf, Right $ iPrintResult "")

447+ Right (TCheck (PRef _ _ n)) -> checkNameType e prf n

448+ Right (TCheck t) -> checkType e prf t

449+ Right (TEval t) -> evalTerm e prf t

450+ Right (TDocStr x) -> docStr e prf x

451+ Right (TSearch t) -> search e prf t

452+ Right tac ->

454453 do (_, e) <- elabStep e saveState

455454 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

456455 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

src/Idris/REPL.hs+22−26

@@ -93,7 +93,6 @@ import System.FSNotify (watchDir, withManager)

9393import System.FSNotify.Devel (allEvents, doAllEvents)

9494import System.IO

9595import System.Process

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

9796import Util.DynamicLinker

9897import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

9998import Util.Pretty hiding ((</>))

@@ -177,9 +176,9 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

177176 IO (IState, FilePath)

178177processNetCmd orig i h fn cmd

179178 = do res <- case parseCmd i "(net)" cmd of

180− Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))

181− Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182− Success (Left err) -> return (Left (Msg err))

179+ Left err -> return (Left (Msg " invalid command"))

180+ Right (Right c) -> runExceptT $ evalStateT (processNet fn c) i

181+ Right (Left err) -> return (Left (Msg err))

183182 case res of

184183 Right x -> return x

185184 Left err -> do hPutStrLn h (show err)

@@ -295,8 +294,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

295294 do c <- colourise

296295 i <- getIState

297296 case parseCmd i "(input)" cmd of

298− Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)

299− Success (Right (Prove mode n')) ->

297+ Left err -> iPrintError . show . fixColour False . parseErrorDoc $ err

298+ Right (Right (Prove mode n')) ->

300299 idrisCatch

301300 (do process fn (Prove mode n')

302301 isetPrompt (mkPrompt mods)

@@ -315,10 +314,10 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

315314 IdeMode.convSExp "abandon-proof" "Abandoned" n

316315 _ -> return ()

317316 iRenderError $ pprintErr ist e)

318− Success (Right cmd) -> idrisCatch

317+ Right (Right cmd) -> idrisCatch

319318 (idemodeProcess fn cmd)

320319 (\e -> getIState >>= iRenderError . flip pprintErr e)

321− Success (Left err) -> iPrintError err

320+ Right (Left err) -> iPrintError err

322321runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

323322 do (unused, compls) <- replCompletion (reverse str, "")

324323 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

@@ -353,8 +352,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

353352 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

354353runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

355354 case parseConst orig name of

356− Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357− Failure _ ->

355+ Right c -> process "(idemode)" (DocStr (Right c) (howMuch w))

356+ Left _ ->

358357 case splitName name of

359358 Left err -> iPrintError err

360359 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

@@ -727,11 +726,10 @@ processInput cmd orig inputs efile

727726 let fn = fromMaybe "" (listToMaybe inputs)

728727 c <- colourise

729728 case parseCmd i "(input)" cmd of

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

731− return (Just inputs)

732− Success (Right Reload) ->

729+ Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)

730+ Right (Right Reload) ->

733731 reload orig inputs

734− Success (Right Watch) ->

732+ Right (Right Watch) ->

735733 if null inputs then

736734 do iputStrLn "No loaded files to watch."

737735 return (Just inputs)

@@ -739,7 +737,7 @@ processInput cmd orig inputs efile

739737 do iputStrLn efile

740738 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

741739 watch orig inputs

742− Success (Right (Load f toline)) ->

740+ Right (Right (Load f toline)) ->

743741 -- The $!! here prevents a space leak on reloading.

744742 -- This isn't a solution - but it's a temporary stopgap.

745743 -- See issue #2386

@@ -749,22 +747,20 @@ processInput cmd orig inputs efile

749747 clearErr

750748 mod <- loadInputs [f] toline

751749 return (Just mod)

752− Success (Right (ModImport f)) ->

750+ Right (Right (ModImport f)) ->

753751 do clearErr

754752 fmod <- loadModule f (IBC_REPL True)

755753 return (Just (inputs ++ maybe [] (:[]) fmod))

756− Success (Right Edit) -> do -- takeMVar stvar

754+ Right (Right Edit) -> do -- takeMVar stvar

757755 edit efile orig

758756 return (Just inputs)

759− Success (Right Proofs) -> do proofs orig

760− return (Just inputs)

761− Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")

762− return Nothing

763− Success (Right cmd ) -> do idrisCatch (process fn cmd)

764− (\e -> do msg <- showErr e ; iputStrLn msg)

765− return (Just inputs)

766− Success (Left err) -> do runIO $ putStrLn err

757+ Right (Right Proofs) -> Just inputs <$ proofs orig

758+ Right (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye")

759+ Right (Right cmd ) -> do idrisCatch (process fn cmd)

760+ (\e -> do msg <- showErr e ; iputStrLn msg)

767761 return (Just inputs)

762+ Right (Left err) -> do runIO $ putStrLn err

763+ return (Just inputs)

768764

769765resolveProof :: Name -> Idris Name

770766resolveProof n'

@@ -1429,7 +1425,7 @@ process fn (Browse ns) =

14291425process fn (MakeDoc s) =

14301426 do istate <- getIState

14311427 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

14331429 parse n = Left n

14341430 (bad, nss) = partitionEithers $ map parse names

14351431 cd <- runIO getCurrentDirectory

src/Idris/REPL/Parser.hs+124−125

@@ -17,10 +17,10 @@ import Idris.Core.TT

1717import Idris.Help

1818import Idris.Imports

1919import Idris.Options

20−import qualified Idris.Parser as P

21−import qualified Idris.Parser.Expr as P

22−import qualified Idris.Parser.Helpers as P

23−import qualified Idris.Parser.Ops as P

20+import qualified Idris.Parser as IP

21+import qualified Idris.Parser.Expr as IP

22+import qualified Idris.Parser.Helpers as IP

23+import qualified Idris.Parser.Ops as IP

2424

2525import Idris.REPL.Commands

2626

@@ -33,15 +33,14 @@ import System.Console.ANSI (Color(..))

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

3434import Text.Parser.Char (anyChar, oneOf)

3535import Text.Parser.Combinators

36−import Text.Trifecta (Result)

3736

38−parseCmd :: IState -> String -> String -> Result (Either String Command)

39−parseCmd i inputname = P.runparser pCmd i inputname . trim

37+parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

38+parseCmd i inputname = IP.runparser pCmd i inputname . trim

4039 where trim = f . f

4140 where f = reverse . dropWhile isSpace

4241

4342type CommandTable = [ ( [String], CmdArg, String

44− , String -> P.IdrisParser (Either String Command) ) ]

43+ , String -> IP.IdrisParser (Either String Command) ) ]

4544

4645setOptions :: [(String, Opt)]

4746setOptions = [("errorcontext", ErrContext),

@@ -168,8 +167,8 @@ parserCommands =

168167 , cmd_refine)

169168 , (["debugunify"], SeqArgs ExprArg ExprArg

170169 , "(Debugging) Try to unify two expressions", const $ do

171− l <- P.simpleExpr defaultSyntax

172− r <- P.simpleExpr defaultSyntax

170+ l <- IP.simpleExpr defaultSyntax

171+ r <- IP.simpleExpr defaultSyntax

173172 eof

174173 return (Right (DebugUnify l r))

175174 )

@@ -188,7 +187,7 @@ optArgCmd names command doc =

188187proofArgCmd names command doc =

189188 (names, NoArg, doc, proofArg command)

190189

191−pCmd :: P.IdrisParser (Either String Command)

190+pCmd :: IP.IdrisParser (Either String Command)

192191pCmd = choice [ do c <- cmd names; parser c

193192 | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

194193 <|> unrecognized

@@ -196,23 +195,23 @@ pCmd = choice [ do c <- cmd names; parser c

196195 <|> eval

197196 where nop = do eof; return (Right NOP)

198197 unrecognized = do

199− P.lchar ':'

198+ IP.lchar ':'

200199 cmd <- many anyChar

201200 let cmd' = takeWhile (/=' ') cmd

202201 return (Left $ "Unrecognized command: " ++ cmd')

203202

204−cmd :: [String] -> P.IdrisParser String

203+cmd :: [String] -> IP.IdrisParser String

205204cmd xs = try $ do

206− P.lchar ':'

205+ IP.lchar ':'

207206 docmd sorted_xs

208207

209208 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

211210

212211 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

213212

214213

215−noArgs :: Command -> String -> P.IdrisParser (Either String Command)

214+noArgs :: Command -> String -> IP.IdrisParser (Either String Command)

216215noArgs cmd name = do

217216 let emptyArgs = do

218217 eof

@@ -222,29 +221,29 @@ noArgs cmd name = do

222221

223222 emptyArgs <|> failure

224223

225−eval :: P.IdrisParser (Either String Command)

224+eval :: IP.IdrisParser (Either String Command)

226225eval = do

227− t <- P.fullExpr defaultSyntax

226+ t <- IP.fullExpr defaultSyntax

228227 return $ Right (Eval t)

229228

230−exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

229+exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)

231230exprArg cmd name = do

232231 let noArg = do

233232 eof

234233 return $ Left ("Usage is :" ++ name ++ " <expression>")

235234

236235 let justOperator = do

237− (op, fc) <- P.symbolicOperatorFC

236+ (op, fc) <- IP.symbolicOperatorFC

238237 eof

239238 return $ Right $ cmd (PRef fc [] (sUN op))

240239

241240 let properArg = do

242− t <- P.fullExpr defaultSyntax

241+ t <- IP.fullExpr defaultSyntax

243242 return $ Right (cmd t)

244243 try noArg <|> try justOperator <|> properArg

245244

246−genArg :: String -> P.IdrisParser a -> (a -> Command)

247− -> String -> P.IdrisParser (Either String Command)

245+genArg :: String -> IP.IdrisParser a -> (a -> Command)

246+ -> String -> IP.IdrisParser (Either String Command)

248247genArg argName argParser cmd name = do

249248 let emptyArgs = do eof; failure

250249 oneArg = do arg <- argParser

@@ -254,24 +253,24 @@ genArg argName argParser cmd name = do

254253 where

255254 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

256255

257−nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

258−nameArg = genArg "name" $ fst <$> P.name

259−fnNameArg = genArg "functionname" $ fst <$> P.fnName

256+nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)

257+nameArg = genArg "name" $ fst <$> IP.name

258+fnNameArg = genArg "functionname" $ fst <$> IP.fnName

260259

261−strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

260+strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

262261strArg = genArg "string" (many anyChar)

263262

264−moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

265−moduleArg = genArg "module" (fmap (toPath . fst) P.identifier)

263+moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

264+moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)

266265 where

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

268267

269−namespaceArg :: ([String] -> Command) -> String -> P.IdrisParser (Either String Command)

270−namespaceArg = genArg "namespace" (fmap (toNS . fst) P.identifier)

268+namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)

269+namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

271270 where

272271 toNS = splitOn "."

273272

274−optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

273+optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)

275274optArg cmd name = do

276275 let emptyArgs = do

277276 eof

@@ -279,7 +278,7 @@ optArg cmd name = do

279278

280279 let oneArg = do

281280 o <- pOption

282− P.whiteSpace

281+ IP.whiteSpace

283282 eof

284283 return (Right (cmd o))

285284

@@ -288,58 +287,58 @@ optArg cmd name = do

288287 try emptyArgs <|> oneArg <|> failure

289288

290289 where

291− pOption :: P.IdrisParser Opt

292− pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (P.symbol a); return b) setOptions

290+ pOption :: IP.IdrisParser Opt

291+ pOption = foldl (<|>) empty $ map (\(a, b) -> do discard (IP.symbol a); return b) setOptions

293292

294−proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

293+proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)

295294proofArg cmd name = do

296295 upd <- option False $ do

297− P.lchar '!'

296+ IP.lchar '!'

298297 return True

299− l <- fst <$> P.natural

300− n <- fst <$> P.name;

298+ l <- fst <$> IP.natural

299+ n <- fst <$> IP.name;

301300 return (Right (cmd upd (fromInteger l) n))

302301

303−cmd_doc :: String -> P.IdrisParser (Either String Command)

302+cmd_doc :: String -> IP.IdrisParser (Either String Command)

304303cmd_doc name = do

305304 let constant = do

306− c <- fmap fst P.constant

305+ c <- fmap fst IP.constant

307306 eof

308307 return $ Right (DocStr (Right c) FullDocs)

309308

310309 let pType = do

311− P.reserved "Type"

310+ IP.reserved "Type"

312311 eof

313− return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

312+ return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)

314313

315314 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

316315

317316 try constant <|> pType <|> fnName

318317

319−cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

318+cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)

320319cmd_consolewidth name = do

321320 w <- pConsoleWidth

322321 return (Right (SetConsoleWidth w))

323322

324323 where

325− pConsoleWidth :: P.IdrisParser ConsoleWidth

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

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

328− <|> do n <- fmap (fromInteger . fst) P.natural

324+ pConsoleWidth :: IP.IdrisParser ConsoleWidth

325+ pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth

326+ <|> do discard (IP.symbol "infinite"); return InfinitelyWide

327+ <|> do n <- fmap (fromInteger . fst) IP.natural

329328 return (ColsWide n)

330329

331−cmd_printdepth :: String -> P.IdrisParser (Either String Command)

332−cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) P.natural)

330+cmd_printdepth :: String -> IP.IdrisParser (Either String Command)

331+cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

333332 return (Right $ SetPrinterDepth d)

334333

335−cmd_execute :: String -> P.IdrisParser (Either String Command)

334+cmd_execute :: String -> IP.IdrisParser (Either String Command)

336335cmd_execute name = do

337− tm <- option maintm (P.fullExpr defaultSyntax)

336+ tm <- option maintm (IP.fullExpr defaultSyntax)

338337 return (Right (Execute tm))

339338 where

340339 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

341340

342−cmd_dynamic :: String -> P.IdrisParser (Either String Command)

341+cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

343342cmd_dynamic name = do

344343 let optArg = do l <- many anyChar

345344 if (l /= "")

@@ -348,101 +347,101 @@ cmd_dynamic name = do

348347 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349348 try optArg <|> failure

350349

351−cmd_pprint :: String -> P.IdrisParser (Either String Command)

350+cmd_pprint :: String -> IP.IdrisParser (Either String Command)

352351cmd_pprint name = do

353352 fmt <- ppFormat

354− P.whiteSpace

355− n <- fmap (fromInteger . fst) P.natural

356− P.whiteSpace

357− t <- P.fullExpr defaultSyntax

353+ IP.whiteSpace

354+ n <- fmap (fromInteger . fst) IP.natural

355+ IP.whiteSpace

356+ t <- IP.fullExpr defaultSyntax

358357 return (Right (PPrint fmt n t))

359358

360359 where

361− ppFormat :: P.IdrisParser OutputFmt

362− ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

363− <|> (discard (P.symbol "latex") >> return LaTeXOutput)

360+ ppFormat :: IP.IdrisParser OutputFmt

361+ ppFormat = (discard (IP.symbol "html") >> return HTMLOutput)

362+ <|> (discard (IP.symbol "latex") >> return LaTeXOutput)

364363

365−cmd_compile :: String -> P.IdrisParser (Either String Command)

364+cmd_compile :: String -> IP.IdrisParser (Either String Command)

366365cmd_compile name = do

367366 let defaultCodegen = Via IBCFormat "c"

368367

369− let codegenOption :: P.IdrisParser Codegen

368+ let codegenOption :: IP.IdrisParser Codegen

370369 codegenOption = do

371− let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

372− viaCodegen = do x <- fst <$> P.identifier

370+ let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode

371+ viaCodegen = do x <- fst <$> IP.identifier

373372 return (Via IBCFormat (map toLower x))

374373 bytecodeCodegen <|> viaCodegen

375374

376375 let hasOneArg = do

377376 i <- get

378− f <- fst <$> P.identifier

377+ f <- fst <$> IP.identifier

379378 eof

380379 return $ Right (Compile defaultCodegen f)

381380

382381 let hasTwoArgs = do

383382 i <- get

384383 codegen <- codegenOption

385− f <- fst <$> P.identifier

384+ f <- fst <$> IP.identifier

386385 eof

387386 return $ Right (Compile codegen f)

388387

389388 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

390389 try hasTwoArgs <|> try hasOneArg <|> failure

391390

392−cmd_addproof :: String -> P.IdrisParser (Either String Command)

391+cmd_addproof :: String -> IP.IdrisParser (Either String Command)

393392cmd_addproof name = do

394393 n <- option Nothing $ do

395− x <- fst <$> P.name

394+ x <- fst <$> IP.name

396395 return (Just x)

397396 eof

398397 return (Right (AddProof n))

399398

400−cmd_log :: String -> P.IdrisParser (Either String Command)

399+cmd_log :: String -> IP.IdrisParser (Either String Command)

401400cmd_log name = do

402− i <- fmap (fromIntegral . fst) P.natural

401+ i <- fmap (fromIntegral . fst) IP.natural

403402 eof

404403 return (Right (LogLvl i))

405404

406−cmd_verb :: String -> P.IdrisParser (Either String Command)

405+cmd_verb :: String -> IP.IdrisParser (Either String Command)

407406cmd_verb name = do

408− i <- fmap (fromIntegral . fst) P.natural

407+ i <- fmap (fromIntegral . fst) IP.natural

409408 eof

410409 return (Right (Verbosity i))

411410

412−cmd_cats :: String -> P.IdrisParser (Either String Command)

411+cmd_cats :: String -> IP.IdrisParser (Either String Command)

413412cmd_cats name = do

414− cs <- sepBy pLogCats (P.whiteSpace)

413+ cs <- sepBy pLogCats (IP.whiteSpace)

415414 eof

416415 return $ Right $ LogCategory (concat cs)

417416 where

418417 badCat = do

419− c <- fst <$> P.identifier

418+ c <- fst <$> IP.identifier

420419 fail $ "Category: " ++ c ++ " is not recognised."

421420

422− pLogCats :: P.IdrisParser [LogCat]

423− pLogCats = try (P.symbol (strLogCat IParse) >> return parserCats)

424− <|> try (P.symbol (strLogCat IElab) >> return elabCats)

425− <|> try (P.symbol (strLogCat ICodeGen) >> return codegenCats)

426− <|> try (P.symbol (strLogCat ICoverage) >> return [ICoverage])

427− <|> try (P.symbol (strLogCat IIBC) >> return [IIBC])

428− <|> try (P.symbol (strLogCat IErasure) >> return [IErasure])

421+ pLogCats :: IP.IdrisParser [LogCat]

422+ pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))

423+ <|> try (elabCats <$ IP.symbol (strLogCat IElab))

424+ <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

425+ <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

426+ <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))

427+ <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))

429428 <|> badCat

430429

431−cmd_let :: String -> P.IdrisParser (Either String Command)

430+cmd_let :: String -> IP.IdrisParser (Either String Command)

432431cmd_let name = do

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

432+ defn <- concat <$> many (IP.decl defaultSyntax)

434433 return (Right (NewDefn defn))

435434

436−cmd_unlet :: String -> P.IdrisParser (Either String Command)

437−cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> P.name)

435+cmd_unlet :: String -> IP.IdrisParser (Either String Command)

436+cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)

438437

439−cmd_loadto :: String -> P.IdrisParser (Either String Command)

438+cmd_loadto :: String -> IP.IdrisParser (Either String Command)

440439cmd_loadto name = do

441− toline <- fmap (fromInteger . fst) P.natural

440+ toline <- fmap (fromInteger . fst) IP.natural

442441 f <- many anyChar;

443442 return (Right (Load f (Just toline)))

444443

445−cmd_colour :: String -> P.IdrisParser (Either String Command)

444+cmd_colour :: String -> IP.IdrisParser (Either String Command)

446445cmd_colour name = fmap Right pSetColourCmd

447446

448447 where

@@ -458,29 +457,29 @@ cmd_colour name = fmap Right pSetColourCmd

458457 , ("default", Nothing)

459458 ]

460459

461− pSetColourCmd :: P.IdrisParser Command

460+ pSetColourCmd :: IP.IdrisParser Command

462461 pSetColourCmd = (do c <- pColourType

463462 let defaultColour = IdrisColour Nothing True False False False

464− opts <- sepBy pColourMod (P.whiteSpace)

463+ opts <- sepBy pColourMod (IP.whiteSpace)

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

466465 return $ SetColour c colour)

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

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

466+ <|> try (IP.symbol "on" >> return ColourOn)

467+ <|> try (IP.symbol "off" >> return ColourOff)

469468

470− pColour :: P.IdrisParser (Maybe Color)

469+ pColour :: IP.IdrisParser (Maybe Color)

471470 pColour = doColour colours

472471 where doColour [] = fail "Unknown colour"

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

474−

475− pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)

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

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

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

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

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

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

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

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

472+ doColour ((s, c):cs) = (try (IP.symbol s) >> return c) <|> doColour cs

473+

474+ pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)

475+ pColourMod = try (doVivid <$ IP.symbol "vivid")

476+ <|> try (doDull <$ IP.symbol "dull")

477+ <|> try (doUnderline <$ IP.symbol "underline")

478+ <|> try (doNoUnderline <$ IP.symbol "nounderline")

479+ <|> try (doBold <$ IP.symbol "bold")

480+ <|> try (doNoBold <$ IP.symbol "nobold")

481+ <|> try (doItalic <$ IP.symbol "italic")

482+ <|> try (doNoItalic <$ IP.symbol "noitalic")

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

485484 where doVivid i = i { vivid = True }

486485 doDull i = i { vivid = False }

@@ -497,44 +496,44 @@ cmd_colour name = fmap Right pSetColourCmd

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

498497 enumFromTo minBound maxBound

499498

500− pColourType :: P.IdrisParser ColourType

499+ pColourType :: IP.IdrisParser ColourType

501500 pColourType = doColourType colourTypes

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

503502 (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

505504

506505idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507506

508−cmd_apropos :: String -> P.IdrisParser (Either String Command)

507+cmd_apropos :: String -> IP.IdrisParser (Either String Command)

509508cmd_apropos = packageBasedCmd (some idChar) Apropos

510509

511−packageBasedCmd :: P.IdrisParser a -> ([PkgName] -> a -> Command)

512− -> String -> P.IdrisParser (Either String Command)

510+packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)

511+ -> String -> IP.IdrisParser (Either String Command)

513512packageBasedCmd valParser cmd name =

514− try (do P.lchar '('

515− pkgs <- sepBy (pkg <* P.whiteSpace) (P.lchar ',')

516− P.lchar ')'

513+ try (do IP.lchar '('

514+ pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

515+ IP.lchar ')'

517516 val <- valParser

518517 return (Right (cmd pkgs val)))

519518 <|> do val <- valParser

520519 return (Right (cmd [] val))

521520 where

522− pkg = either fail pure . pkgName =<< P.packageName

521+ pkg = either fail pure . pkgName =<< IP.packageName

523522

524−cmd_search :: String -> P.IdrisParser (Either String Command)

523+cmd_search :: String -> IP.IdrisParser (Either String Command)

525524cmd_search = packageBasedCmd

526− (P.fullExpr (defaultSyntax { implicitAllowed = True })) Search

525+ (IP.fullExpr (defaultSyntax { implicitAllowed = True })) Search

527526

528−cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

527+cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)

529528cmd_proofsearch name = do

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

531− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

532− hints <- many (fst <$> P.fnName)

529+ upd <- option False (True <$ IP.lchar '!')

530+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

531+ hints <- many (fst <$> IP.fnName)

533532 return (Right (DoProofSearch upd True l n hints))

534533

535−cmd_refine :: String -> P.IdrisParser (Either String Command)

534+cmd_refine :: String -> IP.IdrisParser (Either String Command)

536535cmd_refine name = do

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

538− l <- fmap (fromInteger . fst) P.natural; n <- fst <$> P.name

539− hint <- fst <$> P.fnName

536+ upd <- option False (do IP.lchar '!'; return True)

537+ l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

538+ hint <- fst <$> IP.fnName

540539 return (Right (DoProofSearch upd False l n [hint]))