A large part of the Ergo compiler is written as a Coq specification from which the compiler is extracted.
Ultimately, one of our goals is to provide a full formal semantics for Ergo in Coq, and prove correct as much of the compilation pipeline as possible.
The Coq source serves a dual purpose: as Ergo's formal semantics and as part of its implementation through extraction. Here are some entry points to the code.
A browsable version of the Coq code (generated using coq2html) is available. Below are some of the main intermediate represntations and compilation phases.
- Ergo: Ergo/Lang/Ergo
- Ergo calculus: ErgoC/Lang/ErgoC
- Ergo NNRC (Named Nested Relational Calculus): ErgoNNRC/Lang/ErgoNNRC
- Ergo to Ergo: Ergo/Lang/ErgoExpand
- Ergo to Ergo: Translation/ErgoNameResolve
Translations between intermediate representations
- ErgoC to ErgoC with types: ErgoCType