coq

package
v0.8.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Sep 6, 2024 License: MIT Imports: 6 Imported by: 0

Documentation

Index

Constants

This section is empty.

Variables

View Source 
var LoopBreak = GallinaIdent("Break")
View Source 
var LoopContinue = GallinaIdent("Continue")
View Source 
var Null = nullLiteral{}

Null represents a nil pointer in Go

Functions

func ImportToPath 

func ImportToPath(pkgPath, pkgName string) string

ImportToPath converts a Go import path to a Coq path

TODO: we basically don't handle the package name (determined by the package 

statement in Go) differing from the basename of its parent directory

func InterfaceMethodName 

func InterfaceMethodName(interfaceName string, funcName string) string

func MethodName 

func MethodName(tyName string, funcName string) string

Types

type AliasDecl 

type AliasDecl struct {
	Name string
	Type Type
}

func (AliasDecl) CoqDecl 

func (t AliasDecl) CoqDecl() string

type ArrayType 

type ArrayType struct {
	Len uint64
	Elt Type
}

func (ArrayType) Coq 

func (t ArrayType) Coq(needs_paren bool) string

type ArrowType 

type ArrowType struct {
	ArgTypes   []Type // Must be non-empty; if no arguments, consists of unitT
	ReturnType Type
}

func (ArrowType) Coq 

func (t ArrowType) Coq(needs_paren bool) string

type BinOp 

type BinOp int

BinOp is an enum for a Coq binary operator 

const (
	OpPlus BinOp = iota
	OpMinus
	OpEquals
	OpNotEquals
	OpLessThan
	OpGreaterThan
	OpLessEq
	OpGreaterEq
	OpAppend
	OpMul
	OpQuot
	OpRem
	OpAnd
	OpOr
	OpXor
	OpLAnd
	OpLOr
	OpShl
	OpShr
)

Constants for the supported Coq binary operators

type BinaryExpr 

type BinaryExpr struct {
	X  Expr
	Op BinOp
	Y  Expr
}

func (BinaryExpr) Coq 

func (be BinaryExpr) Coq(needs_paren bool) string

type Binder 

type Binder *IdentExpr

type Binding 

type Binding struct {
	// Names is a list to support anonymous and tuple-destructuring bindings.
	//
	// If Names is an empty list the binding is anonymous.
	Names []string
	Expr  Expr
}

Binding is a Coq binding (a part of a Bind expression)

Note that a Binding is not an Expr. This is because emitting a binding requires knowing if it is the last binding in a sequence (in which case no binder should be written). A more accurate representation would be a cons representation, but this recursive structure is more awkward to work with; in practice delaying handling the special last-binding to printing time is easier.

func NewAnon 

func NewAnon(e Expr) Binding

NewAnon constructs an anonymous binding for an expression.

func (Binding) AddTo 

func (b Binding) AddTo(pp *buffer)

AddTo adds a binding as a non-terminal line to a block

func (Binding) Unwrap 

func (b Binding) Unwrap() (e Expr, ok bool)

Unwrap returns the expression in a Binding expected to be anonymous.

type BlockExpr 

type BlockExpr struct {
	Bindings []Binding
}

A BlockExpr is a sequence of bindings, ending with some expression.

func (BlockExpr) Coq 

func (be BlockExpr) Coq(needs_paren bool) string

type BoolLiteral 

type BoolLiteral bool
var (
	False BoolLiteral = false
	True  BoolLiteral = true
)

func (BoolLiteral) Coq 

func (b BoolLiteral) Coq(needs_paren bool) string

type ByteLiteral 

type ByteLiteral struct {
	Value uint8
}

func (ByteLiteral) Coq 

func (l ByteLiteral) Coq(needs_paren bool) string

type CallExpr 

type CallExpr struct {
	MethodName Expr
	TypeArgs   []Expr
	Args       []Expr
}

CallExpr includes primitives and references to other functions.

func NewCallExpr 

func NewCallExpr(name Expr, args ...Expr) CallExpr

NewCallExpr is a convenience to construct a CallExpr statically, especially for a fixed number of arguments.

func (CallExpr) Coq 

func (s CallExpr) Coq(needs_paren bool) string

type CommentDecl 

type CommentDecl string

CommentDecl is a top-level comment

Pretends to be a declaration so it can sit among declarations within a file.

func NewComment 

func NewComment(s string) CommentDecl

NewComment creates a CommentDecl with proper whitespacing.

func (CommentDecl) CoqDecl 

func (d CommentDecl) CoqDecl() string

CoqDecl implements the Decl interface

For CommentDecl this emits a Coq top-level comment.

type ConstDecl 

type ConstDecl struct {
	Name     string
	Type     Type
	Val      Expr
	Comment  string
	AddTypes bool
}

func (ConstDecl) CoqDecl 

func (d ConstDecl) CoqDecl() string

type Decl 

type Decl interface {
	CoqDecl() string
}

Decl is a FuncDecl, StructDecl, CommentDecl, or ConstDecl

type DerefExpr 

type DerefExpr struct {
	X  Expr
	Ty Expr
}

func (DerefExpr) Coq 

func (e DerefExpr) Coq(needs_paren bool) string

type Expr 

type Expr interface {
	// If needs_paren is true, this should be generated with parentheses.
	Coq(needs_paren bool) string
}
var Skip Expr = GallinaIdent("Skip")

func NewTuple 

func NewTuple(es []Expr) Expr

NewTuple is a smart constructor that wraps multiple expressions in a TupleExpr

func StructDesc 

func StructDesc(name string) Expr

type FieldDecl 

type FieldDecl struct {
	Name string
	Type Type
}

FieldDecl is a name:type declaration (for a struct or function binders)

func (FieldDecl) Coq 

func (d FieldDecl) Coq(needs_paren bool) string

func (FieldDecl) CoqBinder 

func (d FieldDecl) CoqBinder() string

type File 

type File struct {
	ImportHeader string
	Footer       string
	PkgPath      string
	GoPackage    string
	Imports      ImportDecls
	Decls        []Decl
}

File represents a complete Coq file (a sequence of declarations).

func (File) Write 

func (f File) Write(w io.Writer)

Write outputs the Coq source for a File. noinspection GoUnhandledErrorResult

type ForLoopExpr 

type ForLoopExpr struct {
	Init Binding
	Cond Expr
	Post Expr
	// the body of the loop
	Body BlockExpr
}

func (ForLoopExpr) Coq 

func (e ForLoopExpr) Coq(needs_paren bool) string

type FuncDecl 

type FuncDecl struct {
	Name       string
	TypeParams []TypeIdent
	Args       []FieldDecl
	ReturnType Type
	Body       Expr
	Comment    string
	AddTypes   bool
}

FuncDecl declares a function, including its parameters and body.

func (FuncDecl) CoqDecl 

func (d FuncDecl) CoqDecl() string

CoqDecl implements the Decl interface

For FuncDecl this emits the Coq vernacular Definition that defines the whole function.

func (FuncDecl) Signature 

func (d FuncDecl) Signature() string

Signature renders the function declaration's bindings

func (FuncDecl) Type 

func (d FuncDecl) Type() string

type FuncLit 

type FuncLit struct {
	Args []FieldDecl
	// TODO: ReturnType Type
	Body Expr
}

FuncLit is an unnamed function literal, consisting of its parameters and body.

func (FuncLit) Coq 

func (e FuncLit) Coq(needs_paren bool) string

type FuncType 

type FuncType struct {
	Params  []string
	Results []string
}

func (FuncType) Coq 

func (t FuncType) Coq(needs_paren bool) string

type GallinaIdent 

type GallinaIdent string

GallinaIdent is a identifier in Gallina (and not a variable)

A GallinaIdent is translated literally to Coq.

func (GallinaIdent) Coq 

func (e GallinaIdent) Coq(needs_paren bool) string

type GallinaString 

type GallinaString string

GallinaString is a Gallina string, wrapped in quotes

This is functionally identical to IdentExpr, but semantically quite different.

func (GallinaString) Coq 

func (s GallinaString) Coq(needs_paren bool) string

type HashTableInsert 

type HashTableInsert struct {
	Value Expr
}

func (HashTableInsert) Coq 

func (e HashTableInsert) Coq(needs_paren bool) string

type IdentExpr 

type IdentExpr string

IdentExpr is a go_lang-level variable

An IdentExpr is quoted in Coq.

func (IdentExpr) Coq 

func (e IdentExpr) Coq(needs_paren bool) string

type IfExpr 

type IfExpr struct {
	Cond Expr
	Then Expr
	Else Expr
}

func (IfExpr) Coq 

func (ife IfExpr) Coq(needs_paren bool) string

type ImportDecl 

type ImportDecl struct {
	Path    string
	Trusted bool
}

These will not end up in `File.Decls`, they are put into `File.Imports` by `translatePackage`.

func (ImportDecl) CoqDecl 

func (decl ImportDecl) CoqDecl() string

type ImportDecls 

type ImportDecls []ImportDecl

ImportDecls groups imports into one declaration so they can be printed without intervening blank spaces.

func (ImportDecls) PrintImports 

func (decls ImportDecls) PrintImports() string

type Int32Literal 

type Int32Literal struct {
	Value uint32
}

func (Int32Literal) Coq 

func (l Int32Literal) Coq(needs_paren bool) string

type IntLiteral 

type IntLiteral struct {
	Value uint64
}

func (IntLiteral) Coq 

func (l IntLiteral) Coq(needs_paren bool) string

type InterfaceDecl 

type InterfaceDecl struct {
	Name    string
	Methods []FieldDecl
	Comment string
}

func (InterfaceDecl) Coq 

func (d InterfaceDecl) Coq(needs_paren bool) string

func (InterfaceDecl) CoqDecl 

func (d InterfaceDecl) CoqDecl() string

type LoggingStmt 

type LoggingStmt struct {
	GoCall string
}

func (LoggingStmt) Coq 

func (s LoggingStmt) Coq(needs_paren bool) string

type MapIterExpr 

type MapIterExpr struct {
	// name of key and value identifiers
	KeyIdent, ValueIdent string
	// map to iterate over
	Map Expr
	// body of loop, with KeyIdent and ValueIdent as free variables
	Body BlockExpr
}

MapIterExpr is a call to the map iteration helper.

func (MapIterExpr) Coq 

func (e MapIterExpr) Coq(needs_paren bool) string

type MapType 

type MapType struct {
	Key   Type
	Value Type
}

func (MapType) Coq 

func (t MapType) Coq(needs_paren bool) string

type NotExpr 

type NotExpr struct {
	X Expr
}

func (NotExpr) Coq 

func (e NotExpr) Coq(needs_paren bool) string

type PackageIdent 

type PackageIdent struct {
	Package string
	Ident   string
}

A Go qualified identifier, which is translated to a Gallina qualified identifier.

func (PackageIdent) Coq 

func (e PackageIdent) Coq(needs_paren bool) string

type PtrType 

type PtrType struct {
}

func (PtrType) Coq 

func (t PtrType) Coq(needs_paren bool) string

type RefExpr 

type RefExpr struct {
	X  Expr
	Ty Expr
}

func (RefExpr) Coq 

func (e RefExpr) Coq(needs_paren bool) string

type ReturnExpr 

type ReturnExpr struct {
	Value Expr
}

func (ReturnExpr) Coq 

func (e ReturnExpr) Coq(needs_paren bool) string

type SliceLoopExpr 

type SliceLoopExpr struct {
	Key   Binder
	Val   Binder
	Ty    Expr
	Slice Expr
	Body  BlockExpr
}

func (SliceLoopExpr) Coq 

func (e SliceLoopExpr) Coq(needs_paren bool) string

type SliceType 

type SliceType struct {
	Value Type
}

func (SliceType) Coq 

func (t SliceType) Coq(needs_paren bool) string

type SpawnExpr 

type SpawnExpr struct {
	Body BlockExpr
}

SpawnExpr is a call to Spawn a thread running a procedure.

The body can capture variables in the environment.

func (SpawnExpr) Coq 

func (e SpawnExpr) Coq(needs_paren bool) string

type StoreStmt 

type StoreStmt struct {
	Dst Expr
	Ty  Expr
	X   Expr
}

func (StoreStmt) Coq 

func (e StoreStmt) Coq(needs_paren bool) string

type StringLiteral 

type StringLiteral struct {
	Value string
}

func (StringLiteral) Coq 

func (l StringLiteral) Coq(needs_paren bool) string

type StructDecl 

type StructDecl struct {
	Name    string
	Fields  []FieldDecl
	Comment string
}

StructDecl is a Coq record for a Go struct

func (StructDecl) CoqDecl 

func (d StructDecl) CoqDecl() string

CoqDecl implements the Decl interface

A struct declaration simply consists of the struct descriptor (wrapped in a module in case we eventually want to add more things related to the struct).

type StructFieldAccessExpr 

type StructFieldAccessExpr struct {
	Struct string
	Field  string
	X      Expr
	// the expression X is a pointer to a struct (whether because of pointer
	// wrapping or because it was a pointer in the program)
	ThroughPointer bool
}

func (StructFieldAccessExpr) Coq 

func (e StructFieldAccessExpr) Coq(needs_paren bool) string

type StructLiteral 

type StructLiteral struct {
	StructName string

	Allocation bool // if true, struct is being allocated on the heap
	// contains filtered or unexported fields
}

A StructLiteral represents a record literal construction using name fields.

Relies on Coq record syntax to correctly order fields for the record's constructor.

func NewStructLiteral 

func NewStructLiteral(structName string) StructLiteral

NewStructLiteral creates a StructLiteral with no values.

func (*StructLiteral) AddField 

func (sl *StructLiteral) AddField(field string, value Expr)

AddField appends a new (field, val) pair to a StructLiteral.

func (StructLiteral) Coq 

func (sl StructLiteral) Coq(needs_paren bool) string

type StructName 

type StructName string

StructName refers to a struct type from its name.

This is Type rather than an Expr.

func (StructName) Coq 

func (t StructName) Coq(needs_paren bool) string

type StructToInterface 

type StructToInterface struct {
	Struct    string
	Interface string
	Methods   []string
}

func (StructToInterface) Coq 

func (d StructToInterface) Coq(needs_paren bool) string

func (StructToInterface) CoqDecl 

func (d StructToInterface) CoqDecl() string

func (StructToInterface) MethodList 

func (d StructToInterface) MethodList() []string

func (StructToInterface) Name 

func (d StructToInterface) Name() string

type StructToInterfaceDecl 

type StructToInterfaceDecl struct {
	Fun       string
	Struct    string
	Interface string
	Arg       string
}

func (StructToInterfaceDecl) Coq 

func (d StructToInterfaceDecl) Coq(needs_paren bool) string

type TupleExpr 

type TupleExpr []Expr

func (TupleExpr) Coq 

func (te TupleExpr) Coq(needs_paren bool) string

type TupleType 

type TupleType []Type

func (TupleType) Coq 

func (tt TupleType) Coq(needs_paren bool) string

type Type 

type Type interface {
	// If needs_paren is true, this should be generated with parentheses.
	Coq(needs_paren bool) string
}

Type represents some Coq type.

Structurally identical to Expr but serves as a nice annotation in the type system for where types are expected.

func NewTupleType 

func NewTupleType(types []Type) Type

NewTupleType is a smart constructor that wraps multiple types in a TupleType

type TypeDef 

type TypeDef struct {
	Name string
	Type Type
}

func (TypeDef) CoqDecl 

func (d TypeDef) CoqDecl() string

type TypeIdent 

type TypeIdent string

TypeIdent is an identifier referencing a type.

Much like the Type interface this is the same as Ident but signals that a Go type rather than a value is being referenced.

func (TypeIdent) Coq 

func (t TypeIdent) Coq(needs_paren bool) string

type UnitLiteral 

type UnitLiteral struct{}
var Tt UnitLiteral = struct{}{}

func (UnitLiteral) Coq 

func (tt UnitLiteral) Coq(needs_paren bool) string

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.