Ergo Compiler

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.

Compiler architecture

Frontend

Code generation

Code Overview

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.

Intermediate representations

• Ergo: Ergo/Lang/Ergo
• Ergo calculus: ErgoC/Lang/ErgoC
• Ergo NNRC (Named Nested Relational Calculus): ErgoNNRC/Lang/ErgoNNRC

Macro expansion

• Ergo to Ergo: Ergo/Lang/ErgoExpand

Namespace resolution

• Ergo to Ergo: Translation/ErgoNameResolve

Translations between intermediate representations

• Ergo to Ergo calculus: Translation/ErgotoErgoC
• ErgoC to Ergo NNRC: Translation/ErgoCtoErgoNNRC

Type checking

• ErgoC to ErgoC with types: ErgoCType