On Tue, Aug 17, 2021 at 4:46 AM Thierry Arnoux <[email protected]> wrote:
> 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 > *. * > > For this "outer parser", you should probably retain the distinction between a string (and store the decoded contents of the string), and a keyword (and store the literal text of the keyword), in an enum. The spec is ambiguous about what a "keyword" is (assuming there is no additional text in the spec on that topic) but I interpret it as an identifier (i.e. something that could be an MM label). Here ( https://github.com/digama0/mm0/blob/master/mm0-hs/src/MM0/FromMM/Parser.hs#L319-L343) is the outer $j parser I wrote for MM0, and it tokenizes into the "Keyword(String)", "String(String)" and "Semi" variants, where identifiers are lexed using the built in haskell lexer (which is approximate, but should yield roughly the same results as MM label identifiers, with the exception that MM thinks 0fin is an identifier while most programming languages disagree). Mario -- 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/CAFXXJSsAqBFQWy1LsXx0GOxwj6pQ%2B84C%2B5tzvP9YO4ygx9HUDw%40mail.gmail.com.
