[Haskell-cafe] How to do reversible parsing?

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Wed Jan 6 20:26:14 UTC 2021

> (unfortunately) nobody cares that reversible parsing actually works.

Well what about
is this not "caring for reversibility"? (in a similar context)

> we cannot be sure about determinism

Assume you come up with a deterministic grammar for Isabelle (say).
How do you want to be sure it is the right one?

Would it not be a good idea to use the given grammar
(extract from sources of tools, e.g.,
- this is already a combinator parser? or from
specification/documentation, e.g.,
http://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf ?)

Best regards, J.

NB: full Isabelle seems quite the challenge to parse: isar-ref 8.4.5
"... parsing may be ambiguous. Isabelle lets the Earley parser
enumerate all possible parse trees... Terms that cannot be
type-checked are filtered out. Unlike regular type reconstruction, ...
the filtering stage only ..."

More information about the Haskell-Cafe mailing list