argumentcomputer / Megaparsec.lean

Lean 4 port of Megaparsec
MIT License
22 stars 4 forks source link

Usability: Duplicated errors shouldn't be reported #11

Closed cognivore closed 2 years ago

cognivore commented 2 years ago

Why?

A degenerate example of us using List for error reporting would be the following parser application:

p = string "123"
Parsec.run "-" (p <|> p <|> p) "322"

The reference implementation of megaparsec is using Sets for error reporting, thus will report "Failed to parse line 1 symbol 1: found '3, expected '1". Our parser will report: "Failed to parse line 1 symbol 1: found '3, expected '1. Failed to parse line 1 symbol 1: found '3, expected '1. Failed to parse line 1 symbol 1: found '3, expected '1.".

How?