Languages, grammars, parsers... :thinking:

Stream: new members

[Ilmārs Cīrulis]

Suppose I define inductive structure for basic logical expression of two boolean variables (A and B, operations AND, OR, IMPLIES, etc.). They have precedence levels and sometimes associativity (left or right) that allows to skip brackets sometimes, if one wants.

Converting from this inductive type to string, taking precedence levels and associativity into account, - that I could manage somehow, I believe. But it seems harder to do the opposite direction - from a string to inductive type.

Is there anything related to this problem (how to write parsers with, ideally, proven correctness or something like that) in Lean?

[Eric Wieser]

Converting from this inductive type to string, taking precedence levels and associativity into account, - that I could manage somehow, I believe.

docs#Repr.reprPrec tries to give you the machinery to do this

[Eric Wieser]

Is there anything related to this problem (how to write parsers with, ideally, proven correctness or something like that) in Lean?

docs#Std.Internal.Parsec is one way, I think

[Eric Wieser]

Do you care about converting from string (command line input, a text file), or would you be happy with syntax within lean source code?

[Ilmārs Cīrulis]

Some time ago I used Javascript library nearley.js that generates parsers, but it has kinda weird way to define language/grammar. (To make a tiny html page that generates Venn diagram of the two variable logical expression. :D)

[Ilmārs Cīrulis]

Converting from the string.

[Ilmārs Cīrulis]

I should take myself to some library and get necessary literature to learn basics and maybe more, probably.

[Eric Wieser]

I think the standard library is enough for you here, as linked above

[Ilmārs Cīrulis]

One weird idea/goal is to make a parser, prove it correct and then "extract" to Javascript, where I can use it on the web.

[Ilmārs Cīrulis]

That's #xy problem (I believe now), because I find it difficult to make an BNF for expressions which are made of operators with different precedence levels and some with specific associativity. So, I thought that it would be nice to find a way to do it automatically, then I daydreamed even further. :sweat_smile: