lakedaemon/mm0kt

mm0 parser, mmu parser, proofchecker, patcher for set.mm.mmà

<style class="fallback">body{visibility:hidden;}</style>

pure kotlin tools for mm0/mmu and set.mm

Introduction

This repository implements in (pure) Kotlin:

• a mm0 parser
• a mmu parser
• a (mm0/mmu) one-pass proofchecker
• a (pipelinable) patcher for set.mm.mm0 and set.mm.mmu
• a patch mm0-ifying set.mm
• a mm0 vs mmu test suite creation framework And provide positive and negative tests in different folders for
• mm0 parsers (folder: parsingMM0 and parsingBoth)
• mmu parsers (folder: parsingMMU and parsingBoth)
• mm0 vs mmu proof checkers (with different stages)
  • matching mm0 statements and mmu directives (folder: matching)
  • registering mm0 statements and mmu directives (folder: registering)
  • parsing with a dynamic parser (folder: dynamicParsing)
  • proof-checking a (mm0, mmu) pair (folder:proofchecking)

Goals

• accurate and correct
  • mm0 parser
  • mmu parser
  • proof-checker
    • string.mm0 (without Input and Output support)
    • hello.mm0 (without Input and Output support)
    • peano.mm0 (without Input and Output support)
    • set.mm.mm0
  • mm0 writer
  • mmu writer
  • patcher
• test suite
• test creation api (tests 52, found bugs 12, fixed bugs 4)
• parsing: -[ ] ascii -[ ] whitechar -[x] id (p1 - f5, 0+u) -[ ] formula -[ ] int
• matching
• registering
• proof checking
• mm0-ification of set.mm (a subset of maths) :
  • turn most mm axioms into theorems
  • introduce definitions, operators, notations whenever sensible
• building a sane fundation for further work on set.mm
• pure Kotlin code base: native, mobile and browser targets
• good performance (set.mm checks in 16 s in single threaded mode)
• low Memory usage : (proof Checking should be a streaming process)
• good error reports
• understand mm0/mmu in depth to build better tools (on a binary spec, with minimum work, I'm looking at you mmb) later, when it makes sense

Non-goals

• build stuff on the binary mmb spec (we will do that much later)
• absolute performance (we wouldn't use parsing and the text based mmu spec otherwise)
• build the shortest proofs possible, in the mm0ifying process

Test-coverage

• ascii
• whitespace
• ids
• math-strings
• ints
• comments
• sorts
• coercions
• simple notations
• notations
• terms
• definitions
• axioms
• theorems

TODO :

• implement Input and Output support
• fix bugs
• export as a library (publish in mavenCentral ?)
• proofCheck each theorem in a dedicated coroutine
• port the patcher to the new architecture
• improve the patch

<style class="fallback">body{visibility:hidden;white-space:pre;font-family:monospace}</style><script src="markdeep.min.js"></script><script src="https://casual-effects.com/markdeep/latest/markdeep.min.js"></script><script>window.alreadyProcessedMarkdeep||(document.body.style.visibility="visible")</script>