datatype.go

Algebraic datatypes, tuples, and enumerations

← Back to Index Complete API Reference (markdown) README All Languages

Types

type Constructor

Constructor represents a datatype constructor.

type ConstructorList

ConstructorList represents a list of datatype constructors.

type Context

Context methods (receiver omitted for clarity)

Methods:

GetDatatypeSortConstructor

func (c *Context) GetDatatypeSortConstructor(sort *Sort, i uint) *FuncDecl

GetDatatypeSortConstructor returns the i-th constructor of a datatype sort.

GetDatatypeSortConstructorAccessor

func (c *Context) GetDatatypeSortConstructorAccessor(sort *Sort, constructorIdx, accessorIdx uint) *FuncDecl

GetDatatypeSortConstructorAccessor returns the accessor for the i-th field of the j-th constructor.

GetDatatypeSortNumConstructors

func (c *Context) GetDatatypeSortNumConstructors(sort *Sort) uint

GetDatatypeSortNumConstructors returns the number of constructors in a datatype sort.

GetDatatypeSortRecognizer

func (c *Context) GetDatatypeSortRecognizer(sort *Sort, i uint) *FuncDecl

GetDatatypeSortRecognizer returns the i-th recognizer of a datatype sort.

MkConstructor

func (c *Context) MkConstructor(name, recognizer string, fieldNames []string, fieldSorts []*Sort, fieldSortRefs []uint) *Constructor

MkConstructor creates a constructor for a datatype. name is the constructor name, recognizer is the recognizer name, fieldNames are the names of the fields, and fieldSorts are the sorts of the fields. fieldSortRefs can be 0 for non-recursive fields or the datatype index for recursive fields.

MkConstructorList

func (c *Context) MkConstructorList(constructors []*Constructor) *ConstructorList

MkConstructorList creates a list of constructors for a datatype.

MkDatatypeSort

func (c *Context) MkDatatypeSort(name string, constructors []*Constructor) *Sort

MkDatatypeSort creates a datatype sort from a constructor list.

MkDatatypeSorts

func (c *Context) MkDatatypeSorts(names []string, constructorLists [][]*Constructor) []*Sort

MkDatatypeSorts creates multiple mutually recursive datatype sorts.

MkEnumSort

func (c *Context) MkEnumSort(name string, enumNames []string) (*Sort, []*FuncDecl, []*FuncDecl)

Enumeration sorts (special case of datatypes) MkEnumSort creates an enumeration sort with the given constants.

MkListSort

func (c *Context) MkListSort(name string, elemSort *Sort) (*Sort, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl)

List sorts (special case of datatypes) MkListSort creates a list sort with the given element sort.

MkTupleSort

func (c *Context) MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort) (*Sort, *FuncDecl, []*FuncDecl)

Tuple sorts (special case of datatypes) MkTupleSort creates a tuple sort with the given field sorts.

← Back to Index