Hello Mario I just wrote a (multi-target pure kotlin) antlr parser for parsing mm0 files. It is buggy, at the moment because it seems that there is an issue with the antlr-kotlin project (that I have reported) with EOF) but It still parses everything except peano.mm0 and x86.mm0
I had to taylor the grammar that you described in mm0.md to antlr and I expect to have made a few errors (I know I have made one with the way I fetch MathString). But I'll soon fix everything. Once I do, I'll publish the antlr grammar file. mm0.md was a great help, I understand a bit more of mm0 and I expect to understand even more soon, once I play with it. Please, could you send me your translated file for set.mm ? (I tried seting up haskell on my computer and to translate it myself and finally gave up... also, I have really no use for Haskell) I'll soon start to write the secondary mm0 parser for math strings. Do you have any advice about it, that could help me ? Also, on another subject : I build Mephistolus for the browser target but there are issues in the transpiling process from kotlin to javascript. I fixed some of them but at this point the app launches but there are (bloody silent javascript) exceptions when I try to reduce statements So I have some more debugging to do (meanwhile I take a pause by looking at mm0 ^^). Best regards, Olivier Le mercredi 22 janvier 2020 22:33:58 UTC+1, Mario Carneiro a écrit : > > > > On Wed, Jan 22, 2020 at 10:51 AM Olivier Binda <[email protected] > <javascript:>> wrote: > >> 5) Mm0 >> a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking >> at you... >> b) parse set.mm0 >> c) extract a list of all mm0 ids >> d) write a parser for mm0 statements >> e) make the mephistolus Statement able to be build on mm0 stuff >> > > I can send you the translated set.mm0 file (or you can run mm0-hs yourself > to perform the translation), but I don't think it is necessarily > representative of the things you will normally find in an MM0 file. It has > no "def"s, for example, because set.mm uses axioms for definitions and > the translator doesn't yet know enough to derive the equivalent def > statement. A more representative sample is peano.mm0. If you want to parse > theorems in set.mm, then the simplest way to get these is to read set.mm > rather than translating it first. > > There are also tools for reading an MM0 file and turning it into an .mmu > file, which has all statements and proofs written as s-expressions. This is > probably much easier to parse, although it can get a bit big. > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/21cda884-6877-4528-9d69-223c558b545e%40googlegroups.com.
