Re: [mizar] Question on Mizar grammar

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi Josef,

> Trying to reverse-engineer the Mizar parser is a bit dangerous - see e.g.
> http://mizar.uwb.edu.pl/forum/archive/0208/msg00043.html,
> http://www.uclic.ucl.ac.uk/usr/jgow/papers/parsing.ps.gz, and
> http://www.uclic.ucl.ac.uk/people/j.gow/papers/alcor-jar.pdf .
Thanks for the pointers, though I have already read the parsing.ps.
I have used both JavaCC and AntLR parser generators in real projects (as part 
of my main work)  but it seems to me that these tools are not suited for 
dealing with Mizar language.

So, I thought about the following alternatives:
1. Use Earley algoritm or GLR, may be with
   ordered CFG in order to generate AST: 
http://www.cis.upenn.edu/~stse/javac/ocfg.pdf
2. Hand-written parser.

Now I am trying the second approach...

> If you just want to parse Mizar in order to do some research about MML, it
> may be much more convenient to use the XML files produced by the Mizar
> parser itself.
At first I want to get deeper understanding of Mizar language, so I am going 
to concentrate on the parser.
About using  XML files produced by the Mizar:
All my Mizar related work will be in public domain, hence the question: 
May I freely use these files? Are there any licensing problems?

> On the other hand, I also think that having Mizar rewritten in a
> high-level language like OCaml would be useful.
My first goal is to create the working parser. I assume it will take 2-3 
months.

> Btw., Andrzej Trybulec 
> wrote me a month ago that "he agrees that Mizar should be open-source", so
> I hope it will happen soon and make such reimplementations easier.
Sounds interesting!

Michael Nedzelsky