proofgen.go

package proofgen

import (
	"fmt"
	"io"
	"strings"

	"github.com/goose-lang/goose/declfilter"
	"github.com/goose-lang/goose/glang"
	"golang.org/x/tools/go/packages"
)

func Package(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filter declfilter.DeclFilter) {
	fmt.Fprintf(w, "(* autogenerated by goose proofgen (types); do not modify *)\n")

	if usingFfi {
		fmt.Fprintf(w, "Require Export New.proof.%s_prelude.\n", ffi)
	} else {
		fmt.Fprintf(w, "Require Export New.proof.proof_prelude.\n")
	}

	coqPath := strings.ReplaceAll(glang.ThisIsBadAndShouldBeDeprecatedGoPathToCoqPath(pkg.PkgPath), "/", ".")
	if filter.HasTrusted() {
		fmt.Fprintf(w, "Require Export New.manualproof.%s.\n", coqPath)
	}

	tr := translateImports(w, pkg, usingFfi, ffi, filter)

	fmt.Fprintf(w, "Require Export New.code.%s.\n", coqPath)
	fmt.Fprintf(w, "Require Export New.golang.theory.\n\n")

	fmt.Fprintf(w, "Module %s.\n", pkg.Name)

	tr.translateImportList(w, pkg)

	translateTypes(w, pkg, usingFfi, ffi, filter)
	translateNames(w, pkg, usingFfi, ffi, filter)
	fmt.Fprintf(w, "End %s.\n", pkg.Name)
}