Stronger AST Library

The AST library in Rodin 2.x contains some flaws that, in some corner cases, could lead to misinterpreting mathematical formulas. These flaws were either present in the original design of the library or were overlooked when introducing mathematical extensions. This page lists these flaws and analyses the possible remedies for them.

String Rendering

In Rodin 2.x, there are several methods for rendering a formula as a String. They all start with the toString prefix.

However, none of these methods takes the actual language as argument. Therefore, the rendering is done for some arbitrary FormulaFactory which the AST library tries to derive from the formula itself. This is not safe, as clashes with reserved words can be introduced (especially, when rendering bound identifier declarations).

The various string rendering methods should take a FormulaFactory parameter defining the language of the formula. This is an incompatible change to the API.

N.B.: There is no need to pass a ITypeEnvironment as the names introduced for bound identifiers only have a local scope.