Documentation
¶
Overview ¶
Package unify implements unification for type inference and elaboration.
The unification algorithm solves constraints of the form `t₁ = t₂` by finding substitutions for metavariables that make the terms equal.
This package implements Miller pattern unification, which handles metavariables applied to distinct bound variables (patterns like `?X x y` where x and y are distinct).
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
Types ¶
type Constraint ¶
Constraint represents an equality constraint between two terms.
type Unifier ¶
type Unifier struct {
// contains filtered or unexported fields
}
Unifier performs unification of type constraints.
func (*Unifier) AddConstraint ¶
AddConstraint adds a constraint to the worklist.
func (*Unifier) GetSolution ¶
GetSolution returns the solution for a metavariable if it exists.
func (*Unifier) Solve ¶
func (u *Unifier) Solve() UnifyResult
Solve processes all constraints and returns the result.
type UnifyError ¶
type UnifyError struct {
Message string
Constraints []Constraint // Remaining constraints when error occurred
}
UnifyError represents an error during unification.
func (*UnifyError) Error ¶
func (e *UnifyError) Error() string
type UnifyResult ¶
type UnifyResult struct {
// Solved maps metavariable IDs to their solutions.
Solved map[int]ast.Term
// Unsolved contains constraints that couldn't be solved.
Unsolved []Constraint
// Errors contains any errors encountered.
Errors []UnifyError
}
UnifyResult represents the result of unification.
func Unify ¶
func Unify(lhs, rhs ast.Term) UnifyResult
Unify is a convenience function that unifies two terms.
func UnifyAll ¶
func UnifyAll(constraints []Constraint) UnifyResult
UnifyAll unifies multiple pairs of terms.
Source Files