unification

Documentation

Index

• Constants
• func ExprListToExprMap(exprList []interfaces.Expr) map[interfaces.Expr]struct{}
• func ExprMapToExprList(exprMap map[interfaces.Expr]struct{}) []interfaces.Expr
• func SimpleInvariantSolverLogger(logf func(format string, v ...interface{})) func([]interfaces.Invariant, []interfaces.Expr) (*InvariantSolution, error)
• func UniqueExprList(exprList []interfaces.Expr) []interfaces.Expr
• type InvariantSolution
  • func SimpleInvariantSolver(invariants []interfaces.Invariant, expected []interfaces.Expr, ...) (*InvariantSolution, error)
  • func (obj *InvariantSolution) ExprList() []interfaces.Expr
• type Unifier
  • func (obj *Unifier) Unify() error

Constants

const (
	// Name is the prefix for our solver log messages.
	Name = "solver: simple"

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

	// AllowRecursion specifies whether we're allowed to use the recursive
	// solver or not. It uses an absurd amount of memory, and might hang
	// your system if a simple solution doesn't exist.
	AllowRecursion = false

	// RecursionDepthLimit specifies the max depth that is allowed.
	// FIXME: RecursionDepthLimit is not currently implemented
	RecursionDepthLimit = 5 // TODO: pick a better value ?

	// RecursionInvariantLimit specifies the max number of invariants we can
	// recurse into.
	RecursionInvariantLimit = 5 // TODO: pick a better value ?
)

Functions

func ExprListToExprMap

func ExprListToExprMap(exprList []interfaces.Expr) map[interfaces.Expr]struct{}

ExprListToExprMap converts a list of expressions to a map that has the unique expr pointers as the keys. This is just an alternate representation of the same data structure. If you have any duplicate values in your list, they'll get removed when stored as a map.

func ExprMapToExprList

func ExprMapToExprList(exprMap map[interfaces.Expr]struct{}) []interfaces.Expr

ExprMapToExprList converts a map of expressions to a list that has the unique expr pointers as the values. This is just an alternate representation of the same data structure.

func SimpleInvariantSolverLogger

func SimpleInvariantSolverLogger(logf func(format string, v ...interface{})) func([]interfaces.Invariant, []interfaces.Expr) (*InvariantSolution, error)

SimpleInvariantSolverLogger is a wrapper which returns a SimpleInvariantSolver with the log parameter of your choice specified. The result satisfies the correct signature for the solver parameter of the Unification function.

func UniqueExprList

func UniqueExprList(exprList []interfaces.Expr) []interfaces.Expr

UniqueExprList returns a unique list of expressions with no duplicates. It does this my converting it to a map and then back. This isn't necessarily the most efficient way, and doesn't preserve list ordering.

Types

type InvariantSolution

type InvariantSolution struct {
	Solutions []*interfaces.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.

func SimpleInvariantSolver

func SimpleInvariantSolver(invariants []interfaces.Invariant, expected []interfaces.Expr, logf func(format string, v ...interface{})) (*InvariantSolution, error)

SimpleInvariantSolver is an iterative invariant solver for AST expressions. It is intended to be very simple, even if it's computationally inefficient.

func (*InvariantSolution) ExprList

func (obj *InvariantSolution) ExprList() []interfaces.Expr

ExprList returns the list of valid expressions. This struct is not part of the invariant interface, but it implements this anyways.

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 func([]interfaces.Invariant, []interfaces.Expr) (*InvariantSolution, error)

	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() 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.