Tools for Compilers

These pages resulted from continuous attempts to create an imperative programming language specialized for the implementation of logic. Implementating logic is particularly difficult because logical algorithms work on tree structures (formulas and proofs) that can have many different forms. Formulas can have different logic operators on top. Only when one knows the top-operator of a formula, one knows how many subtrees it has, and which types they have. This makes static type checking of logical algorithms difficult. In my view, the root source of the problem is a problem that all programming languages with static type checking have: We don't know how to statically type check unions of types. One can view the general type of formulas as a union of subtypes, defined by the operator on top. If one could always determine at compile time the correct subtype, the type checking problem would be solved. This problem showed up in logic, but it is present in nearly all application domains.

Currentl approaches (union, std::variant, inheritance, type casts, std::optional, std::expected, use of nullptr, use of special error-value like std::string::npos) do not allow static type checking. Some of them are dynamically type checked, which means that an error will be generated at run time, when a wrong subtype is accessed. This is the case for std::variant, inheritance, std::optional, and std::expected. The other approaches result in UB when a wrong subtype is accessed. Dynamic type checking is better than UB, but static type checking would stil be better because it guarantees that never a wrong subtype will be accessed at run time.

Matching or visitors can be statically type checked, but they are not flexible, they inefficient, too verbose, and simply don't fit into the imperative paradigm.

Static type checking for sum and partial types is out of reach of current type checking algorithms, but I am hoping to solve the theoretical problems, and obtain practical procedures. Despite the unsolved theoretical problem, the programming language project resulted in techniques and tools that make it easy to implement logic in C++, so that in a broader sense, the goal of being able to implement logic in an efficient and elegant way, was obtained. Students have implemented proof checkers, and the tools have been repeatedly used in a course on compiler construction.

The following software was developed in the course of this project:

The parser generator works similar to Yacc, but fully supports C++ and RAII. It creates LALR parsers, and in addition allows extending the language at run time, which is needed for example by Prolog, where operators can be created a run time. The paraser generator generates C++ code for a working parser, as well as an implementation of a symbol class.

The tokenizer generator does not create code for a complete tokenizer, but only a classifier. The classifier reads a part of the input and determines to which type of symbol it belongs. Generating C++ code for a full tokenizer would result in tokenizers that are too rigid to be useful. It is important that is possible to extend the generated classifier by hand. This is needed if one wants to include non-regular tokens, or create a tokenizers that indentation into account.

The tokenizer and parser generator together are called Maphoon. I have used Maphoon many times, in implementation of logic, in implementation of experimental compilers, and in teaching. It just works. I recommend that you use it. Maphoon can be obtained from here.

The tree-class generator reads specifications of tree-like (algebraic) datatypes, and creates C++ implementations of these datatypes. It is called TreeGen. The specifications are as concise as in a functional language (if not more concise), while at the same time compiled to efficient C++ code. The generated tree classes have an API that is pleasant to use. In particular, they have value semantics, and use RAII. TreeGen is by itself written in C++. It can be obtained from here.

Turing Machine Simulator

Using Maphoon, I created an interface to a simulator for Turing machines. It is fast, easy to use, and it can handle non-deterministic Turing machines. It can be obtained from here. It doesn't have anything to do with the rest of the project. I created it for teaching, and to test Maphoon.

Presentation at C++ Now (2023)

I gave a presentation at C++Now 2023 with title 'Trees for Logic and Parsing'. The slides and the code fragments that were shown in the lecture are here, and here is a recording of the presentation. Note, however that the tree generator has been improved significantly since the presentation.

Presentation at C++-now (2022)

I gave a lecture at C++Now 2022 about parsing, tokenizing and Maphoon. The slides and the code fragments that were shown in the lecture are here, and this is a recording of the presentation.

Proof Checking with 3-Valued Logic

PHOLI Partial Higher-Order Logic with Interfaces is a generalization of Partial Classical Logic to higher-order logic. The long term goal of PHOLI is to be able to model mathematics and prove theorems in a pleasant way. This goal is still far away. The modeling part is fine, but proving is still very unpleasant.

Attempts to implement earlier versions of PHOLI were the reason why I started looking at programming languages. Before I had tried to implement PHOLI in C++, Haskell and Prolog, and I didn't like any of these languages. Haskell and Prolog are nice, but not suitable for implementing PHOLI. The current version of PHOLI uses Maphoon for parsing formulas, and TreeGen for creating the formula and proof data structures. Without TreeGen PHOLI would probably not be implementable. The last version of PHOLI is on GitHub. At this moment (beginning 2026), it is possible to do small proofs. The underlying three-valued logic is quite tricky, and I found a suitable calculus only in September 2025. It is possible to prove theorems in the current version, but still too hard. Some more rewrites will be necessary in order to make proving a pleasant experience. The modeling part is already nice.

Slide Sets

Compilers

My page with teaching materials contains slides that may be helpful when creating your own compiler. The slides contain explanations about tokenizing, parsing, type checking and intermediate code generation. The slides also contain implementation hints.

Lambda Calculus

In Fall 2023, I taught lambda calculus to master students. I created slides about basic lambda calculus, inductive data types, and the Hindley-Milner type checking algorithm. I think that the natural way to present the HM algorithm is by using a clause based approach. Slides are here. I tell this, because this topic is related to compilers.

Author

This page was created by Hans de Nivelle.

Acknowledgements

Thanks to Danel Batyrbek, Witold Charatonik, Aleksandra Kireeva, Tatyana Korotkova, Akhmetzhan Kussainov, Dina Muktubayeva, Cláudia Nalon, Zhandarbek Saginov, Olzhas Zhangeldinov.

Special thanks for Zoltan Teki for extensively testing Maphoon, and requesting additional features. He found a bug in the tokenizer generator, and thanks to him Maphoon now supports move-only attributes.

Parts of this research were sponsored by Nazarbayev University through the Faculty Development Competitive Research Grant Program (FDCRGP), under grant number 021220FD1651.