[ refactor ] Multiline error report (#1155)

src/Core/Core.idr

@@ -140,8 +140,7 @@ data Error : Type where
      CantFindPackage : String -> Error
      LitFail : FC -> Error
      LexFail : FC -> String -> Error
-     ParseFail : (Show token, Pretty token) =>
-               FC -> String -> List token -> Error
+     ParseFail : FC -> String -> Error
      ModuleNotFound : FC -> ModuleIdent -> Error
      CyclicImports : List ModuleIdent -> Error
      ForceNeeded : Error
@@ -307,7 +306,7 @@ Show Error where
   show (CantFindPackage fname) = "Can't find package " ++ fname
   show (LitFail fc) = show fc ++ ":Can't parse literate"
   show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")"
-  show (ParseFail fc err toks) = "Parse error (" ++ show err ++ "): " ++ show toks
+  show (ParseFail fc err) = "Parse error (" ++ show err ++ ")"
   show (ModuleNotFound fc ns)
       = show fc ++ ":" ++ show ns ++ " not found"
   show (CyclicImports ns)
@@ -389,7 +388,7 @@ getErrorLoc (FileErr _ _) = Nothing
 getErrorLoc (CantFindPackage _) = Nothing
 getErrorLoc (LitFail loc) = Just loc
 getErrorLoc (LexFail loc _) = Just loc
-getErrorLoc (ParseFail loc _ _) = Just loc
+getErrorLoc (ParseFail loc _) = Just loc
 getErrorLoc (ModuleNotFound loc _) = Just loc
 getErrorLoc (CyclicImports _) = Nothing
 getErrorLoc ForceNeeded = Nothing

src/Idris/Error.idr

@@ -412,7 +412,7 @@ perror (LitFail fc)
     = pure $ errorDesc (reflow "Can't parse literate.") <+> line <+> !(ploc fc)
 perror (LexFail fc msg)
     = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc)
-perror (ParseFail fc msg toks)
+perror (ParseFail fc msg)
     = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc)
 perror (ModuleNotFound fc ns)
     = pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty ns) <++> reflow "not found") <+> line <+> !(ploc fc)

src/Idris/IDEMode/Parser.idr

@@ -49,7 +49,7 @@ idelex str
            -- Add the EndInput token so that we'll have a line and column
            -- number to read when storing spans in the file
            (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
-                                               [MkBounded EndInput False l c l c])
+                                               [MkBounded EndInput False (MkBounds l c l c)])
            (_, fail) => Left fail
     where
       notComment : WithBounds Token -> Bool

src/Idris/Parser.idr

@@ -689,7 +689,7 @@ mutual
            the (SourceEmptyRule PTerm) $ case nsdo.val of
                 (ns, "do") =>
                    do commit
-                      actions <- bounds (block (doAct fname))
+                      actions <- Core.bounds (block (doAct fname))
                       let fc = boundToFC fname (mergeBounds nsdo actions)
                       pure (PDoBlock fc ns (concat actions.val))
                 _ => fail "Not a namespaced 'do'"
@@ -784,11 +784,11 @@ mutual
   export
   singlelineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
   singlelineStr q fname idents
-      = do b <- bounds $ do strBegin
+      = do b <- bounds $ do begin <- bounds strBegin
                             commit
                             xs <- many $ bounds $ (interpBlock q fname idents) <||> strLitLines
                             pstrs <- case traverse toPStr xs of
-                                          Left err => fatalError err
+                                          Left err => fatalLoc begin.bounds err
                                           Right pstrs => pure $ pstrs
                             strEnd
                             pure pstrs
@@ -1455,7 +1455,7 @@ topDecl fname indents
   <|> do d <- directiveDecl fname indents
          pure [d]
   <|> do dstr <- bounds (terminal "Expected CG directive"
-                          (\x => case x.val of
+                          (\x => case x of
                                       CGDirective d => Just d
                                       _ => Nothing))
          pure [let cgrest = span isAlphaNum dstr.val in

src/Libraries/Text/Bounded.idr

@@ -2,37 +2,63 @@ module Libraries.Text.Bounded
 
 %default total
 
+
+public export
+record Bounds where
+  constructor MkBounds
+  startLine : Int
+  startCol : Int
+  endLine : Int
+  endCol : Int
+
+Show Bounds where
+  showPrec d (MkBounds sl sc el ec) =
+    showCon d "MkBounds" (concat [showArg sl, showArg sc, showArg el, showArg ec])
+
+export
+startBounds : Bounds -> (Int, Int)
+startBounds b = (b.startLine, b.startCol)
+
+export
+endBounds : Bounds -> (Int, Int)
+endBounds b = (b.endLine, b.endCol)
+
+export
+Eq Bounds where
+  (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
+      sl == sl'
+   && sc == sc'
+   && el == el'
+   && ec == ec'
+
 public export
 record WithBounds ty where
   constructor MkBounded
   val : ty
   isIrrelevant : Bool
-  startLine : Int
-  startCol : Int
-  endLine : Int
-  endCol : Int
+  bounds : Bounds
 
 export
 start : WithBounds ty -> (Int, Int)
-start b = (b.startLine, b.startCol)
+start = startBounds . bounds
 
 export
 end : WithBounds ty -> (Int, Int)
-end b = (b.endLine, b.endCol)
+end = endBounds . bounds
 
 export
 Eq ty => Eq (WithBounds ty) where
-  (MkBounded val ir sl sc el ec) == (MkBounded val' ir' sl' sc' el' ec') =
-    val == val' && ir == ir' && sl == sl' && sc == sc' && el == el' && ec == ec'
+  (MkBounded val ir bd) == (MkBounded val' ir' bd') =
+    val == val' && ir == ir' && bd == bd'
 
 export
 Show ty => Show (WithBounds ty) where
-  showPrec d (MkBounded val ir sl sc el ec) =
-    showCon d "MkBounded" (concat [showArg ir, showArg val, showArg sl, showArg sc, showArg el, showArg ec])
+  showPrec d (MkBounded val ir bd) =
+    showCon d "MkBounded" (concat [showArg ir, showArg val, showArg bd])
 
 export
 Functor WithBounds where
-  map f (MkBounded val ir sl sc el ec) = MkBounded (f val) ir sl sc el ec
+  map f (MkBounded val ir bd) = MkBounded (f val) ir bd
 
 export
 Foldable WithBounds where
@@ -40,25 +66,25 @@ Foldable WithBounds where
 
 export
 Traversable WithBounds where
-  traverse f (MkBounded v a b c d e) = (\ v => MkBounded v a b c d e) <$> f v
+  traverse f (MkBounded v a bd) = (\ v => MkBounded v a bd) <$> f v
 
 export
 irrelevantBounds : ty -> WithBounds ty
-irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1)
+irrelevantBounds x = MkBounded x True (MkBounds (-1) (-1) (-1) (-1))
 
 export
 removeIrrelevance : WithBounds ty -> WithBounds ty
-removeIrrelevance (MkBounded val ir sl sc el ec) = MkBounded val True sl sc el ec
+removeIrrelevance (MkBounded val ir bd) = MkBounded val True bd
 
 export
 mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
-mergeBounds (MkBounded _ True _ _ _ _) (MkBounded val True _ _ _ _) = irrelevantBounds val
-mergeBounds (MkBounded _ True _ _ _ _) b2 = b2
-mergeBounds b1 (MkBounded val True _ _ _ _) = const val <$> b1
+mergeBounds (MkBounded _ True _) (MkBounded val True _) = irrelevantBounds val
+mergeBounds (MkBounded _ True _) b2 = b2
+mergeBounds b1 (MkBounded val True _) = const val <$> b1
 mergeBounds b1 b2 =
   let (ur, uc) = min (start b1) (start b2)
       (lr, lc) = max (end b1) (end b2) in
-      MkBounded b2.val False ur uc lr lc
+      MkBounded b2.val False (MkBounds ur uc lr lc)
 
 export
 joinBounds : WithBounds (WithBounds ty) -> WithBounds ty

src/Libraries/Text/Lexer/Core.idr

@@ -131,7 +131,7 @@ public export
 TokenMap : (tokenType : Type) -> Type
 TokenMap tokenType = List (Lexer, String -> tokenType)
 
-tokenise : (WithBounds a -> Bool) ->
+tokenise : (a -> Bool) ->
            (line : Int) -> (col : Int) ->
            List (WithBounds a) -> TokenMap a ->
            List Char -> (List (WithBounds a), (Int, Int, List Char))
@@ -139,7 +139,7 @@ tokenise pred line col acc tmap str
     = case getFirstToken tmap str of
            Just (tok, line', col', rest) =>
            -- assert total because getFirstToken must consume something
-               if pred tok
+               if pred tok.val
                   then (reverse acc, (line, col, []))
                   else assert_total (tokenise pred line' col' (tok :: acc) tmap rest)
            Nothing => (reverse acc, (line, col, str))
@@ -161,7 +161,7 @@ tokenise pred line col acc tmap str
                Just (tok, rest) =>
                  let line' = line + cast (countNLs tok)
                      col' = getCols tok col in
-                     Just (MkBounded (fn (fastPack (reverse tok))) False line col line' col',
+                     Just (MkBounded (fn (fastPack (reverse tok))) False (MkBounds line col line' col'),
                            line', col', rest)
                Nothing => getFirstToken ts str
 
@@ -176,7 +176,7 @@ lex tmap str
           (ts, (l, c, fastPack str'))
 
 export
-lexTo : (WithBounds a -> Bool) ->
+lexTo : (a -> Bool) ->
         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lexTo pred tmap str
     = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in

src/Libraries/Text/Lexer/Tokenizer.idr

@@ -110,7 +110,7 @@ tokenise reject tokenizer line col acc str
     getFirstMatch (Match lex fn) str
         = let Just (tok, line', col', rest) = getNext lex line col str
                 | _ => Left NoRuleApply
-              tok' = MkBounded (fn tok) False line col line' col'
+              tok' = MkBounded (fn tok) False (MkBounds line col line' col')
            in Right ([tok'], line', col', rest)
     getFirstMatch (Compose begin mapBegin tagger middleFn endFn mapEnd) str
         = let Just (beginTok', line', col' , rest) = getNext begin line col str
@@ -118,7 +118,7 @@ tokenise reject tokenizer line col acc str
               tag = tagger beginTok'
               middle = middleFn tag
               end = endFn tag
-              beginTok'' = MkBounded (mapBegin beginTok') False line col line' col'
+              beginTok'' = MkBounded (mapBegin beginTok') False (MkBounds line col line' col')
               (midToks, (reason, line'', col'', rest'')) =
                     tokenise end middle line' col' [] rest
            in case reason of
@@ -126,7 +126,7 @@ tokenise reject tokenizer line col acc str
                    _ => let Just (endTok', lineEnd, colEnd, restEnd) =
                                 getNext end line'' col'' rest''
                               | _ => Left $ ComposeNotClosing (line, col) (line', col')
-                            endTok'' = MkBounded (mapEnd endTok') False line'' col'' lineEnd colEnd
+                            endTok'' = MkBounded (mapEnd endTok') False (MkBounds line'' col'' lineEnd colEnd)
                          in Right ([endTok''] ++ reverse midToks ++ [beginTok''], lineEnd, colEnd, restEnd)
     getFirstMatch (Alt t1 t2) str
         = case getFirstMatch t1 str of

src/Libraries/Text/Literate.idr

@@ -64,13 +64,13 @@ rawTokens delims ls =
 ||| Merge the tokens into a single source file.
 reduce : List (WithBounds Token) -> List String -> String
 reduce [] acc = fastAppend (reverse acc)
-reduce (MkBounded (Any x) _ _ _ _ _ :: rest) acc =
+reduce (MkBounded (Any x) _ _ :: rest) acc =
   -- newline will always be tokenized as a single token
   if x == "\n"
   then reduce rest ("\n"::acc)
   else reduce rest acc
 
-reduce (MkBounded (CodeLine m src) _ _ _ _ _ :: rest) acc =
+reduce (MkBounded (CodeLine m src) _ _ :: rest) acc =
     if m == trim src
     then reduce rest ("\n"::acc)
     else reduce rest ((substr (length m + 1) -- remove space to right of marker.
@@ -78,11 +78,11 @@ reduce (MkBounded (CodeLine m src) _ _ _ _ _ :: rest) acc =
                               src
                       )::acc)
 
-reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
-  reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | [] = reduce rest acc -- 1
-  reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: ys) with (snocList ys)
-    reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
-    reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
+reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
+  reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | [] = reduce rest acc -- 1
+  reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s :: ys) with (snocList ys)
+    reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
+    reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
         -- the "\n" counts for the open deliminator; the closing deliminator should always be followed by a (Any "\n"), so we don't add a newline
         reduce rest (unlines srcs :: "\n" :: acc)
 
@@ -185,7 +185,7 @@ isLiterateLine : (specification : LiterateStyle)
               -> (str : String)
               -> Pair (Maybe String) String
 isLiterateLine (MkLitStyle delims markers _) str with (lex (rawTokens delims markers) str)
-  isLiterateLine (MkLitStyle delims markers _) str | ([MkBounded (CodeLine m str') _ _ _ _ _], (_,_, "")) = (Just m, str')
+  isLiterateLine (MkLitStyle delims markers _) str | ([MkBounded (CodeLine m str') _ _], (_,_, "")) = (Just m, str')
   isLiterateLine (MkLitStyle delims markers _) str | (_, _) = (Nothing, str)
 
 ||| Given a 'literate specification' embed the given code using the

src/Libraries/Text/Parser.idr

@@ -16,8 +16,8 @@ match : (Eq k, TokenKind k) =>
         (kind : k) ->
         Grammar (Token k) True (TokType kind)
 match k = terminal "Unrecognised input" $
-    \t => if t.val.kind == k
-             then Just $ tokValue k t.val.text
+    \t => if t.kind == k
+             then Just $ tokValue k t.text
              else Nothing
 
 ||| Optionally parse a thing, with a default value if the grammar doesn't

src/Libraries/Text/Parser/Core.idr

@@ -18,11 +18,11 @@ import public Libraries.Text.Bounded
 export
 data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
      Empty : (val : ty) -> Grammar tok False ty
-     Terminal : String -> (WithBounds tok -> Maybe a) -> Grammar tok True a
-     NextIs : String -> (WithBounds tok -> Bool) -> Grammar tok False tok
+     Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
+     NextIs : String -> (tok -> Bool) -> Grammar tok False tok
      EOF : Grammar tok False ()
 
-     Fail : Bool -> String -> Grammar tok c ty
+     Fail : (location : Maybe Bounds) -> Bool -> String -> Grammar tok c ty
      Try : Grammar tok c ty -> Grammar tok c ty
 
      Commit : Grammar tok False ()
@@ -46,6 +46,7 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
            Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) ->
            Grammar tok (c1 && c2) ty
      Bounds : Grammar tok c ty -> Grammar tok c (WithBounds ty)
+     Position : Grammar tok False Bounds
 
 ||| Sequence two grammars. If either consumes some input, the sequence is
 ||| guaranteed to consume some input. If the first one consumes input, the
@@ -94,7 +95,7 @@ export
 {c : _} ->
 Functor (Grammar tok c) where
   map f (Empty val)  = Empty (f val)
-  map f (Fail fatal msg) = Fail fatal msg
+  map f (Fail bd fatal msg) = Fail bd fatal msg
   map f (Try g) = Try (map f g)
   map f (MustWork g) = MustWork (map f g)
   map f (Terminal msg g) = Terminal msg (map f . g)
@@ -167,10 +168,10 @@ export %inline
 export
 mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
 mapToken f (Empty val) = Empty val
-mapToken f (Terminal msg g) = Terminal msg (g . map f)
-mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . map f)) (Empty . f)
+mapToken f (Terminal msg g) = Terminal msg (g . f)
+mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
 mapToken f EOF = EOF
-mapToken f (Fail fatal msg) = Fail fatal msg
+mapToken f (Fail bd fatal msg) = Fail bd fatal msg
 mapToken f (Try g) = Try (mapToken f g)
 mapToken f (MustWork g) = MustWork (mapToken f g)
 mapToken f Commit = Commit
@@ -184,6 +185,7 @@ mapToken f (ThenEmpty act next)
   = ThenEmpty (mapToken f act) (mapToken f next)
 mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
 mapToken f (Bounds act) = Bounds (mapToken f act)
+mapToken f Position = Position
 
 ||| Always succeed with the given value.
 export %inline
@@ -192,7 +194,7 @@ pure = Empty
 
 ||| Check whether the next token satisfies a predicate
 export %inline
-nextIs : String -> (WithBounds tok -> Bool) -> Grammar tok False tok
+nextIs : String -> (tok -> Bool) -> Grammar tok False tok
 nextIs = NextIs
 
 ||| Look at the next token in the input
@@ -203,17 +205,21 @@ peek = nextIs "Unrecognised token" (const True)
 ||| Succeeds if running the predicate on the next token returns Just x,
 ||| returning x. Otherwise fails.
 export %inline
-terminal : String -> (WithBounds tok -> Maybe a) -> Grammar tok True a
+terminal : String -> (tok -> Maybe a) -> Grammar tok True a
 terminal = Terminal
 
 ||| Always fail with a message
 export %inline
 fail : String -> Grammar tok c ty
-fail = Fail False
+fail = Fail Nothing False
 
 export %inline
 fatalError : String -> Grammar tok c ty
-fatalError = Fail True
+fatalError = Fail Nothing True
+
+export %inline
+fatalLoc : Bounds -> String -> Grammar tok c ty
+fatalLoc b = Fail (Just b) True
 
 ||| Catch a fatal error
 export %inline
@@ -240,85 +246,87 @@ export %inline
 bounds : Grammar tok c ty -> Grammar tok c (WithBounds ty)
 bounds = Bounds
 
+export %inline
+position : Grammar tok False Bounds
+position = Position
+
 data ParseResult : Type -> Type -> Type where
      Failure : (committed : Bool) -> (fatal : Bool) ->
-               (err : String) -> (rest : List (WithBounds tok)) -> ParseResult tok ty
+               (err : String) -> (location : Maybe Bounds) -> ParseResult tok ty
      Res : (committed : Bool) ->
            (val : WithBounds ty) -> (more : List (WithBounds tok)) -> ParseResult tok ty
 
-mutual
-  doParse : (commit : Bool) ->
-            (act : Grammar tok c ty) ->
-            (xs : List (WithBounds tok)) ->
-            ParseResult tok ty
-  doParse com (Empty val) xs = Res com (irrelevantBounds val) xs
-  doParse com (Fail fatal str) xs = Failure com fatal str xs
-  doParse com (Try g) xs = case doParse com g xs of
-    -- recover from fatal match but still propagate the 'commit'
-    Failure com _ msg ts => Failure com False msg ts
-    res => res
-  doParse com Commit xs = Res True (irrelevantBounds ()) xs
-  doParse com (MustWork g) xs =
-    case assert_total (doParse com g xs) of
-         Failure com' _ msg ts => Failure com' True msg ts
-         res => res
-  doParse com (Terminal err f) [] = Failure com False "End of input" []
-  doParse com (Terminal err f) (x :: xs) =
-    case f x of
-         Nothing => Failure com False err (x :: xs)
-         Just a => Res com (const a <$> x) xs
-  doParse com EOF [] = Res com (irrelevantBounds ()) []
-  doParse com EOF (x :: xs) = Failure com False "Expected end of input" (x :: xs)
-  doParse com (NextIs err f) [] = Failure com False "End of input" []
-  doParse com (NextIs err f) (x :: xs)
-        = if f x
-             then Res com (removeIrrelevance x) (x :: xs)
-             else Failure com False err (x :: xs)
-  doParse com (Alt {c1} {c2} x y) xs
-      = case doParse False x xs of
-             Failure com' fatal msg ts
-                => if com' || fatal
-                          -- If the alternative had committed, don't try the
-                          -- other branch (and reset commit flag)
-                     then Failure com fatal msg ts
-                     else assert_total (doParse False y xs)
--- Successfully parsed the first option, so use the outer commit flag
-             Res _ val xs => Res com val xs
-  doParse com (SeqEmpty act next) xs
-      = case assert_total (doParse com act xs) of
-             Failure com fatal msg ts => Failure com fatal msg ts
-             Res com v xs =>
-               case assert_total (doParse com (next v.val) xs) of
-                    Failure com' fatal msg ts => Failure com' fatal msg ts
-                    Res com' v' xs => Res com' (mergeBounds v v') xs
-  doParse com (SeqEat act next) xs
-      = case assert_total (doParse com act xs) of
-             Failure com fatal msg ts => Failure com fatal msg ts
-             Res com v xs =>
-                   case assert_total (doParse com (next v.val) xs) of
-                        Failure com' fatal msg ts => Failure com' fatal msg ts
-                        Res com' v' xs => Res com' (mergeBounds v v') xs
-  doParse com (ThenEmpty act next) xs
-      = case assert_total (doParse com act xs) of
-             Failure com fatal msg ts => Failure com fatal msg ts
-             Res com v xs =>
-               case assert_total (doParse com next xs) of
-                    Failure com' fatal msg ts => Failure com' fatal msg ts
-                    Res com' v' xs => Res com' (mergeBounds v v') xs
-  doParse com (ThenEat act next) xs
-      = case assert_total (doParse com act xs) of
-             Failure com fatal msg ts => Failure com fatal msg ts
-             Res com v xs =>
-                   case assert_total (doParse com next xs) of
-                        Failure com' fatal msg ts => Failure com' fatal msg ts
-                        Res com' v' xs => Res com' (mergeBounds v v') xs
-  doParse com (Bounds act) xs
-      = case assert_total (doParse com act xs) of
-             Failure com fatal msg ts => Failure com fatal msg ts
-             Res com v xs => Res com (const v <$> v) xs
+mergeWith : WithBounds ty -> ParseResult tok sy -> ParseResult tok sy
+mergeWith x (Res committed val more) = Res committed (mergeBounds x val) more
+mergeWith x v = v
+
+doParse : (commit : Bool) ->
+          (act : Grammar tok c ty) ->
+          (xs : List (WithBounds tok)) ->
+          ParseResult tok ty
+doParse com (Empty val) xs = Res com (irrelevantBounds val) xs
+doParse com (Fail location fatal str) xs = Failure com fatal str (maybe (bounds <$> head' xs) Just location)
+doParse com (Try g) xs = case doParse com g xs of
+  -- recover from fatal match but still propagate the 'commit'
+  Failure com _ msg ts => Failure com False msg ts
+  res => res
+doParse com Commit xs = Res True (irrelevantBounds ()) xs
+doParse com (MustWork g) xs =
+  case assert_total (doParse com g xs) of
+       Failure com' _ msg ts => Failure com' True msg ts
+       res => res
+doParse com (Terminal err f) [] = Failure com False "End of input" Nothing
+doParse com (Terminal err f) (x :: xs) =
+  case f x.val of
+       Nothing => Failure com False err (Just x.bounds)
+       Just a => Res com (const a <$> x) xs
+doParse com EOF [] = Res com (irrelevantBounds ()) []
+doParse com EOF (x :: xs) = Failure com False "Expected end of input" (Just x.bounds)
+doParse com (NextIs err f) [] = Failure com False "End of input" Nothing
+doParse com (NextIs err f) (x :: xs)
+      = if f x.val
+           then Res com (removeIrrelevance x) (x :: xs)
+           else Failure com False err (Just x.bounds)
+doParse com (Alt {c1} {c2} x y) xs
+    = case doParse False x xs of
+           Failure com' fatal msg ts
+              => if com' || fatal
+                        -- If the alternative had committed, don't try the
+                        -- other branch (and reset commit flag)
+                   then Failure com fatal msg ts
+                   else assert_total (doParse False y xs)
+           -- Successfully parsed the first option, so use the outer commit flag
+           Res _ val xs => Res com val xs
+doParse com (SeqEmpty act next) xs
+    = case assert_total (doParse com act xs) of
+           Failure com fatal msg ts => Failure com fatal msg ts
+           Res com v xs =>
+             mergeWith v (assert_total $ doParse com (next v.val) xs)
+doParse com (SeqEat act next) xs
+    = case assert_total (doParse com act xs) of
+           Failure com fatal msg ts => Failure com fatal msg ts
+           Res com v xs =>
+             mergeWith v (assert_total $ doParse com (next v.val) xs)
+doParse com (ThenEmpty act next) xs
+    = case assert_total (doParse com act xs) of
+           Failure com fatal msg ts => Failure com fatal msg ts
+           Res com v xs =>
+             mergeWith v (assert_total $ doParse com next xs)
+doParse com (ThenEat act next) xs
+    = case assert_total (doParse com act xs) of
+           Failure com fatal msg ts => Failure com fatal msg ts
+           Res com v xs =>
+             mergeWith v (assert_total $ doParse com next xs)
+doParse com (Bounds act) xs
+    = case assert_total (doParse com act xs) of
+           Failure com fatal msg ts => Failure com fatal msg ts
+           Res com v xs => Res com (const v <$> v) xs
+doParse com Position [] = Failure com False "End of input" Nothing
+doParse com Position (x :: xs)
+    = Res com (irrelevantBounds x.bounds) (x :: xs)
 
 public export
-data ParsingError tok = Error String (List (WithBounds tok))
+data ParsingError tok = Error String (Maybe Bounds)
 
 ||| Parse a list of tokens according to the given grammar. If successful,
 ||| returns a pair of the parse result and the unparsed tokens (the remaining

src/Parser/Lexer/Package.idr

@@ -121,7 +121,7 @@ lex : String -> Either (Int, Int, String) (List (WithBounds Token))
 lex str =
   case lexTo (const False) rawTokens str of
        (tokenData, (l, c, "")) =>
-         Right $ (filter (useful . val) tokenData) ++ [MkBounded EndOfInput False l c l c]
+         Right $ (filter (useful . val) tokenData) ++ [MkBounded EndOfInput False (MkBounds l c l c)]
        (_, fail) => Left fail
   where
     useful : Token -> Bool

src/Parser/Lexer/Source.idr

@@ -358,7 +358,7 @@ lexTo reject str
            -- Add the EndInput token so that we'll have a line and column
            -- number to read when storing spans in the file
            (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
-                                      [MkBounded EndInput False l c l c])
+                                      [MkBounded EndInput False (MkBounds l c l c)])
            (_, fail) => Left fail
     where
       notComment : WithBounds Token -> Bool

src/Parser/Rule/Common.idr

@@ -15,25 +15,12 @@ EmptyRule token ty = Grammar token False ty
 
 export
 location : {token : _} -> EmptyRule token (Int, Int)
-location
-    = do tok <- removeIrrelevance <$> bounds peek
-         pure $ start tok
+location = startBounds <$> position
 
 export
 endLocation : {token : _} -> EmptyRule token (Int, Int)
-endLocation
-    = do tok <- removeIrrelevance <$> bounds peek
-         pure $ end tok
-
-export
-position : {token : _} -> EmptyRule token ((Int, Int), (Int, Int))
-position
-    = do tok <- removeIrrelevance <$> bounds peek
-         pure (start tok, end tok)
-
+endLocation = endBounds <$> position
 
 export
 column : {token : _ } -> EmptyRule token Int
-column
-    = do (line, col) <- location
-         pure col
+column = snd <$> location

src/Parser/Rule/Package.idr

@@ -20,63 +20,63 @@ PackageEmptyRule = EmptyRule Token
 export
 equals : Rule ()
 equals = terminal "Expected equals"
-                      (\x => case x.val of
+                      (\x => case x of
                                   Equals => Just ()
                                   _ => Nothing)
 
 export
 lte : Rule ()
 lte = terminal "Expected <="
-                      (\x => case x.val of
+                      (\x => case x of
                                   LTE => Just ()
                                   _ => Nothing)
 
 export
 gte : Rule ()
 gte = terminal "Expected >="
-                      (\x => case x.val of
+                      (\x => case x of
                                   GTE => Just ()
                                   _ => Nothing)
 
 export
 lt : Rule ()
 lt = terminal "Expected <="
-                      (\x => case x.val of
+                      (\x => case x of
                                   LT => Just ()
                                   _ => Nothing)
 
 export
 gt : Rule ()
 gt = terminal "Expected >="
-                      (\x => case x.val of
+                      (\x => case x of
                                   GT => Just ()
                                   _ => Nothing)
 
 export
 eqop : Rule ()
 eqop = terminal "Expected =="
-                      (\x => case x.val of
+                      (\x => case x of
                                   EqOp => Just ()
                                   _ => Nothing)
 
 export
 andop : Rule ()
 andop = terminal "Expected &&"
-                      (\x => case x.val of
+                      (\x => case x of
                                   AndOp => Just ()
                                   _ => Nothing)
 
 export
 eoi : Rule ()
 eoi = terminal "Expected end of input"
-               (\x => case x.val of
+               (\x => case x of
                            EndOfInput => Just ()
                            _ => Nothing)
 
 export
 exactProperty : String -> Rule String
 exactProperty p = terminal ("Expected property " ++ p)
-                           (\x => case x.val of
+                           (\x => case x of
                                        DotSepIdent Nothing p' =>
                                          if p == p' then Just p
                                          else Nothing
@@ -85,35 +85,35 @@ exactProperty p = terminal ("Expected property " ++ p)
 export
 stringLit : Rule String
 stringLit = terminal "Expected string"
-                     (\x => case x.val of
+                     (\x => case x of
                                  StringLit str => Just str
                                  _ => Nothing)
 
 export
 integerLit : Rule Integer
 integerLit = terminal "Expected integer"
-                     (\x => case x.val of
+                     (\x => case x of
                                  IntegerLit i => Just i
                                  _ => Nothing)
 
 export
 namespacedIdent : Rule (Maybe Namespace, String)
 namespacedIdent = terminal "Expected namespaced identifier"
-                           (\x => case x.val of
+                           (\x => case x of
                                        DotSepIdent ns n => Just (ns, n)
                                        _ => Nothing)
 
 export
 moduleIdent : Rule ModuleIdent
 moduleIdent = terminal "Expected module identifier"
-                       (\x => case x.val of
+                       (\x => case x of
                                    DotSepIdent ns m => Just $ nsAsModuleIdent (mkNestedNamespace ns m)
                                    _ => Nothing)
 
 export
 packageName : Rule String
 packageName = terminal "Expected package name"
-                       (\x => case x.val of
+                       (\x => case x of
                                    DotSepIdent Nothing str =>
                                      if isIdent AllowDashes str then Just str
                                      else Nothing
@@ -122,13 +122,13 @@ packageName = terminal "Expected package name"
 export
 dot' : Rule ()
 dot' = terminal "Expected dot"
-                (\x => case x.val of
+                (\x => case x of
                             Dot => Just ()
                             _ => Nothing)
 
 sep' : Rule ()
 sep' = terminal "Expected separator"
-                (\x => case x.val of
+                (\x => case x of
                             Separator => Just ()
                             _ => Nothing)
 

src/Parser/Rule/Source.idr

@@ -21,7 +21,7 @@ SourceEmptyRule = EmptyRule Token
 
 export
 eoi : SourceEmptyRule ()
-eoi = do ignore $ nextIs "Expected end of input" (isEOI . val)
+eoi = ignore $ nextIs "Expected end of input" isEOI
   where
     isEOI : Token -> Bool
     isEOI EndInput = True
@@ -31,7 +31,7 @@ export
 constant : Rule Constant
 constant
     = terminal "Expected constant"
-               (\x => case x.val of
+               (\x => case x of
                            CharLit c => case getCharLit c of
                                              Nothing => Nothing
                                              Just c' => Just (Ch c')
@@ -50,7 +50,7 @@ constant
 
 documentation' : Rule String
 documentation' = terminal "Expected documentation comment"
-                          (\x => case x.val of
+                          (\x => case x of
                                       DocComment d => Just d
                                       _ => Nothing)
 
@@ -62,7 +62,7 @@ export
 intLit : Rule Integer
 intLit
     = terminal "Expected integer literal"
-               (\x => case x.val of
+               (\x => case x of
                            IntegerLit i => Just i
                            _ => Nothing)
 
@@ -70,7 +70,7 @@ export
 onOffLit : Rule Bool
 onOffLit
     = terminal "Expected on or off"
-               (\x => case x.val of
+               (\x => case x of
                            Ident "on" => Just True
                            Ident "off" => Just False
                            _ => Nothing)
@@ -79,7 +79,7 @@ export
 strLit : Rule String
 strLit
     = terminal "Expected string literal"
-               (\x => case x.val of
+               (\x => case x of
                            StringLit n s => escape n s
                            _ => Nothing)
 
@@ -88,7 +88,7 @@ export
 strLitLines : Rule (List1 String)
 strLitLines
     = terminal "Expected string literal"
-               (\x => case x.val of
+               (\x => case x of
                            StringLit n s => traverse (escape n . fastPack)
                                                      (splitAfter isNL (fastUnpack s))
                            _ => Nothing)
@@ -96,35 +96,35 @@ strLitLines
 export
 strBegin : Rule ()
 strBegin = terminal "Expected string begin"
-               (\x => case x.val of
+               (\x => case x of
                            StringBegin False => Just ()
                            _ => Nothing)
 
 export
 multilineBegin : Rule ()
 multilineBegin = terminal "Expected multiline string begin"
-               (\x => case x.val of
+               (\x => case x of
                            StringBegin True => Just ()
                            _ => Nothing)
 
 export
 strEnd : Rule ()
 strEnd = terminal "Expected string end"
-               (\x => case x.val of
+               (\x => case x of
                            StringEnd => Just ()
                            _ => Nothing)
 
 export
 interpBegin : Rule ()
 interpBegin = terminal "Expected string interp begin"
-               (\x => case x.val of
+               (\x => case x of
                            InterpBegin => Just ()
                            _ => Nothing)
 
 export
 interpEnd : Rule ()
 interpEnd = terminal "Expected string interp end"
-               (\x => case x.val of
+               (\x => case x of
                            InterpEnd => Just ()
                            _ => Nothing)
 
@@ -135,7 +135,7 @@ simpleStr = strBegin *> commit *> (option "" strLit) <* strEnd
 export
 aDotIdent : Rule String
 aDotIdent = terminal "Expected dot+identifier"
-               (\x => case x.val of
+               (\x => case x of
                            DotIdent s => Just s
                            _ => Nothing)
 
@@ -147,7 +147,7 @@ export
 symbol : String -> Rule ()
 symbol req
     = terminal ("Expected '" ++ req ++ "'")
-               (\x => case x.val of
+               (\x => case x of
                            Symbol s => if s == req then Just ()
                                                    else Nothing
                            _ => Nothing)
@@ -156,7 +156,7 @@ export
 keyword : String -> Rule ()
 keyword req
     = terminal ("Expected '" ++ req ++ "'")
-               (\x => case x.val of
+               (\x => case x of
                            Keyword s => if s == req then Just ()
                                                     else Nothing
                            _ => Nothing)
@@ -165,7 +165,7 @@ export
 exactIdent : String -> Rule ()
 exactIdent req
     = terminal ("Expected " ++ req)
-               (\x => case x.val of
+               (\x => case x of
                            Ident s => if s == req then Just ()
                                       else Nothing
                            _ => Nothing)
@@ -174,7 +174,7 @@ export
 pragma : String -> Rule ()
 pragma n =
   terminal ("Expected pragma " ++ n)
-    (\x => case x.val of
+    (\x => case x of
       Pragma s =>
         if s == n
           then Just ()
@@ -185,7 +185,7 @@ export
 operator : Rule Name
 operator
     = terminal "Expected operator"
-               (\x => case x.val of
+               (\x => case x of
                            Symbol s =>
                                 if s `elem` reservedSymbols
                                    then Nothing
@@ -195,7 +195,7 @@ operator
 identPart : Rule String
 identPart
     = terminal "Expected name"
-               (\x => case x.val of
+               (\x => case x of
                            Ident str => Just str
                            _ => Nothing)
 
@@ -203,7 +203,7 @@ export
 namespacedIdent : Rule (Maybe Namespace, String)
 namespacedIdent
     = terminal "Expected namespaced name"
-        (\x => case x.val of
+        (\x => case x of
             DotSepIdent ns n => Just (Just ns, n)
             Ident i => Just (Nothing, i)
             _ => Nothing)
@@ -216,7 +216,7 @@ export
 moduleIdent : Rule ModuleIdent
 moduleIdent
     = terminal "Expected module identifier"
-        (\x => case x.val of
+        (\x => case x of
             DotSepIdent ns n => Just (mkModuleIdent (Just ns) n)
             Ident i => Just (mkModuleIdent Nothing i)
             _ => Nothing)
@@ -229,7 +229,7 @@ export
 holeName : Rule String
 holeName
     = terminal "Expected hole name"
-               (\x => case x.val of
+               (\x => case x of
                            HoleIdent str => Just str
                            _ => Nothing)
 
@@ -348,7 +348,7 @@ export
 atEnd : (indent : IndentInfo) -> SourceEmptyRule ()
 atEnd indent
     = eoi
-  <|> do ignore $ nextIs "Expected end of block" (isTerminator . val)
+  <|> do ignore $ nextIs "Expected end of block" isTerminator
   <|> do col <- Common.column
          if (col <= indent)
             then pure ()

src/Parser/Support.idr

@@ -30,11 +30,11 @@ fromLexError fname (_, l, c, _)
 
 export
 fromParsingError : (Show token, Pretty token) => String -> ParsingError token -> Error
-fromParsingError fname (Error msg []) = ParseFail {token=token} (MkFC fname (0, 0) (0, 0)) (msg +> '.') []
-fromParsingError fname (Error msg (t::ts))
+fromParsingError fname (Error msg Nothing) = ParseFail (MkFC fname (0, 0) (0, 0)) (msg +> '.')
+fromParsingError fname (Error msg (Just t))
     = let l = t.startLine
           c = t.startCol in
-          ParseFail (MkFC fname (l, c) (l, c + 1)) (msg +> '.') (val <$> (t :: ts))
+          ParseFail (MkFC fname (l, c) (l, c + 1)) (msg +> '.')
 
 export
 hex : Char -> Maybe Int

tests/idris2/perror007/expected

@@ -82,11 +82,10 @@ StrError10.idr:3:1--3:2
 1/1: Building StrError11 (StrError11.idr)
 Error: Multi-line string is expected to begin with """.
 
-StrError11.idr:3:5--3:6
+StrError11.idr:2:7--2:8
  1 | foo : String
  2 | foo = "a
- 3 |     "
-         ^
+           ^
 
 1/1: Building StrError12 (StrError12.idr)
 Error: While processing multi-line string. Line is less indented than the closing delimiter.