Many thanks for the description of the KLR parser! I'll take the time to read and understand it!
Concerning the parsing of $j comments, I've implemented it in two steps: * a first step, which is completely agnostic of the usage, and for which I've followed the Metamath book, chapter 4.4.3 : Additional Information Comment ($j). This states: /Within an additional information comment is a sequence of one or more commands of the form command arg arg ... ; where each of the zero or more arg values can be either a quoted string or a keyword. Note that every command ends in an unquoted semicolon.// /This step does not interpret the commands, but simply saves them as list of arguments in the database. At this step, I'm removing the quotes if there were any/. / // * only in a second step does the parser, if and when it is invoked, fetch the "ambiguous_prefix" commands and interprets the arguments in its own specific way. I'm also using the "$j syntax" parser commands, to get a list of type codes, find out which one is the "provable" type code and that the final result of statements shall be wff. This way, any other part, or user of the library also has access to all parser commands, pre-processed in a very minimal way. BR, _ Thierry -- 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/af66f181-5171-3b93-bade-e530a3233640%40gmx.net.
