Code Organization

This figure represents the general architecture of the compiler with its all intermediate languages and the different compilation paths. The languages are:

The general organization of the source code available in Q*cert is the following:

In the coq directory, each language has its own directory with a subdirectory Lang containing the AST and the definition of the semantics of the language. Then, depending on the language, some additional subdirectory can be present. For example, it is possible to find a Optim subdirectory containing the optimizer for the language, or a typing subdirectory containing the type checker. The directory Basic directory contains some the data-model which is shared between all languages. This directory also contains some utility functions. The directory Translation contains all the translation functions that compiles a language into another. Finally, the directory compiler contains the compiler driver.