References and dependencies

.glob files record what every name resolves to. The library joins them across the project, so you can ask both directions without reading Rocq's output yourself.

Who uses a name

whoUses takes a name and returns each place that mentions it.

let printUses (project: RocqProject) (name: string) =
    for edge in whoUses project name do
        match edge.Owner with
        | DeclarationOwner index ->
            let owner = project.Declarations[index]
            let ownerName = defaultArg owner.Declaration.Name owner.Declaration.Id
            printfn "%-12s %-24s %d in its %A" project.Files[owner.File].Module ownerName edge.Count edge.Where
        | FileOwner index -> printfn "top level of %s" project.Files[index].Path

For total in the example project:

Tally.Core   total                    1 in its Body
Tally.Laws   total_append             3 in its Statement
Tally.Laws   total_append_empty       2 in its Statement
Tally.Laws   totals_differ_falsified  2 in its Statement
Tally.Laws   generated_sum            1 in its Statement
Tally.Prose  doc_paragraphs           1 in its Body
Tally.Prose  markdown_forms           1 in its Body
Tally.Prose  titled_theorem           1 in its Statement

usesOf does the same for a Node, when a name alone is ambiguous. symbolsNamed lists the candidates.

What a declaration uses

usesBy runs the other way, from an owner to its targets. A target outside the project is an ExternalSymbolNode, which records its module and name.

let printDependencies (project: RocqProject) (name: string) =
    let index =
        project.Declarations
        |> Array.findIndex (fun entry -> entry.Declaration.Name = Some name)

    for edge in usesBy project (DeclarationOwner index) do
        match edge.Target with
        | SymbolNode symbol -> printfn "project: %s" project.Symbols[symbol].Symbol.Name
        | ExternalSymbolNode external ->
            let node: ExternalNode = project.CrossReferences.Externals[external]
            printfn "outside: %s" node.Qualified

For total_append:

project: tally
project: total
project: append
project: add_regroup
outside: ::type_scope:x_'='_x
outside: ::nat_scope:x_'+'_x

Between files

RocqProject.FileGraph holds the Require edges and the reference counts between files.

let printFileGraph (project: RocqProject) =
    let moduleOf (file: int) =
        project.Files[file].Module

    for from, target in project.FileGraph.Requires do
        printfn "%s requires %s" (moduleOf from) (moduleOf target)

    for from, external in project.FileGraph.ExternalRequires do
        printfn "%s requires %s, outside the project" (moduleOf from) external

    for reference in project.FileGraph.References do
        printfn "%s refers to %s %d times" (moduleOf reference.From) (moduleOf reference.To) reference.Count

Tally.Laws requires Tally.Core
Tally.Prose requires Tally.Core
Tally.Core refers to Tally.Core 23 times
Tally.Laws refers to Tally.Core 31 times
Tally.Laws refers to Tally.Laws 26 times
Tally.Prose refers to Tally.Core 12 times
Tally.Prose refers to Tally.Prose 3 times