b1a4264 · Idris-dev · git.iko.soy

CHANGELOG.md+7

@@ -79,6 +79,13 @@

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

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

8181 some subtle deviations in parsing from previous versions of Idris.

82++ Many more errors now report beginning *and* ending position (which may be

83+ on different lines), instead of just a single point. The format is

84+ `Foo.idr:9:7-15:` if ending column is on the same line or

85+ `Foo.idr:9:7-10:15:` if the ending column is on a different line.

86++ Error messages were changed so that the last column is inclusive, e.g.

87+ `Foo.idr:9:7-15:` includes column 15. Previously the error would have read

88+ `Foo.idr:9:7-16:`.

8289

8390## Packaging Updates

8491

idris.cabal+3−2

@@ -206,10 +206,11 @@ Library

206206 , Idris.ModeCommon

207207 , Idris.Options

208208 , Idris.Parser

209+ , Idris.Parser.Data

210+ , Idris.Parser.Expr

209211 , Idris.Parser.Helpers

210212 , Idris.Parser.Ops

211− , Idris.Parser.Expr

212− , Idris.Parser.Data

213+ , Idris.Parser.Stack

213214 , Idris.PartialEval

214215 , Idris.Primitives

215216 , Idris.ProofSearch

src/Idris/Completion.hs+1−1

@@ -20,7 +20,7 @@ import Idris.Help

2020import Idris.Imports (installedPackages)

2121import Idris.Parser.Expr (TacticArg(..))

2222import qualified Idris.Parser.Expr (constants, tactics)

23−import Idris.Parser.Helpers (opChars)

23+import Idris.Parser.Ops (opChars)

2424import Idris.REPL.Parser (allHelp, setOptions)

2525

2626import Control.Monad.State.Strict

src/Idris/Core/TT.hs+20−27

@@ -47,7 +47,7 @@ module Idris.Core.TT(

4747 , pEraseType, pmap, pprintRaw, pprintTT, pprintTTClause, prettyEnv, psubst

4848 , pToV, pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget

4949 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep

50− , sImplementationN, sMN, sNS, spanFC, str, subst, substNames, substTerm

50+ , sImplementationN, sMN, sNS, str, subst, substNames, substTerm

5151 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull

5252 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName

5353 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

@@ -59,9 +59,9 @@ import Util.Pretty hiding (Str)

5959

6060-- Work around AMP without CPP

6161import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,

62− Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),

63− Show(..), String, div, error, fst, mod, not, otherwise, read,

64− snd, ($), (&&), (.), (||))

62+ Integer, Maybe(..), Monad(..), Monoid(..), Num(..), Ord(..),

63+ Ordering(..), Show(..), String, div, error, fst, max, min, mod,

64+ not, otherwise, read, snd, ($), (&&), (.), (||))

6565

6666import Control.Applicative (Alternative, Applicative(..))

6767import qualified Control.Applicative as A (Alternative(..))

@@ -87,7 +87,7 @@ data Option = TTypeInTType

8787 | CheckConv

8888 deriving Eq

8989

90−-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'

90+-- | Source location. These are typically produced by 'Idris.Parser.Stack.withExtent'

9191data FC = FC { _fc_fname :: String, -- ^ Filename

9292 _fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

9393 _fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

@@ -117,29 +117,22 @@ fc_end (FC _ _ end) = end

117117fc_end NoFC = (0, 0)

118118fc_end (FileFC f) = (0, 0)

119119

120−-- | Get the largest span containing the two FCs

121−spanFC :: FC -> FC -> FC

122−spanFC (FC f start end) (FC f' start' end')

123− | f == f' = FC f (minLocation start start') (maxLocation end end')

124− | otherwise = NoFC

125− where minLocation (l, c) (l', c') =

126− case compare l l' of

127− LT -> (l, c)

128− EQ -> (l, min c c')

129− GT -> (l', c')

130− maxLocation (l, c) (l', c') =

131− case compare l l' of

132− LT -> (l', c')

133− EQ -> (l, max c c')

134− GT -> (l, c)

135−spanFC fc@(FC f _ _) (FileFC f') | f == f' = fc

120+instance Monoid FC where

121+ mempty = NoFC

122+

123+ -- | Get the largest span containing the two FCs

124+ mappend (FC f start end) (FC f' start' end')

125+ | f == f' = FC f (min start start') (max end end')

126+ | otherwise = NoFC

127+ mappend fc@(FC f _ _) (FileFC f') | f == f' = fc

128+ | otherwise = NoFC

129+ mappend (FileFC f') fc@(FC f _ _) | f == f' = fc

130+ | otherwise = NoFC

131+ mappend (FileFC f) (FileFC f') | f == f' = FileFC f

136132 | otherwise = NoFC

137−spanFC (FileFC f') fc@(FC f _ _) | f == f' = fc

138− | otherwise = NoFC

139−spanFC (FileFC f) (FileFC f') | f == f' = FileFC f

140− | otherwise = NoFC

141−spanFC NoFC fc = fc

142−spanFC fc NoFC = fc

133+ mappend NoFC fc = fc

134+ mappend fc NoFC = fc

135+

143136

144137-- | Determine whether the first argument is completely contained in the second

145138fcIn :: FC -> FC -> Bool

src/Idris/IdrisDoc.hs+1−1

@@ -18,7 +18,7 @@ import Idris.Docs

1818import Idris.Docstrings (nullDocstring)

1919import qualified Idris.Docstrings as Docstrings

2020import Idris.Options

21−import Idris.Parser.Helpers (opChars)

21+import Idris.Parser.Ops (opChars)

2222import IRTS.System (getIdrisDataFileByName)

2323

2424import Control.Applicative ((<|>))

src/Idris/Package/Parser.hs+18−19

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

1111import Idris.CmdOptions

1212import Idris.Imports

1313import Idris.Package.Common

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

15− identifier, isEol, lchar, packageName,

16− parseErrorDoc, reserved, runparser, someSpace,

17− stringLiteral)

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

15+ lchar, packageName, parseErrorDoc, reserved,

16+ runparser, someSpace, stringLiteral)

1817

1918import Control.Applicative

2019import Control.Monad.State.Strict

@@ -27,7 +26,7 @@ import qualified Text.Megaparsec as P

2726import qualified Text.Megaparsec.Char as P

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

2928

30−type PParser = StateT PkgDesc IdrisInnerParser

29+type PParser = Parser PkgDesc

3130

3231parseDesc :: FilePath -> IO PkgDesc

3332parseDesc fp = do

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

6261-- | Parses a filename.

6362-- |

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

65−filename :: (MonadicParsing m) => m String

64+filename :: Parsing m => m String

6665filename = (do

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

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

6968 -- it will also accept hyphens

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

71− filename <- fst <$> stringLiteral

70+ filename <- stringLiteral

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

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

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

73+ <|> show <$> iName []

7574 case filenameErrorMessage filename of

7675 Just errorMessage -> fail errorMessage

7776 Nothing -> return filename)

@@ -99,36 +98,36 @@ filename = (do

9998 checkThat (path == takeFileName path)

10099 "filename must contain no directory component"

101100

102−textUntilEol :: MonadicParsing m => m String

101+textUntilEol :: Parsing m => m String

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

104103

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

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

107106 modify $ \st -> f st value

108107

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

108+commaSep :: Parsing m => m a -> m [a]

110109commaSep p = P.sepBy1 p (lchar ',')

111110

112111pClause :: PParser ()

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

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

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

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

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

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

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

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

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

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

120119 , idris_opts = pkgs ++ idris_opts st })

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Parser.hs+205−204

@@ -85,8 +85,8 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP

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

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

8787 noArgs docs

88− reservedHL "module"

89− (i, ifc) <- identifier

88+ keyword "module"

89+ (i, ifc) <- withExtent identifier

9090 P.option ';' (lchar ';')

9191 let modName = moduleName i

9292 return (fmap fst docs,

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

116116@

117117 -}

118118import_ :: IdrisParser ImportInfo

119−import_ = do fc <- getFC

120− reservedHL "import"

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

122− (id, idfc) <- identifier

123− newName <- optional (do reservedHL "as"

124− identifier)

119+import_ = do fc <- extent $ keyword "import"

120+ reexport <- P.option False (True <$ keyword "public")

121+ (id, idfc) <- withExtent identifier

122+ newName <- optional (do keyword "as"

123+ withExtent identifier)

125124 P.option ';' (lchar ';')

126125 return $ ImportInfo reexport (toPath id)

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

@@ -137,17 +136,17 @@ import_ = do fc <- getFC

137136@

138137 -}

139138prog :: SyntaxInfo -> IdrisParser [PDecl]

140−prog syn = do whiteSpace

141− decls <- many (decl syn)

142− let c = concat decls

143− case maxline syn of

144− Nothing -> do notOpenBraces; P.eof

145− _ -> return ()

139+prog syn = do (decls, fc) <- withExtent $ do

140+ whiteSpace

141+ decls <- concat <$> many (decl syn)

142+ case maxline syn of

143+ Nothing -> do notOpenBraces; P.eof

144+ _ -> return ()

145+ return decls

146146 ist <- get

147− fc <- getFC

148147 put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),

149148 ibc_write = IBCParsedRegion fc : ibc_write ist }

150− return c

149+ return decls

151150

152151{-| Parses a top-level declaration

153152

@@ -198,7 +197,7 @@ internalDecl syn

198197 <|> fail "End of readable input"

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

200199 declBody b =

201− P.try (implementation True syn)

200+ P.try (implementation syn)

202201 <|> P.try (openInterface syn)

203202 <|> declBody' b

204203 <|> using_ syn

@@ -248,13 +247,8 @@ decl' syn = fixity

248247externalDecl :: SyntaxInfo -> IdrisParser [PDecl]

249248externalDecl syn = do i <- get

250249 notEndBlock

251− FC fn start _ <- getFC

252− decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)

253− FC _ _ end <- getFC

254− let outerFC = FC fn start end

255− return $ map (mapPDeclFC (fixFC outerFC)

256− (fixFCH fn outerFC))

257− decls

250+ (decls, fc@(FC fn _ _)) <- withExtent $ declExtensions syn (syntaxRulesList $ syntax_rules i)

251+ return $ map (mapPDeclFC (fixFC fc) (fixFCH fn fc)) decls

258252 where

259253 -- | Fix non-highlighting FCs to prevent spurious error location reports

260254 fixFC :: FC -> FC -> FC

@@ -360,18 +354,14 @@ declExtension syn ns rules =

360354 ruleGroup _ _ = False

361355

362356 extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

363− extSymbol (Keyword n) = do fc <- reservedFC (show n)

364− highlightP fc AnnKeyword

365− return Nothing

357+ extSymbol (Keyword n) = Nothing <$ keyword (show n)

366358 extSymbol (Expr n) = do tm <- expr syn

367359 return $ Just (n, SynTm tm)

368360 extSymbol (SimpleExpr n) = do tm <- simpleExpr syn

369361 return $ Just (n, SynTm tm)

370− extSymbol (Binding n) = do (b, fc) <- name

362+ extSymbol (Binding n) = do (b, fc) <- withExtent name

371363 return $ Just (n, SynBind fc b)

372− extSymbol (Symbol s) = do fc <- symbolFC s

373− highlightP fc AnnKeyword

374− return Nothing

364+ extSymbol (Symbol s) = Nothing <$ highlight AnnKeyword (symbol s)

375365

376366{-| Parses a syntax extension declaration (and adds the rule to parser state)

377367

@@ -380,10 +370,8 @@ declExtension syn ns rules =

380370@

381371-}

382372syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

383−syntaxDecl syn = do s <- syntaxRule syn

384− i <- get

385− put (i `addSyntax` s)

386− fc <- getFC

373+syntaxDecl syn = do (s, fc) <- withExtent $ syntaxRule syn

374+ modify $ \i -> i `addSyntax` s

387375 return (PSyntax fc s)

388376

389377-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.

@@ -428,9 +416,9 @@ syntaxRule syn

428416 = do sty <- P.try (do

429417 pushIndent

430418 sty <- P.option AnySyntax

431− (TermSyntax <$ reservedHL "term"

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

433− reservedHL "syntax"

419+ (TermSyntax <$ keyword "term"

420+ <|> PatternSyntax <$ keyword "pattern")

421+ keyword "syntax"

434422 return sty)

435423 syms <- some syntaxSym

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

@@ -441,7 +429,7 @@ syntaxRule syn

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

442430 terminator

443431 return (Rule (mkSimple syms) tm sty)

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

432+ <|> do keyword "decl"; keyword "syntax"

445433 syms <- some syntaxSym

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

447435 let ns = mapMaybe getName syms

@@ -542,13 +530,13 @@ SyntaxSym ::= '[' Name_t ']'

542530@

543531 -}

544532syntaxSym :: IdrisParser SSymbol

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

533+syntaxSym = P.try (do lchar '['; n <- name; lchar ']'

546534 return (Expr n))

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

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

548536 return (Binding n))

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

537+ <|> do n <- iName []

550538 return (Keyword n)

551− <|> do sym <- fmap fst stringLiteral

539+ <|> do sym <- stringLiteral

552540 return (Symbol sym)

553541 <?> "syntax symbol"

554542

@@ -582,10 +570,9 @@ fnDecl' syn = (checkDeclFixity $

582570 pushIndent

583571 (doc, argDocs) <- docstring syn

584572 (opts, acc) <- fnOpts

585− (n_in, nfc) <- fnName

573+ (n_in, nfc) <- withExtent fnName

586574 let n = expandNS syn n_in

587− fc <- getFC

588− lchar ':'

575+ fc <- extent $ lchar ':'

589576 return (doc, argDocs, fc, opts, n, nfc, acc))

590577 ty <- typeExpr (allowImp syn)

591578 terminator

@@ -655,16 +642,15 @@ NameTimesList ::=

655642@

656643-}

657644fnOpt :: IdrisParser FnOpt

658−fnOpt = do reservedHL "total"; return TotalFn

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

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

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

645+fnOpt = do keyword "total"; return TotalFn

646+ <|> PartialFn <$ keyword "partial"

647+ <|> CoveringFn <$ keyword "covering"

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

662649 return $ CExport c

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

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

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

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

667− fc <- getFC

653+ <|> do fc <- P.try $ extent $ lchar '%' *> reserved "assert_total"

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

669655 return AssertTotal

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

@@ -676,11 +662,11 @@ fnOpt = do reservedHL "total"; return TotalFn

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

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

678664 return $ Specialise ns

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

665+ <|> Implicit <$ keyword "implicit"

680666 <?> "function modifier"

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

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

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

668+ nameTimes = do n <- fnName

669+ t <- P.option Nothing (do reds <- natural

684670 return (Just (fromInteger reds)))

685671 return (n, t)

686672

@@ -700,16 +686,15 @@ postulate syn = do (doc, ext)

700686 return (doc, ext)

701687 ist <- get

702688 (opts, acc) <- fnOpts

703− (n_in, nfc) <- fnName

689+ (n_in, nfc) <- withExtent fnName

704690 let n = expandNS syn n_in

705691 lchar ':'

706692 ty <- typeExpr (allowImp syn)

707− fc <- getFC

708− terminator

693+ fc <- extent $ terminator

709694 addAcc n acc

710695 return (PPostulate ext doc syn fc nfc opts n ty)

711696 <?> "postulate"

712− where ppostDecl = do fc <- reservedHL "postulate"; return False

697+ where ppostDecl = do fc <- keyword "postulate"; return False

713698 <|> do lchar '%'; reserved "extern"; return True

714699

715700{-| Parses a using declaration

@@ -722,7 +707,7 @@ Using ::=

722707 -}

723708using_ :: SyntaxInfo -> IdrisParser [PDecl]

724709using_ syn =

725− do reservedHL "using"

710+ do keyword "using"

726711 lchar '('; ns <- usingDeclList syn; lchar ')'

727712 openBlock

728713 let uvars = using syn

@@ -741,23 +726,24 @@ Params ::=

741726-}

742727params :: SyntaxInfo -> IdrisParser [PDecl]

743728params syn =

744− do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

729+ do (ns, fc) <- withExtent $ do

730+ keyword "parameters"

731+ lchar '(' *> typeDeclList syn <* lchar ')'

745732 let ns' = [(n, ty) | (_, n, _, ty) <- ns]

746733 openBlock

747734 let pvars = syn_params syn

748735 ds <- many (decl syn { syn_params = pvars ++ ns' })

749736 closeBlock

750− fc <- getFC

751737 return [PParams fc ns' (concat ds)]

752738 <?> "parameters declaration"

753739

754740-- | Parses an open block

755741openInterface :: SyntaxInfo -> IdrisParser [PDecl]

756742openInterface syn =

757− do reservedHL "using"

758− reservedHL "implementation"

759− fc <- getFC

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

743+ do (ns, fc) <- withExtent $ do

744+ keyword "using"

745+ keyword "implementation"

746+ P.sepBy1 (withExtent fnName) (lchar ',')

761747

762748 openBlock

763749 ds <- many (decl syn)

@@ -779,11 +765,10 @@ Mutual ::=

779765-}

780766mutual :: SyntaxInfo -> IdrisParser [PDecl]

781767mutual syn =

782− do reservedHL "mutual"

768+ do fc <- extent $ keyword "mutual"

783769 openBlock

784770 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

785771 closeBlock

786− fc <- getFC

787772 return [PMutual fc (concat ds)]

788773 <?> "mutual block"

789774

@@ -797,8 +782,8 @@ Namespace ::=

797782-}

798783namespace :: SyntaxInfo -> IdrisParser [PDecl]

799784namespace syn =

800− do reservedHL "namespace"

801− (n, nfc) <- identifier

785+ do keyword "namespace"

786+ (n, nfc) <- withExtent identifier

802787 openBlock

803788 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })

804789 closeBlock

@@ -812,7 +797,7 @@ namespace syn =

812797@

813798-}

814799implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]

815−implementationBlock syn = do reservedHL "where"

800+implementationBlock syn = do keyword "where"

816801 openBlock

817802 ds <- many (fnDecl syn)

818803 closeBlock

@@ -835,7 +820,7 @@ InterfaceBlock ::=

835820@

836821-}

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

838−interfaceBlock syn = do reservedHL "where"

823+interfaceBlock syn = do keyword "where"

839824 openBlock

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

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

@@ -844,7 +829,7 @@ interfaceBlock syn = do reservedHL "where"

844829 ist <- get

845830 let cd' = annotate syn ist cd

846831

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

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

848833 <|> do x <- data_ syn

849834 return [x]

850835 <|> fnDecl syn)

@@ -853,7 +838,7 @@ interfaceBlock syn = do reservedHL "where"

853838 <?> "interface block"

854839 where

855840 constructor :: IdrisParser (Name, FC)

856− constructor = reservedHL "constructor" *> fnName

841+ constructor = keyword "constructor" *> withExtent fnName

857842

858843 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

859844 annotate syn ist = annotCode $ tryFullExpr syn ist

@@ -879,33 +864,33 @@ interface_ syn = do (doc, argDocs, acc)

879864 acc <- accessibility

880865 interfaceKeyword

881866 return (doc, argDocs, acc))

882− fc <- getFC

883− cons <- constraintList syn

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

885− (n_in, nfc) <- fnName

886− let n = expandNS syn n_in

887− cs <- many carg

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

867+ ((cons', n, nfc, cs, fds), fc) <- withExtent $ do

868+ cons <- constraintList syn

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

870+ (n_in, nfc) <- withExtent fnName

871+ let n = expandNS syn n_in

872+ cs <- many carg

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

874+ return (cons', n, nfc, cs, fds)

875+

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

890877 accData acc n (concatMap declared ds)

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

892879 <?> "interface declaration"

893880 where

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

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

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

896883

897884 interfaceKeyword :: IdrisParser ()

898− interfaceKeyword = reservedHL "interface"

899− <|> do reservedHL "class"

900− fc <- getFC

885+ interfaceKeyword = keyword "interface"

886+ <|> do fc <- extent $ keyword "class"

901887 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

902888

903889 carg :: IdrisParser (Name, FC, PTerm)

904− carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'

890+ carg = do lchar '('; (i, ifc) <- withExtent name; lchar ':'; ty <- expr syn; lchar ')'

905891 return (i, ifc, ty)

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

907− fc <- getFC

908− return (i, ifc, PType fc)

892+ <|> do (i, ifc) <- withExtent name

893+ return (i, ifc, PType ifc)

909894

910895{-| Parses an interface implementation declaration

911896

@@ -919,41 +904,39 @@ interface_ syn = do (doc, argDocs, acc)

919904ImplementationName ::= '[' Name ']';

920905@

921906-}

922−implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

923−implementation kwopt syn

924− = do ist <- get

925− (doc, argDocs) <- docstring syn

907+implementation :: SyntaxInfo -> IdrisParser [PDecl]

908+implementation syn = do (doc, argDocs) <- docstring syn

926909 (opts, acc) <- fnOpts

927− if kwopt then optional implementationKeyword

928− else do implementationKeyword

929− return (Just ())

930−

931− fc <- getFC

932− en <- optional implementationName

933− cs <- constraintList syn

934− let cs' = [(c, ty) | (_, c, _, ty) <- cs]

935− (cn, cnfc) <- fnName

936− args <- many (simpleExpr syn)

910+ optional implementationKeyword

911+

912+ ((en, cs, cs', cn, cnfc, args, pnames), fc) <- withExtent $ do

913+ en <- optional implementationName

914+ cs <- constraintList syn

915+ let cs' = [(c, ty) | (_, c, _, ty) <- cs]

916+ (cn, cnfc) <- withExtent fnName

917+ args <- many (simpleExpr syn)

918+ pnames <- implementationUsing

919+ return (en, cs, cs', cn, cnfc, args, pnames)

920+

937921 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

938922 let t = bindList (\r -> PPi constraint { pcount = r }) cs sc

939− pnames <- implementationUsing

923+

940924 ds <- implementationBlock syn

941925 return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

942926 <?> "implementation declaration"

943927 where implementationName :: IdrisParser Name

944− implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

928+ implementationName = do lchar '['; n_in <- fnName; lchar ']'

945929 let n = expandNS syn n_in

946930 return n

947931 <?> "implementation name"

948932 implementationKeyword :: IdrisParser ()

949− implementationKeyword = reservedHL "implementation"

950− <|> do reservedHL "instance"

951− fc <- getFC

933+ implementationKeyword = keyword "implementation"

934+ <|> do fc <- extent $ keyword "instance"

952935 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

953936

954937 implementationUsing :: IdrisParser [Name]

955− implementationUsing = do reservedHL "using"

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

938+ implementationUsing = do keyword "using"

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

957940 return (map fst ns)

958941 <|> return []

959942

@@ -995,7 +978,7 @@ NameList ::=

995978usingDeclList :: SyntaxInfo -> IdrisParser [Using]

996979usingDeclList syn

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

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

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

999982 lchar ':'

1000983 t <- typeExpr (disallowImp syn)

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

@@ -1011,12 +994,12 @@ UsingDecl ::=

1011994@

1012995-}

1013996usingDecl :: SyntaxInfo -> IdrisParser Using

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

997+usingDecl syn = P.try (do x <- fnName

1015998 lchar ':'

1016999 t <- typeExpr (disallowImp syn)

10171000 return (UImplicit x t))

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

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

1001+ <|> do c <- fnName

1002+ xs <- many fnName

10201003 return (UConstraint c xs)

10211004 <?> "using declaration"

10221005

@@ -1027,8 +1010,7 @@ Pattern ::= Clause;

10271010@

10281011-}

10291012pattern :: SyntaxInfo -> IdrisParser PDecl

1030−pattern syn = do fc <- getFC

1031− clause <- clause syn

1013+pattern syn = do (clause, fc) <- withExtent (clause syn)

10321014 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later

10331015 <?> "pattern"

10341016

@@ -1039,13 +1021,12 @@ CAF ::= 'let' FnName '=' Expr Terminator;

10391021@

10401022-}

10411023caf :: SyntaxInfo -> IdrisParser PDecl

1042−caf syn = do reservedHL "let"

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

1024+caf syn = do keyword "let"

1025+ (n, fc) <- withExtent (expandNS syn <$> fnName)

10441026 pushIndent

10451027 lchar '='

10461028 t <- indented $ expr syn

10471029 terminator

1048− fc <- getFC

10491030 return (PCAF fc n t)

10501031 <?> "constant applicative form declaration"

10511032

@@ -1078,9 +1059,7 @@ rhs syn n = do lchar '='

10781059 indentGt

10791060 expr syn

10801061 <|> do symbol "?=";

1081− fc <- getFC

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

1083− return n)

1062+ (name, fc) <- withExtent $ P.option n' (symbol "{" *> fnName <* symbol "}")

10841063 r <- expr syn

10851064 return (addLet fc name r)

10861065 <|> impossible

@@ -1124,8 +1103,8 @@ WhereOrTerminator ::= WhereBlock | Terminator;

11241103-}

11251104clause :: SyntaxInfo -> IdrisParser PClause

11261105clause syn

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

1128− fc <- getFC

1106+ = appExtent (do

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

11291108 ist <- get

11301109 n <- case lastParse ist of

11311110 Just t -> return t

@@ -1134,22 +1113,21 @@ clause syn

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

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

11361115 <|> ([], []) <$ terminator

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

1116+ return $ \fc -> PClauseR fc wargs r wheres) <|> (do

11381117 popIndent

1139− reservedHL "with"

1118+ keyword "with"

11401119 wval <- simpleExpr syn

11411120 pn <- optProof

11421121 openBlock

11431122 ds <- some $ fnDecl syn

11441123 let withs = concat ds

11451124 closeBlock

1146− return $ PWithR fc wargs wval pn withs)

1125+ return $ \fc -> PWithR fc wargs wval pn withs))

11471126 <|> do ty <- P.try (do pushIndent

11481127 ty <- simpleExpr syn

11491128 symbol "<=="

11501129 return ty)

1151− fc <- getFC

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

1130+ (n, fc) <- withExtent (expandNS syn <$> fnName)

11531131 r <- rhs syn n

11541132 let wsyn = syn { syn_namespace = [] }

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

@@ -1164,15 +1142,14 @@ clause syn

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

11651143 pushIndent

11661144 l <- argExpr syn

1167− (op, nfc) <- symbolicOperatorFC

1145+ (op, nfc) <- withExtent symbolicOperator

11681146 when (op == "=" || op == "?=" ) $

11691147 fail "infix clause definition with \"=\" and \"?=\" not supported "

11701148 return (l, op, nfc))

11711149 let n = expandNS syn (sUN op)

11721150 r <- argExpr syn

1173− fc <- getFC

11741151 wargs <- many (wExpr syn)

1175− (do rs <- rhs syn n

1152+ (do (rs, fc) <- withExtent (rhs syn n)

11761153 let wsyn = syn { syn_namespace = [] }

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

11781155 <|> ([], []) <$ terminator

@@ -1181,9 +1158,11 @@ clause syn

11811158 put (ist { lastParse = Just n })

11821159 return $ PClause fc n capp wargs rs wheres) <|> (do

11831160 popIndent

1184− reservedHL "with"

1185− wval <- bracketed syn

1186− pn <- optProof

1161+ ((wval, pn), fc) <- withExtent $ do

1162+ keyword "with"

1163+ wval <- bracketed syn

1164+ pn <- optProof

1165+ return (wval, pn)

11871166 openBlock

11881167 ds <- some $ fnDecl syn

11891168 closeBlock

@@ -1193,35 +1172,37 @@ clause syn

11931172 put (ist { lastParse = Just n })

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

11951174 <|> do pushIndent

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

1197− fc <- getFC

1175+ (n_in, nfc) <- withExtent fnName; let n = expandNS syn n_in

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

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

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

12011179 wargs <- many (wExpr syn)

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

1203− (do r <- rhs syn n

1180+ (do (r, fc) <- withExtent (rhs syn n)

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

12041182 let wsyn = syn { syn_namespace = [] }

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

12061184 <|> ([], []) <$ terminator

12071185 ist <- get

12081186 put (ist { lastParse = Just n })

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

1210− reservedHL "with"

1188+ keyword "with"

12111189 ist <- get

12121190 put (ist { lastParse = Just n })

1213− wval <- bracketed syn

1214− pn <- optProof

1191+ ((wval, pn), fc) <- withExtent $ do

1192+ wval <- bracketed syn

1193+ pn <- optProof

1194+ return (wval, pn)

12151195 openBlock

12161196 ds <- some $ fnDecl syn

1217− let withs = map (fillLHSD n capp wargs) $ concat ds

12181197 closeBlock

12191198 popIndent

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

1200+ let withs = map (fillLHSD n capp wargs) $ concat ds

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

12211202 <?> "function clause"

12221203 where

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

1224− n <- fnName

1204+ optProof = P.option Nothing (do keyword "proof"

1205+ n <- withExtent fnName

12251206 return (Just n))

12261207

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

@@ -1255,7 +1236,7 @@ WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

12551236-}

12561237whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

12571238whereBlock n syn

1258− = do reservedHL "where"

1239+ = do keyword "where"

12591240 ds <- indentedBlock1 (decl syn)

12601241 let dns = concatMap (concatMap declared) ds

12611242 return (concat ds, map (\x -> (x, decoration syn x)) dns)

@@ -1274,7 +1255,7 @@ Codegen ::= 'C'

12741255@

12751256-}

12761257codegen_ :: IdrisParser Codegen

1277−codegen_ = do n <- fst <$> identifier

1258+codegen_ = do n <- identifier

12781259 return (Via IBCFormat (map toLower n))

12791260 <|> do reserved "Bytecode"; return Bytecode

12801261 <?> "code generation language"

@@ -1315,27 +1296,27 @@ Directive' ::= 'lib' CodeGen String_t

13151296directive :: SyntaxInfo -> IdrisParser [PDecl]

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

13171298 cgn <- codegen_

1318− lib <- fmap fst stringLiteral

1299+ lib <- stringLiteral

13191300 return [PDirective (DLib cgn lib)]

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

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

1302+ cgn <- codegen_; obj <- stringLiteral

13221303 return [PDirective (DLink cgn obj)]

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

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

1305+ cgn <- codegen_; flag <- stringLiteral

13251306 return [PDirective (DFlag cgn flag)]

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

13271308 cgn <- codegen_

1328− hdr <- fst <$> stringLiteral

1309+ hdr <- stringLiteral

13291310 return [PDirective (DInclude cgn hdr)]

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

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

13311312 return [PDirective (DHide n)]

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

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

13331314 return [PDirective (DFreeze n)]

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

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

13351316 return [PDirective (DThaw n)]

13361317 -- injectivity assertins are intended for debugging purposes

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

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

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

13391320 return [PDirective (DInjective n)]

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

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

@@ -1351,34 +1332,33 @@ directive syn = do P.try (lchar '%' *> reserved "lib")

13511332 put (i { default_total = tot } )

13521333 return [PDirective (DDefault tot)]

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

1354− i <- fst <$> natural

1335+ i <- natural

13551336 return [PDirective (DLogging i)]

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

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

1338+ libs <- P.sepBy1 stringLiteral (lchar ',')

13581339 return [PDirective (DDynamicLibs libs)]

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

1360− (ty, tyFC) <- fnName

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

1341+ (ty, tyFC) <- withExtent fnName

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

13621343 return [PDirective (DNameHint ty tyFC ns)]

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

1364− (fn, nfc) <- fnName

1365− (arg, afc) <- fnName

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

1345+ (fn, nfc) <- withExtent fnName

1346+ (arg, afc) <- withExtent fnName

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

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

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

13691350 return [PDirective (DLanguage ext)]

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

1371− n <- fst <$> fnName

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

1352+ n <- fnName

1353+ alt <- P.option "" stringLiteral

13731354 return [PDirective (DDeprecate n alt)]

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

1375− n <- fst <$> fnName

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

1356+ n <- fnName

1357+ alt <- P.option "" stringLiteral

13771358 return [PDirective (DFragile n alt)]

1378− <|> do fc <- getFC

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

1380− fn <- fst <$> fnName

1381− arg <- fst <$> iName []

1359+ <|> do fc <- extent $ P.try (lchar '%' *> reserved "used")

1360+ fn <- fnName

1361+ arg <- iName []

13821362 return [PDirective (DUsed fc fn arg)]

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

13841364 b <- on_off

@@ -1405,9 +1385,9 @@ Totality ::= 'partial' | 'total' | 'covering'

14051385-}

14061386totality :: IdrisParser DefaultTotality

14071387totality

1408− = do reservedHL "total"; return DefaultCheckingTotal

1409− <|> do reservedHL "partial"; return DefaultCheckingPartial

1410− <|> do reservedHL "covering"; return DefaultCheckingCovering

1388+ = do keyword "total"; return DefaultCheckingTotal

1389+ <|> do keyword "partial"; return DefaultCheckingPartial

1390+ <|> do keyword "covering"; return DefaultCheckingCovering

14111391

14121392{-| Parses a type provider

14131393

@@ -1418,25 +1398,20 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

14181398 -}

14191399provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1421− fc1 <- getFC

1422− lchar '%'

1423− fc2 <- reservedFC "provide"

1424− highlightP (spanFC fc1 fc2) AnnKeyword

1401+ highlight AnnKeyword $ lchar '%' *> reserved "provide"

14251402 return doc)

14261403 provideTerm doc <|> providePostulate doc

14271404 <?> "type provider"

14281405 where provideTerm doc =

1429− do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1430− fc <- getFC

1431− reservedHL "with"

1432− e <- expr syn <?> "provider expression"

1406+ do lchar '('; (n, nfc) <- withExtent fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1407+ keyword "with"

1408+ (e, fc) <- withExtent (expr syn) <?> "provider expression"

14331409 return [PProvider doc syn fc nfc (ProvTerm t e) n]

14341410 providePostulate doc =

1435− do reservedHL "postulate"

1436− (n, nfc) <- fnName

1437− fc <- getFC

1438− reservedHL "with"

1439− e <- expr syn <?> "provider expression"

1411+ do keyword "postulate"

1412+ (n, nfc) <- withExtent fnName

1413+ keyword "with"

1414+ (e, fc) <- withExtent (expr syn) <?> "provider expression"

14401415 return [PProvider doc syn fc nfc (ProvPostulate e) n]

14411416

14421417{-| Parses a transform

@@ -1452,8 +1427,7 @@ transform syn = do P.try (lchar '%' *> reserved "transform")

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

14531428-- return False)

14541429 l <- expr syn

1455− fc <- getFC

1456− symbol "==>"

1430+ fc <- extent $ symbol "==>"

14571431 r <- expr syn

14581432 return [PTransform fc False l r]

14591433 <?> "transform"

@@ -1466,12 +1440,8 @@ RunElabDecl ::= '%' 'runElab' Expr

14661440-}

14671441runElabDecl :: SyntaxInfo -> IdrisParser PDecl

14681442runElabDecl syn =

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

1470− lchar '%'

1471− fc' <- reservedFC "runElab"

1472− return (spanFC fc fc'))

1443+ do kwFC <- P.try (highlight AnnKeyword (extent $ lchar '%' *> reserved "runElab"))

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

1474− highlightP kwFC AnnKeyword

14751445 return $ PRunElabDecl kwFC script (syn_namespace syn)

14761446 <?> "top-level elaborator script"

14771447

@@ -1482,7 +1452,7 @@ parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

14821452

14831453{-| Parses a constant form input -}

14841454parseConst :: IState -> String -> Either ParseError Const

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

1455+parseConst st = runparser constant st "(input)"

14861456

14871457{-| Parses a tactic from input -}

14881458parseTactic :: IState -> String -> Either ParseError PTactic

@@ -1501,7 +1471,7 @@ parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> ela

15011471 (expressionTactic ["t", "type"] ECheck) <|>

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

15031473 (do reserved "doc"

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

1474+ doc <- (Right <$> constant) <|> (Left <$> fnName)

15051475 P.eof

15061476 return (EDocStr doc))

15071477 <?> "elab command"

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

15131483 spaced parser = indentGt *> parser

15141484

15151485-- | Parse module header and imports

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

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

15171487parseImports fname input

15181488 = do i <- getIState

15191489 case runparser imports i fname input of

@@ -1525,13 +1495,13 @@ parseImports fname input

15251495 return x

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

15271497 [ImportInfo],

1528− Maybe ParseState),

1498+ Maybe Mark),

15291499 [(FC, OutputAnnotation)], IState)

15301500 imports = do optional shebang

15311501 whiteSpace

15321502 (mdoc, mname, annots) <- moduleHeader

15331503 ps_exp <- many import_

1534− mrk <- P.getParserState

1504+ mrk <- mark

15351505 isEof <- lookAheadMatches P.eof

15361506 let mrk' = if isEof

15371507 then Nothing

@@ -1558,15 +1528,15 @@ fixColour True doc = doc

15581528

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

15601530-- documentation strings.

1561−parseProg :: SyntaxInfo -> FilePath -> String -> Maybe ParseState -> Idris [PDecl]

1531+parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]

15621532parseProg syn fname input mrk

15631533 = do i <- getIState

15641534 case runparser mainProg i fname input of

1565− Left err -> do let fc = parseErrorFC err

1535+ Left err -> do let fc = errorExtent err

15661536 i <- getIState

15671537 case idris_outputmode i of

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

1569− IdeMode n h -> iWarn fc (Util.Pretty.text $ parseErrorMessage err)

1539+ IdeMode n h -> iWarn fc (Util.Pretty.text $ errorMessage err)

15701540 putIState (i { errSpan = Just fc })

15711541 return []

15721542 Right (x, i) -> do putIState i

@@ -1576,11 +1546,42 @@ parseProg syn fname input mrk

15761546 mainProg = case mrk of

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

15781548 Just mrk -> do

1579− P.setParserState mrk

1549+ restore mrk

15801550 ds <- prog syn

15811551 i' <- get

15821552 return (ds, i')

15831553

1554+-- | Collect 'PClauses' with the same function name

1555+collect :: [PDecl] -> [PDecl]

1556+collect (c@(PClauses _ o _ _) : ds)

1557+ = clauses (cname c) [] (c : ds)

1558+ where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

1559+ clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

1560+ | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

1561+ clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)

1562+ | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds

1563+ clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

1564+ clauses Nothing acc (x:xs) = collect xs

1565+ clauses Nothing acc [] = []

1566+

1567+ cname :: PDecl -> Maybe Name

1568+ cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

1569+ cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n

1570+ cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

1571+ cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing

1572+ fcOf :: PDecl -> FC

1573+ fcOf (PClauses fc _ _ _) = fc

1574+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

1575+collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds

1576+collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

1577+collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

1578+collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')

1579+ = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

1580+collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')

1581+ = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'

1582+collect (d : ds) = d : collect ds

1583+collect [] = []

1584+

15841585{-| Load idris module and show error if something wrong happens -}

15851586loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

15861587loadModule f phase

@@ -1681,8 +1682,8 @@ loadSource lidr f toline

16811682 ]

16821683 prep = map T.pack . reverse . Spl.splitOn [pathSeparator]

16831684 aliasNames = [ (alias, fc)

1684− | ImportInfo { import_rename = Just (alias, _)

1685− , import_location = fc } <- imports

1685+ | ImportInfo { import_rename = Just (alias, fc)

1686+ } <- imports

16861687 ]

16871688 histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

16881689 case map head . filter ((/= 1) . length) $ histogram of

src/Idris/Parser/Data.hs+42−48

@@ -5,7 +5,8 @@ Description : Parse Data declarations.

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

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

9+ MultiParamTypeClasses, PatternGuards #-}

910module Idris.Parser.Data where

1011

1112import Idris.AbsSyntax

@@ -30,7 +31,8 @@ Record ::=

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

3132-}

3233record :: SyntaxInfo -> IdrisParser PDecl

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

34+record syn = (appExtent $ do

35+ (doc, paramDocs, acc, opts) <- P.try (do

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

3537 ist <- get

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

@@ -40,19 +42,18 @@ record syn = do (doc, paramDocs, acc, opts) <- P.try (do

4042 opts <- dataOpts []

4143 co <- recordI

4244 return (doc', paramDocs', acc, opts ++ co))

43− fc <- getFC

44− (tyn_in, nfc) <- fnName

45+ (tyn_in, nfc) <- withExtent fnName

4546 let tyn = expandNS syn tyn_in

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

4748 syn_namespace syn }

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

49+ params <- P.manyTill (recordParameter rsyn) (keyword "where")

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

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

5152 case cname of

5253 Just cn' -> accData acc tyn (fst cn' : fnames)

5354 Nothing -> return ()

54− return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

55− <?> "record type declaration"

55+ return $ \fc -> PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn)

56+ <?> "record type declaration"

5657 where

5758 getName (Just (n, _), _, _, _) = Just n

5859 getName _ = Nothing

@@ -60,11 +61,10 @@ record syn = do (doc, paramDocs, acc, opts) <- P.try (do

6061 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

6162 recordBody syn tyn = do

6263 ist <- get

63− fc <- getFC

6464

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

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

67− n <- constructor

67+ n <- withExtent constructor

6868 return (Just n, doc))

6969

7070 let constructorDoc' = annotate syn ist constructorDoc

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

7777 fieldLine syn = do

7878 doc <- optional docComment

7979 c <- optional $ lchar '{'

80− let oneName = (do (n, nfc) <- fnName

80+ let oneName = (do (n, nfc) <- withExtent fnName

8181 return $ Just (expandNS syn n, nfc))

8282 <|> (symbol "_" >> return Nothing)

8383 ns <- commaSeparated oneName

@@ -91,9 +91,8 @@ record syn = do (doc, paramDocs, acc, opts) <- P.try (do

9191 Nothing -> Nothing

9292 return $ map (\n -> (n, p, t, doc')) ns

9393

94− constructor :: IdrisParser (Name, FC)

95− constructor = (reservedHL "constructor") *> fnName

96−

94+ constructor :: (Parsing m, MonadState IState m) => m Name

95+ constructor = keyword "constructor" *> fnName

9796

9897 endPlicity :: Maybe Char -> IdrisParser Plicity

9998 endPlicity (Just _) = do lchar '}'

@@ -115,26 +114,25 @@ recordParameter syn =

115114 where

116115 namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)

117116 namedTy syn =

118− do (n, nfc) <- fnName

117+ do (n, nfc) <- withExtent fnName

119118 lchar ':'

120119 ty <- typeExpr (allowImp syn)

121120 return (expandNS syn n, nfc, ty)

122121 onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)

123122 onlyName syn =

124− do (n, nfc) <- fnName

125− fc <- getFC

126− return (expandNS syn n, nfc, PType fc)

123+ do (n, nfc) <- withExtent fnName

124+ return (expandNS syn n, nfc, PType nfc)

127125

128126{- | Parses data declaration type (normal or codata)

129127DataI ::= 'data' | 'codata';

130128-}

131129dataI :: IdrisParser DataOpts

132−dataI = do reservedHL "data"; return []

133− <|> do reservedHL "codata"; return [Codata]

130+dataI = do keyword "data"; return []

131+ <|> do keyword "codata"; return [Codata]

134132

135133recordI :: IdrisParser DataOpts

136−recordI = do reservedHL "record"; return []

137− <|> do reservedHL "corecord"; return [Codata]

134+recordI = do keyword "record"; return []

135+ <|> do keyword "corecord"; return [Codata]

138136

139137{- | Parses if a data should not have a default eliminator

140138DefaultEliminator ::= 'noelim'?

@@ -142,11 +140,11 @@ DefaultEliminator ::= 'noelim'?

142140dataOpts :: DataOpts -> IdrisParser DataOpts

143141dataOpts opts

144142 = do let kw = "%elim"

145− fc <- reservedFC kw

143+ fc <- extent $ reserved kw

146144 warnElim fc kw

147145 dataOpts (DefaultEliminator : DefaultCaseFun : opts)

148146 <|> do let kw = "%case"

149− fc <- reservedFC kw

147+ fc <- extent $ reserved kw

150148 warnElim fc kw

151149 dataOpts (DefaultCaseFun : opts)

152150 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

@@ -185,25 +183,24 @@ data_ syn = (checkDeclFixity $

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

186184 | (n, d) <- argDocs ]

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

188− fc <- getFC

189− (tyn_in, nfc) <- fnName

186+ (tyn_in, nfc) <- withExtent fnName

190187 (do P.try (lchar ':')

191188 ty <- typeExpr (allowImp syn)

192189 let tyn = expandNS syn tyn_in

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

194− reservedHL "where"

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

191+ keyword "where"

195192 cons <- indentedBlock (constructor syn)

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

197− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))

194+ return $ PData doc argDocs syn nfc dataOpts (PDatadecl tyn nfc ty cons))

198195 terminator

199196 return d) <|> (do

200197 args <- many (do notEndApp

201− x <- fst <$> name

198+ x <- name

202199 return x)

203− let ty = bindArgs (map (const (PType fc)) args) (PType fc)

200+ let ty = bindArgs (map (const (PType nfc)) args) (PType nfc)

204201 let tyn = expandNS syn tyn_in

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

206− P.try (lchar '=') <|> do reservedHL "where"

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

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

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

208205 let n = show tyn_in ++ " "

209206 let s = kw ++ n

@@ -215,12 +212,12 @@ data_ syn = (checkDeclFixity $

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

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

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

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

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

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

220217 do let cty = bindArgs cargs conty

221218 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

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

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

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

224221 terminator

225222 return d))

226223 <?> "data type declaration"

@@ -242,12 +239,12 @@ data_ syn = (checkDeclFixity $

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

243240constructor syn

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

245− (cn_in, nfc) <- fnName; fc <- getFC

242+ (cn_in, nfc) <- withExtent fnName

246243 let cn = expandNS syn cn_in

247244 lchar ':'

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

249− P.sepBy1 (fst <$> name) (lchar ','))

250− ty <- typeExpr (allowImp syn)

246+ P.sepBy1 name (lchar ','))

247+ (ty, fc) <- withExtent $ typeExpr (allowImp syn)

251248 ist <- get

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

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

@@ -261,24 +258,23 @@ constructor syn

261258-}

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

263260simpleConstructor syn

264− = do (doc, _) <- P.option noDocs (P.try docComment)

261+ = (appExtent $ do

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

265263 ist <- get

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

267− (cn_in, nfc) <- fnName

265+ (cn_in, nfc) <- withExtent fnName

268266 let cn = expandNS syn cn_in

269− fc <- getFC

270267 args <- many (do notEndApp

271268 simpleExpr syn)

272269 checkNameFixity cn

273− return (doc', [], cn, nfc, args, fc, [])

274− <?> "constructor"

275−

270+ return $ \fc -> (doc', [], cn, nfc, args, fc, []))

271+ <?> "constructor"

276272{- | Parses a dsl block declaration

277273DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

278274 -}

279275dsl :: SyntaxInfo -> IdrisParser PDecl

280−dsl syn = do reservedHL "dsl"

281− n <- fst <$> fnName

276+dsl syn = do keyword "dsl"

277+ n <- fnName

282278 bs <- indentedBlock (overload syn)

283279 let dsl = mkDSL bs (dsl_info syn)

284280 checkDSL dsl

@@ -315,12 +311,10 @@ OverloadIdentifier ::= 'let' | Identifier;

315311Overload ::= OverloadIdentifier '=' Expr;

316312-}

317313overload :: SyntaxInfo -> IdrisParser (String, PTerm)

318−overload syn = do (o, fc) <- identifier <|> do fc <- reservedFC "let"

319− return ("let", fc)

314+overload syn = do o <- highlight AnnKeyword $ identifier <|> "let" <$ reserved "let"

320315 if o `notElem` overloadable

321316 then fail $ show o ++ " is not an overloading"

322317 else do

323− highlightP fc AnnKeyword

324318 lchar '='

325319 t <- expr syn

326320 return (o, t)

src/Idris/Parser/Expr.hs+161−237

@@ -93,10 +93,7 @@ expr' syn = P.try (externalExpr syn)

9393{- | Parses a user-defined expression -}

9494externalExpr :: SyntaxInfo -> IdrisParser PTerm

9595externalExpr syn = do i <- get

96− (FC fn start _) <- getFC

97− expr <- extensions syn (syntaxRulesList $ syntax_rules i)

98− (FC _ _ end) <- getFC

99− let outerFC = FC fn start end

96+ (expr, outerFC@(FC fn _ _)) <- withExtent $ extensions syn (syntaxRulesList $ syntax_rules i)

10097 return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)

10198 <?> "user-defined expression"

10299 where -- Fix non-highlighting FCs by approximating with the span of the syntax application

@@ -151,18 +148,14 @@ extension syn ns rules =

151148 ruleGroup _ _ = False

152149

153150 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

154− extensionSymbol (Keyword n) = do fc <- reservedFC (show n)

155− highlightP fc AnnKeyword

156− return Nothing

151+ extensionSymbol (Keyword n) = Nothing <$ keyword (show n)

157152 extensionSymbol (Expr n) = do tm <- expr syn

158153 return $ Just (n, SynTm tm)

159154 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

160155 return $ Just (n, SynTm tm)

161− extensionSymbol (Binding n) = do (b, fc) <- name

156+ extensionSymbol (Binding n) = do (b, fc) <- withExtent name

162157 return $ Just (n, SynBind fc b)

163− extensionSymbol (Symbol s) = do fc <- symbolFC s

164− highlightP fc AnnKeyword

165− return Nothing

158+ extensionSymbol (Symbol s) = Nothing <$ highlight AnnKeyword (symbol s)

166159

167160 flatten :: PTerm -> PTerm -- flatten application

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

@@ -302,9 +295,7 @@ Impossible ::= 'impossible'

302295@

303296-}

304297impossible :: IdrisParser PTerm

305−impossible = do fc <- reservedFC "impossible"

306− highlightP fc AnnKeyword

307− return PImpossible

298+impossible = PImpossible <$ keyword "impossible"

308299

309300{- | Parses a case expression

310301@

@@ -313,11 +304,10 @@ CaseExpr ::=

313304@

314305-}

315306caseExpr :: SyntaxInfo -> IdrisParser PTerm

316−caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC

317− scr <- expr syn; kw2 <- reservedFC "of";

307+caseExpr syn = do keyword "case"

308+ (scr, fc) <- withExtent $ expr syn

309+ keyword "of"

318310 opts <- indentedBlock1 (caseOption syn)

319− highlightP kw1 AnnKeyword

320− highlightP kw2 AnnKeyword

321311 return (PCase fc scr opts)

322312 <?> "case expression"

323313

@@ -346,9 +336,8 @@ ProofExpr ::=

346336@

347337-}

348338proofExpr :: SyntaxInfo -> IdrisParser PTerm

349−proofExpr syn = do kw <- reservedFC "proof"

339+proofExpr syn = do kw <- extent $ keyword "proof"

350340 ts <- indentedBlock1 (tactic syn)

351− highlightP kw AnnKeyword

352341 warnTacticDeprecation kw

353342 return $ PProof ts

354343 <?> "proof block"

@@ -361,9 +350,8 @@ TacticsExpr :=

361350@

362351-}

363352tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

364−tacticsExpr syn = do kw <- reservedFC "tactics"

353+tacticsExpr syn = do kw <- extent $ keyword "tactics"

365354 ts <- indentedBlock1 (tactic syn)

366− highlightP kw AnnKeyword

367355 warnTacticDeprecation kw

368356 return $ PTactics ts

369357 <?> "tactics block"

@@ -395,40 +383,37 @@ SimpleExpr ::=

395383simpleExpr :: SyntaxInfo -> IdrisParser PTerm

396384simpleExpr syn =

397385 P.try (simpleExternalExpr syn)

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

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

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

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

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

388+ <|> do lchar '%'; fc <- extent $ reserved "implementation"; return (PResolveTC fc)

389+ <|> do lchar '%'; fc <- extent $ reserved "instance"

402390 parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."

403391 return (PResolveTC fc)

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

392+ <|> do reserved "elim_for"; (t, fc) <- withExtent $ fnName; return (PRef fc [] (SN $ ElimN t))

405393 <|> proofExpr syn

406394 <|> tacticsExpr syn

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

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

409− <|> PType <$> reservedFC "Type"

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

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

412− <|> do (c, cfc) <- constant

413− fc <- getFC

414− return (modifyConst syn fc (PConstant cfc c))

415− <|> do symbol "'"; fc <- getFC; str <- fst <$> name

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

396+ <|> do fc <- extent $ reserved "AnyType"; return $ PUniverse fc AllTypes

397+ <|> PType <$> extent (reserved "Type")

398+ <|> do fc <- extent $ reserved "UniqueType"; return $ PUniverse fc UniqueType

399+ <|> do fc <- extent $ reserved "NullType"; return $ PUniverse fc NullType

400+ <|> do (c, cfc) <- withExtent constant

401+ return (modifyConst syn cfc (PConstant cfc c))

402+ <|> do symbol "'"; (str, fc) <- withExtent name

416403 return (PApp fc (PRef fc [] (sUN "Symbol_"))

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

418− <|> do (x, fc) <- fnName

405+ <|> do (x, fc) <- withExtent fnName

419406 if inPattern syn

420407 then P.option (PRef fc [fc] x)

421408 (do reservedOp "@"

422− s <- simpleExpr syn

423− fcIn <- getFC

409+ (s, fcIn) <- withExtent $ simpleExpr syn

424410 return (PAs fcIn x s))

425411 else return (PRef fc [fc] x)

426412 <|> idiom syn

427413 <|> listExpr syn

428414 <|> alt syn

429415 <|> do reservedOp "!"

430− s <- simpleExpr syn

431− fc <- getFC

416+ (s, fc) <- withExtent $ simpleExpr syn

432417 return (PAppBind fc s [])

433418 <|> bracketed (disallowImp syn)

434419 <|> quasiquote syn

@@ -443,8 +428,7 @@ Bracketed ::= '(' Bracketed'

443428@

444429 -}

445430bracketed :: SyntaxInfo -> IdrisParser PTerm

446−bracketed syn = do (FC fn (sl, sc) _) <- getFC

447− lchar '(' <?> "parenthesized expression"

431+bracketed syn = do (FC fn (sl, sc) _) <- extent (lchar '(') <?> "parenthesized expression"

448432 bracketed' (FC fn (sl, sc) (sl, sc+1)) (syn { withAppAllowed = True })

449433

450434{- |Parses the rest of an expression in braces

@@ -461,11 +445,10 @@ Bracketed' ::=

461445-}

462446bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm

463447bracketed' open syn =

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

465− lchar ')'

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

448+ do fc <- extent (addExtent open *> lchar ')')

449+ return $ PTrue fc TypeOrTerm

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

468− <|> P.try (do (opName, fc) <- operatorName

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

469452 guardNotPrefix opName

470453

471454 e <- expr syn

@@ -474,9 +457,8 @@ bracketed' open syn =

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

475458 pexp e]))

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

477− P.try (do (opName, _) <- operatorName

460+ P.try (do (opName, fc) <- withExtent operatorName

478461 lchar ')'

479− fc <- getFC

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

481463 (PApp fc (PRef fc [] opName) [pexp l,

482464 pexp (PRef fc [] (sMN 1000 "ARG"))]))

@@ -508,21 +490,21 @@ dependentPair pun prev openFC syn =

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

509491 where nametypePart = do

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

511− (ln, lnfc) <- name

512− colonFC <- lcharFC ':'

493+ (ln, lnfc) <- withExtent name

494+ colonFC <- extent (lchar ':')

513495 return (ln, lnfc, colonFC)

514496 lty <- expr' syn

515− starsFC <- reservedOpFC "**"

497+ starsFC <- extent $ reservedOp "**"

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

517499 namePart = P.try $ do

518− (ln, lnfc) <- name

519− starsFC <- reservedOpFC "**"

500+ (ln, lnfc) <- withExtent name

501+ starsFC <- extent $ reservedOp "**"

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

521503 exprPart isEnd = do

522504 e <- expr syn

523505 sepFCE <-

524− let stars = (Left <$> reservedOpFC "**")

525− ending = (Right <$> lcharFC ')')

506+ let stars = (Left <$> extent (reservedOp "**"))

507+ ending = (Right <$> extent (lchar ')'))

526508 in if isEnd then ending else stars <|> ending

527509 case sepFCE of

528510 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn

@@ -539,13 +521,13 @@ dependentPair pun prev openFC syn =

539521bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

540522bracketedExpr syn openParenFC e =

541523 do lchar ')'; return e

542− <|> do exprs <- some (do comma <- lcharFC ','

524+ <|> do exprs <- some (do comma <- extent (lchar ',')

543525 r <- expr syn

544526 return (r, comma))

545− closeParenFC <- lcharFC ')'

527+ closeParenFC <- extent (lchar ')')

546528 let hilite = [openParenFC, closeParenFC] ++ map snd exprs

547529 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

548− <|> do starsFC <- reservedOpFC "**"

530+ <|> do starsFC <- extent $ reservedOp "**"

549531 dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn

550532 <?> "end of bracketed expression"

551533 where mergePairs :: [(PTerm, FC)] -> PTerm

@@ -560,7 +542,7 @@ bracketedExpr syn openParenFC e =

560542modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

561543modifyConst syn fc (PConstant inFC (BI x))

562544 | not (inPattern syn)

563− = PConstSugar inFC $ -- wrap in original location for highlighting

545+ = PConstSugar inFC $ -- wrap in original span for highlighting

564546 PAlternative [] FirstSuccess

565547 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

566548 : consts)

@@ -612,10 +594,8 @@ UnifyLog ::=

612594 ;

613595-}

614596unifyLog :: SyntaxInfo -> IdrisParser PTerm

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

616− tm <- simpleExpr syn

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

618− return (PUnifyLog tm)

597+unifyLog syn = do P.try $ highlight AnnKeyword $ lchar '%' *> reserved "unifyLog"

598+ PUnifyLog <$> simpleExpr syn

619599 <?> "unification log expression"

620600

621601{- | Parses a new-style tactics expression

@@ -624,10 +604,8 @@ RunTactics ::=

624604 ;

625605-}

626606runElab :: SyntaxInfo -> IdrisParser PTerm

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

628− fc <- getFC

629− tm <- simpleExpr syn

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

607+runElab syn = do P.try $ highlight AnnKeyword $ lchar '%' *> reserved "runElab"

608+ (tm, fc) <- withExtent $ simpleExpr syn

631609 return $ PRunElab fc tm (syn_namespace syn)

632610 <?> "new-style tactics expression"

633611

@@ -637,10 +615,9 @@ Disamb ::=

637615 ;

638616-}

639617disamb :: SyntaxInfo -> IdrisParser PTerm

640−disamb syn = do kw <- reservedFC "with"

641− ns <- P.sepBy1 (fst <$> name) (lchar ',')

618+disamb syn = do keyword "with"

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

642620 tm <- expr' syn

643− highlightP kw AnnKeyword

644621 return (PDisamb (map tons ns) tm)

645622 <?> "namespace disambiguation expression"

646623 where tons (NS n s) = txt (show n) : s

@@ -671,26 +648,24 @@ MatchApp ::=

671648@

672649-}

673650app :: SyntaxInfo -> IdrisParser PTerm

674−app syn = do f <- simpleExpr syn

675− (do P.try $ reservedOp "<=="

676− fc <- getFC

677− ff <- fst <$> fnName

678− return (PLet fc RigW (sMN 0 "match") NoFC

679− f

680− (PMatchApp fc ff)

681− (PRef fc [] (sMN 0 "match")))

682− <?> "matching application expression") <|>

683− (do fc <- getFC

684− i <- get

685− args <- many (do notEndApp; arg syn)

686− wargs <- if withAppAllowed syn && not (inPattern syn)

687− then many (do notEndApp; reservedOp "|"; expr' syn)

688− else return []

689− case args of

690− [] -> return f

691− _ -> return (withApp fc (flattenFromInt fc f args) wargs))

692− <?> "function application"

693− where

651+app syn = (appExtent $ do

652+ f <- simpleExpr syn

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

654+ ff <- fnName

655+ return (\fc -> (PLet fc RigW (sMN 0 "match") NoFC

656+ f

657+ (PMatchApp fc ff)

658+ (PRef fc [] (sMN 0 "match"))))

659+ <?> "matching application expression") <|>

660+ (do args <- many (do notEndApp; arg syn)

661+ wargs <- if withAppAllowed syn && not (inPattern syn)

662+ then many (do notEndApp; reservedOp "|"; expr' syn)

663+ else return []

664+ case args of

665+ [] -> return $ \fc -> f

666+ _ -> return $ \fc -> (withApp fc (flattenFromInt fc f args) wargs)))

667+ <?> "function application"

668+ where

694669 -- bit of a hack to deal with the situation where we're applying a

695670 -- literal to an argument, which we may want for obscure applications

696671 -- of fromInteger, and this will help disambiguate better.

@@ -732,8 +707,7 @@ ImplicitArg ::=

732707-}

733708implicitArg :: SyntaxInfo -> IdrisParser PArg

734709implicitArg syn = do lchar '{'

735− (n, nfc) <- name

736− fc <- getFC

710+ (n, nfc) <- withExtent name

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

738712 expr syn)

739713 lchar '}'

@@ -760,55 +734,43 @@ constraintArg syn = do symbol "@{"

760734

761735-}

762736quasiquote :: SyntaxInfo -> IdrisParser PTerm

763−quasiquote syn = do startFC <- symbolFC "`("

737+quasiquote syn = (highlight AnnQuasiquote $ do

738+ highlight AnnKeyword $ symbol "`("

764739 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,

765740 inPattern = False }

766741 g <- optional $

767− do fc <- symbolFC ":"

768− ty <- expr syn { inPattern = False } -- don't allow antiquotes

769− return (ty, fc)

770− endFC <- symbolFC ")"

771− mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]

772− case g of

773− Just (_, fc) -> highlightP fc AnnKeyword

774− _ -> return ()

775− return $ PQuasiquote e (fst <$> g)

776− <?> "quasiquotation"

777−

742+ do highlight AnnKeyword $ symbol ":"

743+ expr syn { inPattern = False } -- don't allow antiquotes

744+ highlight AnnKeyword $ symbol ")"

745+ return $ PQuasiquote e g)

746+ <?> "quasiquotation"

778747{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

779748

780749> Unquote ::= ',' Expr

781750

782751-}

783752unquote :: SyntaxInfo -> IdrisParser PTerm

784−unquote syn = do guard (syn_in_quasiquote syn > 0)

785− startFC <- symbolFC "~"

753+unquote syn = (highlight AnnAntiquote $ do

754+ guard (syn_in_quasiquote syn > 0)

755+ highlight AnnKeyword $ symbol "~"

786756 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }

787− endFC <- getFC

788− highlightP startFC AnnKeyword

789− highlightP (spanFC startFC endFC) AnnAntiquote

790− return $ PUnquote e

791− <?> "unquotation"

792−

757+ return $ PUnquote e)

758+ <?> "unquotation"

793759{-| Parses a quotation of a name (for using the elaborator to resolve boring details)

794760

795761> NameQuote ::= '`{' Name '}'

796762

797763-}

798764namequote :: SyntaxInfo -> IdrisParser PTerm

799−namequote syn = do (startFC, res) <-

800− P.try (do fc <- symbolFC "`{{"

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

802− (do fc <- symbolFC "`{"

803− return (fc, True))

804− (n, nfc) <- fnName

805− endFC <- if res then symbolFC "}" else symbolFC "}}"

806− mapM_ (uncurry highlightP)

807− [ (startFC, AnnKeyword)

808− , (endFC, AnnKeyword)

809− , (spanFC startFC endFC, AnnQuasiquote)

810− ]

811− return $ PQuoteName n res nfc

765+namequote syn = highlight AnnQuasiquote ((P.try $ do

766+ highlight AnnKeyword $ symbol "`{{"

767+ (n, nfc) <- withExtent fnName

768+ highlight AnnKeyword $ symbol "}}"

769+ return (PQuoteName n False nfc))

770+ <|> (do highlight AnnKeyword $ symbol "`{"

771+ (n, nfc) <- withExtent fnName

772+ highlight AnnKeyword $ symbol "}"

773+ return (PQuoteName n True nfc)))

812774 <?> "quoted name"

813775

814776

@@ -834,13 +796,13 @@ data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm

834796

835797recordType :: SyntaxInfo -> IdrisParser PTerm

836798recordType syn =

837− do kw <- reservedFC "record"

838− lchar '{'

839− fgs <- fieldGetOrSet

840− lchar '}'

841− fc <- getFC

842− rec <- optional (do notEndApp; simpleExpr syn)

843− highlightP kw AnnKeyword

799+ do ((fgs, rec), fc) <- withExtent $ do

800+ keyword "record"

801+ lchar '{'

802+ fgs <- fieldGetOrSet

803+ lchar '}'

804+ rec <- optional (do notEndApp; simpleExpr syn)

805+ return (fgs, rec)

844806 case fgs of

845807 Left fields ->

846808 case rec of

@@ -868,7 +830,7 @@ recordType syn =

868830 <?> "field setter"

869831

870832 fieldGet :: IdrisParser [Name]

871− fieldGet = P.sepBy1 (fst <$> fnName) (symbol "->")

833+ fieldGet = P.sepBy1 fnName (symbol "->")

872834

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

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

@@ -939,12 +901,10 @@ LambdaTail ::=

939901lambda :: SyntaxInfo -> IdrisParser PTerm

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

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

942− fc <- getFC

943− sc <- lambdaTail

904+ (sc, fc) <- withExtent lambdaTail

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

945906 <|>

946− (do ps <- P.sepBy (do fc <- getFC

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

907+ (do ps <- P.sepBy (do (e, fc) <- withExtent $ simpleExpr (disallowImp (syn { inPattern = True }))

948908 return (fc, e))

949909 (lchar ',')

950910 sc <- lambdaTail

@@ -967,16 +927,13 @@ RewriteTerm ::=

967927@

968928-}

969929rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

970−rewriteTerm syn = do kw <- reservedFC "rewrite"

971− fc <- getFC

972− prf <- expr syn

930+rewriteTerm syn = do keyword "rewrite"

931+ (prf, fc) <- withExtent $ expr syn

973932 giving <- optional (do symbol "==>"; expr' syn)

974933 using <- optional (do reserved "using"

975− (n, _) <- name

934+ n <- name

976935 return n)

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

978− highlightP kw AnnKeyword

979− highlightP kw' AnnKeyword

936+ keyword "in"; sc <- expr syn

980937 return (PRewrite fc using prf sc giving)

981938 <?> "term rewrite expression"

982939

@@ -992,10 +949,9 @@ TypeSig' ::=

992949@

993950 -}

994951let_ :: SyntaxInfo -> IdrisParser PTerm

995−let_ syn = P.try (do kw <- reservedFC "let"

952+let_ syn = P.try (do keyword "let"

996953 ls <- indentedBlock (let_binding syn)

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

998− highlightP kw AnnKeyword; highlightP kw' AnnKeyword

954+ keyword "in"; sc <- expr syn

999955 return (buildLets ls sc))

1000956 <?> "let binding"

1001957 where buildLets [] sc = sc

@@ -1004,8 +960,7 @@ let_ syn = P.try (do kw <- reservedFC "let"

1004960 buildLets ((fc, pat, ty, v, alts) : ls) sc

1005961 = PCase fc v ((pat, buildLets ls sc) : alts)

1006962

1007−let_binding syn = do fc <- getFC;

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

963+let_binding syn = do (pat, fc) <- withExtent $ expr' (syn { inPattern = True })

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

1010965 lchar '='

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

@@ -1022,14 +977,12 @@ If ::= 'if' Expr 'then' Expr 'else' Expr

1022977

1023978-}

1024979if_ :: SyntaxInfo -> IdrisParser PTerm

1025−if_ syn = (do ifFC <- reservedFC "if"

1026− fc <- getFC

1027− c <- expr syn

1028− thenFC <- reservedFC "then"

980+if_ syn = (do keyword "if"

981+ (c, fc) <- withExtent $ expr syn

982+ keyword "then"

1029983 t <- expr syn

1030− elseFC <- reservedFC "else"

984+ keyword "else"

1031985 f <- expr syn

1032− mapM_ (flip highlightP AnnKeyword) [ifFC, thenFC, elseFC]

1033986 return (PIfThenElse fc c t f))

1034987 <?> "conditional expression"

1035988

@@ -1043,13 +996,11 @@ QuoteGoal ::=

1043996@

1044997 -}

1045998quoteGoal :: SyntaxInfo -> IdrisParser PTerm

1046−quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;

1047− kw2 <- reservedFC "by"

999+quoteGoal syn = do keyword "quoteGoal"; n <- name;

1000+ keyword "by"

10481001 r <- expr syn

1049− kw3 <- reservedFC "in"

1050− fc <- getFC

1051− sc <- expr syn

1052− mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]

1002+ keyword "in"

1003+ (sc, fc) <- withExtent $ expr syn

10531004 return (PGoal fc r n sc)

10541005 <?> "quote goal expression"

10551006

@@ -1081,18 +1032,17 @@ explicitPi opts st syn

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

10821033

10831034autoImplicit opts st syn

1084− = do kw <- reservedFC "auto"

1035+ = do keyword "auto"

10851036 when (st == Static) $ fail "auto implicits can not be static"

10861037 xt <- typeDeclList syn

10871038 lchar '}'

10881039 symbol "->"

10891040 sc <- expr (allowConstr syn)

1090− highlightP kw AnnKeyword

10911041 return (bindList (\r -> PPi

10921042 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) r)) xt sc)

10931043

10941044defaultImplicit opts st syn = do

1095− kw <- reservedFC "default"

1045+ keyword "default"

10961046 when (st == Static) $ fail "default implicits can not be static"

10971047 ist <- get

10981048 script' <- simpleExpr syn

@@ -1101,7 +1051,6 @@ defaultImplicit opts st syn = do

11011051 lchar '}'

11021052 symbol "->"

11031053 sc <- expr (allowConstr syn)

1104− highlightP kw AnnKeyword

11051054 return (bindList (\r -> PPi (TacImp [] Dynamic script r)) xt sc)

11061055

11071056normalImplicit opts st syn = do

@@ -1195,7 +1144,7 @@ constraintList1 syn = P.try (do lchar '('

11951144 reservedOp "=>"

11961145 return [(RigW, defname, NoFC, t)])

11971146 <?> "type constraint list"

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

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

11991148 e <- expr (disallowImp syn)

12001149 return (RigW, n, fc, e))

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

@@ -1219,12 +1168,12 @@ FunctionSignatureList ::=

12191168-}

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

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

1222− (x, xfc) <- fnName

1171+ (x, xfc) <- withExtent fnName

12231172 lchar ':'

12241173 t <- typeExpr (disallowImp syn)

12251174 return (rig, x, xfc, t))

12261175 (lchar ','))

1227− <|> do ns <- P.sepBy1 name (lchar ',')

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

12281177 lchar ':'

12291178 t <- typeExpr (disallowImp syn)

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

@@ -1246,16 +1195,15 @@ NameOrPlaceHolder ::= Name | '_';

12461195@

12471196-}

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

1249−tyOptDeclList syn = P.sepBy1 (do (x, fc) <- nameOrPlaceholder

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

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

12511200 expr syn)

12521201 return (RigW, x, fc, t))

12531202 (lchar ',')

12541203 <?> "type declaration list"

1255− where nameOrPlaceholder :: IdrisParser (Name, FC)

1204+ where nameOrPlaceholder :: IdrisParser Name

12561205 nameOrPlaceholder = fnName

1257− <|> do symbol "_"

1258− return (sMN 0 "underscore", NoFC)

1206+ <|> sMN 0 "underscore" <$ reservedOp "_"

12591207 <?> "name or placeholder"

12601208

12611209{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]

@@ -1280,26 +1228,20 @@ ExprList ::=

12801228@

12811229 -}

12821230listExpr :: SyntaxInfo -> IdrisParser PTerm

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

1284− lchar '['; fc <- getFC;

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

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

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

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

1231+listExpr syn = do (FC f (l, c) _) <- extent (lchar '[')

1232+ (do (FC _ _ (l', c')) <- extent (lchar ']') <?> "end of list expression"

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

1234+ <|> (do (x, fc) <- withExtent (expr (syn { withAppAllowed = False })) <?> "expression"

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

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

12911237 lchar ']'

12921238 return (PDoBlock (map addGuard qs ++

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

12941240 [pexp x])]))) <|>

1295− (do xs <- many (do (FC fn (sl, sc) _) <- getFC

1296− lchar ',' <?> "list element"

1297− let commaFC = FC fn (sl, sc) (sl, sc + 1)

1241+ (do xs <- many (do commaFC <- extent (lchar ',') <?> "list element"

12981242 elt <- expr syn

12991243 return (elt, commaFC))

1300− (FC fn (sl, sc) _) <- getFC

1301− lchar ']' <?> "end of list expression"

1302− let rbrackFC = FC fn (sl, sc) (sl, sc+1)

1244+ rbrackFC <- extent (lchar ']') <?> "end of list expression"

13031245 return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))

13041246 <?> "list expression"

13051247 where

@@ -1326,10 +1268,8 @@ DoBlock ::=

13261268 -}

13271269doBlock :: SyntaxInfo -> IdrisParser PTerm

13281270doBlock syn

1329− = do kw <- reservedFC "do"

1330− ds <- indentedBlock1 (do_ syn)

1331− highlightP kw AnnKeyword

1332− return (PDoBlock ds)

1271+ = do keyword "do"

1272+ PDoBlock <$> indentedBlock1 (do_ syn)

13331273 <?> "do block"

13341274

13351275{- | Parses an expression inside a do block

@@ -1346,45 +1286,35 @@ Do ::=

13461286-}

13471287do_ :: SyntaxInfo -> IdrisParser PDo

13481288do_ syn

1349− = P.try (do kw <- reservedFC "let"

1350− (i, ifc) <- name

1289+ = P.try (do keyword "let"

1290+ (i, ifc) <- withExtent name

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

13521292 expr' syn)

13531293 reservedOp "="

1354− fc <- getFC

1355− e <- expr syn

1356− highlightP kw AnnKeyword

1294+ (e, fc) <- withExtent $ expr syn

13571295 return (DoLet fc RigW i ifc ty e))

1358− <|> P.try (do kw <- reservedFC "let"

1296+ <|> P.try (do keyword "let"

13591297 i <- expr' syn

13601298 reservedOp "="

1361− fc <- getFC

1362− sc <- expr syn

1363− highlightP kw AnnKeyword

1299+ (sc, fc) <- withExtent $ expr syn

13641300 return (DoLetP fc i sc))

1365− <|> P.try (do kw <- reservedFC "rewrite"

1366− fc <- getFC

1367− sc <- expr syn

1368− highlightP kw AnnKeyword

1301+ <|> P.try (do (sc, fc) <- withExtent (keyword "rewrite" *> expr syn)

13691302 return (DoRewrite fc sc))

1370− <|> P.try (do (i, ifc) <- name

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

13711304 symbol "<-"

1372− fc <- getFC

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

1305+ (e, fc) <- withExtent $ expr (syn { withAppAllowed = False });

13741306 P.option (DoBind fc i ifc e)

13751307 (do lchar '|'

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

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

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

13791311 symbol "<-"

1380− fc <- getFC

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

1312+ (e, fc) <- withExtent $ expr (syn { withAppAllowed = False });

13821313 P.option (DoBindP fc i e [])

13831314 (do lchar '|'

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

13851316 return (DoBindP fc i e ts)))

1386− <|> do e <- expr syn

1387− fc <- getFC

1317+ <|> do (e, fc) <- withExtent $ expr syn

13881318 return (DoExp fc e)

13891319 <?> "do block expression"

13901320

@@ -1402,8 +1332,7 @@ Idiom ::= '[|' Expr '|]';

14021332idiom :: SyntaxInfo -> IdrisParser PTerm

14031333idiom syn

14041334 = do symbol "[|"

1405− fc <- getFC

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

1335+ (e, fc) <- withExtent $ expr (syn { withAppAllowed = False })

14071336 symbol "|]"

14081337 return (PIdiom fc e)

14091338 <?> "expression in idiom brackets"

@@ -1446,16 +1375,14 @@ constants =

14461375 ]

14471376

14481377-- | Parse a constant and its source span

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

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

1451− | (name, ty) <- constants

1452− ]

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

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

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

1456− <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1457− <|> do (c, fc) <- P.try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1458− <?> "constant or literal"

1378+constant :: Parsing m => m Idris.Core.TT.Const

1379+constant = P.choice [ ty <$ reserved name | (name, ty) <- constants ]

1380+ <|> P.try (Fl <$> float)

1381+ <|> BI <$> natural

1382+ <|> Str <$> verbatimStringLiteral

1383+ <|> Str <$> stringLiteral

1384+ <|> P.try (Ch <$> charLiteral) --Currently ambigous with symbols

1385+ <?> "constant or literal"

14591386

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

14611388

@@ -1465,13 +1392,11 @@ VerbatimString_t ::=

14651392;

14661393@

14671394 -}

1468−verbatimStringLiteral :: IdrisParser (String, FC)

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

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

1395+verbatimStringLiteral :: Parsing m => m String

1396+verbatimStringLiteral = token $ do P.try $ string "\"\"\""

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

14721398 moreQuotes <- P.many $ P.char '"'

1473− (FC _ _ end) <- getFC

1474− return (str ++ moreQuotes, FC f start end)

1399+ return $ str ++ moreQuotes

14751400

14761401{- | Parses a static modifier

14771402

@@ -1482,9 +1407,8 @@ Static ::=

14821407@

14831408-}

14841409static :: IdrisParser Static

1485−static = do reserved "%static"; return Static

1486− <|> do reserved "[static]"

1487− fc <- getFC

1410+static = Static <$ reserved "%static"

1411+ <|> do fc <- extent $ reserved "[static]"

14881412 parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")

14891413 return Static

14901414 <|> return Dynamic

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

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

15431467tactics =

15441468 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1545− do ns <- P.sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1469+ do ns <- P.sepBy (spaced name) (lchar ','); return $ Intro ns)

15461470 , noArgs ["intros"] Intros

15471471 , noArgs ["unfocus"] Unfocus

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

1549− do n <- spaced (fst <$> fnName)

1473+ do n <- spaced fnName

15501474 imps <- many imp

15511475 return $ Refine n imps)

15521476 , (["claim"], Nothing, \syn ->

1553− do n <- indentGt *> (fst <$> name)

1477+ do n <- indentGt *> name

15541478 goal <- indentGt *> expr syn

15551479 return $ Claim n goal)

15561480 , (["mrefine"], Just ExprTArg, const $

1557− do n <- spaced (fst <$> fnName)

1481+ do n <- spaced fnName

15581482 return $ MatchRefine n)

15591483 , expressionTactic ["rewrite"] Rewrite

15601484 , expressionTactic ["case"] CaseTac

15611485 , expressionTactic ["induction"] Induction

15621486 , expressionTactic ["equiv"] Equiv

15631487 , (["let"], Nothing, \syn -> -- FIXME syntax for let

1564− do n <- (indentGt *> (fst <$> name))

1488+ do n <- (indentGt *> name)

15651489 (do indentGt *> lchar ':'

15661490 ty <- indentGt *> expr' syn

15671491 indentGt *> lchar '='

@@ -1574,7 +1498,7 @@ tactics =

15741498 return $ LetTac n (desugar syn i t)))

15751499

15761500 , (["focus"], Just ExprTArg, const $

1577− do n <- spaced (fst <$> name)

1501+ do n <- spaced name

15781502 return $ Focus n)

15791503 , expressionTactic ["exact"] Exact

15801504 , expressionTactic ["applyTactic"] ApplyTactic

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

15901514 , noArgs ["trivial"] Trivial

15911515 , noArgs ["unify"] DoUnify

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

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

1517+ do depth <- P.option 10 natural

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

15951519 , noArgs ["implementation"] TCImplementation

15961520 , noArgs ["solve"] Solve

@@ -1606,11 +1530,11 @@ tactics =

16061530 , expressionTactic [":t", ":type"] TCheck

16071531 , expressionTactic [":search"] TSearch

16081532 , (["fail"], Just StringLitTArg, const $

1609− do msg <- fst <$> stringLiteral

1533+ do msg <- stringLiteral

16101534 return $ TFail [Idris.Core.TT.TextPart msg])

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

16121536 do whiteSpace

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

1537+ doc <- (Right <$> constant) <|> (Left <$> fnName)

16141538 P.eof

16151539 return (TDocStr doc))

16161540 ]

src/Idris/Parser/Helpers.hs+132−223

@@ -5,8 +5,69 @@ Description : Utilities for Idris' parser.

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9−module Idris.Parser.Helpers where

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

9+module Idris.Parser.Helpers

10+ ( module Idris.Parser.Stack

11+ -- * The parser

12+ , IdrisParser

13+ , parseErrorDoc

14+ -- * Space

15+ , whiteSpace

16+ , someSpace

17+ , eol

18+ , isEol

19+ -- * Basic parsers

20+ , char

21+ , symbol

22+ , string

23+ , lookAheadMatches

24+ -- * Terminals

25+ , lchar

26+ , reserved

27+ , docComment

28+ , token

29+ , natural

30+ , charLiteral

31+ , stringLiteral

32+ , float

33+ -- * Names

34+ , bindList

35+ , maybeWithNS

36+ , iName

37+ , name

38+ , identifier

39+ , packageName

40+ -- * Access

41+ , accessibility

42+ , accData

43+ , addAcc

44+ -- * Warnings and errors

45+ , fixErrorMsg

46+ , parserWarning

47+ , clearParserWarnings

48+ , reportParserWarnings

49+ -- * Highlighting

50+ , highlight

51+ , keyword

52+ -- * Indentation

53+ , pushIndent

54+ , popIndent

55+ , indentGt

56+ , notOpenBraces

57+ -- * Indented blocks

58+ , openBlock

59+ , closeBlock

60+ , terminator

61+ , notEndBlock

62+ , indentedBlock

63+ , indentedBlock1

64+ , indentedBlockS

65+ , indented

66+ -- * Miscellaneous

67+ , notEndApp

68+ , commaSeparated

69+ )

70+where

1071

1172import Idris.AbsSyntax

1273import Idris.Core.Evaluate

@@ -15,6 +76,7 @@ import Idris.Delaborate (pprintErr)

1576import Idris.Docstrings

1677import Idris.Options

1778import Idris.Output (iWarn)

79+import Idris.Parser.Stack

1880

1981import Prelude hiding (pi)

2082

@@ -28,8 +90,6 @@ import qualified Data.List.NonEmpty as NonEmpty

2890import qualified Data.Map as M

2991import Data.Maybe

3092import qualified Data.Text as T

31−import Data.Void (Void(..))

32−import System.FilePath

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

3494import qualified Text.Megaparsec as P

3595import qualified Text.Megaparsec.Char as P

@@ -38,62 +98,26 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP

3898

3999

40100-- | Idris parser with state used during parsing

41−type IdrisParser = StateT IState IdrisInnerParser

42−type IdrisInnerParser = P.Parsec Void String

43−type ParseState = P.State String

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

45−

46−parseErrorPretty :: ParseError -> String

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

101+type IdrisParser = Parser IState

48102

49103parseErrorDoc :: ParseError -> PP.Doc

50−parseErrorDoc = PP.string . parseErrorPretty

51−

52−parseErrorFC :: ParseError -> FC

53−parseErrorFC (ParseError _ err) = sourcePositionFC pos

54− where

55− (pos NonEmpty.:| _) = P.errorPos err

56−

57−parseErrorMessage :: ParseError -> String

58−parseErrorMessage (ParseError _ err) = P.parseErrorTextPretty err

104+parseErrorDoc = PP.string . prettyError

59105

106+someSpace :: Parsing m => m ()

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

60108

61−-- | Generalized monadic parsing constraint type

62−type MonadicParsing m = (P.MonadParsec Void String m)

109+token :: Parsing m => m a -> m a

110+token p = trackExtent p <* whiteSpace

63111

64−someSpace :: MonadicParsing m => m ()

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

112+highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

113+highlight annot p = do

114+ (result, fc) <- withExtent p

115+ modify $ \ist -> ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist }

116+ return result

66117

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

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

69− -- See Issue #1594

70− r <- p

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

72− whiteSpace

73− return (r, FC fn (sl, sc) (el, ec))

74−

75−token :: MonadicParsing m => m a -> m a

76−token p = p <* whiteSpace

77−

78−-- | Helper to run Idris inner parser based stateT parsers

79−runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res

80−runparser p i inputname s =

81− case P.parse (evalStateT p i) inputname s of

82− Left err -> Left $ ParseError s err

83− Right v -> Right v

84−

85−

86−highlightP :: FC -> OutputAnnotation -> IdrisParser ()

87−highlightP fc annot = do ist <- get

88− put ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist}

89−

90−noDocCommentHere :: String -> IdrisParser ()

91−noDocCommentHere msg =

92− optional (do fc <- getFC

93− docComment

94− ist <- get

95− put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

96− pure ()

118+-- | Parse a reserved identfier, highlighting it as a keyword

119+keyword :: (Parsing m, MonadState IState m) => String -> m ()

120+keyword str = highlight AnnKeyword (reserved str)

97121

98122clearParserWarnings :: Idris ()

99123clearParserWarnings = do ist <- getIState

@@ -120,7 +144,7 @@ parserWarning fc warnOpt warnErr = do

120144{- * Space, comments and literals (token/lexing like parsers) -}

121145

122146-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

123−simpleWhiteSpace :: MonadicParsing m => m ()

147+simpleWhiteSpace :: Parsing m => m ()

124148simpleWhiteSpace = () <$ P.satisfy isSpace

125149

126150-- | Checks if a charcter is end of line

@@ -129,7 +153,7 @@ isEol '\n' = True

129153isEol _ = False

130154

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

132−eol :: MonadicParsing m => m ()

156+eol :: Parsing m => m ()

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

134158

135159{- | Consumes a single-line comment

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

138162 SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;

139163@

140164 -}

141−singleLineComment :: MonadicParsing m => m ()

165+singleLineComment :: Parsing m => m ()

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

143167

144168{- | Consumes a multi-line comment

@@ -158,10 +182,10 @@ singleLineComment = P.hidden (() <$ string "--" *> many (P.satisfy (not . isEol)

158182 ;

159183@

160184-}

161−multiLineComment :: MonadicParsing m => m ()

185+multiLineComment :: Parsing m => m ()

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

163187 <|> string "{-" *> inCommentChars

164− where inCommentChars :: MonadicParsing m => m ()

188+ where inCommentChars :: Parsing m => m ()

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

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

167191 <|> string "|||" *> many (P.satisfy (not . isEol)) *> eol *> inCommentChars

@@ -188,7 +212,7 @@ docComment = do dc <- pushIndent *> docCommentLine

188212 return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),

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

190214

191− where docCommentLine :: MonadicParsing m => m String

215+ where docCommentLine :: Parsing m => m String

192216 docCommentLine = P.hidden $ P.try $ do

193217 string "|||"

194218 many (P.satisfy (==' '))

@@ -203,33 +227,33 @@ docComment = do dc <- pushIndent *> docCommentLine

203227 P.many (P.satisfy isSpace)

204228 P.char '@'

205229 P.many (P.satisfy isSpace)

206− n <- fst <$> name

230+ n <- name

207231 P.many (P.satisfy isSpace)

208232 docs <- P.many (P.satisfy (not . isEol))

209233 P.eol ; someSpace

210234 return (n, docs)

211235

212236-- | Parses some white space

213−whiteSpace :: MonadicParsing m => m ()

237+whiteSpace :: Parsing m => m ()

214238whiteSpace = someSpace <|> pure ()

215239

216240-- | Parses a string literal

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

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

241+stringLiteral :: Parsing m => m String

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

219243

220244-- | Parses a char literal

221−charLiteral :: IdrisParser (Char, FC)

222−charLiteral = tokenFC . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''

245+charLiteral :: Parsing m => m Char

246+charLiteral = token . P.try $ P.char '\'' *> P.charLiteral <* P.char '\''

223247

224248-- | Parses a natural number

225−natural :: IdrisParser (Integer, FC)

226−natural = tokenFC ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)

227− <|> P.try (P.char '0' *> P.char' 'o' *> P.octal)

228− <|> P.try P.decimal)

249+natural :: Parsing m => m Integer

250+natural = token ( P.try (P.char '0' *> P.char' 'x' *> P.hexadecimal)

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

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

229253

230254-- | Parses a floating point number

231−float :: IdrisParser (Double, FC)

232−float = tokenFC . P.try $ P.float

255+float :: Parsing m => m Double

256+float = token . P.try $ P.float

233257

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

235259

@@ -244,106 +268,67 @@ reservedIdentifiers = HS.fromList

244268 , "rewrite", "syntax", "then", "total", "using", "where", "with"

245269 ]

246270

247−identifierOrReserved :: MonadicParsing m => m String

271+identifierOrReserved :: Parsing m => m String

248272identifierOrReserved = token $ P.try $ do

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

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

251275 return $ c : cs

252276

253−char :: MonadicParsing m => Char -> m Char

277+char :: Parsing m => Char -> m Char

254278char = P.char

255279

256−string :: MonadicParsing m => String -> m String

280+string :: Parsing m => String -> m String

257281string = P.string

258282

259283-- | Parses a character as a token

260−lchar :: MonadicParsing m => Char -> m Char

284+lchar :: Parsing m => Char -> m Char

261285lchar = token . P.char

262286

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

264−lcharFC :: MonadicParsing m => Char -> m FC

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

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

267− return $ FC file (l, c) (l, c+1)

268−

269−symbol :: MonadicParsing m => String -> m ()

270−symbol = void . P.symbol someSpace

271−

272−symbolFC :: MonadicParsing m => String -> m FC

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

274− symbol str

275− return $ FC file (l, c) (l, c + length str)

287+symbol :: Parsing m => String -> m ()

288+symbol = void . token . P.string

276289

277290-- | Parses a reserved identifier

278−reserved :: MonadicParsing m => String -> m ()

291+reserved :: Parsing m => String -> m ()

279292reserved name = token $ P.try $ do

280293 P.string name

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

282295

283−-- | Parses a reserved identifier, computing its span. Assumes that

284−-- reserved identifiers never contain line breaks.

285−reservedFC :: MonadicParsing m => String -> m FC

286−reservedFC str = do (FC file (l, c) _) <- getFC

287− reserved str

288− return $ FC file (l, c) (l, c + length str)

289−

290−-- | Parse a reserved identfier, highlighting its span as a keyword

291−reservedHL :: String -> IdrisParser ()

292−reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

293−

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

295−-- | Parses a reserved operator

296−reservedOp :: MonadicParsing m => String -> m ()

297−reservedOp name = token $ P.try $

298− do string name

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

300−

301−reservedOpFC :: MonadicParsing m => String -> m FC

302−reservedOpFC name = do (FC f (l, c) _) <- getFC

303− reservedOp name

304− return (FC f (l, c) (l, c + length name))

305−

306296-- | Parses an identifier as a token

307−identifier :: (MonadicParsing m) => m (String, FC)

297+identifier :: Parsing m => m String

308298identifier = P.try $ do

309− (FC f (l, c) _) <- getFC

310299 ident <- identifierOrReserved

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

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

313− return (ident, FC f (l, c) (l, c + length ident))

302+ return ident

314303

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

316−iName :: (MonadicParsing m) => [String] -> m (Name, FC)

317−iName bad = maybeWithNS identifier False bad <?> "name"

305+iName :: Parsing m => [String] -> m Name

306+iName bad = maybeWithNS identifier bad <?> "name"

318307

319308-- | Parses an string possibly prefixed by a namespace

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

321−maybeWithNS parser ascend bad = do

322− fc <- getFC

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

309+maybeWithNS :: Parsing m => m String -> [String] -> m Name

310+maybeWithNS parser bad = do

311+ i <- P.option "" (P.lookAhead identifier)

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

325− let transf = if ascend then id else reverse

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

327− return (mkName (x, xs), fc)

328− where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

329− parserNoNS parser = do startFC <- getFC

330− (x, nameFC) <- parser

331− return (x, "", spanFC startFC nameFC)

332− parserNS :: MonadicParsing m => m (String, FC) -> String -> m (String, String, FC)

333− parserNS parser ns = do startFC <- getFC

334− xs <- string ns

335− lchar '.'; (x, nameFC) <- parser

336− return (x, xs, spanFC startFC nameFC)

337− parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

313+ mkName <$> P.choice (reverse (parserNoNS parser : parsersNS parser i))

314+ where parserNoNS :: Parsing m => m String -> m (String, String)

315+ parserNoNS = fmap (\x -> (x, ""))

316+ parserNS :: Parsing m => m String -> String -> m (String, String)

317+ parserNS parser ns = do xs <- trackExtent (string ns)

318+ lchar '.'

319+ x <- parser

320+ return (x, xs)

321+ parsersNS :: Parsing m => m String -> String -> [m (String, String)]

338322 parsersNS parser i = [P.try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

339323

340324-- | Parses a name

341−name :: IdrisParser (Name, FC)

342−name = (<?> "name") $ do

325+name :: (Parsing m, MonadState IState m) => m Name

326+name = do

343327 keywords <- syntax_keywords <$> get

344328 aliases <- module_aliases <$> get

345− (n, fc) <- iName keywords

346− return (unalias aliases n, fc)

329+ n <- iName keywords

330+ return (unalias aliases n)

331+ <?> "name"

347332 where

348333 unalias :: M.Map [T.Text] [T.Text] -> Name -> Name

349334 unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'

@@ -370,57 +355,14 @@ mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))

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

371356 (x, '.':y) -> x : parseNS y

372357

373−opChars :: String

374−opChars = ":!#$%&*+./<=>?@\\^|-~"

375−

376−operatorLetter :: MonadicParsing m => m Char

377−operatorLetter = P.oneOf opChars

378−

379358-- | Parse a package name

380−packageName :: MonadicParsing m => m String

359+packageName :: Parsing m => m String

381360packageName = (:) <$> P.oneOf firstChars <*> many (P.oneOf remChars)

382361 where firstChars = ['a'..'z'] ++ ['A'..'Z']

383362 remChars = ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['-','_']

384363

385−commentMarkers :: [String]

386−commentMarkers = [ "--", "|||" ]

387−

388−invalidOperators :: [String]

389−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]

390−

391−-- | Parses an operator

392−symbolicOperator :: MonadicParsing m => m String

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

394− when (op `elem` (invalidOperators ++ commentMarkers)) $

395− fail $ op ++ " is not a valid operator"

396− return op

397−

398−-- | Parses an operator

399−symbolicOperatorFC :: MonadicParsing m => m (String, FC)

400−symbolicOperatorFC = do (FC f (l, c) _) <- getFC

401− op <- symbolicOperator

402− return (op, FC f (l, c) (l, c + length op))

403−

404364{- * Position helpers -}

405365

406−sourcePositionFC :: P.SourcePos -> FC

407−sourcePositionFC (P.SourcePos name line column) =

408− -- TODO: Change to actual spanning

409− -- Issue #1594 on the Issue Tracker.

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

411− FC f (lineNumber, columnNumber) (lineNumber, columnNumber)

412− where

413− lineNumber = P.unPos line

414− columnNumber = P.unPos column

415− (dir, file) = splitFileName name

416− f = if dir == addTrailingPathSeparator "."

417− then file

418− else name

419−

420−{- | Get file position as FC -}

421−getFC :: MonadicParsing m => m FC

422−getFC = sourcePositionFC <$> P.getPosition

423−

424366{-* Syntax helpers-}

425367-- | Bind constraints to term

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

@@ -429,7 +371,7 @@ bindList b ((r, n, fc, t):bs) sc = b r n fc t (bindList b bs sc)

429371

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

431373 separated by commas and optional whitespace. -}

432−commaSeparated :: MonadicParsing m => m a -> m [a]

374+commaSeparated :: Parsing m => m a -> m [a]

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

434376

435377{- * Layout helpers -}

@@ -449,11 +391,11 @@ popIndent = do ist <- get

449391

450392

451393-- | Gets current indentation

452−indent :: MonadicParsing m => m Int

394+indent :: Parsing m => m Int

453395indent = P.unPos . P.sourceColumn <$> P.getPosition

454396

455397-- | Gets last indentation

456−lastIndent :: IdrisParser Int

398+lastIndent :: (MonadState IState m) => m Int

457399lastIndent = do ist <- get

458400 case indent_stack ist of

459401 (x : xs) -> return x

@@ -492,7 +434,7 @@ indentedBlockS p = do openBlock

492434

493435

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

495−lookAheadMatches :: MonadicParsing m => m a -> m Bool

437+lookAheadMatches :: Parsing m => m a -> m Bool

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

497439

498440-- | Parses a start of block

@@ -563,7 +505,7 @@ notEndBlock = do ist <- get

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

564506 _ -> return ()

565507

566−indentGt :: IdrisParser ()

508+indentGt :: (Parsing m, MonadState IState m) => m ()

567509indentGt = do

568510 li <- lastIndent

569511 i <- indent

@@ -579,20 +521,18 @@ notOpenBraces = do ist <- get

579521{- | Parses an accessibilty modifier (e.g. public, private) -}

580522accessibility' :: IdrisParser Accessibility

581523accessibility'

582− = do reserved "public";

524+ = do fc <- extent $ reserved "public"

583525 gotexp <- optional (reserved "export")

584526 case gotexp of

585527 Just _ -> return ()

586528 Nothing -> do

587529 ist <- get

588− fc <- getFC

589530 put ist { parserWarnings =

590531 (fc, Msg "'public' is deprecated. Use 'public export' instead.")

591532 : parserWarnings ist }

592533 return Public

593− <|> do reserved "abstract";

534+ <|> do fc <- extent $ reserved "abstract"

594535 ist <- get

595− fc <- getFC

596536 put ist { parserWarnings =

597537 (fc, Msg "The 'abstract' keyword is deprecated. Use 'export' instead.")

598538 : parserWarnings ist }

@@ -626,34 +566,3 @@ accData a n ns = do addAcc n a

626566{- | Error message with possible fixes list -}

627567fixErrorMsg :: String -> [String] -> String

628568fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)

629−

630−-- | Collect 'PClauses' with the same function name

631−collect :: [PDecl] -> [PDecl]

632−collect (c@(PClauses _ o _ _) : ds)

633− = clauses (cname c) [] (c : ds)

634− where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

635− clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

636− | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

637− clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)

638− | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds

639− clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

640− clauses Nothing acc (x:xs) = collect xs

641− clauses Nothing acc [] = []

642−

643− cname :: PDecl -> Maybe Name

644− cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

645− cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n

646− cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

647− cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing

648− fcOf :: PDecl -> FC

649− fcOf (PClauses fc _ _ _) = fc

650−collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

651−collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds

652−collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

653−collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

654−collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')

655− = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

656−collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')

657− = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'

658−collect (d : ds) = d : collect ds

659−collect [] = []

src/Idris/Parser/Ops.hs+45−25

@@ -6,7 +6,7 @@ License : BSD3

66Maintainer : The Idris Community.

77-}

88{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,

9− PatternGuards #-}

9+ MultiParamTypeClasses, PatternGuards #-}

1010module Idris.Parser.Ops where

1111

1212import Idris.AbsSyntax

@@ -16,7 +16,6 @@ import Idris.Parser.Helpers

1616import Prelude hiding (pi)

1717

1818import Control.Applicative

19−import Control.Arrow (first)

2019import Control.Monad

2120import Control.Monad.State.Strict

2221import Data.Char (isAlpha)

@@ -24,6 +23,7 @@ import Data.List

2423import Data.List.NonEmpty (fromList)

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

2625import qualified Text.Megaparsec as P

26+import qualified Text.Megaparsec.Char as P

2727import qualified Text.Megaparsec.Expr as P

2828

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

@@ -43,7 +43,7 @@ table fixes

4343

4444 noFixityBacktickOperator :: P.Operator IdrisParser PTerm

4545 noFixityBacktickOperator = P.InfixN $ do

46− (n, fc) <- backtickOperator

46+ (n, fc) <- withExtent backtickOperator

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

4848

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

@@ -73,19 +73,18 @@ table fixes

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

7474 binary name ctor f

7575 | isBacktick name = ctor $ P.try $ do

76− (n, fc) <- backtickOperator

76+ (n, fc) <- withExtent backtickOperator

7777 guard $ show (nsroot n) == name

7878 return $ f fc n

7979 | otherwise = ctor $ do

8080 indentGt

81− fc <- reservedOpFC name

81+ fc <- extent $ reservedOp name

8282 indentGt

8383 return $ f fc (sUN name)

8484

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

8686 prefix name f = P.Prefix $ do

87− reservedOp name

88− fc <- getFC

87+ fc <- extent $ reservedOp name

8988 indentGt

9089 return (f fc)

9190

@@ -97,7 +96,7 @@ table fixes

9796 ;

9897@

9998-}

100−backtickOperator :: IdrisParser (Name, FC)

99+backtickOperator :: (Parsing m, MonadState IState m) => m Name

101100backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name

102101

103102{- | Parses an operator name (either a symbolic name or a backtick-quoted name)

@@ -109,8 +108,8 @@ backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') nam

109108 ;

110109@

111110-}

112−operatorName :: IdrisParser (Name, FC)

113−operatorName = first sUN <$> symbolicOperatorFC

111+operatorName :: (Parsing m, MonadState IState m) => m Name

112+operatorName = sUN <$> symbolicOperator

114113 <|> backtickOperator

115114

116115{- | Parses an operator in function position i.e. enclosed by `()', with an

@@ -124,15 +123,9 @@ operatorName = first sUN <$> symbolicOperatorFC

124123@

125124

126125-}

127−operatorFront :: IdrisParser (Name, FC)

128−operatorFront = P.try (do (FC f (l, c) _) <- getFC

129− op <- lchar '(' *> reservedOp "=" <* lchar ')'

130− return (eqTy, FC f (l, c) (l, c+3)))

131− <|> maybeWithNS (do (FC f (l, c) _) <- getFC

132− op <- lchar '(' *> symbolicOperator

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

134− lchar ')'

135− return (op, (FC f (l, c) (l', c' + 1)))) False []

126+operatorFront :: Parsing m => m Name

127+operatorFront = do P.try $ lchar '(' *> (eqTy <$ reservedOp "=") <* lchar ')'

128+ <|> maybeWithNS (lchar '(' *> symbolicOperator <* lchar ')') []

136129

137130{- | Parses a function (either normal name or operator)

138131

@@ -140,7 +133,7 @@ operatorFront = P.try (do (FC f (l, c) _) <- getFC

140133 FnName ::= Name | OperatorFront;

141134@

142135-}

143−fnName :: IdrisParser (Name, FC)

136+fnName :: (Parsing m, MonadState IState m) => m Name

144137fnName = P.try operatorFront <|> name <?> "function name"

145138

146139{- | Parses a fixity declaration

@@ -151,10 +144,12 @@ Fixity ::=

151144@

152145-}

153146fixity :: IdrisParser PDecl

154−fixity = do pushIndent

155− f <- fixityType; i <- fst <$> natural;

156− ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')

157− terminator

147+fixity = do ((f, i, ops), fc) <- withExtent $ do

148+ pushIndent

149+ f <- fixityType; i <- natural

150+ ops <- P.sepBy1 (show . nsroot <$> operatorName) (lchar ',')

151+ terminator

152+ return (f, i, ops)

158153 let prec = fromInteger i

159154 istate <- get

160155 let infixes = idris_infixes istate

@@ -165,7 +160,6 @@ fixity = do pushIndent

165160 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)

166161 , ibc_write = map IBCFix fs ++ ibc_write istate

167162 })

168− fc <- getFC

169163 return (PFix fc (f prec) ops)

170164 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""

171165 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill

@@ -219,3 +213,29 @@ fixityType = do reserved "infixl"; return Infixl

219213 <|> do reserved "infix"; return InfixN

220214 <|> do reserved "prefix"; return PrefixN

221215 <?> "fixity type"

216+

217+opChars :: String

218+opChars = ":!#$%&*+./<=>?@\\^|-~"

219+

220+operatorLetter :: Parsing m => m Char

221+operatorLetter = P.oneOf opChars

222+

223+commentMarkers :: [String]

224+commentMarkers = [ "--", "|||" ]

225+

226+invalidOperators :: [String]

227+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]

228+

229+-- | Parses an operator

230+symbolicOperator :: Parsing m => m String

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

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

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

234+ return op

235+

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

237+-- | Parses a reserved operator

238+reservedOp :: Parsing m => String -> m ()

239+reservedOp name = token $ P.try $

240+ do string name

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

src/Idris/Parser/Stack.hsnew file+139

@@ -0,0 +1,139 @@

1+{-|

2+Module : Idris.Parser.Stack

3+Description : Idris parser stack and its primitives.

4+

5+License : BSD3

6+Maintainer : The Idris Community.

7+-}

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

9+module Idris.Parser.Stack

10+ ( -- * Parsing

11+ Parser(..)

12+ , Parsing(..)

13+ , runparser

14+ -- * Parse errors

15+ , ParseError

16+ , errorExtent

17+ , errorMessage

18+ , prettyError

19+ -- * Mark and restore

20+ , Mark

21+ , mark

22+ , restore

23+

24+ -- * Tracking the extent of productions

25+ --

26+ -- The parser stack automatically builds up the extent of any parse from

27+ -- the extents of sub-parsers wrapped with @trackExtent@.

28+ , getFC

29+ , addExtent

30+ , trackExtent

31+ , extent

32+ , withExtent

33+ , appExtent

34+ )

35+where

36+

37+import Idris.Core.TT (FC(..))

38+

39+import Control.Arrow (app)

40+import Control.Monad.State.Strict (StateT(..), evalStateT)

41+import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,

42+ runWriterT, tell)

43+import qualified Data.List.NonEmpty as NonEmpty

44+import Data.Void (Void(..))

45+import System.FilePath (addTrailingPathSeparator, splitFileName)

46+import qualified Text.Megaparsec as P

47+

48+{- * Parsing -}

49+

50+-- | Our parser stack with state of type @s@

51+type Parser s = StateT s (WriterT FC (P.Parsec Void String))

52+

53+-- | A constraint for parsing without state

54+type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)

55+

56+-- | Run the Idris parser stack

57+runparser :: Parser st res -> st -> String -> String -> Either ParseError res

58+runparser p i inputname s =

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

60+ Left err -> Left $ ParseError s err

61+ Right v -> Right $ fst v

62+

63+{- * Parse errors -}

64+

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

66+

67+-- | Retrieve a parse error's FC

68+errorExtent :: ParseError -> FC

69+errorExtent (ParseError _ err) = sourcePositionFC pos

70+ where

71+ (pos NonEmpty.:| _) = P.errorPos err

72+

73+-- | A single-line parse error message, including location.

74+errorMessage :: ParseError -> String

75+errorMessage (ParseError _ err) = P.parseErrorTextPretty err

76+

77+-- | A fully formatted parse error, with caret and bar, etc.

78+prettyError :: ParseError -> String

79+prettyError (ParseError s err) = P.parseErrorPretty' s err

80+

81+{- * Mark and restore -}

82+

83+type Mark = P.State String

84+

85+-- | Retrieve the parser state so we can restart from this point later.

86+mark :: Parsing m => m Mark

87+mark = P.getParserState

88+

89+restore :: Parsing m => Mark -> m ()

90+restore = P.setParserState

91+

92+{- * Tracking the extent of productions -}

93+

94+sourcePositionFC :: P.SourcePos -> FC

95+sourcePositionFC (P.SourcePos name line column) =

96+ FC f (lineNumber, columnNumber) (lineNumber, columnNumber)

97+ where

98+ lineNumber = P.unPos line

99+ columnNumber = P.unPos column

100+ (dir, file) = splitFileName name

101+ f = if dir == addTrailingPathSeparator "."

102+ then file

103+ else name

104+

105+-- | Get the current parse position.

106+--

107+-- This is useful when the position is needed in a way unrelated to the

108+-- heirarchy of parsers. Prefer using @withExtent@ and friends.

109+getFC :: Parsing m => m FC

110+getFC = sourcePositionFC <$> P.getPosition

111+

112+-- | Add an extent (widen) our current parsing context.

113+addExtent :: MonadWriter FC m => FC -> m ()

114+addExtent = tell

115+

116+-- | Run a parser and track its extent.

117+--

118+-- Wrap bare Megaparsec parsers with this to make them "visible" in error

119+-- messages. Do not wrap whitespace or comment parsers. If you find an

120+-- extent is taking trailing whitespace, it's likely there's a double-wrapped

121+-- parser (usually via @Idris.Parser.Helpers.token@).

122+trackExtent :: Parsing m => m a -> m a

123+trackExtent p = do (FC f (sr, sc) _) <- getFC

124+ result <- p

125+ (FC f _ (er, ec)) <- getFC

126+ addExtent (FC f (sr, sc) (er, max 1 (ec - 1)))

127+ return result

128+

129+-- | Run a parser, discard its value, and return its extent.

130+extent :: MonadWriter FC m => m a -> m FC

131+extent = fmap snd . withExtent

132+

133+-- | Run a parser and return its value and extent.

134+withExtent :: MonadWriter FC m => m a -> m (a, FC)

135+withExtent = listen

136+

137+-- | Run a parser and inject the extent after via function application.

138+appExtent :: MonadWriter FC m => m (FC -> a) -> m a

139+appExtent = fmap app . withExtent

src/Idris/REPL.hs+1−1

@@ -1427,7 +1427,7 @@ process fn (Browse ns) =

14271427process fn (MakeDoc s) =

14281428 do istate <- getIState

14291429 let names = words s

1430− parse n | Right x <- runparser (fmap fst name) istate fn n = Right x

1430+ parse n | Right x <- runparser name istate fn n = Right x

14311431 parse n = Left n

14321432 (bad, nss) = partitionEithers $ map parse names

14331433 cd <- runIO getCurrentDirectory

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

@@ -235,7 +235,7 @@ exprArg cmd name = do

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

236236

237237 let justOperator = do

238− (op, fc) <- IP.symbolicOperatorFC

238+ (op, fc) <- IP.withExtent IP.symbolicOperator

239239 P.eof

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

241241

@@ -256,19 +256,19 @@ genArg argName argParser cmd name = do

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

257257

258258nameArg, fnNameArg :: (Name -> Command) -> String -> IP.IdrisParser (Either String Command)

259−nameArg = genArg "name" $ fst <$> IP.name

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

259+nameArg = genArg "name" IP.name

260+fnNameArg = genArg "functionname" IP.fnName

261261

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

263263strArg = genArg "string" (P.many P.anyChar)

264264

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

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

266+moduleArg = genArg "module" (fmap toPath IP.identifier)

267267 where

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

269269

270270namespaceArg :: ([String] -> Command) -> String -> IP.IdrisParser (Either String Command)

271−namespaceArg = genArg "namespace" (fmap (toNS . fst) IP.identifier)

271+namespaceArg = genArg "namespace" (fmap toNS IP.identifier)

272272 where

273273 toNS = splitOn "."

274274

@@ -297,21 +297,21 @@ proofArg cmd name = do

297297 upd <- P.option False $ do

298298 IP.lchar '!'

299299 return True

300− l <- fst <$> IP.natural

301− n <- fst <$> IP.name;

300+ l <- IP.natural

301+ n <- IP.name

302302 return (Right (cmd upd (fromInteger l) n))

303303

304304cmd_doc :: String -> IP.IdrisParser (Either String Command)

305305cmd_doc name = do

306306 let constant = do

307− c <- fmap fst IP.constant

307+ c <- IP.constant

308308 P.eof

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

310310

311311 let pType = do

312312 IP.reserved "Type"

313313 P.eof

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

314+ return $ Right (DocStr (Left $ sUN "Type") FullDocs)

315315

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

317317

@@ -326,11 +326,11 @@ cmd_consolewidth name = do

326326 pConsoleWidth :: IP.IdrisParser ConsoleWidth

327327 pConsoleWidth = do discard (IP.symbol "auto"); return AutomaticWidth

328328 <|> do discard (IP.symbol "infinite"); return InfinitelyWide

329− <|> do n <- fmap (fromInteger . fst) IP.natural

329+ <|> do n <- fromInteger <$> IP.natural

330330 return (ColsWide n)

331331

332332cmd_printdepth :: String -> IP.IdrisParser (Either String Command)

333−cmd_printdepth _ = do d <- optional (fmap (fromInteger . fst) IP.natural)

333+cmd_printdepth _ = do d <- optional (fromInteger <$> IP.natural)

334334 return (Right $ SetPrinterDepth d)

335335

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

@@ -353,7 +353,7 @@ cmd_pprint :: String -> IP.IdrisParser (Either String Command)

353353cmd_pprint name = do

354354 fmt <- ppFormat

355355 IP.whiteSpace

356− n <- fmap (fromInteger . fst) IP.natural

356+ n <- fromInteger <$> IP.natural

357357 IP.whiteSpace

358358 t <- IP.fullExpr defaultSyntax

359359 return (Right (PPrint fmt n t))

@@ -370,20 +370,20 @@ cmd_compile name = do

370370 let codegenOption :: IP.IdrisParser Codegen

371371 codegenOption = do

372372 let bytecodeCodegen = discard (IP.symbol "bytecode") *> return Bytecode

373− viaCodegen = do x <- fst <$> IP.identifier

373+ viaCodegen = do x <- IP.identifier

374374 return (Via IBCFormat (map toLower x))

375375 bytecodeCodegen <|> viaCodegen

376376

377377 let hasOneArg = do

378378 i <- get

379− f <- fst <$> IP.identifier

379+ f <- IP.identifier

380380 P.eof

381381 return $ Right (Compile defaultCodegen f)

382382

383383 let hasTwoArgs = do

384384 i <- get

385385 codegen <- codegenOption

386− f <- fst <$> IP.identifier

386+ f <- IP.identifier

387387 P.eof

388388 return $ Right (Compile codegen f)

389389

@@ -393,20 +393,20 @@ cmd_compile name = do

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

394394cmd_addproof name = do

395395 n <- P.option Nothing $ do

396− x <- fst <$> IP.name

396+ x <- IP.name

397397 return (Just x)

398398 P.eof

399399 return (Right (AddProof n))

400400

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

402402cmd_log name = do

403− i <- fmap (fromIntegral . fst) IP.natural

403+ i <- fromIntegral <$> IP.natural

404404 P.eof

405405 return (Right (LogLvl i))

406406

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

408408cmd_verb name = do

409− i <- fmap (fromIntegral . fst) IP.natural

409+ i <- fromIntegral <$> IP.natural

410410 P.eof

411411 return (Right (Verbosity i))

412412

@@ -417,7 +417,7 @@ cmd_cats name = do

417417 return $ Right $ LogCategory (concat cs)

418418 where

419419 badCat = do

420− c <- fst <$> IP.identifier

420+ c <- IP.identifier

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

422422

423423 pLogCats :: IP.IdrisParser [LogCat]

@@ -435,11 +435,11 @@ cmd_let name = do

435435 return (Right (NewDefn defn))

436436

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

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

438+cmd_unlet name = Right . Undefine <$> P.many IP.name

439439

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

441441cmd_loadto name = do

442− toline <- fmap (fromInteger . fst) IP.natural

442+ toline <- fromInteger <$> IP.natural

443443 f <- P.many P.anyChar

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

445445

@@ -529,13 +529,13 @@ cmd_search = packageBasedCmd

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

530530cmd_proofsearch name = do

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

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

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

532+ l <- fromInteger <$> IP.natural; n <- IP.name

533+ hints <- P.many IP.fnName

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

535535

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

537537cmd_refine name = do

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

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

540− hint <- fst <$> IP.fnName

539+ l <- fromInteger <$> IP.natural; n <- IP.name

540+ hint <- IP.fnName

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

test/basic002/expected+2−2

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

1−test006.idr:25:23-28:

1+test006.idr:25:23-27:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−test006.idr:32:23-28:

3+test006.idr:32:23-27:

44This style of tactic proof is deprecated. See %runElab for the replacement.

55[False, True, False, True, False, True]

test/basic006/expected+1−1

@@ -1,4 +1,4 @@

1−test020a.idr:16:18:When checking right hand side of foo with expected type

1+test020a.idr:16:10-19:When checking right hand side of foo with expected type

22 List a

33

44When checking an application of function Prelude.List.reverse:

test/basic009/expected+3−3

@@ -1,7 +1,7 @@

11MAIN-PASS

2−Faulty.idr:6:9-12:num is bound as an implicit

2+Faulty.idr:6:9-11:num is bound as an implicit

33 Did you mean to refer to A.num?

4−Faulty.idr:7:7:When checking right hand side of fault with expected type

4+Faulty.idr:7:7-12:When checking right hand side of fault with expected type

55 num = 0

66

77Type mismatch between

@@ -14,4 +14,4 @@ Specifically:

1414 0

1515 and

1616 num

17−Multiple.idr:3:1:import alias not unique: "X"

17+Multiple.idr:3:21:import alias not unique: "X"

test/basic018/expected+3−3

@@ -1,10 +1,10 @@

1−basic018.idr:7:12-17:

1+basic018.idr:7:12-16:

22thing is bound as an implicit

33 Did you mean to refer to Main.thing?

4−basic018.idr:12:8-13:

4+basic018.idr:12:8-12:

55thing is bound as an implicit

66 Did you mean to refer to Main.thing?

7−basic018.idr:13:6:When checking right hand side of test with expected type

7+basic018.idr:13:6-11:When checking right hand side of test with expected type

88 thing = S 41

99

1010Type mismatch between

test/directives001/expected+4−4

@@ -2,11 +2,11 @@ directives001.idr:14:7:Use of deprecated name directives001.Foo

22To be replaced with `Bar`.

33directives001.idr:14:7:Use of deprecated name directives001.Foo

44To be replaced with `Bar`.

5−directives001.idr:15:7:Use of deprecated name directives001.Foo

5+directives001.idr:15:7-13:Use of deprecated name directives001.Foo

66To be replaced with `Bar`.

7−directives001.idr:15:7:Use of deprecated name directives001.Foo

7+directives001.idr:15:7-13:Use of deprecated name directives001.Foo

88To be replaced with `Bar`.

9−directives001.idr:26:8:Use of a fragile construct directives001.mkBar

9+directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

1010How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

11−directives001.idr:26:8:Use of a fragile construct directives001.mkBar

11+directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar

1212How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.

test/directives002/expected+1−1

@@ -1,2 +1,2 @@

1−directives002.idr:12:3:

1+directives002.idr:12:3-14:28:

22directives002.Main.main is possibly not total due to: directives002.loop

test/effects003/expected+1−1

@@ -1,4 +1,4 @@

1−hangman.idr:204:8-13:

1+hangman.idr:204:8-12:

22This style of tactic proof is deprecated. See %runElab for the replacement.

33------------

44

test/error003/expected+2−1

@@ -1,4 +1,5 @@

1−ErrorReflection.idr:68:5:When checking right hand side of bad with expected type

1+ErrorReflection.idr:68:5-20:

2+When checking right hand side of bad with expected type

23 Tm [] TUnit

34

45DSL type error: (t(504) => t'(503)) doesn't match ()

test/error004/expected+2−2

@@ -1,10 +1,10 @@

1−FunErrTest.idr:35:17:

1+FunErrTest.idr:35:12-18:

22When checking right hand side of badCadr1 with expected type

33 Int

44

55When checking argument cons2 to function FunErrTest.cadr:

66 Could not prove that [] has at least two elements.

7−FunErrTest.idr:38:17:

7+FunErrTest.idr:38:12-19:

88When checking right hand side of badCadr2 with expected type

99 Int

1010

test/error005/expected+5−5

@@ -1,29 +1,29 @@

1−error005.idr:13:1:When checking right hand side of two with expected type

1+error005.idr:11:7:When checking right hand side of two with expected type

22 Fin 2

33

44When checking argument prf to function Data.Fin.fromInteger:

55 When using 2 as a literal for a Fin 2

66 2 is not strictly less than 2

7−error005.idr:16:1:When checking right hand side of hahaha with expected type

7+error005.idr:14:12:When checking right hand side of hahaha with expected type

88 Fin n

99

1010When checking argument prf to function Data.Fin.fromInteger:

1111 When using 0 as a literal for a Fin n

1212 0 is not strictly less than n

13−error005.idr:22:1:When checking right hand side of notOk with expected type

13+error005.idr:20:11:When checking right hand side of notOk with expected type

1414 Fin (plus 2 n)

1515

1616When checking argument prf to function Data.Fin.fromInteger:

1717 When using 2 as a literal for a Fin (S (S n))

1818 2 is not strictly less than S (S n)

19−error005.idr:23:24:When checking right hand side of b0rken with expected type

19+error005.idr:23:12-24:When checking right hand side of b0rken with expected type

2020 Fin 3

2121

2222When checking argument prf to function Data.Fin.fromInteger:

2323 When using n as a literal for a Fin 3

2424 Could not show that n is less than 3 because n is a bound

2525 variable instead of a constant Integer

26−error005.idr:28:1:When checking right hand side of x with expected type

26+error005.idr:26:17:When checking right hand side of x with expected type

2727 Fin 4

2828

2929When checking argument prf to function Data.Fin.fromInteger:

test/error006/expected+1−1

@@ -1,2 +1,2 @@

1−WithPatsNoWith.idr:4:5:When checking left hand side of foo:

1+WithPatsNoWith.idr:4:15-20:When checking left hand side of foo:

22unexpected patterns outside of "with" block

test/error007/expected+1−1

@@ -1,4 +1,4 @@

1−error007.idr:26:17:

1+error007.idr:26:7-29:

22When checking right hand side of answer_to_connection with expected type

33 IO Int

44

test/ffi002/expected+1−1

@@ -1 +1 @@

1−test023.idr:20:21:Type provider error: Always fails

1+test023.idr:20:26-36:Type provider error: Always fails

test/interactive010/expected+1−1

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

11Prelude.List.(++) : List a -> List a -> List a

22Prelude.Strings.(++) : String -> String -> String

3−(input):1:11:a is not an implicit argument of Prelude.Interfaces./

3+(input):1:7-20:a is not an implicit argument of Prelude.Interfaces./

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>

test/interfaces008/expected+1−1

@@ -1,2 +1,2 @@

1−interfaces008.idr:20:18:

1+interfaces008.idr:20:18-23:

22Default implementations must be for a super interface constraint on the containing interface.

test/layout001/expected+2−2

@@ -59,7 +59,7 @@ Wrong indention: should be greater than context indentation

5959 | ^

6060Wrong indention: should be greater than context indentation

6161

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

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

6363 Maybe Int

6464

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

@@ -70,4 +70,4 @@ When checking an application of function Prelude.Applicative.pure:

7070 | ^

7171not end of block

7272

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

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

test/meta002/expected+3−3

@@ -1,12 +1,12 @@

1−DataDef.idr:74:1-9:

1+DataDef.idr:74:1-8:

22While running an elaboration script, the following error occurred:

33Prelude.Either.Either is already defined as a datatype.

4−Tacs.idr:299:15:

4+Tacs.idr:299:15-300:78:

55When checking right hand side of testElab3 with expected type

66 DPair Ty (Tm [])

77

88Unifying ty and ARR ty t would lead to infinite value

9−AgdaStyleReflection.idr:315:5:

9+AgdaStyleReflection.idr:315:5-20:

1010When checking right hand side of baz with expected type

1111 (Nat, Void)

1212

test/meta003/expected+1−1

@@ -1,4 +1,4 @@

1−BadDef.idr:14:1-9:

1+BadDef.idr:14:1-8:

22While running an elaboration script, the following error occurred:

33Type mismatch between

44 ()

test/meta004/expected+1−1

@@ -1,3 +1,3 @@

1−meta004.idr:50:1-9:

1+meta004.idr:50:1-8:

22While running an elaboration script, the following error occurred:

33Not an impossible case

test/proof001/expected+2−2

@@ -1,4 +1,4 @@

1−test029.idr:29:25-30:

1+test029.idr:29:25-29:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−test029.idr:36:25-30:

3+test029.idr:36:25-29:

44This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof002/expected+4−4

@@ -1,10 +1,10 @@

1−Reflect.idr:175:21-26:

1+Reflect.idr:175:21-25:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−Reflect.idr:184:21-26:

3+Reflect.idr:184:21-25:

44This style of tactic proof is deprecated. See %runElab for the replacement.

5−Reflect.idr:192:15-20:

5+Reflect.idr:192:15-19:

66This style of tactic proof is deprecated. See %runElab for the replacement.

7−test030a.idr:12:26-14:1:

7+test030a.idr:12:26-37:

88When checking right hand side of testReflect1 with expected type

99 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs

1010

test/proof003/expected+6−6

@@ -1,14 +1,14 @@

1−Parity.idr:17:18-23:

1+Parity.idr:17:18-22:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−Parity.idr:24:18-23:

3+Parity.idr:24:18-22:

44This style of tactic proof is deprecated. See %runElab for the replacement.

5−test015.idr:88:15-20:

5+test015.idr:88:15-19:

66This style of tactic proof is deprecated. See %runElab for the replacement.

7−test015.idr:97:16-21:

7+test015.idr:97:16-20:

88This style of tactic proof is deprecated. See %runElab for the replacement.

9−test015.idr:107:20-25:

9+test015.idr:107:20-24:

1010This style of tactic proof is deprecated. See %runElab for the replacement.

11−test015.idr:142:20-25:

11+test015.idr:142:20-24:

1212This style of tactic proof is deprecated. See %runElab for the replacement.

131300101010

141401011001

test/proof007/expected+1−1

@@ -1,4 +1,4 @@

1−DefaultArgUnknownName.idr:9:6:

1+DefaultArgUnknownName.idr:9:6-23:

22When checking right hand side of test with expected type

33 ()

44

test/proof008/expected+1−1

@@ -1,2 +1,2 @@

1−ClaimAndUnfocus.idr:8:27-32:

1+ClaimAndUnfocus.idr:8:27-31:

22This style of tactic proof is deprecated. See %runElab for the replacement.

test/proof011/expected+4−2

@@ -1,4 +1,5 @@

1−proof011.idr:19:9:When checking right hand side of vassoc' with expected type

1+proof011.idr:20:5-21:18:

2+When checking right hand side of vassoc' with expected type

23 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

34

45rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

@@ -7,7 +8,8 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

78 x ::

89 (xs ++ ys) ++

910 zs

10−proof011a.idr:13:9:When checking right hand side of vassoc' with expected type

11+proof011a.idr:14:5-37:

12+When checking right hand side of vassoc' with expected type

1113 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

1214

1315rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::

test/quasiquote003/expected+1−1

@@ -1,4 +1,4 @@

1−NoInfer.idr:11:5:When checking right hand side of zzz with expected type

1+NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type

22 TT

33

44No such variable k

test/quasiquote004/expected+4−4

@@ -1,10 +1,10 @@

1−Quasiquote004.idr:39:26-31:

1+Quasiquote004.idr:39:26-30:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−Quasiquote004.idr:42:28-33:

3+Quasiquote004.idr:42:28-32:

44This style of tactic proof is deprecated. See %runElab for the replacement.

5−Quasiquote004.idr:50:27-32:

5+Quasiquote004.idr:50:27-31:

66This style of tactic proof is deprecated. See %runElab for the replacement.

7−Quasiquote004.idr:50:25:

7+Quasiquote004.idr:50:25-51:18:

88When checking right hand side of Quasiquote004.getMeNat' with expected type

99 String

1010

test/quasiquote006/expected+3−3

@@ -1,15 +1,15 @@

1−quasiquote006.idr:9:3:

1+quasiquote006.idr:9:3-10:

22When checking right hand side of b with expected type

33 TTName

44

55Can't disambiguate name: ForeignEnv.Nil,

66 Prelude.List.Nil

7−quasiquote006.idr:12:3:

7+quasiquote006.idr:12:3-17:

88When checking right hand side of c with expected type

99 TTName

1010

1111No such variable alsdkjflkj

12−quasiquote006.idr:15:3:

12+quasiquote006.idr:15:3-11:

1313When checking right hand side of d with expected type

1414 TTName

1515

test/reg017/expected+2−2

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

1−reg017.idr:5:17-24:

1+reg017.idr:5:17-23:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−reg017.idr:8:17-24:

3+reg017.idr:8:17-23:

44This style of tactic proof is deprecated. See %runElab for the replacement.

554

test/reg027/expected+1−1

@@ -1,2 +1,2 @@

11<<int fn>>

2−reg027a.idr:9:16:Overlapping implementation: Show (Int -> a) already defined

2+reg027a.idr:9:16-30:Overlapping implementation: Show (Int -> a) already defined

test/regression002/expected+43−42

@@ -1,13 +1,13 @@

1−reg003a.idr:4:11:When checking type of Main.ECons:

1+reg003a.idr:4:13-38:When checking type of Main.ECons:

22No such variable OddList

3−reg003a.idr:7:11:When checking type of Main.OCons:

3+reg003a.idr:7:13-38:When checking type of Main.OCons:

44No such variable EvenList

55reg003a.idr:9:6:When checking type of Main.test:

66No such variable EvenList

7−reg006.idr:17:1:

7+reg006.idr:17:1-23:

88RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

9−reg007.lidr:8:3:A.n is already defined

10−reg007.lidr:12:13-19:When checking right hand side of hurrah with expected type

9+reg007.lidr:8:3-13:A.n is already defined

10+reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type

1111 0 = 1

1212

1313Type mismatch between

@@ -20,40 +20,40 @@ Specifically:

2020 1

2121 and

2222 0

23−reg010.idr:5:15:

23+reg010.idr:5:28-31:

2424When checking left hand side of with block in usubst.unsafeSubst:

2525Can't match on with block in usubst.unsafeSubst warg a P x x px

26−reg018a.idr:16:1:

26+reg018a.idr:16:1-18:

2727conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

28−reg018a.idr:21:1:

28+reg018a.idr:21:1-42:

2929conat.loopForever is possibly not total due to: conat.minusCoNat

30−reg018b.idr:8:1:

30+reg018b.idr:8:1-28:

3131A.showB is possibly not total due to recursive path A.showB --> A.showB

32−reg018b.idr:11:1:

32+reg018b.idr:11:1-6:

3333A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

34−reg018c.idr:21:1:

34+reg018c.idr:21:1-22:21:

3535CodataTest.inf is possibly not total due to: with block in CodataTest.inf

36−reg018d.idr:8:1:Main.pull is not total as there are missing cases

37−reg023.idr:7:5:When checking right hand side of bad with expected type

36+reg018d.idr:8:1-39:Main.pull is not total as there are missing cases

37+reg023.idr:7:5-7:When checking right hand side of bad with expected type

3838 f Nat

3939

4040Type mismatch between

4141 Nat (Type of 0)

4242and

4343 f Nat (Expected type)

44−reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

45−reg028a.idr:17:14-19:

44+reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad

45+reg028a.idr:17:14-18:

4646This style of tactic proof is deprecated. See %runElab for the replacement.

47−reg028a.idr:11:1:

47+reg028a.idr:11:1-14:

4848tbad.qsort' is possibly not total due to: with block in tbad.qsort'

49−reg034.idr:6:5:When checking left hand side of bar:

49+reg034.idr:6:16-21:When checking left hand side of bar:

5050Can't match on bar xs xs Refl

51−reg034.idr:9:5:When checking left hand side of foo:

51+reg034.idr:9:16-21:When checking left hand side of foo:

5252Can't match on foo f x x Refl

53−reg035b.idr:8:6:No such variable __pi_arg

54−reg044.idr:4:6-11:

53+reg035b.idr:8:12-38:No such variable __pi_arg

54+reg044.idr:4:6-10:

5555This style of tactic proof is deprecated. See %runElab for the replacement.

56−reg044.idr:4:4:When checking right hand side of Main.pf with expected type

56+reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type

5757 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

5858

5959Type mismatch between

@@ -66,9 +66,9 @@ Specifically:

6666 b

6767 and

6868 a

69−reg049.idr:2:9:When checking constructor Main.Bogus:

69+reg049.idr:2:11-14:When checking constructor Main.Bogus:

7070Void is not Main.Foo

71−reg049.idr:5:6:When checking right hand side of uhOh with expected type

71+reg049.idr:5:6-12:When checking right hand side of uhOh with expected type

7272 Void

7373

7474No such variable Bogus

@@ -84,41 +84,41 @@ No such variable Bogus

8484 | ^

8585unexpected Operator without known fixity: !!

8686

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

87+reg054.idr:18:19-24:When checking left hand side of inf:

8888When checking an application of constructor Main.MkInfer:

8989 Attempting concrete match on polymorphic argument: 0

90−reg054.idr:34:7:When checking left hand side of weird:

90+reg054.idr:34:20-24:When checking left hand side of weird:

9191No explicit types on left hand side: Char

92−reg054.idr:37:8:When checking left hand side of weird':

92+reg054.idr:37:32-34:When checking left hand side of weird':

9393No explicit types on left hand side: Nat

94−reg054.idr:40:1-8:When checking left hand side of tctrick:

94+reg054.idr:40:1-7:When checking left hand side of tctrick:

9595When checking an application of Main.tctrick:

9696 Type mismatch between

9797 Maybe a1 (Type of Just x)

9898 and

9999 a (Expected type)

100−reg055.idr:5:3:When checking left hand side of g:

100+reg055.idr:5:9-11:When checking left hand side of g:

101101Can't match on g (f 0)

102−reg055.idr:8:3:When checking left hand side of h:

102+reg055.idr:8:7-9:When checking left hand side of h:

103103Can't match on h x x

104−reg055a.idr:8:5:When checking left hand side of foo:

104+reg055a.idr:8:20-23:When checking left hand side of foo:

105105When checking an application of constructor Foo.CAny:

106106 Attempting concrete match on polymorphic argument: Nothing

107−reg055a.idr:13:7:When checking left hand side of Foo.apply:

107+reg055a.idr:13:25-27:When checking left hand side of Foo.apply:

108108Can't match on apply (\x, y => x) a

109−reg056.idr:7:7:dodgy n m Refl is a valid case

110−reg056.idr:10:6:nonk Refl is a valid case

111−reg068.idr:1:6:Main.nat has a name which may be implicitly bound.

109+reg056.idr:7:16-25:dodgy n m Refl is a valid case

110+reg056.idr:10:11-20:nonk Refl is a valid case

111+reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.

112112This is likely to lead to problems!

113−reg068.idr:2:6:Main.ze has a name which may be implicitly bound.

113+reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.

114114This is likely to lead to problems!

115−reg068.idr:2:8-11:

115+reg068.idr:2:8-10:

116116nat is bound as an implicit

117117 Did you mean to refer to Main.nat?

118−reg068.idr:2:6:When checking constructor Main.ze:

118+reg068.idr:2:8-10:When checking constructor Main.ze:

119119Type level variable nat is not Main.nat

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

121−reg070.idr:7:1:

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

121+reg070.idr:7:1-7:

122122Test_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

123123./reg076.idr:8:1:

124124 |

@@ -132,7 +132,8 @@ Missing fixity declaration for Main.:>

132132 | ^

133133Missing fixity declaration for Main.:>>

134134

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

135+DoubleEquality.idr:4:83-103:

136+When checking right hand side of oops with expected type

136137 Void

137138

138139When checking argument value to function Prelude.Basics.the:

@@ -146,5 +147,5 @@ When checking argument value to function Prelude.Basics.the:

146147 -0.0

147148 and

148149 0.0

149−Canonicity.idr:9:1:Canonicity.f is not total as there are missing cases

150−Canonicity.idr:12:1:Canonicity.NaN is possibly not total due to: Canonicity.f

150+Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases

151+Canonicity.idr:12:1-20:Canonicity.NaN is possibly not total due to: Canonicity.f

test/sourceLocation001/expected+8−8

@@ -1,19 +1,19 @@

1−SourceLoc.idr:12:19-26:

1+SourceLoc.idr:12:19-25:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−SourceLoc.idr:21:19-24:

3+SourceLoc.idr:21:19-23:

44This style of tactic proof is deprecated. See %runElab for the replacement.

5−SourceLoc.idr:41:20-27:

5+SourceLoc.idr:41:20-26:

66This style of tactic proof is deprecated. See %runElab for the replacement.

7−SourceLoc.idr:99:18-23:

7+SourceLoc.idr:99:18-22:

88This style of tactic proof is deprecated. See %runElab for the replacement.

99Testing using definition

10−FileLoc "SourceLoc.idr" (17, 11) (17, 17)

10+FileLoc "SourceLoc.idr" (17, 11) (17, 16)

1111Testing using inline tactics

12−FileLoc "SourceLoc.idr" (21, 17) (21, 17)

12+FileLoc "SourceLoc.idr" (21, 17) (21, 38)

1313Testing using metavariable with later definition

14−FileLoc "SourceLoc.idr" (99, 16) (99, 16)

14+FileLoc "SourceLoc.idr" (99, 16) (100, 16)

1515-----------------------

1616Success!

17−Error at FileLoc "SourceLoc.idr" (73, 23) (73, 26)

17+Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)

1818Success!

1919Success!

test/syntax001/expected+2−2

@@ -1,4 +1,4 @@

1−Syntax.idr:6:7-9:1:When checking right hand side of foo with expected type

1+Syntax.idr:6:7-18:When checking right hand side of foo with expected type

22 Nat

33

44When checking an application of function Prelude.Interfaces.+:

@@ -6,7 +6,7 @@ When checking an application of function Prelude.Interfaces.+:

66 String (Type of "argh")

77 and

88 Nat (Expected type)

9−SyntaxTest.idr:5:7-6:1:When checking right hand side of foo with expected type

9+SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type

1010 Nat

1111

1212When checking an application of function Prelude.Interfaces.+:

test/totality001/expected+3−3

@@ -1,3 +1,3 @@

1−test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad

2−test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3−test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

1+test010.idr:15:1-30:Main.foo is possibly not total due to: Main.MkBad

2+test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:1-23:main.bar is possibly not total due to: main.MkBad

test/totality002/expected+3−3

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

1−test017.idr:94:26-31:

1+test017.idr:94:26-30:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−test017a.idr:7:1:

3+test017a.idr:7:1-24:

44scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

5−test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

5+test017b.idr:4:1-9:foo.foo is possibly not total due to recursive path foo.foo

test/totality003/expected+1−1

@@ -1,2 +1,2 @@

1−totality003a.idr:5:1:

1+totality003a.idr:5:1-13:

22smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort

test/totality004/expected+2−2

@@ -1,4 +1,4 @@

11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]

2−totality004a.idr:13:1:

2+totality004a.idr:13:1-44:

33Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process

4−totality004a.idr:24:1:Main.main is possibly not total due to: Main.process

4+totality004a.idr:24:1-60:Main.main is possibly not total due to: Main.process

test/totality006/expected+3−3

@@ -1,4 +1,4 @@

1−totality006.idr:8:1:Main.prf is not total as there are missing cases

2−totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

3−totality006b.idr:10:1:

1+totality006.idr:8:1-29:Main.prf is not total as there are missing cases

2+totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case

3+totality006b.idr:10:1-34:

44totality006b.blargh is not total as there are missing cases

test/totality007/expected+2−2

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

11Entering directory `./src'

2−Totality.idr:4:1:

2+Totality.idr:4:1-9:

33Totality.foo is not total as there are missing cases

4−Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases

4+Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases

55Leaving directory `./src'

test/totality008/expected+1−1

@@ -1 +1 @@

1−totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.C2

1+totality008.idr:7:1-14:Main.ElimT is possibly not total due to: Main.C2

test/totality009/expected+9−9

@@ -1,10 +1,10 @@

1−TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases

2−TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25

1+TestLambdaPossible.idr:9:25-34:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

2+TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

33TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

4−TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

5−TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25 is not total as there are missing cases

6−TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25

7−TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

8−TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

9−TestLambdaPossible2.idr:10:1:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25

10−TestLambdaPossible2.idr:14:1:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

4+TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

5+TestLambdaPossible.idr:9:15-35:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases

6+TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34

7+TestLambdaPossible.idr:12:18-13:40:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

8+TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

9+TestLambdaPossible2.idr:10:1-35:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34

10+TestLambdaPossible2.idr:14:1-15:40:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

test/totality010/expected+2−2

@@ -1,2 +1,2 @@

1−totality010.idr:27:1:Main.evenNotS is not total as there are missing cases

2−totality010.idr:30:1:Main.bad is possibly not total due to: Main.evenNotS

1+totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases

2+totality010.idr:30:1-40:Main.bad is possibly not total due to: Main.evenNotS

test/totality011/expected+1−1

@@ -1,2 +1,2 @@

1−totality011.lidr:22:3:

1+totality011.lidr:22:3-57:

22Main.weCanOnlyGetOlder is not total as there are missing cases

test/totality012/expected+2−2

@@ -1,4 +1,4 @@

1−totality012a.idr:9:1:

1+totality012a.idr:9:1-10:27:

22Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2

3−totality012b.idr:11:1:

3+totality012b.idr:11:1-17:33:

44Main.echo is possibly not total due to recursive path Main.echo

test/totality013/expected+2−2

@@ -1,3 +1,3 @@

1−totality013a.idr:5:3:

1+totality013a.idr:5:3-49:

22Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

3−totality013a.idr:9:3:Main.mtot is possibly not total due to: Main.foo

3+totality013a.idr:9:3-36:Main.mtot is possibly not total due to: Main.foo

test/totality014/expected+4−4

@@ -1,8 +1,8 @@

1−totality014.idr:1:6:Universe inconsistency.

1+totality014.idr:1:6-9:Universe inconsistency.

22 Working on: ./totality014.idr.w

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

7− ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

8− ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

6+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

7+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}

8+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}

test/totality015/expected+3−3

@@ -1,4 +1,4 @@

1−totality015a.idr:52:3:

1+totality015a.idr:52:3-53:

22Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz

3−totality015a.idr:42:3:Main.correct is possibly not total due to: Main.quiz

4−totality015a.idr:47:3:Main.wrong is possibly not total due to: Main.quiz

3+totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz

4+totality015a.idr:47:3-49:28:Main.wrong is possibly not total due to: Main.quiz

test/totality016/expected+9−9

@@ -1,9 +1,9 @@

1−totality016.idr:15:1:Main.f1 is not total as there are missing cases

2−totality016.idr:19:1:Main.f2 is not total as there are missing cases

3−totality016.idr:23:1:Main.f3 is not total as there are missing cases

4−totality016.idr:27:1:Main.g1 is not total as there are missing cases

5−totality016.idr:31:1:Main.g2 is not total as there are missing cases

6−totality016.idr:35:1:Main.h1 is not total as there are missing cases

7−totality016.idr:39:1:Main.h2 is not total as there are missing cases

8−totality016.idr:43:1:Main.h3 is not total as there are missing cases

9−totality016.idr:47:1:Main.h4 is not total as there are missing cases

1+totality016.idr:15:1-21:Main.f1 is not total as there are missing cases

2+totality016.idr:19:1-24:Main.f2 is not total as there are missing cases

3+totality016.idr:23:1-29:Main.f3 is not total as there are missing cases

4+totality016.idr:27:1-14:Main.g1 is not total as there are missing cases

5+totality016.idr:31:1-17:Main.g2 is not total as there are missing cases

6+totality016.idr:35:1-16:Main.h1 is not total as there are missing cases

7+totality016.idr:39:1-19:Main.h2 is not total as there are missing cases

8+totality016.idr:43:1-25:Main.h3 is not total as there are missing cases

9+totality016.idr:47:1-30:Main.h4 is not total as there are missing cases

test/totality017/expected+6−6

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

1−totality017.idr:19:1:Main.g1 is not total as there are missing cases

2−totality017.idr:25:1:Main.g2 is not total as there are missing cases

3−totality017.idr:31:1:Main.g3 is not total as there are missing cases

4−totality017.idr:37:1:Main.g4 is not total as there are missing cases

5−totality017.idr:42:1:Main.f' is not total as there are missing cases

6−totality017.idr:47:1:Main.f is not total as there are missing cases

1+totality017.idr:19:1-15:Main.g1 is not total as there are missing cases

2+totality017.idr:25:1-17:Main.g2 is not total as there are missing cases

3+totality017.idr:31:1-13:Main.g3 is not total as there are missing cases

4+totality017.idr:37:1-36:Main.g4 is not total as there are missing cases

5+totality017.idr:42:1-11:Main.f' is not total as there are missing cases

6+totality017.idr:47:1-17:Main.f is not total as there are missing cases

test/totality018/expected+1−1

@@ -1 +1 @@

1−totality018.idr:12:1:Main.bar is not total as there are missing cases

1+totality018.idr:12:1-10:Main.bar is not total as there are missing cases

test/totality019/expected+2−2

@@ -1,2 +1,2 @@

1−totality019.idr:8:1:Main.testCov is not total as there are missing cases

2−totality019.idr:12:1:Main.testCov' is not total as there are missing cases

1+totality019.idr:8:1-36:Main.testCov is not total as there are missing cases

2+totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases

test/totality020/expected+2−2

@@ -1,2 +1,2 @@

1−totality020.idr:4:5:bug _ _ Refl is a valid case

2−totality020.idr:7:5:foo a b Refl is a valid case

1+totality020.idr:4:14-23:bug _ _ Refl is a valid case

2+totality020.idr:7:14-23:foo a b Refl is a valid case

test/totality021/expected+6−5

@@ -1,9 +1,10 @@

1−totality021.idr:8:1:

1+totality021.idr:8:1-67:

22Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'

3−totality021.idr:12:1:

3+totality021.idr:12:1-66:

44Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'

5−totality021.idr:18:1:Main.v is possibly not total due to: Main.sLevelNotSLevel

6−totality021a.idr:9:1:

5+totality021.idr:18:1-26:

6+Main.v is possibly not total due to: Main.sLevelNotSLevel

7+totality021a.idr:9:1-37:

78Main.noNonEmptyPointInt is not total as there are missing cases

8−totality021a.idr:12:1:

9+totality021a.idr:12:1-31:

910Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt

test/totality022/expected+1−1

@@ -1 +1 @@

1−totality022.idr:7:3:f _ [] (RSnoc _ _) is a valid case

1+totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case

test/totality023/expected+1−1

@@ -1,2 +1,2 @@

1−totality023.idr:9:1:

1+totality023.idr:9:1-10:27:

22Main.run is possibly not total due to recursive path Main.run --> Main.run

test/tutorial002/expected+3−3

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

1−tutorial002.idr:41:25-30:

1+tutorial002.idr:41:25-29:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−tutorial002.idr:48:18-23:

3+tutorial002.idr:48:18-22:

44This style of tactic proof is deprecated. See %runElab for the replacement.

5−tutorial002.idr:54:18-23:

5+tutorial002.idr:54:18-22:

66This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial004/expected+2−2

@@ -1,4 +1,4 @@

1−tutorial004.idr:46:14-19:

1+tutorial004.idr:46:14-18:

22This style of tactic proof is deprecated. See %runElab for the replacement.

3−tutorial004.idr:53:14-19:

3+tutorial004.idr:53:14-18:

44This style of tactic proof is deprecated. See %runElab for the replacement.

test/tutorial006/expected+2−2

@@ -1,4 +1,4 @@

1−tutorial006a.idr:5:23-25:

1+tutorial006a.idr:5:23-24:

22When checking right hand side of vapp with expected type

33 Vect (S len + m) a

44

@@ -13,7 +13,7 @@ When checking argument xs to constructor Data.Vect.:::

1313 plus len len

1414 and

1515 plus len m

16−tutorial006b.idr:10:10:

16+tutorial006b.idr:10:37-50:

1717When checking right hand side of with block in Main.parity with expected type

1818 Parity (S (S (j + j)))

1919

test/unique004/expected+10−10

@@ -1,26 +1,26 @@

1−unique001a.idr:35:11:Type mismatch between

1+unique001a.idr:35:14-43:50:Type mismatch between

22 Int -> String

33and

44 UniqueType (Int -> String)

5−unique001a.idr:46:12:Type mismatch between

5+unique001a.idr:46:15-54:28:Type mismatch between

66 Int -> String

77and

88 UniqueType (Int -> String)

9−unique001a.idr:57:12:Type mismatch between

9+unique001a.idr:57:15-62:33:Type mismatch between

1010 UniqueType (Int -> String)

1111and

1212 Int -> String

13−unique001b.idr:18:7:Borrowed name xs must not be used on RHS

14−unique001c.idr:47:6:Unique name f is used more than once

15−unique001d.idr:4:7:Borrowed name x must not be used on RHS

16−unique001e.idr:4:10:

13+unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS

14+unique001c.idr:47:12-62:Unique name f is used more than once

15+unique001d.idr:4:16-18:Borrowed name x must not be used on RHS

16+unique001e.idr:4:12-40:

1717Constructor Main.Nil has a UniqueType, but the data type does not

18−unique002.idr:17:5:Unique name xs is used more than once

19−unique002a.idr:17:5:Type mismatch between

18+unique002.idr:17:8-20:19:Unique name xs is used more than once

19+unique002a.idr:17:8-20:19:Type mismatch between

2020 Int -> String

2121and

2222 UniqueType (Int -> String)

23−unique003.idr:20:5:Type mismatch between

23+unique003.idr:20:8-24:19:Type mismatch between

2424 Int -> String

2525and

2626 UniqueType (Int -> String)

test/universes001/expected+5−5

@@ -1,9 +1,9 @@

1−universes001.idr:7:5:Universe inconsistency.

1+universes001.idr:7:5-21:Universe inconsistency.

22 Working on: ./universes001.idr.x

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

7− ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6}

8− ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6}

9− ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

6+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

7+ ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}

8+ ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}

9+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}

test/universes002/expected+5−5

@@ -1,9 +1,9 @@

1−universes002.idr:45:9:Universe inconsistency.

1+universes002.idr:45:9-48:Universe inconsistency.

22 Working on: ./universes002.idr.b1

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

7− ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6}

8− ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

9− ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6}

6+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

7+ ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}

8+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}

9+ ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}