Below, we list some important invariants, which have guided us in the implementation of the compiler.

Unique types for output programs

The main part of the compiler is devoted to associate unique meanings to each subexpression of the input program. Each symbol foo can have several meanings foo#1, foo#2, etc., depending on the context. These possible meanings foo#1, foo#2, etc. are created during the declaration phase. For instance, expressions foo 1 and foo "hop" might be compiled as (foo#1)(1) and (foo#2)("hop").

The main routine compile associates a list of possible meanings of type OBJ to a subexpression of the input program of type PRG. The constructor of the type OBJ takes both the resulting output program and its type as arguments (and optionally some priorities). In fact, each output program is unambiguous and therefore has a unique type. When constructing an instance of type OBJ, this type is cached, which allows subsequently for the automatic retrieval of the type of an output program.

Constant environments during main compilation

The symbols of an environment are bound to their possible meanings during the declaration phase. During the main compilation phase, these meanings can no longer change. In particular, the set of converters in the environment remains fixed, which allows us to cache inferred compositions of converters and the resolution of function applications for functions and arguments of given types.