Documentation ¶
Overview ¶
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 https://github.com/tchajed/goose for a high-level overview. The source also has some design documentation at https://github.com/tchajed/goose/tree/master/docs.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type ConversionError ¶
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) file:lineno for the goose code that threw the // error GooseCaller string // file: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 ¶
func (e *ConversionError) Error() string
type Ctx ¶
Ctx is a context for resolving Go code's types and source code
func NewCtx ¶
NewCtx loads a context for files passed directly, rather than loaded from a packages. Errors from this function are errors during type-checking.
func NewPkgCtx ¶ added in v0.3.0
func NewPkgCtx(pkg *packages.Package, tr Translator) Ctx
NewPkgCtx initializes a context based on a properly loaded package
type ExprValUsage ¶ added in v0.4.0
type ExprValUsage int
Says how the result of the currently generated expression will be used
const ( // The result of this expression will only be used locally, or entirelz discarded ExprValLocal ExprValUsage = iota // The result of this expression will be returned from the current function // (i.e., the "early return" control effect is available here) ExprValReturned // The result of this expression will control the current loop // (i.e., the "break/continue" control effect is available here) ExprValLoop )
type MultipleErrors ¶
type MultipleErrors []error
func (MultipleErrors) Error ¶
func (es MultipleErrors) Error() string
type Translator ¶ added in v0.3.0
Translator has global configuration for translation
TODO: need a better name for this (Translator is somehow global stuff, Config is per-package)
TODO: fix duplication with Config, perhaps embed a Translator in a Config
func (Translator) TranslatePackages ¶ added in v0.3.0
func (tr Translator) TranslatePackages(modDir string, pkgPattern ...string) (files []coq.File, errs []error, patternErr error)
TranslatePackages loads packages by a list of patterns and translates them all, producing one file per matched package.
The errs list contains errors corresponding to each package (in parallel with the files list). patternErr is only non-nil if the patterns themselves have a syntax error.
Directories ¶
Path | Synopsis |
---|---|
cmd
|
|
internal
|
|
examples/append_log
Append-only, sequential, crash-safe log.
|
Append-only, sequential, crash-safe log. |
examples/async
async just uses the async disk FFI
|
async just uses the async disk FFI |
examples/comments
comments tests package comments, like this one it has multiple files
|
comments tests package comments, like this one it has multiple files |
examples/simpledb
Package simpledb implements a one-table version of LevelDB It buffers all writes in memory; to make data durable, call Compact().
|
Package simpledb implements a one-table version of LevelDB It buffers all writes in memory; to make data durable, call Compact(). |
examples/unittest
unittest is a package full of many independent and small translation examples unittest has two package comments
|
unittest is a package full of many independent and small translation examples unittest has two package comments |
Package machine is a support library for operations on integers.
|
Package machine is a support library for operations on integers. |
filesys
Package filesys is a support library providing access to a single directory in the filesystem.
|
Package filesys is a support library providing access to a single directory in the filesystem. |