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:
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-
$pstatements that are in scope for that statement. - Skip (that is, don't try to parse) syntax-related statements:
$fstatements;- statements whose expression starts with
TOP; $astatements 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...)
marnix
