774d1b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4170 from eraserhd/megaparsec

774d1b6Niklas Larsson9 years ago

CHANGELOG.md+5

compare with master

unifiedsplit

@@ -45,6 +45,7 @@

45 * Generalised many combinators to use an unknown `commit` flag where possible.

47## Tool Updates

48+

48+ Private functions are no longer visible in the REPL except for modules

49+ Private functions are no longer visible in the REPL except for modules

49 that are explicitly loaded.

50 that are explicitly loaded.

50+ The --interface option now creates CommonJS modules on the node backend.

51+ The --interface option now creates CommonJS modules on the node backend.

@@ -52,8 +53,12 @@

52 as they were given in the source files.

53 as they were given in the source files.

53+ Backslash, braces and percent symbols are now correctly pretty printed

54+ Backslash, braces and percent symbols are now correctly pretty printed

54 in LaTeX.

55 in LaTeX.

56++ Parse errors have a new format, similar to GHC 8.2's default, due to a

57+ switch from Trifecta to Megaparsec for parsing. This could possibly cause

58+ some subtle deviations in parsing from previous versions of Idris.

56## Packaging Updates

60## Packaging Updates

61+

57+ Package names now only accept a restrictive charset of letters, numbers and the `-_` characters.

62+ Package names now only accept a restrictive charset of letters, numbers and the `-_` characters.

58 Package names are also case insensitive

63 Package names are also case insensitive

appveyor.yml+2−2

@@ -5,13 +5,13 @@ init:

6 mkdir C:\ghc

8− Invoke-WebRequest "http://downloads.haskell.org/~ghc/7.10.3/ghc-7.10.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

8+ Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.2.1/ghc-8.2.1-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

10 7z x C:\ghc\ghc.tar.xz -oC:\ghc

12 7z x C:\ghc\ghc.tar -oC:\ghc

14− $env:PATH="$env:PATH;c:\ghc\ghc-7.10.3\bin;$HOME\AppData\Roaming\cabal\bin"

14+ $env:PATH="$env:PATH;c:\ghc\ghc-8.2.1\bin;$HOME\AppData\Roaming\cabal\bin"

16 cabal update

idris.cabal+4−2

@@ -286,10 +286,10 @@ Library

286 , fingertree >= 0.1 && < 0.2

287 , haskeline >= 0.7 && < 0.8

288 , ieee754 >= 0.7 && < 0.9

289+ , megaparsec >= 6.2 && <6.3

289 , mtl >= 2.1 && < 2.3

290 , mtl >= 2.1 && < 2.3

290 , network < 2.7

291 , network < 2.7

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

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

292− , parsers >= 0.9 && < 0.13

293 , pretty < 1.2

294 , process < 1.7

295 , regex-tdfa >= 1.2

@@ -300,7 +300,6 @@ Library

300 , time >= 1.4 && < 1.9

301 , transformers < 0.6

302 , transformers-compat >= 0.3

303− , trifecta >= 1.6 && < 1.8

304 , uniplate >=1.6 && < 1.7

303 , uniplate >=1.6 && < 1.7

305 , unordered-containers < 0.3

304 , unordered-containers < 0.3

306 , utf8-string < 1.1

305 , utf8-string < 1.1

@@ -310,6 +309,9 @@ Library

310 , fsnotify >= 0.2 && < 2.2

309 , fsnotify >= 0.2 && < 2.2

311 , async < 2.2

310 , async < 2.2

312

311

312+ if !impl(ghc >= 8.0)

313+ Build-Depends: semigroups == 0.18.*

314+

313 Default-Language: Haskell2010

315 Default-Language: Haskell2010

314 ghc-prof-options: -auto-all -caf-all

316 ghc-prof-options: -auto-all -caf-all

315

317

src/Idris/AbsSyntaxTree.hs+1−2

@@ -269,7 +269,6 @@ data IState = IState {

269 , lastParse :: Maybe Name

270 , indent_stack :: [Int]

271 , brace_stack :: [Maybe Int]

272− , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?

273 , idris_parsedSpan :: Maybe FC

272 , idris_parsedSpan :: Maybe FC

274 , hide_list :: Ctxt Accessibility

273 , hide_list :: Ctxt Accessibility

275 , default_access :: Accessibility

274 , default_access :: Accessibility

@@ -407,7 +406,7 @@ idrisInit = IState initContext S.empty []

407 emptyContext emptyContext emptyContext emptyContext

406 emptyContext emptyContext emptyContext emptyContext

408 emptyContext

407 emptyContext

409 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

408 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

410− [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

409+ [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

411 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

410 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

412 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

411 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

413 emptyContext S.empty M.empty emptyContext initialInteractiveOpts

412 emptyContext S.empty M.empty emptyContext initialInteractiveOpts

src/Idris/IdeMode.hs+12−11

@@ -15,6 +15,7 @@ import Idris.Core.Binary ()

15import Idris.Core.TT

17import Control.Applicative hiding (Const)

18+import Control.Arrow (left)

18import qualified Data.Binary as Binary

19import qualified Data.Binary as Binary

19import qualified Data.ByteString.Base64 as Base64

20import qualified Data.ByteString.Base64 as Base64

20import qualified Data.ByteString.Lazy as Lazy

21import qualified Data.ByteString.Lazy as Lazy

@@ -24,9 +25,9 @@ import Data.Maybe (isJust)

24import qualified Data.Text as T

25import qualified Data.Text as T

25import Numeric

26import Numeric

26import System.IO

27import System.IO

28+import qualified Text.Megaparsec as P

29+import qualified Text.Megaparsec.Char as P

27import Text.Printf

30import Text.Printf

28−import qualified Text.Trifecta as P

29−import qualified Text.Trifecta.Delta as P

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

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

32getNChar _ 0 s = return (reverse s)

33getNChar _ 0 s = return (reverse s)

@@ -205,28 +206,31 @@ escape = concatMap escapeChar

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

206 escapeChar '"' = "\\\""

206 escapeChar c = [c]

207 escapeChar c = [c]

207

208

209+type Parser a = P.Parsec () String a

210+

211+sexp :: Parser SExp

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

212+sexp = SexpList <$> P.between (P.char '(') (P.char ')') (sexp `P.sepBy` (P.char ' '))

209 <|> atom

213 <|> atom

210

214

215+atom :: Parser SExp

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

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

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

217 <|> P.char ':' *> atomC

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

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

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

219+ <|> do ints <- some P.digitChar

215 case readDec ints of

220 case readDec ints of

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

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

217 _ -> return (StringAtom ints)

222 _ -> return (StringAtom ints)

218

223

224+atomC :: Parser SExp

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

225atomC = BoolAtom True <$ P.string "True"

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

226 <|> BoolAtom False <$ P.string "False"

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

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

222

228

229+quotedChar :: Parser Char

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

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

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

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

225 <|> P.noneOf "\""

232 <|> P.noneOf "\""

226

233

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

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

229−

230data Opt = ShowImpl | ErrContext deriving Show

234data Opt = ShowImpl | ErrContext deriving Show

231

235

232data WhatDocs = Overview | Full

236data WhatDocs = Overview | Full

@@ -321,10 +325,7 @@ parseMessage x = case receiveString x of

321 Left err -> Left err

325 Left err -> Left err

322

326

323receiveString :: String -> Either Err SExp

327receiveString :: String -> Either Err SExp

324−receiveString x =

328+receiveString = left (const $ Msg "parse failure") . P.parse sexp "(unknown)"

325− case parseSExp x of

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

327− P.Success r -> Right r

328

329

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

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

330convSExp pre s id =

331convSExp pre s id =

src/Idris/Package/Parser.hs+16−32

@@ -5,15 +5,16 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}

8+{-# LANGUAGE FlexibleContexts #-}

9module Idris.Package.Parser where

11import Idris.CmdOptions

12import Idris.Imports

13import Idris.Package.Common

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

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

15− lchar, packageName, parseErrorDoc, reserved,

15+ identifier, isEol, lchar, packageName,

16− runparser, someSpace')

16+ parseErrorDoc, reserved, runparser, someSpace,

17+ stringLiteral)

18import Control.Applicative

19import Control.Applicative

19import Control.Monad.State.Strict

20import Control.Monad.State.Strict

@@ -21,29 +22,12 @@ import Data.List (union)

21import System.Directory (doesFileExist)

22import System.Directory (doesFileExist)

22import System.Exit

23import System.Exit

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

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

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

26+import qualified Text.Megaparsec as P

27+import qualified Text.Megaparsec.Char as P

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

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

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

26−import qualified Text.Trifecta as P

27−

28−type PParser = StateT PkgDesc P.Parser

29−

30−#if MIN_VERSION_base(4,9,0)

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

32− line = lift P.line

33− {-# INLINE line #-}

34− position = lift P.position

35− {-# INLINE position #-}

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

37− {-# INLINE slicedWith #-}

38− rend = lift P.rend

39− {-# INLINE rend #-}

40− restOfLine = lift P.restOfLine

41− {-# INLINE restOfLine #-}

42−#endif

43−

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

45− someSpace = someSpace'

30+type PParser = StateT PkgDesc IdrisInnerParser

48parseDesc :: FilePath -> IO PkgDesc

32parseDesc :: FilePath -> IO PkgDesc

49parseDesc fp = do

33parseDesc fp = do

@@ -65,7 +49,7 @@ pPkg :: PParser PkgDesc

65pPkg = do

49pPkg = do

66 reserved "package"

50 reserved "package"

67 p <- pPkgName

51 p <- pPkgName

68− someSpace'

52+ someSpace

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

53 modify $ \st -> st { pkgname = p }

70 some pClause

54 some pClause

71 st <- get

55 st <- get

@@ -84,7 +68,7 @@ filename = (do

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

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

85 -- it will also accept hyphens

69 -- it will also accept hyphens

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

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

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

71+ filename <- fst <$> stringLiteral

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

72 -- Through at least version 0.9.19.1, IPKG executable values were

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

73 -- possibly namespaced identifiers, like foo.bar.baz.

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

74 <|> show . fst <$> iName []

@@ -116,10 +100,10 @@ filename = (do

116 "filename must contain no directory component"

100 "filename must contain no directory component"

117

101

118textUntilEol :: MonadicParsing m => m String

102textUntilEol :: MonadicParsing m => m String

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

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

120

104

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

105clause :: String -> PParser a -> (PkgDesc -> a -> PkgDesc) -> PParser ()

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

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

123 modify $ \st -> f st value

107 modify $ \st -> f st value

124

108

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

109commaSep :: MonadicParsing m => m a -> m [a]

@@ -129,8 +113,8 @@ pClause :: PParser ()

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

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

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

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

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

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

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

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

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

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

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

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

119 in st { pkgdeps = ps `union` pkgdeps st

136 , idris_opts = pkgs ++ idris_opts st })

120 , idris_opts = pkgs ++ idris_opts st })

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

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

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

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

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

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

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

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

132+ <|> clause "brief" (fst <$> stringLiteral) (\st v -> st { pkgbrief = Just v })

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

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

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

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

src/Idris/Parser.hs+18−19

@@ -44,12 +44,12 @@ import Prelude hiding (pi)

44import Control.Applicative hiding (Const)

45import Control.Monad

46import Control.Monad.State.Strict

47−import qualified Data.ByteString.UTF8 as UTF8

48import Data.Char

47import Data.Char

49import Data.Foldable (asum)

48import Data.Foldable (asum)

50import Data.Function

49import Data.Function

51import Data.Generics.Uniplate.Data (descendM)

50import Data.Generics.Uniplate.Data (descendM)

52import Data.List

51import Data.List

52+import qualified Data.List.NonEmpty as NonEmpty

53import qualified Data.List.Split as Spl

54import qualified Data.Map as M

55import Data.Maybe

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

57import qualified Data.Text as T

58import qualified System.Directory as Dir (makeAbsolute)

59import System.FilePath

60+import Text.Megaparsec ((<?>))

61+import qualified Text.Megaparsec as P

62+import qualified Text.Megaparsec.Char as P

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

63import 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

65{-

66@

@@ -433,20 +433,20 @@ syntaxRule syn

433 reservedHL "syntax"

434 return sty)

435 syms <- some syntaxSym

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

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

437 let ns = mapMaybe getName syms

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

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

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

440 lchar '='

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

442 terminator

443 return (Rule (mkSimple syms) tm sty)

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

445 syms <- some syntaxSym

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

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

447 let ns = mapMaybe getName syms

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

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

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

450 lchar '='

451 openBlock

452 dec <- some (decl syn)

@@ -577,7 +577,7 @@ fnDecl syn = P.try (do notEndBlock

577@

578-}

579fnDecl' :: SyntaxInfo -> IdrisParser PDecl

580−fnDecl' syn = checkDeclFixity $

580+fnDecl' syn = (checkDeclFixity $

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

582 pushIndent

583 (doc, argDocs) <- docstring syn

@@ -595,7 +595,7 @@ fnDecl' syn = checkDeclFixity $

595 return (PTy doc argDocs syn fc opts' n nfc ty)

596 <|> postulate syn

597 <|> caf syn

598− <|> pattern syn

598+ <|> pattern syn)

599 <?> "function declaration"

600

601{-| Parses a series of function and accessbility options

@@ -1513,25 +1513,25 @@ parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> ela

1513 spaced parser = indentGt *> parser

1514

1515-- | Parse module header and imports

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

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

1517parseImports fname input

1518 = do i <- getIState

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

1519+ case runparser imports i fname input of

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

1520+ Left err -> ifail . show . parseErrorDoc $ err

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

1521+ Right (x, annots, i) ->

1522 do putIState i

1523 fname' <- runIO $ Dir.makeAbsolute fname

1524 sendHighlighting $ addPath annots fname'

1525 return x

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

1527 [ImportInfo],

1528− Maybe P.Delta),

1528+ Maybe ParseState),

1529 [(FC, OutputAnnotation)], IState)

1530 imports = do optional shebang

1531 whiteSpace

1532 (mdoc, mname, annots) <- moduleHeader

1533 ps_exp <- many import_

1534− mrk <- P.mark

1534+ mrk <- P.getParserState

1535 isEof <- lookAheadMatches P.eof

1536 let mrk' = if isEof

1537 then Nothing

@@ -1573,8 +1573,7 @@ fixColour True doc = doc

1573

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

1575-- documentation strings.

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

1576+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe ParseState -> Idris [PDecl]

1577− Idris [PDecl]

1578parseProg syn fname input mrk

1577parseProg syn fname input mrk

1579 = do i <- getIState

1578 = do i <- getIState

1580 case runparser mainProg i fname input of

1579 case runparser mainProg i fname input of

@@ -1596,7 +1595,7 @@ parseProg syn fname input mrk

1596 mainProg = case mrk of

1595 mainProg = case mrk of

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

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

1598 Just mrk -> do

1597 Just mrk -> do

1599− P.release mrk

1598+ P.setParserState mrk

1600 ds <- prog syn

1599 ds <- prog syn

1601 i' <- get

1600 i' <- get

1602 return (ds, i')

1601 return (ds, i')

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

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

22import Control.Monad.State.Strict

23import Data.List

24import Data.Maybe

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

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

26−import qualified Text.Trifecta as P

26+import qualified Text.Megaparsec as P

28{- | Parses a record type declaration

29Record ::=

@@ -169,7 +169,7 @@ SimpleConstructorList ::=

169 ;

170-}

171data_ :: SyntaxInfo -> IdrisParser PDecl

172−data_ syn = checkDeclFixity $

172+data_ syn = (checkDeclFixity $

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

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

175 pushIndent

@@ -219,7 +219,7 @@ data_ syn = checkDeclFixity $

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

220 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))

221 terminator

222− return d)

222+ return d))

223 <?> "data type declaration"

224 where

225 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

src/Idris/Parser/Expr.hs+15−16

@@ -5,8 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,

9− TupleSections #-}

8+{-# LANGUAGE FlexibleContexts, TupleSections #-}

10module Idris.Parser.Expr where

9module Idris.Parser.Expr where

12import Idris.AbsSyntax

11import Idris.AbsSyntax

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

25import Data.Function (on)

24import Data.Function (on)

26import Data.List

25import Data.List

27import Data.Maybe

26import Data.Maybe

28−import Text.Parser.Expression

27+import Text.Megaparsec ((<?>))

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

30−import qualified Text.Trifecta as P

28+import qualified Text.Megaparsec as P

29+import qualified Text.Megaparsec.Char as P

30+import qualified Text.Megaparsec.Expr as P

32-- | Allow implicit type declarations

33allowImp :: SyntaxInfo -> SyntaxInfo

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

76-}

77opExpr :: SyntaxInfo -> IdrisParser PTerm

78opExpr syn = do i <- get

79− buildExpressionParser (table (idris_infixes i))

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

80− (expr' syn)

82{- | Parses either an internally defined expression or

81{- | Parses either an internally defined expression or

83 a user-defined one

82 a user-defined one

@@ -1283,9 +1282,9 @@ ExprList ::=

1283listExpr :: SyntaxInfo -> IdrisParser PTerm

1282listExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

1285 lchar '['; fc <- getFC;

1284 lchar '['; fc <- getFC;

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1466,12 +1465,12 @@ VerbatimString_t ::=

1466;

1465;

1467@

1466@

1468 -}

1467 -}

1469−verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1468+verbatimStringLiteral :: IdrisParser (String, FC)

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

1469+verbatimStringLiteral = token $ do (FC f start _) <- getFC

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

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

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

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

1473− (FC _ _ end) <- getFC

1472+ (FC _ _ end) <- getFC

1474− return (str, FC f start end)

1473+ return (str, FC f start end)

1475

1474

1476{- | Parses a static modifier

1475{- | Parses a static modifier

1477

1476

src/Idris/Parser/Helpers.hs+95−140

@@ -5,9 +5,7 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances,

8+{-# LANGUAGE ConstraintKinds, FlexibleContexts #-}

9− GeneralizedNewtypeDeriving, PatternGuards, StandaloneDeriving,

10− TypeSynonymInstances #-}

11module Idris.Parser.Helpers where

9module Idris.Parser.Helpers where

13import Idris.AbsSyntax

11import Idris.AbsSyntax

@@ -23,71 +21,58 @@ import Prelude hiding (pi)

23import Control.Applicative

21import Control.Applicative

24import Control.Monad

22import Control.Monad

25import Control.Monad.State.Strict

23import Control.Monad.State.Strict

26−import qualified Data.ByteString.UTF8 as UTF8

27import Data.Char

24import Data.Char

28import qualified Data.HashSet as HS

25import qualified Data.HashSet as HS

29import Data.List

26import Data.List

27+import qualified Data.List.NonEmpty as NonEmpty

30import qualified Data.Map as M

28import qualified Data.Map as M

31import Data.Maybe

29import Data.Maybe

32import qualified Data.Text as T

30import qualified Data.Text as T

31+import Data.Void (Void(..))

33import System.FilePath

32import System.FilePath

33+import Text.Megaparsec ((<?>))

34−import qualified Text.Parser.Char as Chr

34+import qualified Text.Megaparsec as P

35−import Text.Parser.LookAhead

35+import qualified Text.Megaparsec.Char as P

36−import qualified Text.Parser.Token as Tok

36+import qualified Text.Megaparsec.Char.Lexer as P hiding (space)

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

38−import Text.Trifecta ((<?>))

38+

39−import qualified Text.Trifecta as P

40−import qualified Text.Trifecta.Delta as P

42-- | Idris parser with state used during parsing

40-- | Idris parser with state used during parsing

43−type IdrisParser = StateT IState P.Parser

41+type IdrisParser = StateT IState IdrisInnerParser

44−

42+type IdrisInnerParser = P.Parsec Void String

45−#if MIN_VERSION_base(4,9,0)

43+type ParseState = P.State String

46−instance {-# OVERLAPPING #-} P.DeltaParsing IdrisParser where

44+data ParseError = ParseError String (P.ParseError (P.Token String) Void)

47− line = lift P.line

45+

48− {-# INLINE line #-}

46+parseErrorPretty :: ParseError -> String

49− position = lift P.position

47+parseErrorPretty (ParseError s err) = P.parseErrorPretty' s err

50− {-# INLINE position #-}

48+

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

49+parseErrorDoc :: ParseError -> PP.Doc

52− {-# INLINE slicedWith #-}

50+parseErrorDoc = PP.string . parseErrorPretty

53− rend = lift P.rend

54− {-# INLINE rend #-}

55− restOfLine = lift P.restOfLine

56− {-# INLINE restOfLine #-}

57−#endif

58−

59−someSpace' :: MonadicParsing m => m ()

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

61−

62−instance {-# OVERLAPPING #-} P.TokenParsing IdrisParser where

63− someSpace = someSpace'

64− token p = do s <- get

65− (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

66− -- See Issue #1594

67− r <- p

68− (FC fn _ (el, ec)) <- getFC

69− whiteSpace

70− put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

71− return r

73-- | Generalized monadic parsing constraint type

52-- | Generalized monadic parsing constraint type

74−type MonadicParsing m = (P.DeltaParsing m, LookAheadParsing m, Monad m)

53+type MonadicParsing m = (P.MonadParsec Void String m)

76−class HasLastTokenSpan m where

55+someSpace :: MonadicParsing m => m ()

77− getLastTokenSpan :: m (Maybe FC)

56+someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

79−instance HasLastTokenSpan IdrisParser where

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

80− getLastTokenSpan = lastTokenSpan <$> get

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

60+ -- See Issue #1594

61+ r <- p

62+ (FC fn _ (el, ec)) <- getFC

63+ whiteSpace

64+ return (r, FC fn (sl, sc) (el, ec))

82−newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }

66+token :: MonadicParsing m => m a -> m a

67+token p = p <* whiteSpace

84-- | Helper to run Idris inner parser based stateT parsers

69-- | Helper to run Idris inner parser based stateT parsers

85−runparser :: StateT st P.Parser res -> st -> String -> String -> Either ParseError res

70+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res

86runparser p i inputname s =

71runparser p i inputname s =

87− case P.parseString (evalStateT p i)

72+ case P.parse (evalStateT p i) inputname s of

88− (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of

89− P.Failure (P.ErrInfo doc _) -> Left (ParseError doc)

73+ Left err -> Left $ ParseError s err

90− P.Success value -> Right value

74+ Right v -> Right v

75+

92highlightP :: FC -> OutputAnnotation -> IdrisParser ()

77highlightP :: FC -> OutputAnnotation -> IdrisParser ()

93highlightP fc annot = do ist <- get

78highlightP fc annot = do ist <- get

@@ -136,7 +121,7 @@ isEol _ = False

136

121

137-- | A parser that succeeds at the end of the line

122-- | A parser that succeeds at the end of the line

138eol :: MonadicParsing m => m ()

123eol :: MonadicParsing m => m ()

139−eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

124+eol = () <$ P.satisfy isEol <|> P.lookAhead P.eof <?> "end of line"

140

125

141{- | Consumes a single-line comment

126{- | Consumes a single-line comment

142

127

@@ -145,10 +130,7 @@ eol = () <$ P.satisfy isEol <|> lookAhead P.eof <?> "end of line"

145@

130@

146 -}

131 -}

147singleLineComment :: MonadicParsing m => m ()

132singleLineComment :: MonadicParsing m => m ()

148−singleLineComment = (string "--" *>

133+singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)) *> eol)

149− many (P.satisfy (not . isEol)) *>

150− eol *> pure ())

151− <?> ""

152

134

153{- | Consumes a multi-line comment

135{- | Consumes a multi-line comment

154

136

@@ -168,9 +150,8 @@ singleLineComment = (string "--" *>

168@

150@

169-}

151-}

170multiLineComment :: MonadicParsing m => m ()

152multiLineComment :: MonadicParsing m => m ()

171−multiLineComment = P.try (string "{-" *> (string "-}") *> pure ())

153+multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())

172− <|> string "{-" *> inCommentChars

154+ <|> string "{-" *> inCommentChars

173− <?> ""

174 where inCommentChars :: MonadicParsing m => m ()

155 where inCommentChars :: MonadicParsing m => m ()

175 inCommentChars = string "-}" *> pure ()

156 inCommentChars = string "-}" *> pure ()

176 <|> P.try (multiLineComment) *> inCommentChars

157 <|> P.try (multiLineComment) *> inCommentChars

@@ -199,56 +180,47 @@ docComment = do dc <- pushIndent *> docCommentLine

199 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

180 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

200

181

201 where docCommentLine :: MonadicParsing m => m String

182 where docCommentLine :: MonadicParsing m => m String

202− docCommentLine = P.try (do string "|||"

183+ docCommentLine = P.hidden $ P.try $ do

184+ string "|||"

203− many (P.satisfy (==' '))

185+ many (P.satisfy (==' '))

204− contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

186+ contents <- P.option "" (do first <- P.satisfy (\c -> not (isEol c || c == '@'))

205− res <- many (P.satisfy (not . isEol))

187+ res <- many (P.satisfy (not . isEol))

206− return $ first:res)

188+ return $ first:res)

207− eol ; someSpace'

189+ eol ; someSpace

208− return contents)

190+ return contents

209− <?> ""

191+

210−

192+ argDocCommentLine :: IdrisParser (Name, String)

211− argDocCommentLine = do string "|||"

193+ argDocCommentLine = do P.string "|||"

212− many (P.satisfy isSpace)

194+ P.many (P.satisfy isSpace)

213− char '@'

195+ P.char '@'

214− many (P.satisfy isSpace)

196+ P.many (P.satisfy isSpace)

215 n <- fst <$> name

197 n <- fst <$> name

216− many (P.satisfy isSpace)

198+ P.many (P.satisfy isSpace)

217− docs <- many (P.satisfy (not . isEol))

199+ docs <- P.many (P.satisfy (not . isEol))

218− eol ; someSpace'

200+ P.eol ; someSpace

219 return (n, docs)

201 return (n, docs)

220

202

221-- | Parses some white space

203-- | Parses some white space

222whiteSpace :: MonadicParsing m => m ()

204whiteSpace :: MonadicParsing m => m ()

223−whiteSpace = Tok.whiteSpace

205+whiteSpace = someSpace <|> pure ()

224

206

225-- | Parses a string literal

207-- | Parses a string literal

226−stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)

208+stringLiteral :: MonadicParsing m => m (String, FC)

227−stringLiteral = do str <- Tok.stringLiteral

209+stringLiteral = tokenFC . P.try $ P.char '"' *> P.manyTill P.charLiteral (P.char '"')

228− fc <- getLastTokenSpan

229− return (str, fromMaybe NoFC fc)

230

210

231-- | Parses a char literal

211-- | Parses a char literal

232−charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)

212+charLiteral :: IdrisParser (Char, FC)

233−charLiteral = do ch <- Tok.charLiteral

213+charLiteral = tokenFC . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''

234− fc <- getLastTokenSpan

235− return (ch, fromMaybe NoFC fc)

236

214

237-- | Parses a natural number

215-- | Parses a natural number

238−natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)

216+natural :: IdrisParser (Integer, FC)

239−natural = do n <- Tok.natural

217+natural = tokenFC ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)

240− fc <- getLastTokenSpan

218+ <|> P.try (P.char '0' *> P.char' 'o' *> P.octal)

241− return (n, fromMaybe NoFC fc)

219+ <|> P.try P.decimal)

242−

243−-- | Parses an integral number

244−integer :: MonadicParsing m => m Integer

245−integer = Tok.integer

246

220

247-- | Parses a floating point number

221-- | Parses a floating point number

248−float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)

222+float :: IdrisParser (Double, FC)

249−float = do f <- Tok.double

223+float = tokenFC . P.try $ P.float

250− fc <- getLastTokenSpan

251− return (f, fromMaybe NoFC fc)

252

224

253{- * Symbols, identifiers, names and operators -}

225{- * Symbols, identifiers, names and operators -}

254

226

@@ -264,30 +236,29 @@ reservedIdentifiers = HS.fromList

264 ]

236 ]

265

237

266identifierOrReserved :: MonadicParsing m => m String

238identifierOrReserved :: MonadicParsing m => m String

267−identifierOrReserved = P.token $ P.try $ do

239+identifierOrReserved = token $ P.try $ do

268 c <- P.satisfy isAlpha <|> P.oneOf "_"

240 c <- P.satisfy isAlpha <|> P.oneOf "_"

269 cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")

241 cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")

270 return $ c : cs

242 return $ c : cs

271

243

272char :: MonadicParsing m => Char -> m Char

244char :: MonadicParsing m => Char -> m Char

273−char = Chr.char

245+char = P.char

274

246

275string :: MonadicParsing m => String -> m String

247string :: MonadicParsing m => String -> m String

276−string = Chr.string

248+string = P.string

277

249

278-- | Parses a character as a token

250-- | Parses a character as a token

279lchar :: MonadicParsing m => Char -> m Char

251lchar :: MonadicParsing m => Char -> m Char

280−lchar = P.token . P.char

252+lchar = token . P.char

281

253

282-- | Parses a character as a token, returning the source span of the character

254-- | Parses a character as a token, returning the source span of the character

283lcharFC :: MonadicParsing m => Char -> m FC

255lcharFC :: MonadicParsing m => Char -> m FC

284lcharFC ch = do (FC file (l, c) _) <- getFC

256lcharFC ch = do (FC file (l, c) _) <- getFC

285− _ <- P.token (char ch)

257+ _ <- token (P.char ch)

286 return $ FC file (l, c) (l, c+1)

258 return $ FC file (l, c) (l, c+1)

287

259

288−-- | Parses string as a token

289symbol :: MonadicParsing m => String -> m ()

260symbol :: MonadicParsing m => String -> m ()

290−symbol = void . Tok.symbol

261+symbol = void . P.symbol someSpace

291

262

292symbolFC :: MonadicParsing m => String -> m FC

263symbolFC :: MonadicParsing m => String -> m FC

293symbolFC str = do (FC file (l, c) _) <- getFC

264symbolFC str = do (FC file (l, c) _) <- getFC

@@ -296,7 +267,7 @@ symbolFC str = do (FC file (l, c) _) <- getFC

296

267

297-- | Parses a reserved identifier

268-- | Parses a reserved identifier

298reserved :: MonadicParsing m => String -> m ()

269reserved :: MonadicParsing m => String -> m ()

299−reserved name = P.token $ P.try $ do

270+reserved name = token $ P.try $ do

300 P.string name

271 P.string name

301 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

272 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

302

273

@@ -314,7 +285,7 @@ reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

314-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

285-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

315-- | Parses a reserved operator

286-- | Parses a reserved operator

316reservedOp :: MonadicParsing m => String -> m ()

287reservedOp :: MonadicParsing m => String -> m ()

317−reservedOp name = P.token $ P.try $

288+reservedOp name = token $ P.try $

318 do string name

289 do string name

319 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)

290 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)

320

291

@@ -328,8 +299,8 @@ identifier :: (MonadicParsing m) => m (String, FC)

328identifier = P.try $ do

299identifier = P.try $ do

329 (FC f (l, c) _) <- getFC

300 (FC f (l, c) _) <- getFC

330 ident <- identifierOrReserved

301 ident <- identifierOrReserved

331− when (ident `HS.member` reservedIdentifiers) $ P.unexpected $ "reserved " ++ ident

302+ when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident

332− when (ident == "_") $ P.unexpected "wildcard"

303+ when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"

333 return (ident, FC f (l, c) (l, c + length ident))

304 return (ident, FC f (l, c) (l, c + length ident))

334

305

335-- | Parses an identifier with possible namespace as a name

306-- | Parses an identifier with possible namespace as a name

@@ -340,8 +311,8 @@ iName bad = maybeWithNS identifier False bad <?> "name"

340maybeWithNS :: (MonadicParsing m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

311maybeWithNS :: (MonadicParsing m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

341maybeWithNS parser ascend bad = do

312maybeWithNS parser ascend bad = do

342 fc <- getFC

313 fc <- getFC

343− i <- P.option "" (lookAhead (fst <$> identifier))

314+ i <- P.option "" (P.lookAhead (fst <$> identifier))

344− when (i `elem` bad) $ P.unexpected "reserved identifier"

315+ when (i `elem` bad) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved identifier"

345 let transf = if ascend then id else reverse

316 let transf = if ascend then id else reverse

346 (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))

317 (x, xs, fc) <- P.choice (transf (parserNoNS parser : parsersNS parser i))

347 return (mkName (x, xs), fc)

318 return (mkName (x, xs), fc)

@@ -410,7 +381,7 @@ invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%

410

381

411-- | Parses an operator

382-- | Parses an operator

412symbolicOperator :: MonadicParsing m => m String

383symbolicOperator :: MonadicParsing m => m String

413−symbolicOperator = do op <- P.token . some $ operatorLetter

384+symbolicOperator = do op <- token . some $ operatorLetter

414 when (op `elem` (invalidOperators ++ commentMarkers)) $

385 when (op `elem` (invalidOperators ++ commentMarkers)) $

415 fail $ op ++ " is not a valid operator"

386 fail $ op ++ " is not a valid operator"

416 return op

387 return op

@@ -422,32 +393,17 @@ symbolicOperatorFC = do (FC f (l, c) _) <- getFC

422 return (op, FC f (l, c) (l, c + length op))

393 return (op, FC f (l, c) (l, c + length op))

423

394

424{- * Position helpers -}

395{- * Position helpers -}

425−{- | Get filename from position (returns "(interactive)" when no source file is given) -}

426−fileName :: P.Delta -> String

427−fileName (P.Directed fn _ _ _ _) = UTF8.toString fn

428−fileName _ = "(interactive)"

429−

430−{- | Get line number from position -}

431−lineNum :: P.Delta -> Int

432−lineNum (P.Lines l _ _ _) = fromIntegral l + 1

433−lineNum (P.Directed _ l _ _ _) = fromIntegral l + 1

434−lineNum _ = 0

435−

436−{- | Get column number from position -}

437−columnNum :: P.Delta -> Int

438−columnNum pos = fromIntegral (P.column pos) + 1

439−

440−

441{- | Get file position as FC -}

396{- | Get file position as FC -}

442getFC :: MonadicParsing m => m FC

397getFC :: MonadicParsing m => m FC

443−getFC = do s <- P.position

398+getFC = do pos <- P.getPosition

399+ let columnNumber = P.unPos . P.sourceColumn $ pos

400+ let lineNumber = P.unPos . P.sourceLine $ pos

444− let (dir, file) = splitFileName (fileName s)

401+ let (dir, file) = splitFileName (P.sourceName pos)

445− let f = if dir == addTrailingPathSeparator "." then file else fileName s

402+ let f = if dir == addTrailingPathSeparator "." then file else P.sourceName pos

446− return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

403+ return $ FC f (lineNumber, columnNumber) (lineNumber, columnNumber) -- TODO: Change to actual spanning

447 -- Issue #1594 on the Issue Tracker.

404 -- Issue #1594 on the Issue Tracker.

448 -- https://github.com/idris-lang/Idris-dev/issues/1594

405 -- https://github.com/idris-lang/Idris-dev/issues/1594

449

406

450−

451{-* Syntax helpers-}

407{-* Syntax helpers-}

452-- | Bind constraints to term

408-- | Bind constraints to term

453bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm

409bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm

@@ -457,15 +413,15 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

457{- | @commaSeparated p@ parses one or more occurences of `p`,

413{- | @commaSeparated p@ parses one or more occurences of `p`,

458 separated by commas and optional whitespace. -}

414 separated by commas and optional whitespace. -}

459commaSeparated :: MonadicParsing m => m a -> m [a]

415commaSeparated :: MonadicParsing m => m a -> m [a]

460−commaSeparated p = p `P.sepBy1` (P.spaces >> P.char ',' >> P.spaces)

416+commaSeparated p = p `P.sepBy1` (P.space >> P.char ',' >> P.space)

461

417

462{- * Layout helpers -}

418{- * Layout helpers -}

463

419

464-- | Push indentation to stack

420-- | Push indentation to stack

465pushIndent :: IdrisParser ()

421pushIndent :: IdrisParser ()

466−pushIndent = do pos <- P.position

422+pushIndent = do columnNumber <- indent

467 ist <- get

423 ist <- get

468− put (ist { indent_stack = (fromIntegral (P.column pos) + 1) : indent_stack ist })

424+ put (ist { indent_stack = columnNumber : indent_stack ist })

469

425

470-- | Pops indentation from stack

426-- | Pops indentation from stack

471popIndent :: IdrisParser ()

427popIndent :: IdrisParser ()

@@ -476,8 +432,8 @@ popIndent = do ist <- get

476

432

477

433

478-- | Gets current indentation

434-- | Gets current indentation

479−indent :: IdrisParser Int

435+indent :: MonadicParsing m => m Int

480−indent = liftM ((+1) . fromIntegral . P.column) P.position

436+indent = P.unPos . P.sourceColumn <$> P.getPosition

481

437

482-- | Gets last indentation

438-- | Gets last indentation

483lastIndent :: IdrisParser Int

439lastIndent :: IdrisParser Int

@@ -520,8 +476,7 @@ indentedBlockS p = do openBlock

520

476

521-- | Checks if the following character matches provided parser

477-- | Checks if the following character matches provided parser

522lookAheadMatches :: MonadicParsing m => m a -> m Bool

478lookAheadMatches :: MonadicParsing m => m a -> m Bool

523−lookAheadMatches p = do match <- lookAhead (optional p)

479+lookAheadMatches p = isJust <$> P.lookAhead (P.optional p)

524− return $ isJust match

525

480

526-- | Parses a start of block

481-- | Parses a start of block

527openBlock :: IdrisParser ()

482openBlock :: IdrisParser ()

@@ -565,7 +520,7 @@ terminator = do lchar ';'; popIndent

565 if c <= l then popIndent else fail "not a terminator"

520 if c <= l then popIndent else fail "not a terminator"

566 <|> do isParen <- lookAheadMatches (P.oneOf ")}")

521 <|> do isParen <- lookAheadMatches (P.oneOf ")}")

567 if isParen then popIndent else fail "not a terminator"

522 if isParen then popIndent else fail "not a terminator"

568− <|> lookAhead P.eof

523+ <|> P.lookAhead P.eof

569

524

570-- | Parses and keeps a terminator

525-- | Parses and keeps a terminator

571keepTerminator :: IdrisParser ()

526keepTerminator :: IdrisParser ()

@@ -575,7 +530,7 @@ keepTerminator = () <$ lchar ';'

575 <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

530 <|> do isParen <- lookAheadMatches (P.oneOf ")}|")

576 isIn <- lookAheadMatches (reserved "in")

531 isIn <- lookAheadMatches (reserved "in")

577 unless (isIn || isParen) $ fail "not a terminator"

532 unless (isIn || isParen) $ fail "not a terminator"

578− <|> lookAhead P.eof

533+ <|> P.lookAhead P.eof

579

534

580-- | Checks if application expression does not end

535-- | Checks if application expression does not end

581notEndApp :: IdrisParser ()

536notEndApp :: IdrisParser ()

@@ -587,7 +542,7 @@ notEndBlock :: IdrisParser ()

587notEndBlock = do ist <- get

542notEndBlock = do ist <- get

588 case brace_stack ist of

543 case brace_stack ist of

589 Just lvl : xs -> do i <- indent

544 Just lvl : xs -> do i <- indent

590− isParen <- lookAheadMatches (char ')')

545+ isParen <- lookAheadMatches (P.char ')')

591 when (i < lvl || isParen) (fail "end of block")

546 when (i < lvl || isParen) (fail "end of block")

592 _ -> return ()

547 _ -> return ()

593

548

src/Idris/Parser/Ops.hs+26−24

@@ -21,39 +21,40 @@ import Control.Monad

21import Control.Monad.State.Strict

22import Data.Char (isAlpha)

23import Data.List

24−import Text.Parser.Expression

24+import Data.List.NonEmpty (fromList)

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

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

26−import qualified Text.Trifecta as P

26+import qualified Text.Megaparsec as P

27+import qualified Text.Megaparsec.Expr as P

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

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

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

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

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

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

31table fixes

32table fixes

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

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

33 toTable (reverse fixes) ++

34 toTable (reverse fixes) ++

34 [[noFixityBacktickOperator],

35 [[noFixityBacktickOperator],

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

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

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

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

37 [noFixityOperator]]

38 [noFixityOperator]]

38 where

39 where

39 flatten :: PTerm -> PTerm -- flatten application

40 flatten :: PTerm -> PTerm -- flatten application

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

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

41 flatten t = t

42 flatten t = t

43− noFixityBacktickOperator :: Operator IdrisParser PTerm

44+ noFixityBacktickOperator :: P.Operator IdrisParser PTerm

44− noFixityBacktickOperator = flip Infix AssocNone $ do

45+ noFixityBacktickOperator = P.InfixN $ do

45 (n, fc) <- backtickOperator

46 (n, fc) <- backtickOperator

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

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

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

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

49− noFixityOperator :: Operator IdrisParser PTerm

50+ noFixityOperator :: P.Operator IdrisParser PTerm

50− noFixityOperator = flip Infix AssocNone $ do

51+ noFixityOperator = P.InfixN $ do

51 indentGt

52 indentGt

52 op <- P.try symbolicOperator

53 op <- P.try symbolicOperator

53− P.unexpected $ "Operator without known fixity: " ++ op

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

55 -- | Calculates table for fixity declarations

56 -- | Calculates table for fixity declarations

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

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

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

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

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

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

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

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

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

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

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

64− assoc (Infixl _) = AssocLeft

65+ assoc (Infixl _) = P.InfixL

65− assoc (Infixr _) = AssocRight

66+ assoc (Infixr _) = P.InfixR

66− assoc (InfixN _) = AssocNone

67+ assoc (InfixN _) = P.InfixN

68 isBacktick :: String -> Bool

69 isBacktick :: String -> Bool

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

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

70 isBacktick _ = False

71 isBacktick _ = False

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

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

73− binary name assoc f

74+ binary name ctor f

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

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

75 (n, fc) <- backtickOperator

76 (n, fc) <- backtickOperator

76 guard $ show (nsroot n) == name

77 guard $ show (nsroot n) == name

77 return $ f fc n

78 return $ f fc n

78− | otherwise = flip Infix assoc $ do

79+ | otherwise = ctor $ do

79 indentGt

80 indentGt

80 fc <- reservedOpFC name

81 fc <- reservedOpFC name

81 indentGt

82 indentGt

82 return $ f fc (sUN name)

83 return $ f fc (sUN name)

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

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

85− prefix name f = Prefix (do reservedOp name

86+ prefix name f = P.Prefix $ do

87+ reservedOp name

86− fc <- getFC

88+ fc <- getFC

87− indentGt

89+ indentGt

88− return (f fc))

90+ return (f fc)

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

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

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

@@ -4,6 +4,7 @@ Description : Parser for the REPL commands.

4License : BSD3

5Maintainer : The Idris Community.

6-}

7+{-# LANGUAGE FlexibleContexts #-}

7module Idris.REPL.Parser (

8module Idris.REPL.Parser (

8 parseCmd

9 parseCmd

9 , help

10 , help

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

31import Data.List.Split (splitOn)

32import Data.List.Split (splitOn)

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

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

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

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

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

35+import qualified Text.Megaparsec as P

35−import Text.Parser.Combinators

36+import qualified Text.Megaparsec.Char as P

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

72 , cmd_apropos)

73 , cmd_apropos)

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

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

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

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

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

170 l <- IP.simpleExpr defaultSyntax

171 l <- IP.simpleExpr defaultSyntax

171 r <- IP.simpleExpr defaultSyntax

172 r <- IP.simpleExpr defaultSyntax

172− eof

173+ P.eof

173 return (Right (DebugUnify l r))

174 return (Right (DebugUnify l r))

174 )

175 )

175 ]

176 ]

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

188 (names, NoArg, doc, proofArg command)

189 (names, NoArg, doc, proofArg command)

189

190

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

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

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

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

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

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

193 <|> unrecognized

194 <|> unrecognized

194 <|> nop

195 <|> nop

195 <|> eval

196 <|> eval

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

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

197 unrecognized = do

198 unrecognized = do

198 IP.lchar ':'

199 IP.lchar ':'

199− cmd <- many anyChar

200+ cmd <- P.many P.anyChar

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

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

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

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

202

203

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

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

204−cmd xs = try $ do

205+cmd xs = P.try $ do

205 IP.lchar ':'

206 IP.lchar ':'

206 docmd sorted_xs

207 docmd sorted_xs

207

208

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

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

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

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

210

211

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

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

212

213

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

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

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

215noArgs cmd name = do

216noArgs cmd name = do

216 let emptyArgs = do

217 let emptyArgs = do

217− eof

218+ P.eof

218 return (Right cmd)

219 return (Right cmd)

219

220

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

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

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

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

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

230exprArg cmd name = do

231exprArg cmd name = do

231 let noArg = do

232 let noArg = do

232− eof

233+ P.eof

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

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

234

235

235 let justOperator = do

236 let justOperator = do

236 (op, fc) <- IP.symbolicOperatorFC

237 (op, fc) <- IP.symbolicOperatorFC

237− eof

238+ P.eof

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

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

239

240

240 let properArg = do

241 let properArg = do

241 t <- IP.fullExpr defaultSyntax

242 t <- IP.fullExpr defaultSyntax

242 return $ Right (cmd t)

243 return $ Right (cmd t)

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

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

244

245

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

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

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

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

247genArg argName argParser cmd name = do

248genArg argName argParser cmd name = do

248− let emptyArgs = do eof; failure

249+ let emptyArgs = do P.eof; failure

249 oneArg = do arg <- argParser

250 oneArg = do arg <- argParser

250− eof

251+ P.eof

251 return (Right (cmd arg))

252 return (Right (cmd arg))

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

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

253 where

254 where

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

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

255

256

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

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

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

259

260

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

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

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

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

262

263

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

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

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

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

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

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

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

274optArg cmd name = do

275optArg cmd name = do

275 let emptyArgs = do

276 let emptyArgs = do

276− eof

277+ P.eof

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

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

278

279

279 let oneArg = do

280 let oneArg = do

280 o <- pOption

281 o <- pOption

281 IP.whiteSpace

282 IP.whiteSpace

282− eof

283+ P.eof

283 return (Right (cmd o))

284 return (Right (cmd o))

284

285

285 let failure = return $ Left "Unrecognized setting"

286 let failure = return $ Left "Unrecognized setting"

286

287

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

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

288

289

289 where

290 where

290 pOption :: IP.IdrisParser Opt

291 pOption :: IP.IdrisParser Opt

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

292

293

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

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

294proofArg cmd name = do

295proofArg cmd name = do

295− upd <- option False $ do

296+ upd <- P.option False $ do

296 IP.lchar '!'

297 IP.lchar '!'

297 return True

298 return True

298 l <- fst <$> IP.natural

299 l <- fst <$> IP.natural

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

303cmd_doc name = do

304cmd_doc name = do

304 let constant = do

305 let constant = do

305 c <- fmap fst IP.constant

306 c <- fmap fst IP.constant

306− eof

307+ P.eof

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

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

308

309

309 let pType = do

310 let pType = do

310 IP.reserved "Type"

311 IP.reserved "Type"

311− eof

312+ P.eof

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

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

313

314

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

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

315

316

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

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

317

318

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

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

319cmd_consolewidth name = do

320cmd_consolewidth name = do

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

333

334

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

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

335cmd_execute name = do

336cmd_execute name = do

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

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

337 return (Right (Execute tm))

338 return (Right (Execute tm))

338 where

339 where

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

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

340

341

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

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

342cmd_dynamic name = do

343cmd_dynamic name = do

343− let optArg = do l <- many anyChar

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

344 if (l /= "")

345 if (l /= "")

345 then return $ Right (DynamicLink l)

346 then return $ Right (DynamicLink l)

346 else return $ Right ListDynamic

347 else return $ Right ListDynamic

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

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

348− try optArg <|> failure

349+ P.try optArg <|> failure

349

350

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

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

351cmd_pprint name = do

352cmd_pprint name = do

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

375 let hasOneArg = do

376 let hasOneArg = do

376 i <- get

377 i <- get

377 f <- fst <$> IP.identifier

378 f <- fst <$> IP.identifier

378− eof

379+ P.eof

379 return $ Right (Compile defaultCodegen f)

380 return $ Right (Compile defaultCodegen f)

380

381

381 let hasTwoArgs = do

382 let hasTwoArgs = do

382 i <- get

383 i <- get

383 codegen <- codegenOption

384 codegen <- codegenOption

384 f <- fst <$> IP.identifier

385 f <- fst <$> IP.identifier

385− eof

386+ P.eof

386 return $ Right (Compile codegen f)

387 return $ Right (Compile codegen f)

387

388

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

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

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

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

390

391

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

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

392cmd_addproof name = do

393cmd_addproof name = do

393− n <- option Nothing $ do

394+ n <- P.option Nothing $ do

394 x <- fst <$> IP.name

395 x <- fst <$> IP.name

395 return (Just x)

396 return (Just x)

396− eof

397+ P.eof

397 return (Right (AddProof n))

398 return (Right (AddProof n))

398

399

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

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

400cmd_log name = do

401cmd_log name = do

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

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

402− eof

403+ P.eof

403 return (Right (LogLvl i))

404 return (Right (LogLvl i))

404

405

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

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

406cmd_verb name = do

407cmd_verb name = do

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

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

408− eof

409+ P.eof

409 return (Right (Verbosity i))

410 return (Right (Verbosity i))

410

411

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

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

412cmd_cats name = do

413cmd_cats name = do

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

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

414− eof

415+ P.eof

415 return $ Right $ LogCategory (concat cs)

416 return $ Right $ LogCategory (concat cs)

416 where

417 where

417 badCat = do

418 badCat = do

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

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

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

420

421

421 pLogCats :: IP.IdrisParser [LogCat]

422 pLogCats :: IP.IdrisParser [LogCat]

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

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

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

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

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

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

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

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

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

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

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

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

428 <|> badCat

429 <|> badCat

429

430

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

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

431cmd_let name = do

432cmd_let name = do

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

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

433 return (Right (NewDefn defn))

434 return (Right (NewDefn defn))

434

435

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

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

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

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

437

438

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

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

439cmd_loadto name = do

440cmd_loadto name = do

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

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

441− f <- many anyChar;

442+ f <- P.many P.anyChar

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

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

443

444

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

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

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

460 pSetColourCmd :: IP.IdrisParser Command

461 pSetColourCmd :: IP.IdrisParser Command

461 pSetColourCmd = (do c <- pColourType

462 pSetColourCmd = (do c <- pColourType

462 let defaultColour = IdrisColour Nothing True False False False

463 let defaultColour = IdrisColour Nothing True False False False

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

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

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

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

465 return $ SetColour c colour)

466 return $ SetColour c colour)

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

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

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

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

468

469

469 pColour :: IP.IdrisParser (Maybe Color)

470 pColour :: IP.IdrisParser (Maybe Color)

470 pColour = doColour colours

471 pColour = doColour colours

471 where doColour [] = fail "Unknown colour"

472 where doColour [] = fail "Unknown colour"

472− 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

473

474

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

484 where doVivid i = i { vivid = True }

485 where doVivid i = i { vivid = True }

485 doDull i = i { vivid = False }

486 doDull i = i { vivid = False }

486 doUnderline i = i { underline = True }

487 doUnderline i = i { underline = True }

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

500 pColourType = doColourType colourTypes

501 pColourType = doColourType colourTypes

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

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

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

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

503− 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

504

505

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

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

506

507

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

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

508cmd_apropos = packageBasedCmd (some idChar) Apropos

509cmd_apropos = packageBasedCmd (some idChar) Apropos

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

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

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

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

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

512packageBasedCmd valParser cmd name =

513packageBasedCmd valParser cmd name =

513− try (do IP.lchar '('

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

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

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

515− IP.lchar ')'

516+ IP.lchar ')'

516− val <- valParser

517+ val <- valParser

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

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

518 <|> do val <- valParser

519 <|> do val <- valParser

519 return (Right (cmd [] val))

520 return (Right (cmd [] val))

520 where

521 where

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

526

527

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

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

528cmd_proofsearch name = do

529cmd_proofsearch name = do

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

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

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

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

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

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

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

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

533

534

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

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

535cmd_refine name = do

536cmd_refine name = do

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

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

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

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

538 hint <- fst <$> IP.fnName

539 hint <- fst <$> IP.fnName

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

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

test/interactive010/expected+14−10

@@ -7,14 +7,18 @@ Usage is :printdef <functionname>

7pat {ty_503} : Type toplevel.u. pat {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. Prelude.Interfaces./ {ty_503} {__interface_504}

9 : pty {ty_503} : Type toplevel.u. pty {__interface_504} : Prelude.Interfaces.Fractional {ty_503}. {ty_503} -> {ty_503} -> {ty_503}

10−(input):1:1: error: expected: ":",

10+(input):1:1:

11+ |

12+1 | /

13+ | ^

14+unexpected '/'

11− dependent type signature,

15+expecting ':', dependent type signature, or end of input

12− end of input

16+

13−/<EOF>

14−^

15−(input):1:1: error: expected: ":",

17+(input):1:1:

18+ |

19+1 | ++

20+ | ^

21+unexpected "++"

16− dependent type signature,

22+expecting ':', dependent type signature, or end of input

17− end of input

23+

18−++<EOF>

19−^

20Can't find implementation for Fractional ty

24Can't find implementation for Fractional ty

test/layout001/expected+67−70

@@ -1,76 +1,73 @@

1−./layout001a.idr:5:1: error: Wrong

1+./layout001a.idr:5:1:

2+ |

3+5 | y

4+ | ^

2− indention: should be greater

5+Wrong indention: should be greater than context indentation

3− than context

4− indentation, expected: space

5−y

6−^

7−./layout001b.idr:5:3: error: Wrong

7+./layout001b.idr:5:3:

8+ |

9+5 | = y

10+ | ^

8− indention: should be greater

11+Wrong indention: should be greater than context indentation

9− than context

12+

10− indentation, expected: space

11−= y

12− ^

13−./layout001c.idr:3:1: error: Wrong

13+./layout001c.idr:3:1:

14+ |

15+3 | 2

16+ | ^

17+= is not a valid operator

14− indention: should be greater

18+Wrong indention: should be greater than context indentation

15− than context

19+

16− indentation, expected: space

17−2

18−^

19−./layout001e.idr:6:1: error: Wrong

20+./layout001e.idr:6:1:

21+ |

22+6 | 3

23+ | ^

20− indention: should be greater

24+Wrong indention: should be greater than context indentation

21− than context

25+

22− indentation, expected: space

23−3

24−^

25−./layout001f.idr:6:2: error: Wrong

26+./layout001f.idr:6:2:

27+ |

28+6 | 3

29+ | ^

26− indention: should be greater

30+Wrong indention: should be greater than context indentation

27− than context

31+

28− indentation, expected: space

29− 3

30− ^

31−./layout001g.idr:6:3: error: Wrong

32+./layout001g.idr:6:3:

33+ |

34+6 | 3

35+ | ^

32− indention: should be greater

36+Wrong indention: should be greater than context indentation

33− than context

37+

34− indentation, expected: space

35− 3

36− ^

37−./layout001h.idr:6:3: error: Wrong

38+./layout001h.idr:6:3:

39+ |

40+6 | 3

41+ | ^

38− indention: should be greater

42+Wrong indention: should be greater than context indentation

39− than context

43+

40− indentation, expected: space

41− 3

42− ^

43−./layout001i.idr:6:4: error: Wrong

44+./layout001i.idr:6:4:

45+ |

46+6 | 3

47+ | ^

44− indention: should be greater

48+Wrong indention: should be greater than context indentation

45− than context

49+

46− indentation, expected: space

47− 3

48− ^

49−./layout001j.idr:6:5: error: Wrong

50+./layout001j.idr:6:5:

51+ |

52+6 | 3

53+ | ^

50− indention: should be greater

54+Wrong indention: should be greater than context indentation

51− than context

55+

52− indentation, expected: space

53− 3

54− ^

55−./layout001l.idr:6:1: error: Wrong

56+./layout001l.idr:6:1:

57+ |

58+6 | y

59+ | ^

56− indention: should be greater

60+Wrong indention: should be greater than context indentation

57− than context

61+

58− indentation, expected: space

59−y

60−^

61mplus1.idr:13:31:When checking right hand side of term with expected type

62mplus1.idr:13:31:When checking right hand side of term with expected type

62 Maybe Int

63 Maybe Int

64When checking an application of function Prelude.Applicative.pure:

65When checking an application of function Prelude.Applicative.pure:

65 No such variable f

66 No such variable f

66−./mplus2.idr:17:37: error: not

67+./mplus2.idr:17:37:

67− end of block, expected: ")",

68+ |

68− "->", ";", "in",

69− ambiguous use of a left-associative operator,

70− ambiguous use of a non-associative operator,

71− ambiguous use of a right-associative operator,

72− do block expression,

73− end of input

74− `mplus` pure f

69+17 | `mplus` pure f

75− ^

70+ | ^

71+not end of block

72+

76mplus3.idr:11:1:warning - Unreachable case: term

73mplus3.idr:11:1:warning - Unreachable case: term

test/pkg004/expected+6−5

@@ -1,5 +1,6 @@

1−Uncaught error: user error (test.ipkg:9:1: error: filename

1+Uncaught error: user error (test.ipkg:9:1:

2+ |

3+9 | <empty line>

4+ | ^

2− must contain no directory

5+filename must contain no directory component

3− component, expected: space

4−<EOF>

5−^ )

6+)

test/pkg004/test.ipkg+1−1

@@ -5,4 +5,4 @@ modules = Main

5opts = "--warnpartial --warnreach --nocolour --quiet --consolewidth 80"

7main = Main

8−executable = "filenames/cannot include\a directory separator"

8+executable = "filenames/cannot include\\a directory separator"

test/regression002/expected+24−24

@@ -72,16 +72,18 @@ reg049.idr:5:6:When checking right hand side of uhOh with expected type

72 Void

74No such variable Bogus

75−./badbangop.idr:7:1: error: ! is

75+./badbangop.idr:7:1:

76− not a valid

76+ |

77− operator, expected: space

78−(!) : List a -> Nat -> Maybe a

77+7 | (!) : List a -> Nat -> Maybe a

79−^

78+ | ^

79+! is not a valid operator

80+

80−./baddoublebang.idr:6:28: error: unexpected

81+./baddoublebang.idr:6:28:

82+ |

83+6 | doubleBang mmn = do pure !!mmn

84+ | ^

81− Operator without known fixity:

85+unexpected Operator without known fixity: !!

82− !!, expected: space

86+

83−doubleBang mmn = do pure !!mmn

84− ^

85reg054.idr:18:5:When checking left hand side of inf:

87reg054.idr:18:5:When checking left hand side of inf:

86When checking an application of constructor Main.MkInfer:

88When checking an application of constructor Main.MkInfer:

87 Attempting concrete match on polymorphic argument: 0

89 Attempting concrete match on polymorphic argument: 0

@@ -118,20 +120,18 @@ Type level variable nat is not Main.nat

118Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn

120Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn

119reg070.idr:7:1:

121reg070.idr:7:1:

120Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

122Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show

121−./reg076.idr:8:1: error: Missing

123+./reg076.idr:8:1:

124+ |

125+8 | <empty line>

126+ | ^

122− fixity declaration for

127+Missing fixity declaration for Main.:>

123− Main.:>, expected: "->", "=>",

128+

124− ambiguous use of a left-associative operator,

125− ambiguous use of a non-associative operator,

126− ambiguous use of a right-associative operator

127−<EOF>

128−^

129−./reg077.idr:3:1: error: Missing

129+./reg077.idr:3:1:

130+ |

131+3 | <empty line>

132+ | ^

130− fixity declaration for

133+Missing fixity declaration for Main.:>>

131− Main.:>>, expected: ")", ";",

134+

132− "in", start of block

133−<EOF>

134−^

135DoubleEquality.idr:4:87:When checking right hand side of oops with expected type

136 Void

137