A quick experiment to demonstrate Metamath formula parsing, where the grammar is embedded in a few additional 'syntax axioms'.

Overview

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-$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...)

Owner
Marnix Klooster
Marnix Klooster
A Brainfuck interpreter written in Python.

A Brainfuck interpreter written in Python.

Ethan Evans 1 Dec 05, 2021
Apache Airflow - A platform to programmatically author, schedule, and monitor workflows

Apache Airflow Apache Airflow (or simply Airflow) is a platform to programmatically author, schedule, and monitor workflows. When workflows are define

The Apache Software Foundation 28.6k Dec 28, 2022
🪄 Auto-generate Streamlit UI from Pydantic Models and Dataclasses.

Streamlit Pydantic Auto-generate Streamlit UI elements from Pydantic models. Getting Started • Documentation • Support • Report a Bug • Contribution •

Lukas Masuch 103 Dec 25, 2022
Stack BOF Protection Bypass Techniques

Stack Buffer Overflow - Protection Bypass Techniques

ommadawn46 18 Dec 28, 2022
Run PD patches in NRT using Python

The files in this repository demonstrate how to use Pure Data (Pd) patches designed to run in Non-Real-Time mode to batch-process (synthesize, analyze, etc) sounds in series using Python.

Jose Henrique Padovani 3 Feb 08, 2022
Программа для практической работы №12 по дисциплине

Информатика: программа для практической работы №12 Код и блок-схема программы для практической работы №12 по дисциплине "Информатика" (I семестр). Сут

Vladislav 1 Dec 07, 2021
A python program for rick rolling people.

Rickware A python program for rick rolling people. (And annoying them too) What is rick roll? Read this wikipedia article - Rickrolling About program

2 Jan 18, 2022
Python library to decorate and beautify strings

outputformater Python library to decorate and beautify your standard output 💖 I

Felipe Delestro Matos 259 Dec 13, 2022
switching computer? changing your setup? You need to automate the download of your current setup? This is the right tool for you :incoming_envelope:

🔮 setup_shift(SS.py) switching computer? changing your setup? You need to automate the download of your current setup? This is the right tool for you

Mohamed Elfaleh 15 Aug 26, 2022
Gerenciador de processos e registros pessoais do Departamento de Fiscalização de Produtos Controlados.

CRManager Gerenciador de processos e registros pessoais do Departamento de Fiscalização de Produtos Controlados. Descrição Este projeto tem como objet

Wolfgang Almeida 1 Nov 15, 2021
A Red Team tool for exfiltrating sensitive data from Jira tickets.

Jir-thief This Module will connect to Jira's API using an access token, export to a word .doc, and download the Jira issues that the target has access

Antonio Piazza 82 Dec 12, 2022
Poetry workspace plugin for Python monorepos.

poetry-workspace-plugin Poetry workspace plugin for Python monorepos. Inspired by Yarn Workspaces. Adds a new subcommand group, poetry workspace, whic

Jack Smith 74 Jan 01, 2023
Dev-meme - A repository that contains memes just for people like us

A repository that contains memes just for people like us. Coders are constantly

Padmashree Jha 4 Oct 31, 2022
LinuxHelper - A collection of utilities for non-technical Linux users accessible via a GUI

Linux Helper A collection of utilities for non-technical Linux users accessible via a GUI This app is still in very early development, expect bugs and

Seth 7 Oct 03, 2022
Keep your company's passwords behind the firewall

TeamVault TeamVault is an open-source web-based shared password manager for behind-the-firewall installation. It requires Python 3.3+ and Postgres (wi

//SEIBERT/MEDIA GmbH 38 Feb 20, 2022
Why write code when you can import it directly from GitHub Copilot?

Copilot Importer Why write code when you can import it directly from GitHub Copilot? What is Copilot Importer? The copilot python module will dynamica

Mythic 41 Jan 04, 2023
Removes all archived super productivity tasks. Just run the python script.

delete-archived-sp-tasks.py Removes all archived super productivity tasks. Just run the python script. This is helpful to do a cleanup every 3-6 month

Ben Herbst 1 Jan 09, 2022
basic tool for NFT. let's spam, this is the easiest way to generate a hell lotta image

NFT generator this is the easiest way to generate a hell lotta image buckle up and follow me! how to first have your image in .png (transparent backgr

34 Nov 18, 2022
Toppr Os Auto Class Joiner

Toppr Os Auto Class Joiner Toppr os is a irritating platform to work with especially for students it takes a while and is problematic most of the time

1 Dec 18, 2021
Easily Generate Revolut Business Cards

RevBusinessCardGen Easily Generate Revolut Business Cards Prerequisites Before you begin, ensure you have met the following requirements: You have ins

Younes™ 35 Dec 14, 2022