<div dir="ltr"><div>You may be interested in the profunctor technique of bidirectional parsing/serialisation, a basic version of which is implemented in the ‘codec’ package: <<a href="https://hackage.haskell.org/package/codec">https://hackage.haskell.org/package/codec</a>>. It was originally intended for binary and textual data formats, but could be used for a conventional textual language as well. I have also used this technique at work to develop a similar library, and found it quite effective & performant once you get the (somewhat delicate) internals correct.<br></div><div><br></div><div> As you suggest, it’s generally not feasible to have “encode linearity” (‘decode . encode = id’; printing omits no information from output) and “decode linearity” (‘encode . decode = id’; parsing discards no info from input). However, it’s worth verifying both “encode preservation” (‘encode . decode . encode = encode’; parsing preserves all info that printing does) and “decode preservation” (‘decode . encode . decode = decode’; printing preserves all info that parsing does).<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jan 2, 2021 at 4:02 PM Askar Safin via Haskell-Cafe <<a href="mailto:haskell-cafe@haskell.org">haskell-cafe@haskell.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi. How to do deterministic reversible parsing in Haskell? Please, point me to some libs or tools.<br>
Or give some advice on how to write such lib or tool. (Also, I am interested in solutions for C or C++.)<br>
<br>
Now let me explain my task in detail.<br>
<br>
I am interested in formal math. I am going to develop various proof checkers. In particular, I want<br>
to develop my PTS checker ( <a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="noreferrer" target="_blank">https://en.wikipedia.org/wiki/Pure_type_system</a> ). Here is example of<br>
existing PTS checker: <a href="http://web.archive.org/web/20180924133846/http://www.cs.kun.nl/~janz/yarrow/" rel="noreferrer" target="_blank">http://web.archive.org/web/20180924133846/http://www.cs.kun.nl/~janz/yarrow/</a> .<br>
Here is example of input this checker accepts (taken from manual):<br>
<br>
Var (+) : Nat -> Nat -> Nat<br>
Def double := \x:Nat. x+x<br>
Def S := (+) one<br>
<br>
Also, I want to develop something similar to Isabelle ( <a href="https://isabelle.in.tum.de/" rel="noreferrer" target="_blank">https://isabelle.in.tum.de/</a> ). Example of<br>
Isabelle input: <a href="https://isabelle.in.tum.de/dist/library/HOL/HOL/HOL.html" rel="noreferrer" target="_blank">https://isabelle.in.tum.de/dist/library/HOL/HOL/HOL.html</a> .<br>
<br>
Also, I am going to write converters between various languages. For example, between input for some<br>
existing PTS checker and my PTS checker.<br>
<br>
In short, I want to write lot of parsers and pretty-printers for various languages. And thus I need<br>
some parsing solution.<br>
<br>
The solution should have the following features:<br>
<br>
1. The parsing should be divided into lexing and parsing. I. e. usual lex + yacc model. Parsing should<br>
be done using usual context-free grammars (CFGs). Left-recursive grammars should be supported (this<br>
leaves out parser combinator libraries). All languages I am going to deal with fit this model. I. e.<br>
I will deal with simple to parse languages, such as Pascal. Not complex ones, like C or C++.<br>
<br>
2. Parsing should be deterministic. I. e. parser should check that CFG is unambiguous. Yes, I know<br>
that this task is impossible to do on Turing machine. But at very least some partial solution will<br>
go. For example, some algorithm, which will check that some reasonable set of CFGs is deterministic.<br>
Or even brute force up to some limit will go. (Yes, this will not give absolutely correct results,<br>
but this will go.) This is example of grammar for PTS in one of my checkers (start symbol is t0):<br>
<br>
t1000 = id<br>
t1000 = "(" t0")"<br>
t999 = t999 t1000<br>
t3 = t4 "::" t3<br>
t3 = "%" id "::" t0 "." t3<br>
t0 = "!!" id "::" t0 "." t0<br>
t1 = t2 "==>" t1<br>
t0 = t1<br>
t1 = t2<br>
t2 = t3<br>
t3 = t4<br>
t4 = t999<br>
t999 = t1000<br>
<br>
If I remember correctly, this grammar is deterministic (checked using brute force up to a limit).<br>
I want solution which will verify that this grammar is deterministic.<br>
<br>
All stages of parsing should be proved as deterministic (i. e. scanner too).<br>
<br>
3. Parsing should be reversible. I. e. pretty-printing should be supported, too. And the tool should<br>
guarantee that parsing and pretty-printing match. Now let me give more precise definition. Let's<br>
assume we have these functions:<br>
<br>
parse :: String -> Maybe X<br>
print :: X -> Maybe String<br>
<br>
As you can see, not every internal representation is printable. This is OK. For example, if internal<br>
representation contains variable names that happen to equal reserved words, then, of course, this is<br>
unprintable representation.<br>
<br>
The tool should guarantee that:<br>
a. Result of parsing should be printable, but printing not necessary should give same string. I. e.<br>
if "parse s == Just x", then "print x /= Nothing". (But not necessary "print x == Just s".)<br>
b. Parsing of result of printing should give same representation. I. e. if "print x == Just s", then<br>
"parse s == Just x"<br>
<br>
4. Not only parsing should generate parse tree (i. e. exact representation of derivation), but also<br>
AST. AST differs from parse tree. For example, AST should not contain braces. I. e. "2 + (3 * 4)" and<br>
"2 + 3 * 4" should give same AST. And the tool should be able parse string to AST and pretty print<br>
AST back to string.<br>
<br>
5. It should be possible to use CFG not known in compile time. Consider Isabelle language. Here is<br>
again example of Isabelle text: <a href="https://isabelle.in.tum.de/dist/library/HOL/HOL/HOL.html" rel="noreferrer" target="_blank">https://isabelle.in.tum.de/dist/library/HOL/HOL/HOL.html</a> . As you can<br>
see the language is divided into inner language and outer language. Strings in inner language are<br>
quoted. Outer language can add productions to inner language. Inner language cannot change itself.<br>
"notation" and "translations" commands add productions to inner language. So inner language is not<br>
known beforehand, it is created dynamically. There is no need to dynamically create scanner, i. e.<br>
it should be possible to dynamically create parser (for inner language), but there is no such<br>
requirement for scanner. Also, parser will not change in the middle of parsing given string.<br>
<br>
Again: let's assume I write parser for my Isabelle analog. Scanner and parser for outer language is<br>
fixed. Scanner for inner language is fixed, too. But parser for inner language is not. I read input<br>
document and add productions to CFG of inner language on the fly. Every time I add production,<br>
resulting CFG should be checked for ambiguity. And when I find inner language string in input, I<br>
process it using just constructed parser for inner language.<br>
<br>
--<br>
<br>
Points 2 and 3 are the most important in this list. If there is solution which contains them alone,<br>
this already will be very good.<br>
<br>
Now let me list considered solutions.<br>
<br>
* Usual combinator libraries (such as parsec) will not go. They don't work with left-recursive CFGs.<br>
They don't check grammars for ambiguities. They don't do reversible parsing. But they allow creating<br>
language on the fly, and this is good thing.<br>
<br>
* Happy and alex will not go. As well as I know Happy can prove unambiguity of some very simple grammars<br>
(i. e. for some set of simple grammars it will not report any conflicts and thus will prove they unambiguity).<br>
It seems this is LR(1) set. But, as well as I know, Happy will report conflicts on PTS grammar given<br>
above, i. e. Happy cannot prove its unambiguity. Also, Happy and Alex cannot pretty-print. And Happy<br>
and Alex don't allow supplying CFG on the fly.<br>
<br>
* Package "earley". Handle arbitrary CFGs, including left-recursive. This is good thing. It seems CFG<br>
can be supplied in runtime. This is good thing, too. Gives all parse trees, thus we can verify that<br>
count of parse trees equals to 1. This is good thing, too. Unfortunately, earley cannot verify CFS's<br>
unambiguity before supplying input. Also, earley doesn't support pretty-printing.<br>
<br>
* PEG libraries. Will not go, I want CFGs.<br>
<br>
* I searched on Hackage reversible parsing libraries. Unfortunately, none of them guarantee<br>
reversibility. I. e. it is very easy to fool these libraries and create parsers and printers not<br>
satisfying equations I gave above. Also, this libraries doesn't have other features I mentioned<br>
<br>
* <a href="http://augeas.net/" rel="noreferrer" target="_blank">http://augeas.net/</a> is very cool project. Unlike nearly everything I found in internet, Augeas<br>
provides guaranteed reversible parsing and pretty-printing (!!!!!). Unfortunately, set of supported<br>
target languages is very limited. Regular languages are supported. And some very limited set of CFGs<br>
is supported. For example, it is possible to construct parser for JSON. But parser for Pascal seems<br>
impossible. Augeas not designed for parsing programming languages. Only simple configuration<br>
languages like JSON, XML, etc. Mutually recursive nonterminals are not supported. Also, Augeas<br>
provides C API, not Haskell one.<br>
<br>
* <a href="https://www.brics.dk/xsugar.html" rel="noreferrer" target="_blank">https://www.brics.dk/xsugar.html</a> is very good. It provides guaranteed reversible translation<br>
between arbitrary language and XML. And XSugar even verifies unambiguity of the CFG using some<br>
sophisticated algorithm. Unfortunately, this algorithm still cannot prove unambiguity of PTS grammar<br>
given above. Also, XSugar is not Haskell library. It is standalone Java app. So, I need to convert<br>
some language to XML, then load this XML to my Haskell program and parse. Also, there is similar lib<br>
<a href="https://www.brics.dk/Xact.html" rel="noreferrer" target="_blank">https://www.brics.dk/Xact.html</a> from same author, but it is for Java, not for Haskell.<br>
<br>
I was able to find only 2 projects, which do guaranteed reversible parsing: mentioned Augeas and<br>
XSugar/Xact. Unfortunately, both are not for Haskell. And both cannot prove unambiguity for my PTS<br>
grammar.<br>
<br>
So, please tell me about solution. Or give advice how to write one.<br>
<br>
Also, let me describe my experience with various algorithms for checking ambiguity of grammar.<br>
<br>
1. Try to construct LR(1) table. If there is no conflicts, then the grammar is unambiguous. It seems<br>
this is algorithm used by bison and happy. Unfortunately it is too weak and cannot prove unambiguity<br>
of my PTS grammar.<br>
2. Try to construct LR(k) table. This algorithm is stronger than LR(1). I was unable to find<br>
implementation of this algorithm in any language. I don't want to write such algorithm.<br>
3. Schmitz's algorithm. <a href="http://www.lsv.fr/~schmitz/pub/expamb.pdf" rel="noreferrer" target="_blank">http://www.lsv.fr/~schmitz/pub/expamb.pdf</a> . Even stronger than LR(k). I<br>
downloaded his bison fork. Unfortunately this bison fork can prove unambiguity for same set of<br>
grammars original bison can (i. e. LR(1)). I. e. it seems Schmitz did not implemented his algorithm.<br>
I don't want to implement his algorithm either.<br>
4. Horizontal and vertical ambiguity checking. <a href="https://www.brics.dk/grammar/kruse.pdf" rel="noreferrer" target="_blank">https://www.brics.dk/grammar/kruse.pdf</a> . This is<br>
algorithm used in XSugar. Unfortunately, it doesn't handle my PTS grammar.<br>
5. Brute force up to some limit. Doesn't give unambiguity guarantee. But I like it, and I will use<br>
it if I don't find anything else. It is the only algorithm which can handle my PTS grammar (and<br>
give enough amount of guarantee), not counting LR(k) and Schmitz's algorithm (I was not able to find<br>
implementations of both).<br>
<br>
I will try to write tool I want, I will write about my progress to this list.<br>
<br>
==<br>
Askar Safin<br>
<a href="https://github.com/safinaskar" rel="noreferrer" target="_blank">https://github.com/safinaskar</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>