Application Development with MMT
In this tutorial, we show how to build a few minimal applications on top of the MMT library. We will not build the applications step by step. But they are chosen to be easy to understand, reproduce, and play with. They cover various but not all of the extension interfaces that MMT provides to application developers.
The following assumes that
- MMT has been installed,
- archives are placed in some folder, which is refered to as
- jEdit is used for editing mmt files. Other editors will work but might make editing awkward.
A Web-Based Editor
This mini-application shows how to easily integrate MMT with HTML pages. It uses
- the core algorithms of MMT,
- the MMT HTTP server,
- the MMT query language,
First we start an MMT server:
server on 8080
Now download the file src/mmt-api/resources/mmt-web/editing-example.html which is provided as part of the MMT sources.
Opening the file in a browser shows two input fields for
- the URI of an MMT theory
- an MMT expression relative to that theory
Clicking the commit button shows the same expression in MathML obtained by
- type reconstruction
- conversion to MathML
Best results of MathML display are obtained in Firefox.
The html file is self-documenting. Open it in a text editor to see how it works.
You can also use your browser’s inspector to see the Ajax request and response that the submit button generates.
An OpenMath Content Dictionary Editor
This mini-application shows how to use MMT as an editor for OpenMath content dictionaries. It uses
- the MMT build system,
- the Exporter extension for defining new build targets,
- the meta-data annotations to MMT content,
- the extensible MMT parser.
Concretely, it exports MMT theories as content dictionaries.
Consider the archive
MMT/examples, which was cloned automatically during setup.
In it, consider the files in the folder
Enter the commands
extension info.kwarc.mmt.openmath.Exporter build MMT/examples openmath http..cds.omdoc.org/examples/tutorial
The first command registers the exporter with MMT. There are several ways to automate this registration. For example, you can script MMT by putting the commands in an
msl file or permanently add the exporter by adding an entry to your
The second one runs the build target all theories:
- The exporter traverses all theories in the
contentfolder, which are organized by their URI. Therefore, we restrict it to the folder
http..cds.omdoc.org/examples/tutorialto export all theories of the tutorial.
- It produces one ocd file per theory in the folder
export/openmath/contentof the archive.
The types and definitions are used to generate FMPs. The meta-data key
@_description is used to give descriptions.
The implemenation is part of the MMT sources in the project
The only file of this project is src/mmt-openmath/src/info/kwarc/mmt/openmath/Exporter.scala.
It is self-documenting.
Adding Computational Rules: LF + Rewriting + Literals
This mini-demo uses explores how to extend MMT’s semantics by dynamically adding rules. It uses
- extensible literals to add primitive natural numbers
- rule-based type checking by adding new rules for computing and unifying with natural numbers
- a ParserExtension to add a new keyword for adding rules for computing with literals
- a ChangeListener that generates new rewrite rules for certain user-annotated constant
Consider the file
tutorial/3-literalsrules.mmt in the archive
It defines the natural numbers and then adds two kinds of rules:
- Computation rules are implemented in the file
scala_realizations/info/kwarc/mmt/examples/tutorialof the archive and added to the theory using the
- Rewrite rules are declared using the annotation
Computation rules is already part of MMT’s core algorithms. This application has to add new ways for adding computation rules dynamically. The implementation is not presented as a minimal example. Instead, we provide links to code in the main MMT packages.
- The keyword
ruleis added by a ParserExtension that is part of the core MMT code and that is loaded by default. It is defined in the file src/mmt-api/src/main/info/kwarc/mmt/api/symbols/RealizedConstant.scala.
role Simplifyis picked up by the ChangeListener defined in the file
[https://github.com/UniFormal/MMT/blob/master/src/mmt-lf/src/info/kwarc/mmt/lf/SimplificationRuleGenerator.scala](src/mmt-lf/src/info/kwarc/mmt/lf/SimplificationRuleGenerator.scala). It inspects the type of each new constant with the appropriate role, generates a rule, and adds it to the theory.