coq

type ArrayType ¶

type ArrayType struct {
	Len uint64
	Elt Type
}

func (t ArrayType) Coq() string

type ArrowType ¶

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

func (t ArrowType) Coq() 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
)

type BinaryExpr ¶

type BinaryExpr struct {
	X  Expr
	Op BinOp
	Y  Expr
}

func (be BinaryExpr) Coq() 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(e Expr) Binding

func (b Binding) AddTo(pp *buffer)

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

type BlockExpr ¶

type BlockExpr struct {
	Bindings []Binding
}

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

func (be BlockExpr) Coq() string

type BoolLiteral ¶

type BoolLiteral bool

var (
	False BoolLiteral = false
	True  BoolLiteral = true
)

func (b BoolLiteral) Coq() string

type ByteLiteral ¶

type ByteLiteral struct {
	Value uint8
}

func (l ByteLiteral) Coq() string

type CallExpr ¶

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

CallExpr includes primitives and references to other functions.

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

func (s CallExpr) Coq() 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(s string) CommentDecl

func (d CommentDecl) CoqDecl() string

type ConstDecl ¶

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

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 (e DerefExpr) Coq() string

type Expr ¶

type Expr interface {
	Coq() string
}

var Skip Expr = GallinaIdent("Skip")

func NewTuple(es []Expr) Expr

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 (d FieldDecl) Coq() string

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 (f File) Write(w io.Writer)

type ForLoopExpr ¶

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

func (e ForLoopExpr) Coq() 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 (d FuncDecl) CoqDecl() string

func (d FuncDecl) Signature() string

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 (e FuncLit) Coq() string

type FuncType ¶

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

func (t FuncType) Coq() string

type GallinaIdent ¶

type GallinaIdent string

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

A GallinaIdent is translated literally to Coq.

func (e GallinaIdent) Coq() 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 (s GallinaString) Coq() string

type HashTableInsert ¶

type HashTableInsert struct {
	Value Expr
}

func (e HashTableInsert) Coq() string

type IdentExpr ¶

type IdentExpr string

IdentExpr is a go_lang-level variable

An IdentExpr is quoted in Coq.

func (e IdentExpr) Coq() string

type IfExpr ¶

type IfExpr struct {
	Cond Expr
	Then Expr
	Else Expr
}

func (ife IfExpr) Coq() 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 (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 (decls ImportDecls) PrintImports() string

type Int32Literal ¶

type Int32Literal struct {
	Value uint32
}

func (l Int32Literal) Coq() string

type IntLiteral ¶

type IntLiteral struct {
	Value uint64
}

func (l IntLiteral) Coq() string

type InterfaceDecl ¶

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

func (d InterfaceDecl) Coq() string

func (d InterfaceDecl) CoqDecl() string

type LoggingStmt ¶

type LoggingStmt struct {
	GoCall string
}

func (s LoggingStmt) Coq() 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 (e MapIterExpr) Coq() string

type MapType ¶

type MapType struct {
	Key   Type
	Value Type
}

func (t MapType) Coq() string

type NotExpr ¶

type NotExpr struct {
	X Expr
}

func (e NotExpr) Coq() string

type PackageIdent ¶

type PackageIdent struct {
	Package string
	Ident   string
}

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

func (e PackageIdent) Coq() string

type PtrType ¶

type PtrType struct {
}

func (t PtrType) Coq() string

type RefExpr ¶

type RefExpr struct {
	X  Expr
	Ty Expr
}

func (e RefExpr) Coq() string

type ReturnExpr ¶

type ReturnExpr struct {
	Value Expr
}

func (e ReturnExpr) Coq() string

type SliceLoopExpr ¶

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

func (e SliceLoopExpr) Coq() string

type SliceType ¶

type SliceType struct {
	Value Type
}

func (t SliceType) Coq() 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 (e SpawnExpr) Coq() string

type StoreStmt ¶

type StoreStmt struct {
	Dst Expr
	Ty  Expr
	X   Expr
}

func (e StoreStmt) Coq() string

type StringLiteral ¶

type StringLiteral struct {
	Value string
}

func (l StringLiteral) Coq() string

type StructDecl ¶

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

StructDecl is a Coq record for a Go struct

func (d StructDecl) CoqDecl() string

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 (e StructFieldAccessExpr) Coq() 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(structName string) StructLiteral

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

func (sl StructLiteral) Coq() string

type StructName ¶

type StructName string

StructName refers to a struct type from its name.

This is Type rather than an Expr.

func (t StructName) Coq() string

type StructToInterface ¶

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

func (d StructToInterface) Coq() string

func (d StructToInterface) CoqDecl() string

func (d StructToInterface) MethodList() []string

func (d StructToInterface) Name() string

type StructToInterfaceDecl ¶

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

func (d StructToInterfaceDecl) Coq() string

type TupleExpr ¶

type TupleExpr []Expr

func (te TupleExpr) Coq() string

type TupleType ¶

type TupleType []Type

func (tt TupleType) Coq() string

type Type ¶

type Type interface {
	Coq() 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(types []Type) Type

type TypeDecl ¶

type TypeDecl struct {
	Name string
	Body Type
}

func (d TypeDecl) 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 (t TypeIdent) Coq() string

type UnitLiteral ¶

type UnitLiteral struct{}

var Tt UnitLiteral = struct{}{}

func (tt UnitLiteral) Coq() string