Warning: Hacked-up code ahead. (But it seems to work...)

What it does

This demonstrates an idea which I posted about several times on the Metamath mailing list [email protected]. Here are links into the Google Groups archive:

• Automated Metamath ambiguity checking
• New marker: "this database is unambiguous"
• Minimalist Metamath

The parsing algorithm only assumes there is a ... $a TOP xyzzy ... $. axiom for each typecode; and that the syntax is expressed in typecodes that start with a lowercase letter (like wff, setvar, and class).

Apart from these new 'syntax axioms', nothing new is needed: no Metamath language extensions, and no $j comments for syntax, garden_path, type_conversions (which metamath-knife relies on).

The algorithm works as follows:

• For every statement expression like |- x y z z y,
• find the unique proof for TOP |- x y z z y
• which uses only the non-$p statements that are in scope for that statement.
• Skip (that is, don't try to parse) syntax-related statements:
  • $f statements;
  • statements whose expression starts with TOP;
  • $a statements whose typecode starts with a lowercase letter.

Each such proof is the parse tree for that statement's expression.

As far as I can see, this works for all of current set.mm and iset.mm.

How to use

Make sure you have a recent Python version. (Tested with 3.8, 3.3+ might work.)

Download a Metamath .mm file, like set.mm.

Extend that .mm file with a ... $a TOP xyzzy ... $. axiom for each typecode, for example by applying set.mm.patch.

Run parseit, for example ./parseit -i set.mm. (This creates a virtual environment.) (The parseit bash script is for UNIX-y systems. On other systems, run the equivalent manually, with or without using a Python virtual environment.)

Enjoy the parsed formulas rolling over your screen. (And observe how statements like opelopabt

|- ( ( A. x A. y ( x = A -> ( ph <-> ps ) ) /\ A. x A. y ( y = B -> ( ps <-> ch ) ) /\ ( A e. V /\ B e. W ) ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )

make it sweat...)