goose: Index | Files | Directories

package goose

import ""

Package goose implements conversion from Go source to Perennial definitions.

The exposed interface allows converting individual files as well as whole packages to a single Coq Ast with all the converted definitions, which include user-defined structs in Go as Coq records and a Perennial procedure for each Go function.

See the Goose README at for a high-level overview. The source also has some design documentation at


Package Files

errors.go goose.go interface.go

type Config Uses

type Config struct {
    AddSourceFileComments bool
    TypeCheck             bool

Config holds global configuration for Coq conversion

func (Config) TranslatePackage Uses

func (config Config) TranslatePackage(pkgPath string, srcDir string) (coq.File, error)

TranslatePackage translates an entire package in a directory to a single Coq Ast with all the declarations in the package.

If the source directory has multiple source files, these are processed in alphabetical order; this must be a topological sort of the definitions or the Coq code will be out-of-order. Realistically files should not have dependencies on each other, although sorting ensures the results are stable and not dependent on map or directory iteration order.

type ConversionError Uses

type ConversionError struct {
    Category string
    // the main description of what went wrong
    Message string
    // the snippet in the source program responsible for the error
    GoCode string
    // (for internal debugging) Ast:lineno for the goose code that threw the
    // error
    GooseCaller string
    // Ast:lineno for the source program where GoCode appears
    GoSrcFile string
    // (for systematic tests)
    Pos, End token.Pos

A ConversionError is a detailed and structured error encountered while converting Go to Coq.

Errors include a category describing the severity of the error.

The category "unsupported" is the only error that should result from normal usage, when attempting to use a feature goose intentionally does not support.

"todo" and "future" are markers for code that could be supported but is not currently handled.

The categories "impossible(go)" and "impossible(no-examples)" indicate a bug in goose (at the very least these cases should be checked and result in an unsupported error)

func (*ConversionError) Error Uses

func (e *ConversionError) Error() string

type Ctx Uses

type Ctx struct {
    // contains filtered or unexported fields

Ctx is a context for resolving Go code's types and source code

func NewCtx Uses

func NewCtx(pkgPath string, fset *token.FileSet, config Config) Ctx

NewCtx initializes a context

func (Ctx) Decls Uses

func (ctx Ctx) Decls(fs ...NamedFile) (decls []coq.Decl, errs []error)

Decls converts an entire package (possibly multiple files) to a list of decls

func (Ctx) TypeCheck Uses

func (ctx Ctx) TypeCheck(pkgName string, files []*ast.File) error

TypeCheck type-checks a set of files and stores the result in the Ctx

This is needed before conversion to Coq to disambiguate some methods.

type MultipleErrors Uses

type MultipleErrors []error

func (MultipleErrors) Error Uses

func (es MultipleErrors) Error() string

type NamedFile Uses

type NamedFile struct {
    Path string
    Ast  *ast.File

func (NamedFile) Name Uses

func (f NamedFile) Name() string


machinePackage machine is a support library for operations on integers.
machine/filesysPackage filesys is a support library providing access to a single directory in the filesystem.

Package goose imports 18 packages (graph). Updated 2020-06-01. Refresh now. Tools for package owners.