5e9d8de · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use Megaparsec for expressions, remove `parsers` dep

commit5e9d8dec9647b0aaf0861daeb36cea27f6e4a430 authorJason Felice <jason.m.felice@gmail.com> dateWed 1 Nov 2017, 21:37 (9 years ago) parent1764f7f

5 files changed+93−108

compare with master

unifiedsplit

idris.cabal−1 src/Idris/Parser/Expr.hs+2−3 src/Idris/Parser/Helpers.hs−14 src/Idris/Parser/Ops.hs+22−21 src/Idris/REPL/Parser.hs+69−69

idris.cabal−1

@@ -289,7 +289,6 @@ Library

289289 , mtl >= 2.1 && < 2.3

290290 , network < 2.7

291291 , optparse-applicative >= 0.13 && < 0.15

292− , parsers >= 0.9 && < 0.13

293292 , pretty < 1.2

294293 , process < 1.7

295294 , regex-tdfa >= 1.2

src/Idris/Parser/Expr.hs+2−3

@@ -25,10 +25,10 @@ import Control.Monad.State.Strict

2525import Data.Function (on)

2626import Data.List

2727import Data.Maybe

28−import Text.Parser.Expression

2928import Text.Megaparsec ((<?>))

3029import qualified Text.Megaparsec as P

3130import qualified Text.Megaparsec.Char as P

31+import qualified Text.Megaparsec.Expr as P

3232

3333-- | Allow implicit type declarations

3434allowImp :: SyntaxInfo -> SyntaxInfo

@@ -77,8 +77,7 @@ expr = pi

7777-}

7878opExpr :: SyntaxInfo -> IdrisParser PTerm

7979opExpr syn = do i <- get

80− buildExpressionParser (table (idris_infixes i))

81− (expr' syn)

80+ P.makeExprParser (expr' syn) (table (idris_infixes i))

8281

8382{- | Parses either an internally defined expression or

8483 a user-defined one

src/Idris/Parser/Helpers.hs−14

@@ -32,8 +32,6 @@ import Data.Maybe

3232import qualified Data.Text as T

3333import Data.Void (Void(..))

3434import System.FilePath

35−import qualified Text.Parser.Char

36−import qualified Text.Parser.Combinators

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

3836import Text.Megaparsec ((<?>))

3937import qualified Text.Megaparsec as P

@@ -59,18 +57,6 @@ type MonadicParsing m = (P.MonadParsec Void String m)

5957someSpace' :: MonadicParsing m => m ()

6058someSpace' = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

6159

62−instance Text.Parser.Combinators.Parsing IdrisInnerParser where

63− eof = P.eof

64− unexpected msg = P.unexpected . P.Label . NonEmpty.fromList $ msg

65− try = P.try

66− (<?>) = (P.<?>)

67− notFollowedBy = P.notFollowedBy

68−

69−instance Text.Parser.Char.CharParsing IdrisInnerParser where

70− satisfy = P.satisfy

71− char = P.char

72− string = P.string

73−

7460tokenFC :: MonadicParsing m => m a -> m (a, FC)

7561tokenFC p = do (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

7662 -- See Issue #1594

src/Idris/Parser/Ops.hs+22−21

@@ -22,39 +22,39 @@ import Control.Monad.State.Strict

2222import Data.Char (isAlpha)

2323import Data.List

2424import Data.List.NonEmpty (fromList)

25−import Text.Parser.Expression

2625import Text.Megaparsec ((<?>))

2726import qualified Text.Megaparsec as P

27+import qualified Text.Megaparsec.Expr as P

2828

2929-- | Creates table for fixity declarations to build expression parser

3030-- using pre-build and user-defined operator/fixity declarations

31−table :: [FixDecl] -> OperatorTable IdrisParser PTerm

31+table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]

3232table fixes

3333 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

3434 toTable (reverse fixes) ++

3535 [[noFixityBacktickOperator],

36− [binary "$" AssocRight $ \fc _ x y -> flatten $ PApp fc x [pexp y]],

37− [binary "=" AssocLeft $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],

36+ [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]],

37+ [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],

3838 [noFixityOperator]]

3939 where

4040 flatten :: PTerm -> PTerm -- flatten application

4141 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

4242 flatten t = t

4343

44− noFixityBacktickOperator :: Operator IdrisParser PTerm

45− noFixityBacktickOperator = flip Infix AssocNone $ do

44+ noFixityBacktickOperator :: P.Operator IdrisParser PTerm

45+ noFixityBacktickOperator = P.InfixN $ do

4646 (n, fc) <- backtickOperator

4747 return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y]

4848

4949 -- | Operator without fixity (throws an error)

50− noFixityOperator :: Operator IdrisParser PTerm

51− noFixityOperator = flip Infix AssocNone $ do

50+ noFixityOperator :: P.Operator IdrisParser PTerm

51+ noFixityOperator = P.InfixN $ do

5252 indentGt

5353 op <- P.try symbolicOperator

5454 P.unexpected . P.Label . fromList $ "Operator without known fixity: " ++ op

5555

5656 -- | Calculates table for fixity declarations

57− toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

57+ toTable :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]

5858 toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

5959

6060 toBin (Fix (PrefixN _) op) = prefix op $ \fc x ->

@@ -62,31 +62,32 @@ table fixes

6262 toBin (Fix f op) = binary op (assoc f) $ \fc n x y ->

6363 PApp fc (PRef fc [] n) [pexp x,pexp y]

6464

65− assoc (Infixl _) = AssocLeft

66− assoc (Infixr _) = AssocRight

67− assoc (InfixN _) = AssocNone

65+ assoc (Infixl _) = P.InfixL

66+ assoc (Infixr _) = P.InfixR

67+ assoc (InfixN _) = P.InfixN

6868

6969 isBacktick :: String -> Bool

7070 isBacktick (c : _) = c == '_' || isAlpha c

7171 isBacktick _ = False

7272

73− binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm

74− binary name assoc f

75− | isBacktick name = flip Infix assoc $ P.try $ do

73+ binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm

74+ binary name ctor f

75+ | isBacktick name = ctor $ P.try $ do

7676 (n, fc) <- backtickOperator

7777 guard $ show (nsroot n) == name

7878 return $ f fc n

79− | otherwise = flip Infix assoc $ do

79+ | otherwise = ctor $ do

8080 indentGt

8181 fc <- reservedOpFC name

8282 indentGt

8383 return $ f fc (sUN name)

8484

85− prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm

86− prefix name f = Prefix (do reservedOp name

87− fc <- getFC

88− indentGt

89− return (f fc))

85+ prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm

86+ prefix name f = P.Prefix $ do

87+ reservedOp name

88+ fc <- getFC

89+ indentGt

90+ return (f fc)

9091

9192{- | Parses a function used as an operator -- enclosed in backticks

9293

src/Idris/REPL/Parser.hs+69−69

@@ -32,8 +32,8 @@ import Data.List

3232import Data.List.Split (splitOn)

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

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

35−import Text.Parser.Char (anyChar, oneOf)

36−import Text.Parser.Combinators

35+import qualified Text.Megaparsec as P

36+import qualified Text.Megaparsec.Char as P

3737

3838parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

3939parseCmd i inputname = IP.runparser pCmd i inputname . trim

@@ -68,7 +68,7 @@ parserCommandsForHelp =

6868 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

6969 , (["doc"], NameArg, "Show internal documentation", cmd_doc)

7070 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

71− , genArg "namespace" (many anyChar) MakeDoc)

71+ , genArg "namespace" (P.many P.anyChar) MakeDoc)

7272 , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

7373 , cmd_apropos)

7474 , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

@@ -170,7 +170,7 @@ parserCommands =

170170 , "(Debugging) Try to unify two expressions", const $ do

171171 l <- IP.simpleExpr defaultSyntax

172172 r <- IP.simpleExpr defaultSyntax

173− eof

173+ P.eof

174174 return (Right (DebugUnify l r))

175175 )

176176 ]

@@ -189,25 +189,25 @@ proofArgCmd names command doc =

189189 (names, NoArg, doc, proofArg command)

190190

191191pCmd :: IP.IdrisParser (Either String Command)

192−pCmd = choice [ do c <- cmd names; parser c

193− | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

192+pCmd = P.choice [ do c <- cmd names; parser c

193+ | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

194194 <|> unrecognized

195195 <|> nop

196196 <|> eval

197− where nop = do eof; return (Right NOP)

197+ where nop = do P.eof; return (Right NOP)

198198 unrecognized = do

199199 IP.lchar ':'

200− cmd <- many anyChar

200+ cmd <- P.many P.anyChar

201201 let cmd' = takeWhile (/=' ') cmd

202202 return (Left $ "Unrecognized command: " ++ cmd')

203203

204204cmd :: [String] -> IP.IdrisParser String

205−cmd xs = try $ do

205+cmd xs = P.try $ do

206206 IP.lchar ':'

207207 docmd sorted_xs

208208

209209 where docmd [] = fail "Could not parse command"

210− docmd (x:xs) = try (IP.reserved x >> return x) <|> docmd xs

210+ docmd (x:xs) = P.try (IP.reserved x >> return x) <|> docmd xs

211211

212212 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

213213

@@ -215,7 +215,7 @@ cmd xs = try $ do

215215noArgs :: Command -> String -> IP.IdrisParser (Either String Command)

216216noArgs cmd name = do

217217 let emptyArgs = do

218− eof

218+ P.eof

219219 return (Right cmd)

220220

221221 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

@@ -230,27 +230,27 @@ eval = do

230230exprArg :: (PTerm -> Command) -> String -> IP.IdrisParser (Either String Command)

231231exprArg cmd name = do

232232 let noArg = do

233− eof

233+ P.eof

234234 return $ Left ("Usage is :" ++ name ++ " <expression>")

235235

236236 let justOperator = do

237237 (op, fc) <- IP.symbolicOperatorFC

238− eof

238+ P.eof

239239 return $ Right $ cmd (PRef fc [] (sUN op))

240240

241241 let properArg = do

242242 t <- IP.fullExpr defaultSyntax

243243 return $ Right (cmd t)

244− try noArg <|> try justOperator <|> properArg

244+ P.try noArg <|> P.try justOperator <|> properArg

245245

246246genArg :: String -> IP.IdrisParser a -> (a -> Command)

247247 -> String -> IP.IdrisParser (Either String Command)

248248genArg argName argParser cmd name = do

249− let emptyArgs = do eof; failure

249+ let emptyArgs = do P.eof; failure

250250 oneArg = do arg <- argParser

251− eof

251+ P.eof

252252 return (Right (cmd arg))

253− try emptyArgs <|> oneArg <|> failure

253+ P.try emptyArgs <|> oneArg <|> failure

254254 where

255255 failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

256256

@@ -259,7 +259,7 @@ nameArg = genArg "name" $ fst <$> IP.name

259259fnNameArg = genArg "functionname" $ fst <$> IP.fnName

260260

261261strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

262−strArg = genArg "string" (many anyChar)

262+strArg = genArg "string" (P.many P.anyChar)

263263

264264moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

265265moduleArg = genArg "module" (fmap (toPath . fst) IP.identifier)

@@ -274,18 +274,18 @@ namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

274274optArg :: (Opt -> Command) -> String -> IP.IdrisParser (Either String Command)

275275optArg cmd name = do

276276 let emptyArgs = do

277− eof

277+ P.eof

278278 return $ Left ("Usage is :" ++ name ++ " <option>")

279279

280280 let oneArg = do

281281 o <- pOption

282282 IP.whiteSpace

283− eof

283+ P.eof

284284 return (Right (cmd o))

285285

286286 let failure = return $ Left "Unrecognized setting"

287287

288− try emptyArgs <|> oneArg <|> failure

288+ P.try emptyArgs <|> oneArg <|> failure

289289

290290 where

291291 pOption :: IP.IdrisParser Opt

@@ -293,7 +293,7 @@ optArg cmd name = do

293293

294294proofArg :: (Bool -> Int -> Name -> Command) -> String -> IP.IdrisParser (Either String Command)

295295proofArg cmd name = do

296− upd <- option False $ do

296+ upd <- P.option False $ do

297297 IP.lchar '!'

298298 return True

299299 l <- fst <$> IP.natural

@@ -304,17 +304,17 @@ cmd_doc :: String -> IP.IdrisParser (Either String Command)

304304cmd_doc name = do

305305 let constant = do

306306 c <- fmap fst IP.constant

307− eof

307+ P.eof

308308 return $ Right (DocStr (Right c) FullDocs)

309309

310310 let pType = do

311311 IP.reserved "Type"

312− eof

312+ P.eof

313313 return $ Right (DocStr (Left $ IP.mkName ("Type", "")) FullDocs)

314314

315315 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

316316

317− try constant <|> pType <|> fnName

317+ P.try constant <|> pType <|> fnName

318318

319319cmd_consolewidth :: String -> IP.IdrisParser (Either String Command)

320320cmd_consolewidth name = do

@@ -334,19 +334,19 @@ cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

334334

335335cmd_execute :: String -> IP.IdrisParser (Either String Command)

336336cmd_execute name = do

337− tm <- option maintm (IP.fullExpr defaultSyntax)

337+ tm <- P.option maintm (IP.fullExpr defaultSyntax)

338338 return (Right (Execute tm))

339339 where

340340 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

341341

342342cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

343343cmd_dynamic name = do

344− let optArg = do l <- many anyChar

344+ let optArg = do l <- P.many P.anyChar

345345 if (l /= "")

346346 then return $ Right (DynamicLink l)

347347 else return $ Right ListDynamic

348348 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349− try optArg <|> failure

349+ P.try optArg <|> failure

350350

351351cmd_pprint :: String -> IP.IdrisParser (Either String Command)

352352cmd_pprint name = do

@@ -376,43 +376,43 @@ cmd_compile name = do

376376 let hasOneArg = do

377377 i <- get

378378 f <- fst <$> IP.identifier

379− eof

379+ P.eof

380380 return $ Right (Compile defaultCodegen f)

381381

382382 let hasTwoArgs = do

383383 i <- get

384384 codegen <- codegenOption

385385 f <- fst <$> IP.identifier

386− eof

386+ P.eof

387387 return $ Right (Compile codegen f)

388388

389389 let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"

390− try hasTwoArgs <|> try hasOneArg <|> failure

390+ P.try hasTwoArgs <|> P.try hasOneArg <|> failure

391391

392392cmd_addproof :: String -> IP.IdrisParser (Either String Command)

393393cmd_addproof name = do

394− n <- option Nothing $ do

394+ n <- P.option Nothing $ do

395395 x <- fst <$> IP.name

396396 return (Just x)

397− eof

397+ P.eof

398398 return (Right (AddProof n))

399399

400400cmd_log :: String -> IP.IdrisParser (Either String Command)

401401cmd_log name = do

402402 i <- fmap (fromIntegral . fst) IP.natural

403− eof

403+ P.eof

404404 return (Right (LogLvl i))

405405

406406cmd_verb :: String -> IP.IdrisParser (Either String Command)

407407cmd_verb name = do

408408 i <- fmap (fromIntegral . fst) IP.natural

409− eof

409+ P.eof

410410 return (Right (Verbosity i))

411411

412412cmd_cats :: String -> IP.IdrisParser (Either String Command)

413413cmd_cats name = do

414− cs <- sepBy pLogCats (IP.whiteSpace)

415− eof

414+ cs <- P.sepBy pLogCats (IP.whiteSpace)

415+ P.eof

416416 return $ Right $ LogCategory (concat cs)

417417 where

418418 badCat = do

@@ -420,26 +420,26 @@ cmd_cats name = do

420420 fail $ "Category: " ++ c ++ " is not recognised."

421421

422422 pLogCats :: IP.IdrisParser [LogCat]

423− pLogCats = try (parserCats <$ IP.symbol (strLogCat IParse))

424− <|> try (elabCats <$ IP.symbol (strLogCat IElab))

425− <|> try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

426− <|> try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

427− <|> try ([IIBC] <$ IP.symbol (strLogCat IIBC))

428− <|> try ([IErasure] <$ IP.symbol (strLogCat IErasure))

423+ pLogCats = P.try (parserCats <$ IP.symbol (strLogCat IParse))

424+ <|> P.try (elabCats <$ IP.symbol (strLogCat IElab))

425+ <|> P.try (codegenCats <$ IP.symbol (strLogCat ICodeGen))

426+ <|> P.try ([ICoverage] <$ IP.symbol (strLogCat ICoverage))

427+ <|> P.try ([IIBC] <$ IP.symbol (strLogCat IIBC))

428+ <|> P.try ([IErasure] <$ IP.symbol (strLogCat IErasure))

429429 <|> badCat

430430

431431cmd_let :: String -> IP.IdrisParser (Either String Command)

432432cmd_let name = do

433− defn <- concat <$> many (IP.decl defaultSyntax)

433+ defn <- concat <$> P.many (IP.decl defaultSyntax)

434434 return (Right (NewDefn defn))

435435

436436cmd_unlet :: String -> IP.IdrisParser (Either String Command)

437−cmd_unlet name = (Right . Undefine) `fmap` many (fst <$> IP.name)

437+cmd_unlet name = (Right . Undefine) `fmap` P.many (fst <$> IP.name)

438438

439439cmd_loadto :: String -> IP.IdrisParser (Either String Command)

440440cmd_loadto name = do

441441 toline <- fmap (fromInteger . fst) IP.natural

442− f <- many anyChar;

442+ f <- P.many P.anyChar

443443 return (Right (Load f (Just toline)))

444444

445445cmd_colour :: String -> IP.IdrisParser (Either String Command)

@@ -461,27 +461,27 @@ cmd_colour name = fmap Right pSetColourCmd

461461 pSetColourCmd :: IP.IdrisParser Command

462462 pSetColourCmd = (do c <- pColourType

463463 let defaultColour = IdrisColour Nothing True False False False

464− opts <- sepBy pColourMod (IP.whiteSpace)

464+ opts <- P.sepBy pColourMod (IP.whiteSpace)

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

466466 return $ SetColour c colour)

467− <|> try (IP.symbol "on" >> return ColourOn)

468− <|> try (IP.symbol "off" >> return ColourOff)

467+ <|> P.try (IP.symbol "on" >> return ColourOn)

468+ <|> P.try (IP.symbol "off" >> return ColourOff)

469469

470470 pColour :: IP.IdrisParser (Maybe Color)

471471 pColour = doColour colours

472472 where doColour [] = fail "Unknown colour"

473− doColour ((s, c):cs) = (try (IP.symbol s) >> return c) <|> doColour cs

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

474474

475475 pColourMod :: IP.IdrisParser (IdrisColour -> IdrisColour)

476− pColourMod = try (doVivid <$ IP.symbol "vivid")

477− <|> try (doDull <$ IP.symbol "dull")

478− <|> try (doUnderline <$ IP.symbol "underline")

479− <|> try (doNoUnderline <$ IP.symbol "nounderline")

480− <|> try (doBold <$ IP.symbol "bold")

481− <|> try (doNoBold <$ IP.symbol "nobold")

482− <|> try (doItalic <$ IP.symbol "italic")

483− <|> try (doNoItalic <$ IP.symbol "noitalic")

484− <|> try (pColour >>= return . doSetColour)

476+ pColourMod = P.try (doVivid <$ IP.symbol "vivid")

477+ <|> P.try (doDull <$ IP.symbol "dull")

478+ <|> P.try (doUnderline <$ IP.symbol "underline")

479+ <|> P.try (doNoUnderline <$ IP.symbol "nounderline")

480+ <|> P.try (doBold <$ IP.symbol "bold")

481+ <|> P.try (doNoBold <$ IP.symbol "nobold")

482+ <|> P.try (doItalic <$ IP.symbol "italic")

483+ <|> P.try (doNoItalic <$ IP.symbol "noitalic")

484+ <|> P.try (pColour >>= return . doSetColour)

485485 where doVivid i = i { vivid = True }

486486 doDull i = i { vivid = False }

487487 doUnderline i = i { underline = True }

@@ -501,9 +501,9 @@ cmd_colour name = fmap Right pSetColourCmd

501501 pColourType = doColourType colourTypes

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

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

504− doColourType ((s,ct):cts) = (try (IP.symbol s) >> return ct) <|> doColourType cts

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

505505

506−idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

506+idChar = P.oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

507507

508508cmd_apropos :: String -> IP.IdrisParser (Either String Command)

509509cmd_apropos = packageBasedCmd (some idChar) Apropos

@@ -511,11 +511,11 @@ cmd_apropos = packageBasedCmd (some idChar) Apropos

511511packageBasedCmd :: IP.IdrisParser a -> ([PkgName] -> a -> Command)

512512 -> String -> IP.IdrisParser (Either String Command)

513513packageBasedCmd valParser cmd name =

514− try (do IP.lchar '('

515− pkgs <- sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

516− IP.lchar ')'

517− val <- valParser

518− return (Right (cmd pkgs val)))

514+ P.try (do IP.lchar '('

515+ pkgs <- P.sepBy (pkg <* IP.whiteSpace) (IP.lchar ',')

516+ IP.lchar ')'

517+ val <- valParser

518+ return (Right (cmd pkgs val)))

519519 <|> do val <- valParser

520520 return (Right (cmd [] val))

521521 where

@@ -527,14 +527,14 @@ cmd_search = packageBasedCmd

527527

528528cmd_proofsearch :: String -> IP.IdrisParser (Either String Command)

529529cmd_proofsearch name = do

530− upd <- option False (True <$ IP.lchar '!')

530+ upd <- P.option False (True <$ IP.lchar '!')

531531 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

532− hints <- many (fst <$> IP.fnName)

532+ hints <- P.many (fst <$> IP.fnName)

533533 return (Right (DoProofSearch upd True l n hints))

534534

535535cmd_refine :: String -> IP.IdrisParser (Either String Command)

536536cmd_refine name = do

537− upd <- option False (do IP.lchar '!'; return True)

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

538538 l <- fmap (fromInteger . fst) IP.natural; n <- fst <$> IP.name

539539 hint <- fst <$> IP.fnName

540540 return (Right (DoProofSearch upd False l n [hint]))