[Haskell-cafe] How to do reversible parsing?

[Johannes Waldmann]

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

Well what about
https://github.com/kolmodin/binary/blob/master/tests/QC.hs#L50
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.,
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Pure/Isar/parse_spec.ML
- 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 ..."