unification

Documentation

Overview

Package unification contains the code related to type unification for the mcl language.

Index

• Constants
• func Register(name string, solver func() Solver)
• type Data
• type EqualsInvariant
• type Init
• type InvariantSolution
• type Solver
  • func Lookup(name string) (Solver, error)
  • func LookupDefault() (Solver, error)
• type Unifier
  • func (obj *Unifier) Unify(ctx context.Context) error

Constants

const (
	// ErrAmbiguous means we couldn't find a solution, but we weren't
	// inconsistent.
	ErrAmbiguous = util.Error("can't unify, no equalities were consumed, we're ambiguous")

	// StrategyNameKey is the string key used when choosing a solver name.
	StrategyNameKey = "name"

	// StrategyOptimizationsKey is the string key used to tell the solver
	// about the specific optimizations you'd like to request. The format
	// can be specific to each solver.
	StrategyOptimizationsKey = "optimizations"
)

Functions

func Register

func Register(name string, solver func() Solver)

Register takes a solver and its name and makes it available for use. It is commonly called in the init() method of the solver at program startup. There is no matching Unregister function.

Types

type Data

type Data struct {
	// UnificationInvariants is an alternate data representation for Solve.
	UnificationInvariants []*interfaces.UnificationInvariant
}

Data contains the input data for the solver to process.

type EqualsInvariant

type EqualsInvariant struct {
	Expr interfaces.Expr
	Type *types.Type
}

EqualsInvariant is an invariant that symbolizes that the expression has a known type. It is used for producing solutions.

type Init

type Init struct {
	// Strategy is a hack to tune unification performance until we have an
	// overall cleaner unification algorithm in place.
	Strategy map[string]string

	// UnifiedState stores a common representation of our unification vars.
	UnifiedState *types.UnifiedState

	Debug bool
	Logf  func(format string, v ...interface{})
}

Init contains some handles that are used to initialize every solver. Each individual solver can choose to omit using some of the fields.

type InvariantSolution

type InvariantSolution struct {
	Solutions []*EqualsInvariant // list of trivial solutions for each node
}

InvariantSolution lists a trivial set of EqualsInvariant mappings so that you can populate your AST with SetType calls in a simple loop.

type Solver

type Solver interface {
	// Init initializes the solver struct before first use.
	Init(*Init) error

	// Solve performs the actual solving. It must return as soon as possible
	// if the context is closed.
	Solve(context.Context, *Data) (*InvariantSolution, error)
}

Solver is the general interface that any solver needs to implement.

func Lookup

func Lookup(name string) (Solver, error)

Lookup returns a pointer to the solver's struct.

func LookupDefault

func LookupDefault() (Solver, error)

LookupDefault attempts to return a "default" solver.

type Unifier

type Unifier struct {
	// AST is the input abstract syntax tree to unify.
	AST interfaces.Stmt

	// Solver is the solver algorithm implementation to use.
	Solver Solver

	// Strategy is a hack to tune unification performance until we have an
	// overall cleaner unification algorithm in place.
	Strategy map[string]string

	// UnifiedState stores a common representation of our unification vars.
	UnifiedState *types.UnifiedState

	Debug bool
	Logf  func(format string, v ...interface{})
}

Unifier holds all the data that the Unify function will need for it to run.

func (*Unifier) Unify

func (obj *Unifier) Unify(ctx context.Context) error

Unify takes an AST expression tree and attempts to assign types to every node using the specified solver. The expression tree returns a list of invariants (or constraints) which must be met in order to find a unique value for the type of each expression. This list of invariants is passed into the solver, which hopefully finds a solution. If it cannot find a unique solution, then it will return an error. The invariants are available in different flavours which describe different constraint scenarios. The simplest expresses that a a particular node id (it's pointer) must be a certain type. More complicated invariants might express that two different node id's must have the same type. This function and logic was invented after the author could not find any proper literature or examples describing a well-known implementation of this process. Improvements and polite recommendations are welcome.