docs/assets/dependencies.dot

// This file produces a graph of dependencies between the generated
//   verification files from the compiler.
// You can build an image with the command 'dot -Tjpg dependencies.dot -o dependencies.jpg'

digraph graphname {
    // AllRefine deps
    NormalProof   -> AllRefine;
    SCorresNormal -> AllRefine;
    CorresProof   -> AllRefine;
    MonoProof     -> AllRefine;

    // NormalProof deps
    ShallowDesugar -> NormalProof;
    ShallowNormal  -> NormalProof;

    ShallowShared -> ShallowNormal;
    ShallowShared -> ShallowDesugar;

    // SCorresNoraml deps
    ShallowNormal -> SCorresNormal;
    DeepNormal    -> SCorresNormal;

    // CorresProof deps
    CorresSetup -> CorresProof;

    ACInstall -> CorresSetup;
    TypeProof -> CorresSetup;

    // MonoProof deps
    DeepNormal -> MonoProof;
    TypeProof  -> MonoProof;
}