Skip to content

Library

FSharp.Data.Rocq has no dependencies beyond FSharp.Core. The examples on this page run against the Tally project.

dotnet add package FSharp.Data.Rocq --prerelease

open FSharp.Data.Rocq.Project
open FSharp.Data.Rocq.Structure

What a project holds

Value Holds
RocqProject.Files Each file's digests, parsed .glob and Model
RocqFile.Model Tokens, sentences, comments, headings, declarations, scopes, imports, notations, symbols, binders, references and diagnostics
RocqProject.Declarations, Symbols Those tables numbered across the project
RocqProject.CrossReferences Mentions between declarations and symbols
RocqProject.FileGraph Dependencies between files

An index or string field that can be absent is an option.

Declarations and proofs

RocqProject.Declarations lists every declaration in project order. Category is a closed union, so a match covers the kinds you care about.

let listTheorems (project: RocqProject) =
    for entry in project.Declarations do
        let declaration = entry.Declaration

        match declaration.Category with
        | Category.Theorem ->
            printfn
                "%-24s %-12s %d proof, %d doc comment"
                (defaultArg declaration.Name declaration.Id)
                project.Files[entry.File].Module
                declaration.Proofs.Length
                declaration.Docs.Length
        | _ -> ()

add_regroup              Tally.Laws   1 proof, 1 doc comment
total_append             Tally.Laws   1 proof, 1 doc comment
total_append_empty       Tally.Laws   1 proof, 1 doc comment
size_stable              Tally.Laws   1 proof, 1 doc comment
size_append              Tally.Laws   1 proof, 1 doc comment
totals_differ_falsified  Tally.Laws   1 proof, 1 doc comment
generated_sum            Tally.Laws   1 proof, 1 doc comment
titled_theorem           Tally.Prose  1 proof, 1 doc comment

Source text

Spans are half-open byte offsets into Model.Bytes. A span gives back the exact bytes of the .v file, so a statement read this way is the statement as written.

let textOf (file: RocqFile) (span: Span) =
    Encoding.UTF8.GetString (file.Model.Bytes, span.Start, span.End - span.Start)

let printStatement (project: RocqProject) (name: string) =
    for entry in project.Declarations do
        if entry.Declaration.Name = Some name then
            let file = project.Files[entry.File]
            printfn "keyword: %A" entry.Declaration.Keyword

            match entry.Declaration.Statement with
            | ValueSome statement -> printfn "statement: %s" (textOf file statement)
            | ValueNone -> ()

            printfn "extent:\n%s" (textOf file entry.Declaration.Extent)

The result for total_append:

keyword: Some "Theorem"
statement: (a b : tally) : total (append a b) = total a + total b
extent:
Theorem total_append (a b : tally) : total (append a b) = total a + total b.
Proof.
  induction a as [| n rest IH].
  - reflexivity.
  - simpl. rewrite IH. symmetry. apply add_regroup.
Qed.

Comments and headings

A comment records its format and the declaration it documents. These are the first comments of Laws.v, with its headings after them:

let printComments (file: RocqFile) =
    for comment in file.Model.Comments |> Array.truncate 6 do
        let lines = (textOf file comment.BodySpan).Trim().Split '\n'
        let firstLine = lines[0].Trim()

        let attachedTo =
            comment.AttachedTo
            |> Option.bind (fun declaration -> file.Model.Declarations[declaration].Name)

        printfn "%-5s %-22s %s" (commentFormatName comment.Format) (defaultArg attachedTo "-") firstLine

    for heading in file.Model.Headings do
        printfn "heading %d: %s" heading.Level heading.Text

md    -                      # Laws
md    -                      ## Arithmetic
doc   add_regroup            Addition regroups.
md    -                      ## Appending
md    total_append           **Appending adds totals.**
md    total_append_empty     **The empty tally changes nothing.**
heading 1: Laws
heading 2: Arithmetic
heading 2: Appending
heading 2: Assumed and unfinished

AttachedTo is the link the navigator uses to place documentation beside a declaration. Prose syntax shows how each format renders.

Stale files

A .glob records the digest of the source it came from. Editing a .v without compiling makes the two disagree, and references would then point at the wrong bytes. So load refuses, and loadWith { AllowStale = true } keeps the lexical data instead.

This example copies the project and adds one comment to Core.v:

let printStaleLoad (projectFile: string) =
    match load projectFile with
    | Ok _ -> printfn "loaded"
    | Error failures ->
        for failure in failures do
            printfn "refused: %s" (describeFailure failure)

    match loadWith { AllowStale = true } projectFile with
    | Ok project ->
        for file in project.Files do
            printfn "%-12s %A, %d symbols" file.Module file.GlobStatus file.Model.Symbols.Length
    | Error _ -> ()

refused: theories/Core.v: stale .glob: it records digest 9ebb8b3ee52a6dfc8589a5e887011937, and the source has 09894747aa4d13e80757c112cfa9bd08. Recompile, or pass --allow-stale for lexical data only
Tally.Core   Stale, 0 symbols
Tally.Laws   Current, 8 symbols
Tally.Prose  Current, 7 symbols

The stale file keeps its tokens, sentences and comments, and has no symbols or references.