constraint

package
v1.5.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Feb 2, 2026 License: MIT Imports: 13 Imported by: 0

Documentation

Overview

Package constraint provides multi-path narrowing constraints for type refinement.

Constraints represent facts learned from conditionals and type guards that refine types along control flow paths. Unlike simple single-variable narrowing, constraints can relate multiple paths (e.g., "if x == y") enabling richer type-level reasoning.

Core Concepts

Path: An SSA-stable identifier for a value (variable.field.index). Paths track identity through control flow using CFG symbol IDs, enabling precise narrowing even when the same variable name refers to different values at different points.

Constraint: A narrowing term that refines types when satisfied. Constraints are AST-free and deterministic, making them suitable for serialization and caching.

Condition: A DNF (disjunctive normal form) formula of constraint conjunctions, representing the complete narrowing information from a conditional expression.

Constraint Kinds

Single-path constraints:

  • Truthy/Falsy: Path evaluates to truthy/falsy value
  • IsNil/NotNil: Path is/is not nil
  • HasType/NotHasType: Path has/lacks a specific type
  • HasField: Path has a specific field (narrows unions)

Literal comparison constraints:

  • FieldEquals/FieldNotEquals: path.field equals/not-equals a literal
  • IndexEquals/IndexNotEquals: path[key] equals/not-equals a literal

Multi-path constraints:

  • EqPath/NotEqPath: Two paths are equal/not-equal
  • FieldEqualsPath/FieldNotEqualsPath: path.field equals/not-equals another path
  • IndexEqualsPath/IndexNotEqualsPath: path[key] equals/not-equals another path
  • KeyOf: Key path is a known key of table path

Solver

The Solver applies constraints to base types, computing narrowed types for each path. It handles constraint combination, contradiction detection, and produces a PathTypes map ready for use by the type checker.

Example

For the code: 

if type(x) == "string" then
    -- x is narrowed to string
end

The constraint HasType{x, string} is applied in the then-branch, and the solver narrows x's type from its declared type to string.

Package constraint provides multi-path narrowing constraints for type refinement.

Constraints represent facts learned from conditionals and type guards that refine types along control flow paths. Unlike simple single-variable narrowing, constraints can relate multiple paths (e.g., "if x == y") enabling richer type-level reasoning.

Core Types

Path: An SSA-stable identifier for a value (variable.field.index). Paths track identity through control flow using CFG symbol IDs, enabling precise narrowing even when the same variable name refers to different values at different points.

Constraint: A narrowing term that refines types when satisfied. Constraints are AST-free and deterministic, making them suitable for serialization and caching.

Condition: A DNF (disjunctive normal form) formula of constraint conjunctions, representing the complete narrowing information from a conditional expression.

Solver: Applies constraints to type environments to produce narrowed types.

FunctionEffect: Describes type refinements a function produces on its parameters.

Interner: Provides constraint interning to reduce allocations for common patterns.

Constraint Kinds

Single-path constraints:

Literal comparison constraints:

Multi-path constraints:

Numeric Constraints

The package provides numeric constraints for arithmetic reasoning via the NumericConstraint interface:

Generic Inference

InferSet provides constraint-based type variable inference using bounds tracking and SCC-based unification (Tarjan's algorithm) for cyclic dependencies.

Example

Creating and applying constraints: 

// Create paths for variables
xPath := constraint.NewPath(xSym, "x")
yPath := constraint.NewPath(ySym, "y")

// Build a condition: x is not nil AND x.kind == "success"
cond := constraint.FromConstraints(
    constraint.NotNil{Path: xPath},
    constraint.FieldEquals{Target: xPath, Field: "kind", Value: typ.LiteralString("success")},
)

// Apply constraints to narrow types
solver := constraint.Solver{Env: env}
narrowed := solver.Apply(cond.AllConstraints(), baseTypes)

Thread Safety

Constraint values are immutable and safe to use concurrently. The Solver is pure and deterministic. The Interner is thread-safe for concurrent use.

Sub-packages

The [theory] sub-package provides modular SMT-style theory solvers:

  • Difference Logic: x - y ≤ c constraints using Bellman-Ford
  • Modular Arithmetic: x % n == k constraints
  • E-Graph: Equality reasoning with congruence closure

Index

Constants

View Source 
const DefaultMaxDisjuncts = 32

DefaultMaxDisjuncts caps the number of disjuncts kept in a Condition.

Variables

This section is empty.

Functions

func ConjunctionContains 

func ConjunctionContains(conj []Constraint, c Constraint) bool

ConjunctionContains checks if a conjunction contains a constraint. Uses binary search since conjunctions are sorted by hash.

func ExprEquals 

func ExprEquals(a, b Expr) bool

ExprEquals compares two Expr values for structural equality.

func FormatSegments 

func FormatSegments(segs []Segment) string

FormatSegments converts path segments to a canonical suffix string. This is the single canonical implementation for segment serialization. Format: .field for SegmentField, ["key"] for SegmentIndexString, [123] for SegmentIndexInt.

func HasKeyOfConstraint 

func HasKeyOfConstraint(cond Condition, tablePath, keyPath Path, resolve PathResolver) bool

HasKeyOfConstraint checks if a KeyOf constraint is guaranteed active in the condition. In DNF, a constraint is guaranteed only if it appears in ALL disjuncts.

func IsBooleanDiscriminantField 

func IsBooleanDiscriminantField(parentType typ.Type, field string, resolver narrow.Resolver) bool

IsBooleanDiscriminantField checks if a field is a boolean literal discriminant in a union type. Parent narrowing for Truthy/Falsy should only apply when the field type is a boolean literal (true/false) that distinguishes union variants.

func IsReturnPath 

func IsReturnPath(p Path) bool

IsReturnPath checks if the path represents a return value (ret[N] format).

func Match 

func Match(pattern, concrete typ.Type, cs *InferSet)

Match walks pattern and concrete types in parallel, collecting constraints.

func MatchCo 

func MatchCo(pattern, concrete typ.Type, cs *InferSet)

MatchCo matches with covariant orientation (for return positions).

func MatchContra 

func MatchContra(pattern, concrete typ.Type, cs *InferSet)

MatchContra matches with contravariant orientation (for parameter positions).

func VisitConstraint 

func VisitConstraint[R any](c Constraint, v ConstraintVisitor[R]) R

VisitConstraint applies the first matching handler in v to c.

func VisitExpr 

func VisitExpr[R any](e Expr, v ExprVisitor[R]) R

VisitExpr applies the first matching handler in v to e.

func VisitNumericConstraint 

func VisitNumericConstraint[R any](c NumericConstraint, v NumericConstraintVisitor[R]) R

VisitNumericConstraint applies the first matching handler in v to c.

Types

type Atom 

type Atom struct {
	Kind    AtomKind
	Left    Term           // primary term
	Right   Term           // second term (for binary relations)
	TypeKey narrow.TypeKey // for HasType/NotHasType
	Mod     int64          // modulus for ModEq
	Rem     int64          // remainder for ModEq
}

Atom is a unified atomic constraint in the constraint language.

func AtomEq 

func AtomEq(left, right Term) Atom

AtomEq creates an equality atom: left == right.

func AtomFalsy 

func AtomFalsy(term Term) Atom

AtomFalsy creates a falsy constraint atom.

func AtomGe 

func AtomGe(left, right Term) Atom

AtomGe creates a greater-or-equal atom: left >= right.

func AtomGt 

func AtomGt(left, right Term) Atom

AtomGt creates a greater-than atom: left > right.

func AtomHasType 

func AtomHasType(term Term, key narrow.TypeKey) Atom

AtomHasType creates a type constraint atom.

func AtomLe 

func AtomLe(left, right Term) Atom

AtomLe creates a less-or-equal atom: left <= right.

func AtomLt 

func AtomLt(left, right Term) Atom

AtomLt creates a less-than atom: left < right.

func AtomModEq 

func AtomModEq(term Term, mod, rem int64) Atom

AtomModEq creates a modular equality atom: term % mod == rem.

func AtomNe 

func AtomNe(left, right Term) Atom

AtomNe creates an inequality atom: left != right.

func AtomNotHasType 

func AtomNotHasType(term Term, key narrow.TypeKey) Atom

AtomNotHasType creates a negated type constraint atom.

func AtomTruthy 

func AtomTruthy(term Term) Atom

AtomTruthy creates a truthy constraint atom.

func NumericConstraintToAtom 

func NumericConstraintToAtom(c NumericConstraint) (Atom, bool)

NumericConstraintToAtom converts a numeric constraint to a unified Atom. Returns (atom, true) for supported constraints, (Atom{}, false) for unsupported.

func TypeConstraintToAtom 

func TypeConstraintToAtom(c Constraint) (Atom, bool)

TypeConstraintToAtom converts a type constraint to a unified Atom. Returns (atom, true) for supported constraints, (Atom{}, false) for unsupported.

func TypeConstraintToAtomWithResolver 

func TypeConstraintToAtomWithResolver(c Constraint, resolve PathResolver) (Atom, bool)

TypeConstraintToAtomWithResolver converts a type constraint to a unified Atom using a PathResolver. Returns (atom, true) for supported constraints, (Atom{}, false) for unsupported.

func (Atom) Equal 

func (a Atom) Equal(other Atom) bool

func (Atom) Hash 

func (a Atom) Hash() uint64

func (Atom) Paths 

func (a Atom) Paths() []PathKey

Paths returns all path keys referenced by this atom.

func (Atom) String 

func (a Atom) String() string

type AtomKind 

type AtomKind uint8

AtomKind classifies atom variants. 

const (
	AtomKindInvalid    AtomKind = iota
	AtomKindEq                  // X == Y
	AtomKindNe                  // X != Y
	AtomKindLt                  // X < Y
	AtomKindLe                  // X <= Y
	AtomKindGt                  // X > Y
	AtomKindGe                  // X >= Y
	AtomKindHasType             // X has type T
	AtomKindNotHasType          // X does not have type T
	AtomKindTruthy              // X is truthy
	AtomKindFalsy               // X is falsy
	AtomKindModEq               // X % M == R
)

type AtomResult 

type AtomResult struct {
	Atoms    []Atom       // successfully converted atoms
	Leftover []Constraint // constraints that couldn't be converted
}

AtomResult holds the result of converting constraints to atoms.

func ToAtoms 

func ToAtoms(constraints []Constraint) AtomResult

ToAtoms converts type constraints to unified Atoms. Constraints that don't map cleanly are returned in Leftover. Uses path.Key() for path resolution (symbol-only keys).

func ToAtomsWithResolver 

func ToAtomsWithResolver(constraints []Constraint, resolve PathResolver) AtomResult

ToAtomsWithResolver converts type constraints to unified Atoms using a PathResolver. The resolver converts Path objects to canonical PathKeys. Constraints that don't map cleanly are returned in Leftover.

type BinOp 

type BinOp struct {
	Op    Op
	Left  Expr
	Right Expr
}

BinOp represents a binary arithmetic operation.

func Add 

func Add(left, right Expr) BinOp

Add creates an addition expression.

func Div 

func Div(left, right Expr) BinOp

Div creates a division expression.

func Mod 

func Mod(left, right Expr) BinOp

Mod creates a modulo expression.

func Mul 

func Mul(left, right Expr) BinOp

Mul creates a multiplication expression.

func Sub 

func Sub(left, right Expr) BinOp

Sub creates a subtraction expression.

func (BinOp) Eval 

func (b BinOp) Eval(env map[string]int64) (int64, bool)

func (BinOp) String 

func (b BinOp) String() string

func (BinOp) Substitute 

func (b BinOp) Substitute(subst map[string]Expr) Expr

func (BinOp) Variables 

func (b BinOp) Variables() []string

type Bounds 

type Bounds struct {
	Lower []typ.Type
	Upper []typ.Type
}

Bounds tracks constraints on a type variable.

func NewBounds 

func NewBounds() *Bounds

NewBounds creates empty bounds.

func (*Bounds) AddLower 

func (b *Bounds) AddLower(t typ.Type)

AddLower adds a lower bound.

func (*Bounds) AddUpper 

func (b *Bounds) AddUpper(t typ.Type)

AddUpper adds an upper bound.

func (*Bounds) Solve 

func (b *Bounds) Solve() (typ.Type, error)

Solve finds a type that satisfies all bounds.

type BoundsError 

type BoundsError struct {
	Lower typ.Type
	Upper typ.Type
}

BoundsError represents unsatisfiable bounds.

func (*BoundsError) Error 

func (e *BoundsError) Error() string

type Condition 

type Condition struct {
	// Disjuncts holds the disjunction of conjunctions.
	// Each inner slice is a conjunction of constraints that must all hold.
	// The condition is satisfied if ANY disjunct is fully satisfied.
	Disjuncts [][]Constraint
}

Condition represents a predicate in disjunctive normal form (DNF).

A condition is a disjunction (OR) of conjunctions (ANDs): 

(A AND B) OR (C AND D) OR (E)

This is represented as a slice of disjuncts, where each disjunct is a slice of constraints that must all be satisfied.

Truth Values

  • Zero disjuncts: false (unsatisfiable, nothing can satisfy this)
  • Single empty disjunct: true (no constraints, everything satisfies this)
  • Non-empty disjuncts: at least one disjunct must be fully satisfied

Canonicalization

Conditions are automatically canonicalized:

  • Constraints within each disjunct are sorted by hash for determinism
  • Duplicate constraints and disjuncts are removed
  • Subsumed disjuncts are eliminated (if A subsumes B, B is removed)
  • If disjuncts exceed DefaultMaxDisjuncts, they are collapsed to common constraints

Example 

// Create: (x is truthy) OR (y is not nil)
cond := constraint.Or(
    constraint.FromConstraints(constraint.Truthy{Path: xPath}),
    constraint.FromConstraints(constraint.NotNil{Path: yPath}),
)

func And 

func And(a, b Condition) Condition

And returns the conjunction of two conditions.

func FalseCondition 

func FalseCondition() Condition

FalseCondition returns an unsatisfiable condition.

func FromConjunction 

func FromConjunction(items []Constraint) Condition

FromConjunction creates a Condition from a conjunction slice.

func FromConstraints 

func FromConstraints(items ...Constraint) Condition

FromConstraints builds a condition with a single conjunction.

func FromDisjuncts 

func FromDisjuncts(conjunctions [][]Constraint) Condition

FromDisjuncts builds a condition from multiple conjunctions. Normalizes once instead of incremental Or to ensure deterministic ordering.

func Not 

func Not(c Condition) Condition

Not negates a condition using De Morgan's laws.

func Or 

func Or(a, b Condition) Condition

Or returns the disjunction of two conditions.

func TrueCondition 

func TrueCondition() Condition

TrueCondition returns a condition that imposes no constraints.

func (Condition) AllConstraints 

func (c Condition) AllConstraints() []Constraint

AllConstraints returns all constraints across all disjuncts (flattened).

func (Condition) DisjunctConstraints 

func (c Condition) DisjunctConstraints(i int) []Constraint

DisjunctConstraints returns the constraints in the i-th disjunct.

func (Condition) Equals 

func (c Condition) Equals(other Condition) bool

Equals compares two conditions for structural equality.

func (Condition) HasConstraints 

func (c Condition) HasConstraints() bool

HasConstraints reports whether any disjunct carries constraints.

func (Condition) Hash 

func (c Condition) Hash() uint64

Hash computes a stable hash for the condition.

func (Condition) IsFalse 

func (c Condition) IsFalse() bool

IsFalse reports whether the condition is unsatisfiable (no disjuncts).

func (Condition) IsTrue 

func (c Condition) IsTrue() bool

IsTrue reports whether the condition imposes no constraints.

func (Condition) MustConstraints 

func (c Condition) MustConstraints() []Constraint

MustConstraints returns constraints that appear in every disjunct.

func (Condition) NumDisjuncts 

func (c Condition) NumDisjuncts() int

NumDisjuncts returns the number of disjuncts.

func (Condition) Substitute 

func (c Condition) Substitute(args []Path) Condition

Substitute replaces placeholder paths using argument paths.

func (Condition) Subsumes 

func (c Condition) Subsumes(other Condition) bool

Subsumes checks if c semantically subsumes (is more general than) other. In DNF, c subsumes other if every disjunct in other is subsumed by some disjunct in c. This means any path satisfying other also satisfies c.

type Const 

type Const struct {
	Value int64
}

Const represents a constant integer value.

func C 

func C(val int64) Const

C creates a constant expression.

func (Const) Eval 

func (c Const) Eval(map[string]int64) (int64, bool)

func (Const) String 

func (c Const) String() string

func (Const) Substitute 

func (c Const) Substitute(map[string]Expr) Expr

func (Const) Variables 

func (Const) Variables() []string

type Constraint 

type Constraint interface {
	Kind() Kind
	Paths() []Path
	Hash() uint64
	Equals(other Constraint) bool
	Substitute(args []Path) (Constraint, bool)
}

Constraint is a narrowing term that refines types when satisfied.

Constraints are AST-free, deterministic, and implement structural equality for memoization. Each constraint tracks which paths it affects via Paths(), enabling efficient incremental narrowing.

Substitute replaces placeholder paths ($0, $1) with concrete argument paths, used when applying function effect constraints at call sites.

func NegateConstraint 

func NegateConstraint(item Constraint) (Constraint, bool)

NegateConstraint negates a single constraint when possible.

func NewConjunction 

func NewConjunction(items ...Constraint) []Constraint

NewConjunction creates a canonicalized conjunction (AND) of constraints.

func SubstituteConjunction 

func SubstituteConjunction(conj []Constraint, args []Path) []Constraint

SubstituteConjunction replaces placeholder paths in a conjunction.

type ConstraintVisitor 

type ConstraintVisitor[R any] struct {
	Truthy             func(Truthy) R
	Falsy              func(Falsy) R
	IsNil              func(IsNil) R
	NotNil             func(NotNil) R
	HasType            func(HasType) R
	NotHasType         func(NotHasType) R
	HasField           func(HasField) R
	FieldEquals        func(FieldEquals) R
	FieldNotEquals     func(FieldNotEquals) R
	IndexEquals        func(IndexEquals) R
	IndexNotEquals     func(IndexNotEquals) R
	EqPath             func(EqPath) R
	NotEqPath          func(NotEqPath) R
	FieldEqualsPath    func(FieldEqualsPath) R
	FieldNotEqualsPath func(FieldNotEqualsPath) R
	IndexEqualsPath    func(IndexEqualsPath) R
	IndexNotEqualsPath func(IndexNotEqualsPath) R
	KeyOf              func(KeyOf) R
	Default            func(Constraint) R
}

ConstraintVisitor dispatches on constraint variants. Nil handlers fall back to Default when provided; otherwise return zero.

type EffectLookupBySym 

type EffectLookupBySym func(sym cfg.SymbolID) *FunctionEffect

EffectLookupBySym retrieves a function's inferred effect by symbol ID.

Used during call site analysis to determine what type refinements a function call produces. Returns nil if the function has no recorded effect.

type Env 

type Env struct {
	// ResolveType converts type keys from HasType constraints to actual types.
	// Required for type guard narrowing (e.g., type(x) == "string").
	ResolveType narrow.TypeResolver

	// Resolver provides field and index type lookups on record/array/map types.
	// Required for field-based narrowing (e.g., x.kind == "success").
	Resolver narrow.Resolver

	// PathTypeAt retrieves the current type of a path at a program point.
	// Used for multi-path constraints like FieldEqualsPath.
	PathTypeAt PathTypeResolver

	// ResolvePath converts unversioned paths to versioned PathKeys.
	// Used for SSA-aware path resolution in ApplyToSingle.
	ResolvePath PathResolver
}

Env provides external resolvers needed for constraint solving.

The solver itself is pure and deterministic; Env supplies the context-specific resolution functions. All fields are optional - the solver degrades gracefully when resolvers are not provided.

Example: 

env := constraint.Env{
    ResolveType: func(key narrow.TypeKey) typ.Type { ... },
    Resolver:    myFieldResolver,
}
solver := constraint.Solver{Env: env}

func (*Env) Field 

func (e *Env) Field(t typ.Type, name string) (typ.Type, bool)

Field resolves a field type using Resolver.

func (*Env) HasResolver 

func (e *Env) HasResolver() bool

HasResolver returns true if Env can resolve field and index queries.

func (*Env) Index 

func (e *Env) Index(t typ.Type, key typ.Type) (typ.Type, bool)

Index resolves an index type using Resolver.

type Eq 

type Eq struct {
	X Path
	Y Path
}

Eq represents x == y.

func (Eq) Equals 

func (c Eq) Equals(o NumericConstraint) bool

func (Eq) Hash 

func (c Eq) Hash() uint64

func (Eq) NumKind 

func (c Eq) NumKind() NumKind

func (Eq) Paths 

func (c Eq) Paths() []Path

type EqConst 

type EqConst struct {
	X Path
	C int64
}

EqConst represents x == c.

func (EqConst) Equals 

func (c EqConst) Equals(o NumericConstraint) bool

func (EqConst) Hash 

func (c EqConst) Hash() uint64

func (EqConst) NumKind 

func (c EqConst) NumKind() NumKind

func (EqConst) Paths 

func (c EqConst) Paths() []Path

type EqPath 

type EqPath struct {
	Left  Path
	Right Path
}

EqPath constrains two paths to have equal values at runtime. When satisfied, the types of both paths can be intersected since they must be compatible. Canonicalized by ordering endpoints for stable hashing.

func NewEqPath 

func NewEqPath(left, right Path) EqPath

func (EqPath) Equals 

func (c EqPath) Equals(o Constraint) bool

func (EqPath) Hash 

func (c EqPath) Hash() uint64

func (EqPath) Kind 

func (c EqPath) Kind() Kind

func (EqPath) Paths 

func (c EqPath) Paths() []Path

func (EqPath) String 

func (c EqPath) String() string

func (EqPath) Substitute 

func (c EqPath) Substitute(args []Path) (Constraint, bool)

type Expr 

type Expr interface {
	String() string
	// Substitute replaces variables according to the substitution map.
	Substitute(subst map[string]Expr) Expr
	// Variables returns all variable names in this expression.
	Variables() []string
	// Eval evaluates the expression given concrete variable values.
	// Returns (value, true) if fully evaluated, (0, false) if unknown variables remain.
	Eval(env map[string]int64) (int64, bool)
	// contains filtered or unexported methods
}

Expr represents an arithmetic expression in the constraint language. Expressions are immutable and can be composed freely.

func Simplify 

func Simplify(e Expr) Expr

Simplify attempts to simplify an expression by constant folding.

type ExprCompare 

type ExprCompare struct {
	Rel   ExprRel
	Left  Expr
	Right Expr
}

ExprCompare represents a relational constraint between expressions.

func EqExpr 

func EqExpr(left, right Expr) ExprCompare

EqExpr creates an equality comparison.

func GeExpr 

func GeExpr(left, right Expr) ExprCompare

GeExpr creates a greater-than-or-equal comparison.

func GtExpr 

func GtExpr(left, right Expr) ExprCompare

GtExpr creates a greater-than comparison.

func LeExpr 

func LeExpr(left, right Expr) ExprCompare

LeExpr creates a less-than-or-equal comparison.

func LtExpr 

func LtExpr(left, right Expr) ExprCompare

LtExpr creates a less-than comparison.

func NeExpr 

func NeExpr(left, right Expr) ExprCompare

NeExpr creates an inequality comparison.

func (ExprCompare) Equals 

func (c ExprCompare) Equals(other ExprCompare) bool

Equals returns true if two ExprCompare values are structurally equal.

func (ExprCompare) String 

func (c ExprCompare) String() string

type ExprRel 

type ExprRel uint8

ExprRel represents a comparison operator for expressions. 

const (
	ExprEq ExprRel = iota
	ExprNe
	ExprLt
	ExprLe
	ExprGt
	ExprGe
)

func (ExprRel) String 

func (r ExprRel) String() string

type ExprVisitor 

type ExprVisitor[R any] struct {
	Var      func(Var) R
	Const    func(Const) R
	BinOp    func(BinOp) R
	Len      func(Len) R
	Param    func(Param) R
	Ret      func(Ret) R
	ParamLen func(ParamLen) R
	RetLen   func(RetLen) R
	Min      func(Min) R
	Max      func(Max) R
	Default  func(Expr) R
}

ExprVisitor dispatches on expression variants. Nil handlers fall back to Default when provided; otherwise return zero.

type Falsy 

type Falsy struct {
	Path Path
}

Falsy requires path to evaluate to a falsy value (nil or false). Narrows the path's type to only nil or false in the then-branch.

func (Falsy) Equals 

func (c Falsy) Equals(o Constraint) bool

func (Falsy) Hash 

func (c Falsy) Hash() uint64

func (Falsy) Kind 

func (c Falsy) Kind() Kind

func (Falsy) Paths 

func (c Falsy) Paths() []Path

func (Falsy) String 

func (c Falsy) String() string

func (Falsy) Substitute 

func (c Falsy) Substitute(args []Path) (Constraint, bool)

type FieldEquals 

type FieldEquals struct {
	Target Path
	Field  string
	Value  *typ.Literal
}

FieldEquals constrains a field on a path to a literal value.

func (FieldEquals) Equals 

func (c FieldEquals) Equals(o Constraint) bool

func (FieldEquals) Hash 

func (c FieldEquals) Hash() uint64

func (FieldEquals) Kind 

func (c FieldEquals) Kind() Kind

func (FieldEquals) Paths 

func (c FieldEquals) Paths() []Path

func (FieldEquals) String 

func (c FieldEquals) String() string

func (FieldEquals) Substitute 

func (c FieldEquals) Substitute(args []Path) (Constraint, bool)

type FieldEqualsPath 

type FieldEqualsPath struct {
	Target Path
	Field  string
	Value  Path
}

FieldEqualsPath constrains target.field to equal a value path.

func (FieldEqualsPath) Equals 

func (c FieldEqualsPath) Equals(o Constraint) bool

func (FieldEqualsPath) Hash 

func (c FieldEqualsPath) Hash() uint64

func (FieldEqualsPath) Kind 

func (c FieldEqualsPath) Kind() Kind

func (FieldEqualsPath) Paths 

func (c FieldEqualsPath) Paths() []Path

func (FieldEqualsPath) String 

func (c FieldEqualsPath) String() string

func (FieldEqualsPath) Substitute 

func (c FieldEqualsPath) Substitute(args []Path) (Constraint, bool)

type FieldNotEquals 

type FieldNotEquals struct {
	Target Path
	Field  string
	Value  *typ.Literal
}

FieldNotEquals constrains a field on a path to NOT equal a literal value.

func (FieldNotEquals) Equals 

func (c FieldNotEquals) Equals(o Constraint) bool

func (FieldNotEquals) Hash 

func (c FieldNotEquals) Hash() uint64

func (FieldNotEquals) Kind 

func (c FieldNotEquals) Kind() Kind

func (FieldNotEquals) Paths 

func (c FieldNotEquals) Paths() []Path

func (FieldNotEquals) String 

func (c FieldNotEquals) String() string

func (FieldNotEquals) Substitute 

func (c FieldNotEquals) Substitute(args []Path) (Constraint, bool)

type FieldNotEqualsPath 

type FieldNotEqualsPath struct {
	Target Path
	Field  string
	Value  Path
}

FieldNotEqualsPath constrains target.field to NOT equal a value path. Used for else-branches in channel select narrowing.

func (FieldNotEqualsPath) Equals 

func (c FieldNotEqualsPath) Equals(o Constraint) bool

func (FieldNotEqualsPath) Hash 

func (c FieldNotEqualsPath) Hash() uint64

func (FieldNotEqualsPath) Kind 

func (c FieldNotEqualsPath) Kind() Kind

func (FieldNotEqualsPath) Paths 

func (c FieldNotEqualsPath) Paths() []Path

func (FieldNotEqualsPath) String 

func (c FieldNotEqualsPath) String() string

func (FieldNotEqualsPath) Substitute 

func (c FieldNotEqualsPath) Substitute(args []Path) (Constraint, bool)

type FunctionEffect 

type FunctionEffect struct {
	// Row is the effect label set (IO, Mutate, Throw, etc.).
	// Stored as typ.EffectInfo to avoid circular import with effect package.
	// The concrete type is effect.Row.
	Row typ.EffectInfo

	// OnReturn: constraints that hold when function returns normally.
	// Used for assert-style functions that error() on failure.
	OnReturn Condition

	// OnTrue: constraints that hold when function returns truthy.
	// Used for type predicate functions like isString(x).
	OnTrue Condition

	// OnFalse: constraints that hold when function returns falsy.
	OnFalse Condition

	// Terminates indicates the function never returns normally.
	// Used for functions that always call error() or similar.
	Terminates bool
}

FunctionEffect describes the type refinements a function produces.

Effects encode how a function call narrows types based on its return value. Three categories are supported:

  • OnReturn: constraints that hold when the function returns normally (used for assert-style functions that error() on failure)
  • OnTrue: constraints that hold when the function returns truthy (used for type predicate functions like isString(x))
  • OnFalse: constraints that hold when the function returns falsy

Placeholder roots ($0, $1, ...) reference parameters by position. At call sites, placeholders are substituted with actual argument paths.

func NewEffect 

func NewEffect(onReturn, onTrue, onFalse []Constraint) *FunctionEffect

NewEffect creates a FunctionEffect from constraint slices.

func (*FunctionEffect) Equals 

func (e *FunctionEffect) Equals(other any) bool

Equals returns true if two function effects are structurally equal. Implements internal.Equaler interface for use in typ.Function.

func (*FunctionEffect) HasAssertSemantics 

func (e *FunctionEffect) HasAssertSemantics() bool

HasAssertSemantics returns true if function has assert-style semantics.

func (*FunctionEffect) HasPredicateSemantics 

func (e *FunctionEffect) HasPredicateSemantics() bool

HasPredicateSemantics returns true if function has predicate semantics.

func (*FunctionEffect) IsEmpty 

func (e *FunctionEffect) IsEmpty() bool

IsEmpty returns true if the effect has no constraints, no row, and doesn't terminate.

func (*FunctionEffect) IsRefinementInfo 

func (e *FunctionEffect) IsRefinementInfo()

IsRefinementInfo implements typ.RefinementInfo.

func (*FunctionEffect) KeysCollectorParamIndex 

func (e *FunctionEffect) KeysCollectorParamIndex() int

KeysCollectorParamIndex checks if the function returns keys of a parameter.

Detects patterns like `for k in pairs(t)` where the function returns keys from a table parameter. Returns the parameter index (0-based) if found, or -1 if the function doesn't have this behavior.

Detection looks for KeyOf constraints in OnReturn where the table is a parameter placeholder ($N) and the key is a return path.

func (*FunctionEffect) Substitute 

func (e *FunctionEffect) Substitute(args []Path) *FunctionEffect

Substitute returns a new FunctionEffect with placeholder paths replaced.

At a call site, parameter placeholders ($0, $1, ...) are replaced with the actual argument paths, producing concrete constraints that can be applied to narrow types at the call location.

type Ge 

type Ge struct {
	X Path
	Y Path
}

Ge represents x >= y.

func (Ge) Equals 

func (c Ge) Equals(o NumericConstraint) bool

func (Ge) Hash 

func (c Ge) Hash() uint64

func (Ge) NumKind 

func (c Ge) NumKind() NumKind

func (Ge) Paths 

func (c Ge) Paths() []Path

type GeConst 

type GeConst struct {
	X Path
	C int64
}

GeConst represents x >= c.

func (GeConst) Equals 

func (c GeConst) Equals(o NumericConstraint) bool

func (GeConst) Hash 

func (c GeConst) Hash() uint64

func (GeConst) NumKind 

func (c GeConst) NumKind() NumKind

func (GeConst) Paths 

func (c GeConst) Paths() []Path

type Gt 

type Gt struct {
	X Path
	Y Path
}

Gt represents x > y.

func (Gt) Equals 

func (c Gt) Equals(o NumericConstraint) bool

func (Gt) Hash 

func (c Gt) Hash() uint64

func (Gt) NumKind 

func (c Gt) NumKind() NumKind

func (Gt) Paths 

func (c Gt) Paths() []Path

type HasField 

type HasField struct {
	Path  Path
	Field string
}

HasField narrows a union to members that have a specific field. Used for truthy field access narrowing: `if x.field then` narrows x to types with field.

func (HasField) Equals 

func (c HasField) Equals(o Constraint) bool

func (HasField) Hash 

func (c HasField) Hash() uint64

func (HasField) Kind 

func (c HasField) Kind() Kind

func (HasField) Paths 

func (c HasField) Paths() []Path

func (HasField) String 

func (c HasField) String() string

func (HasField) Substitute 

func (c HasField) Substitute(args []Path) (Constraint, bool)

type HasType 

type HasType struct {
	Path Path
	Type narrow.TypeKey
}

HasType constrains a path to have a specific runtime type. Generated from type(x) == "string" checks and similar guards. TypeKey identifies the type category (string, number, table, etc.).

func (HasType) Equals 

func (c HasType) Equals(o Constraint) bool

func (HasType) Hash 

func (c HasType) Hash() uint64

func (HasType) Kind 

func (c HasType) Kind() Kind

func (HasType) Paths 

func (c HasType) Paths() []Path

func (HasType) String 

func (c HasType) String() string

func (HasType) Substitute 

func (c HasType) Substitute(args []Path) (Constraint, bool)

type IndexEquals 

type IndexEquals struct {
	Target Path
	Key    typ.Type
	Value  *typ.Literal
}

IndexEquals constrains an index on a path to a literal value.

func (IndexEquals) Equals 

func (c IndexEquals) Equals(o Constraint) bool

func (IndexEquals) Hash 

func (c IndexEquals) Hash() uint64

func (IndexEquals) Kind 

func (c IndexEquals) Kind() Kind

func (IndexEquals) Paths 

func (c IndexEquals) Paths() []Path

func (IndexEquals) String 

func (c IndexEquals) String() string

func (IndexEquals) Substitute 

func (c IndexEquals) Substitute(args []Path) (Constraint, bool)

type IndexEqualsPath 

type IndexEqualsPath struct {
	Target Path
	Key    typ.Type
	Value  Path
}

IndexEqualsPath constrains target[key] to equal a value path.

func (IndexEqualsPath) Equals 

func (c IndexEqualsPath) Equals(o Constraint) bool

func (IndexEqualsPath) Hash 

func (c IndexEqualsPath) Hash() uint64

func (IndexEqualsPath) Kind 

func (c IndexEqualsPath) Kind() Kind

func (IndexEqualsPath) Paths 

func (c IndexEqualsPath) Paths() []Path

func (IndexEqualsPath) String 

func (c IndexEqualsPath) String() string

func (IndexEqualsPath) Substitute 

func (c IndexEqualsPath) Substitute(args []Path) (Constraint, bool)

type IndexNotEquals 

type IndexNotEquals struct {
	Target Path
	Key    typ.Type
	Value  *typ.Literal
}

IndexNotEquals constrains an index on a path to NOT equal a literal value.

func (IndexNotEquals) Equals 

func (c IndexNotEquals) Equals(o Constraint) bool

func (IndexNotEquals) Hash 

func (c IndexNotEquals) Hash() uint64

func (IndexNotEquals) Kind 

func (c IndexNotEquals) Kind() Kind

func (IndexNotEquals) Paths 

func (c IndexNotEquals) Paths() []Path

func (IndexNotEquals) String 

func (c IndexNotEquals) String() string

func (IndexNotEquals) Substitute 

func (c IndexNotEquals) Substitute(args []Path) (Constraint, bool)

type IndexNotEqualsPath 

type IndexNotEqualsPath struct {
	Target Path
	Key    typ.Type
	Value  Path
}

IndexNotEqualsPath constrains target[key] to NOT equal a value path.

func (IndexNotEqualsPath) Equals 

func (c IndexNotEqualsPath) Equals(o Constraint) bool

func (IndexNotEqualsPath) Hash 

func (c IndexNotEqualsPath) Hash() uint64

func (IndexNotEqualsPath) Kind 

func (c IndexNotEqualsPath) Kind() Kind

func (IndexNotEqualsPath) Paths 

func (c IndexNotEqualsPath) Paths() []Path

func (IndexNotEqualsPath) String 

func (c IndexNotEqualsPath) String() string

func (IndexNotEqualsPath) Substitute 

func (c IndexNotEqualsPath) Substitute(args []Path) (Constraint, bool)

type InferSet 

type InferSet struct {
	// contains filtered or unexported fields
}

InferSet collects bounds for type variables during generic type inference.

InferSet implements constraint-based type inference using bounds tracking. It collects subtype relationships between type variables and concrete types, then solves for the most specific types that satisfy all constraints.

Algorithm

1. Constraints are added via InferSet.AddSubtype and InferSet.AddEqual 2. Lower bounds (types that are subtypes of the variable) are joined 3. Upper bounds (types that the variable must be a subtype of) are met 4. Cyclic dependencies are resolved using Tarjan's SCC algorithm 5. InferSet.Solve returns a substitution mapping variables to concrete types

Example 

cs := constraint.NewInferSet()
tv := typ.NewTypeVar(1)

// T is a supertype of string (string <: T)
cs.AddSubtype(typ.String, tv)

// T is a subtype of any (T <: any)
cs.AddSubtype(tv, typ.Any)

subst, err := cs.Solve()
// subst[1] == typ.String

Cyclic Dependencies

When type variables form cycles (T1 <: T2 <: T3 <: T1), InferSet uses Tarjan's algorithm to find strongly connected components and unifies all variables in each SCC to a single representative.

func NewInferSet 

func NewInferSet() *InferSet

NewInferSet creates an empty inference constraint set.

func (*InferSet) AddEqual 

func (c *InferSet) AddEqual(a, b typ.Type)

AddEqual records that two types must be equal.

func (*InferSet) AddSubtype 

func (c *InferSet) AddSubtype(sub, super typ.Type)

AddSubtype records sub <: super. If sub is TypeVar, super becomes upper bound. If super is TypeVar, sub becomes lower bound.

func (*InferSet) Solve 

func (c *InferSet) Solve() (InferSubstitution, error)

Solve attempts to solve all constraints.

type InferSubstitution 

type InferSubstitution map[int]typ.Type

InferSubstitution maps type variable IDs to their solved types.

func (InferSubstitution) Apply 

func (s InferSubstitution) Apply(t typ.Type) typ.Type

Apply applies this substitution to a type.

type Interner 

type Interner struct {
	// contains filtered or unexported fields
}

Interner provides constraint interning to reduce allocations for common patterns. Thread-safe for concurrent use.

Interning is beneficial when the same constraints are created repeatedly, such as Truthy/Falsy/IsNil/NotNil on frequently-accessed paths. Interned constraints share storage, reducing GC pressure in hot paths.

Usage: 

interner := NewInterner()
c1 := interner.Truthy(path)
c2 := interner.Truthy(path)  // returns same instance as c1

func NewInterner 

func NewInterner() *Interner

NewInterner creates a new constraint interner.

func (*Interner) Clear 

func (i *Interner) Clear()

Clear removes all interned constraints.

func (*Interner) Falsy 

func (i *Interner) Falsy(p Path) Falsy

Falsy returns an interned Falsy constraint for the given path.

func (*Interner) IsNil 

func (i *Interner) IsNil(p Path) IsNil

IsNil returns an interned IsNil constraint for the given path.

func (*Interner) NotNil 

func (i *Interner) NotNil(p Path) NotNil

NotNil returns an interned NotNil constraint for the given path.

func (*Interner) Size 

func (i *Interner) Size() int

Size returns the total number of interned constraints.

func (*Interner) Truthy 

func (i *Interner) Truthy(p Path) Truthy

Truthy returns an interned Truthy constraint for the given path.

type IsNil 

type IsNil struct {
	Path Path
}

IsNil requires path to be nil.

func (IsNil) Equals 

func (c IsNil) Equals(o Constraint) bool

func (IsNil) Hash 

func (c IsNil) Hash() uint64

func (IsNil) Kind 

func (c IsNil) Kind() Kind

func (IsNil) Paths 

func (c IsNil) Paths() []Path

func (IsNil) String 

func (c IsNil) String() string

func (IsNil) Substitute 

func (c IsNil) Substitute(args []Path) (Constraint, bool)

type KeyOf 

type KeyOf struct {
	Table Path
	Key   Path
}

KeyOf constrains a key path to be a known key of a table path. When satisfied, index access table[key] is guaranteed to return a value, allowing removal of the optional wrapper from the result type. Generated from patterns like: for k in pairs(t) do t[k] end

func (KeyOf) Equals 

func (c KeyOf) Equals(o Constraint) bool

func (KeyOf) Hash 

func (c KeyOf) Hash() uint64

func (KeyOf) Kind 

func (c KeyOf) Kind() Kind

func (KeyOf) Paths 

func (c KeyOf) Paths() []Path

func (KeyOf) String 

func (c KeyOf) String() string

func (KeyOf) Substitute 

func (c KeyOf) Substitute(args []Path) (Constraint, bool)

type Kind 

type Kind uint8

Kind classifies a constraint term for dispatch and serialization. 

const (
	KindInvalid Kind = iota
	KindTruthy
	KindFalsy
	KindIsNil
	KindNotNil
	KindHasType
	KindNotHasType
	KindHasField
	KindFieldEquals
	KindFieldNotEquals
	KindIndexEquals
	KindIndexNotEquals
	KindEqPath
	KindNotEqPath
	KindFieldEqualsPath
	KindFieldNotEqualsPath
	KindIndexEqualsPath
	KindIndexNotEqualsPath
	KindKeyOf
)

type Le 

type Le struct {
	X Path
	Y Path
	C int64
}

Le represents x - y <= c.

func (Le) Equals 

func (c Le) Equals(o NumericConstraint) bool

func (Le) Hash 

func (c Le) Hash() uint64

func (Le) NumKind 

func (c Le) NumKind() NumKind

func (Le) Paths 

func (c Le) Paths() []Path

type LeConst 

type LeConst struct {
	X Path
	C int64
}

LeConst represents x <= c.

func (LeConst) Equals 

func (c LeConst) Equals(o NumericConstraint) bool

func (LeConst) Hash 

func (c LeConst) Hash() uint64

func (LeConst) NumKind 

func (c LeConst) NumKind() NumKind

func (LeConst) Paths 

func (c LeConst) Paths() []Path

type LeLenOf 

type LeLenOf struct {
	X     Path // variable being bounded
	Array Path // array whose length is the upper bound
}

LeLenOf represents x <= len(arr), a symbolic upper bound.

func (LeLenOf) Equals 

func (c LeLenOf) Equals(o NumericConstraint) bool

func (LeLenOf) Hash 

func (c LeLenOf) Hash() uint64

func (LeLenOf) NumKind 

func (c LeLenOf) NumKind() NumKind

func (LeLenOf) Paths 

func (c LeLenOf) Paths() []Path

type Len 

type Len struct {
	Of string // variable name of the array
}

Len represents the length of a symbolic array/tuple.

func L 

func L(name string) Len

L creates a length expression.

func (Len) Eval 

func (l Len) Eval(env map[string]int64) (int64, bool)

func (Len) String 

func (l Len) String() string

func (Len) Substitute 

func (l Len) Substitute(subst map[string]Expr) Expr

func (Len) Variables 

func (l Len) Variables() []string

type Lt 

type Lt struct {
	X Path
	Y Path
}

Lt represents x < y.

func (Lt) Equals 

func (c Lt) Equals(o NumericConstraint) bool

func (Lt) Hash 

func (c Lt) Hash() uint64

func (Lt) NumKind 

func (c Lt) NumKind() NumKind

func (Lt) Paths 

func (c Lt) Paths() []Path

type Max 

type Max struct {
	Left  Expr
	Right Expr
}

Max represents the maximum of two expressions.

func MaxExpr 

func MaxExpr(left, right Expr) Max

MaxExpr creates a max expression.

func (Max) Eval 

func (m Max) Eval(env map[string]int64) (int64, bool)

func (Max) String 

func (m Max) String() string

func (Max) Substitute 

func (m Max) Substitute(subst map[string]Expr) Expr

func (Max) Variables 

func (m Max) Variables() []string

type Min 

type Min struct {
	Left  Expr
	Right Expr
}

Min represents the minimum of two expressions.

func MinExpr 

func MinExpr(left, right Expr) Min

MinExpr creates a min expression.

func (Min) Eval 

func (m Min) Eval(env map[string]int64) (int64, bool)

func (Min) String 

func (m Min) String() string

func (Min) Substitute 

func (m Min) Substitute(subst map[string]Expr) Expr

func (Min) Variables 

func (m Min) Variables() []string

type ModEq 

type ModEq struct {
	X Path
	M int64
	R int64
}

ModEq represents x % m == r.

func (ModEq) Equals 

func (c ModEq) Equals(o NumericConstraint) bool

func (ModEq) Hash 

func (c ModEq) Hash() uint64

func (ModEq) NumKind 

func (c ModEq) NumKind() NumKind

func (ModEq) Paths 

func (c ModEq) Paths() []Path

type NotEqPath 

type NotEqPath struct {
	Left  Path
	Right Path
}

NotEqPath constrains two paths to NOT be equal. Used for negation of EqPath in inequality conditions.

func NewNotEqPath 

func NewNotEqPath(left, right Path) NotEqPath

func (NotEqPath) Equals 

func (c NotEqPath) Equals(o Constraint) bool

func (NotEqPath) Hash 

func (c NotEqPath) Hash() uint64

func (NotEqPath) Kind 

func (c NotEqPath) Kind() Kind

func (NotEqPath) Paths 

func (c NotEqPath) Paths() []Path

func (NotEqPath) String 

func (c NotEqPath) String() string

func (NotEqPath) Substitute 

func (c NotEqPath) Substitute(args []Path) (Constraint, bool)

type NotHasType 

type NotHasType struct {
	Path Path
	Type narrow.TypeKey
}

NotHasType constrains a path to NOT have a type key. Used for negation of HasType in inequality conditions.

func (NotHasType) Equals 

func (c NotHasType) Equals(o Constraint) bool

func (NotHasType) Hash 

func (c NotHasType) Hash() uint64

func (NotHasType) Kind 

func (c NotHasType) Kind() Kind

func (NotHasType) Paths 

func (c NotHasType) Paths() []Path

func (NotHasType) String 

func (c NotHasType) String() string

func (NotHasType) Substitute 

func (c NotHasType) Substitute(args []Path) (Constraint, bool)

type NotNil 

type NotNil struct {
	Path Path
}

NotNil requires path to be non-nil.

func (NotNil) Equals 

func (c NotNil) Equals(o Constraint) bool

func (NotNil) Hash 

func (c NotNil) Hash() uint64

func (NotNil) Kind 

func (c NotNil) Kind() Kind

func (NotNil) Paths 

func (c NotNil) Paths() []Path

func (NotNil) String 

func (c NotNil) String() string

func (NotNil) Substitute 

func (c NotNil) Substitute(args []Path) (Constraint, bool)

type NumKind 

type NumKind uint8

NumKind classifies numeric constraint terms. 

const (
	NumInvalid NumKind = iota
	NumLe              // x - y <= c
	NumLt              // x < y
	NumGe              // x >= y
	NumGt              // x > y
	NumEq              // x == y
	NumEqConst         // x == c
	NumLeConst         // x <= c
	NumGeConst         // x >= c
	NumModEq           // x % m == r
	NumLeLenOf         // x <= len(arr)
)

type NumericConstraint 

type NumericConstraint interface {
	NumKind() NumKind
	Paths() []Path
	Hash() uint64
	Equals(other NumericConstraint) bool
}

NumericConstraint is a marker interface for numeric constraints.

type NumericConstraintVisitor 

type NumericConstraintVisitor[R any] struct {
	Le      func(Le) R
	Lt      func(Lt) R
	Ge      func(Ge) R
	Gt      func(Gt) R
	Eq      func(Eq) R
	EqConst func(EqConst) R
	LeConst func(LeConst) R
	GeConst func(GeConst) R
	ModEq   func(ModEq) R
	LeLenOf func(LeLenOf) R
	Default func(NumericConstraint) R
}

NumericConstraintVisitor dispatches on numeric constraint variants. Nil handlers fall back to Default when provided; otherwise return zero.

type Op 

type Op int

Op represents an arithmetic operator. 

const (
	OpAdd Op = iota // +
	OpSub           // -
	OpMul           // *
	OpDiv           // /
	OpMod           // %
)

func (Op) String 

func (op Op) String() string

type Param 

type Param struct {
	Index int // 0-based parameter index
}

Param represents a reference to a function parameter by index. Used in function refinements: len(Param(0)) = 5

func P 

func P(index int) Param

P creates a parameter reference expression.

func (Param) Eval 

func (p Param) Eval(env map[string]int64) (int64, bool)

func (Param) String 

func (p Param) String() string

func (Param) Substitute 

func (p Param) Substitute(subst map[string]Expr) Expr

func (Param) Variables 

func (p Param) Variables() []string

type ParamLen 

type ParamLen struct {
	Index int // 0-based parameter index
}

ParamLen represents the length of a function parameter. Shorthand for Len applied to Param.

func PL 

func PL(index int) ParamLen

PL creates a parameter length expression.

func (ParamLen) Eval 

func (p ParamLen) Eval(env map[string]int64) (int64, bool)

func (ParamLen) String 

func (p ParamLen) String() string

func (ParamLen) Substitute 

func (p ParamLen) Substitute(subst map[string]Expr) Expr

func (ParamLen) Variables 

func (p ParamLen) Variables() []string

type Path 

type Path struct {
	Root     string       // Variable name (optional for symbol paths, required for placeholders)
	Symbol   cfg.SymbolID // SymbolID for identity (0 if unresolved/placeholder)
	Segments []Segment
	Version  int // SSA version ID (0 = unspecified, non-zero binds path to a specific version)
}

Path identifies a runtime value through its access path (variable.field.index).

Paths are the fundamental identity mechanism for type narrowing. They track values across control flow using SSA-style symbol IDs, enabling precise narrowing even when the same variable name refers to different bindings.

Symbol provides SSA identity; Root is optional for display when Symbol is set. When Symbol is non-zero, it is the primary identity for the path root. Placeholder paths ($0, $1, etc.) use Root only with Symbol=0 and are substituted with concrete paths when applying function effects at call sites.

Examples:

  • {Root: "x", Symbol: 5}: Variable x with symbol ID 5
  • {Root: "x", Symbol: 5, Segments: [{Field, "name", 0}]}: x.name
  • {Root: "$0", Symbol: 0}: Placeholder for first function parameter

func NewPath 

func NewPath(sym cfg.SymbolID, name string) Path

NewPath creates a path with the given symbol and display name. This is the primary constructor for resolved paths.

Example: 

path := NewPath(sym, "x")           // x
path := NewPath(sym, "x").Field("y") // x.y

func NewPlaceholder 

func NewPlaceholder(index int) Path

NewPlaceholder creates a placeholder path for function effect parameters. Index 0 creates $0, index 1 creates $1, etc.

Example: 

p0 := NewPlaceholder(0) // $0 (first parameter)
p1 := NewPlaceholder(1) // $1 (second parameter)

func ParamPath 

func ParamPath(index int) Path

ParamPath returns the path for a parameter value. Uses the $N format which is recognized by IsPlaceholder() and PlaceholderIndex().

func RetPath 

func RetPath(index int) Path

RetPath returns the path for a return value.

func SplitFieldPath 

func SplitFieldPath(path Path) (parent Path, field string, ok bool)

SplitFieldPath splits a path into its parent path and field name. Returns false if the path has no field segments. The returned parent path owns its own segment slice (safe to mutate).

func (Path) Append 

func (p Path) Append(seg Segment) Path

Append returns a new path with the given segment appended. Returns an empty path if the receiver is empty.

func (Path) DisplayRoot 

func (p Path) DisplayRoot(nameResolver func(cfg.SymbolID) string) string

DisplayRoot returns the display name for the path root. For symbol-rooted paths, uses the provided nameResolver to get the name. For placeholder paths (Symbol=0), returns the Root field directly.

func (Path) Equal 

func (p Path) Equal(other Path) bool

Equal returns true if two paths have the same identity. Symbol-based identity takes precedence when available.

func (Path) Field 

func (p Path) Field(name string) Path

Field returns a new path with a field access segment appended.

Example: 

path.Field("name")  // path.name
path.Field("a").Field("b") // path.a.b

func (Path) FieldName 

func (p Path) FieldName() string

FieldName returns the field name if the last segment is a field access. Returns empty string if not a field access.

func (Path) HasSymbol 

func (p Path) HasSymbol() bool

HasSymbol returns true if this path has a resolved SymbolID.

func (Path) Hash 

func (p Path) Hash() uint64

Hash returns a 64-bit hash of the path for use in hash-based collections. Symbol-based identity is used when available, otherwise Root is hashed.

func (Path) IndexInt 

func (p Path) IndexInt(index int) Path

IndexInt returns a new path with an integer index segment appended.

Example: 

path.IndexInt(0)  // path[0]
path.IndexInt(1)  // path[1]

func (Path) IndexStr 

func (p Path) IndexStr(key string) Path

IndexStr returns a new path with a string index segment appended.

Example: 

path.IndexStr("key")  // path["key"]

func (Path) IsEmpty 

func (p Path) IsEmpty() bool

IsEmpty returns true if the path has no identity (no Root and no Symbol).

func (Path) IsFieldAccess 

func (p Path) IsFieldAccess() bool

IsFieldAccess returns true if the last segment is a field access.

func (Path) IsPlaceholder 

func (p Path) IsPlaceholder() bool

IsPlaceholder returns true if this path is a placeholder (used in function effects). Placeholders have Symbol == 0 and Root matching $0, $1, etc.

func (Path) Key 

func (p Path) Key() PathKey

Key returns a stable key representation of the path. Format: sym<SymbolID>@<VersionID><segments> for versioned symbol paths, sym<SymbolID><segments> for unversioned symbol paths, <Root><segments> for placeholders. For versioned flow lookups, prefer pathkey.Resolver.KeyAt.

func (Path) LastSegment 

func (p Path) LastSegment() (Segment, bool)

LastSegment returns the final segment of the path, if any. Returns (segment, true) if the path has segments, (zero, false) otherwise.

func (Path) Less 

func (p Path) Less(other Path) bool

Less provides a stable ordering for canonicalization. Compares by Symbol first when both are set, otherwise by Root.

func (Path) Parent 

func (p Path) Parent() Path

Parent returns the path without its last segment. Returns an empty path if there are no segments.

Example: 

path.Field("a").Field("b").Parent() // path.a

func (Path) PlaceholderIndex 

func (p Path) PlaceholderIndex() int

PlaceholderIndex returns the parameter index if this path's root is a placeholder ($0, $1, etc). Returns -1 if not a placeholder.

func (Path) String 

func (p Path) String() string

String returns a human-readable representation of the path. Format: root.field[index] where root is either the variable name or $symN for symbol-only paths.

func (Path) Substitute 

func (p Path) Substitute(args []Path) (Path, bool)

Substitute replaces placeholder roots with actual argument paths. Only paths with Symbol == 0 and Root matching $0, $1, etc. are substituted. Returns (result, true) on success, (empty, false) if placeholder out of range or arg path empty.

func (Path) ValidateSymbol 

func (p Path) ValidateSymbol() string

ValidateSymbol checks the symbol-first identity invariant. For resolved paths (non-empty, non-placeholder), Symbol must be non-zero. Returns empty string if valid, error message if invalid. Used for debug-mode assertions.

type PathKey 

type PathKey string

PathKey is a stable string key for map usage.

func SortedPathKeys 

func SortedPathKeys[T any](m map[PathKey]T) []PathKey

SortedPathKeys returns PathKeys in deterministic order for map iteration.

type PathResolver 

type PathResolver func(Path) PathKey

PathResolver resolves unversioned constraint paths to versioned PathKeys.

type PathTypeResolver 

type PathTypeResolver func(PathKey) typ.Type

PathTypeResolver resolves a constraint path key to its type at a program point.

type Ret 

type Ret struct {
	Index int // 0-based return value index
}

Ret represents a reference to a function return value by index. Used in function refinements: len(Ret(0)) = len(Param(0))

func R 

func R(index int) Ret

R creates a return value reference expression.

func (Ret) Eval 

func (r Ret) Eval(env map[string]int64) (int64, bool)

func (Ret) String 

func (r Ret) String() string

func (Ret) Substitute 

func (r Ret) Substitute(subst map[string]Expr) Expr

func (Ret) Variables 

func (r Ret) Variables() []string

type RetLen 

type RetLen struct {
	Index int // 0-based return value index
}

RetLen represents the length of a function return value. Shorthand for Len applied to Ret.

func RL 

func RL(index int) RetLen

RL creates a return length expression.

func (RetLen) Eval 

func (r RetLen) Eval(env map[string]int64) (int64, bool)

func (RetLen) String 

func (r RetLen) String() string

func (RetLen) Substitute 

func (r RetLen) Substitute(subst map[string]Expr) Expr

func (RetLen) Variables 

func (r RetLen) Variables() []string

type Segment 

type Segment struct {
	Kind  SegmentKind
	Name  string
	Index int
}

Segment identifies a single field or index access step on a path. For field access (.name), Kind is SegmentField and Name holds the field name. For string index (["key"]), Kind is SegmentIndexString and Name holds the key. For integer index ([1]), Kind is SegmentIndexInt and Index holds the value.

type SegmentKind 

type SegmentKind uint8

SegmentKind describes how a path accesses a nested value. 

const (
	SegmentField SegmentKind = iota
	SegmentIndexString
	SegmentIndexInt
)

type Solver 

type Solver struct {
	Env Env
}

Solver applies constraints to type environments to produce narrowed types.

The solver is pure and deterministic: given the same constraints and base types, it always produces the same narrowed types. This enables memoization and incremental re-analysis.

The solver iterates until a fixed point is reached, propagating narrowing information across related paths (e.g., EqPath narrows both endpoints).

func (Solver) Apply 

func (s Solver) Apply(constraints []Constraint, base map[PathKey]typ.Type) map[PathKey]typ.Type

Apply applies a conjunction of constraints to base types and returns narrowed types.

The solver iterates through constraints, applying each one and propagating narrowing information until no further changes occur. Unknown paths in constraints are ignored.

For large constraint sets (>100 constraints), the solver uses path-based work skipping: after the first iteration, only constraints that reference paths which changed in the previous iteration are re-evaluated.

func (Solver) ApplyToSingle 

func (s Solver) ApplyToSingle(constraints []Constraint, target PathKey, base typ.Type, resolve PathResolver) typ.Type

ApplyToSingle applies a conjunction of constraints to a single path, returning the narrowed type. Only constraints whose resolved path matches target are applied.

type Term 

type Term struct {
	Kind  TermKind
	Path  PathKey // for Var and Len
	Const int64   // for Const
}

Term represents a value in the constraint language.

func TermConst 

func TermConst(c int64) Term

TermConst creates a constant term from an integer value.

func TermLen 

func TermLen(key PathKey) Term

TermLen creates a length term from a path key.

func TermNil 

func TermNil() Term

TermNil returns the nil term.

func TermVar 

func TermVar(key PathKey) Term

TermVar creates a variable term from a path key.

func (Term) Equal 

func (t Term) Equal(other Term) bool

func (Term) Hash 

func (t Term) Hash() uint64

func (Term) IsConst 

func (t Term) IsConst() bool

func (Term) IsLen 

func (t Term) IsLen() bool

func (Term) IsNil 

func (t Term) IsNil() bool

func (Term) IsVar 

func (t Term) IsVar() bool

func (Term) Paths 

func (t Term) Paths() []PathKey

Paths returns all path keys referenced by this term.

func (Term) String 

func (t Term) String() string

type TermKind 

type TermKind uint8

TermKind classifies term variants. 

const (
	TermKindInvalid TermKind = iota
	TermKindVar              // variable path reference
	TermKindLen              // length of array/table
	TermKindConst            // integer constant
	TermKindNil              // nil value
)

type Truthy 

type Truthy struct {
	Path Path
}

Truthy requires path to evaluate to a truthy value (not nil and not false). Removes nil and false from the path's type in the then-branch.

func (Truthy) Equals 

func (c Truthy) Equals(o Constraint) bool

func (Truthy) Hash 

func (c Truthy) Hash() uint64

func (Truthy) Kind 

func (c Truthy) Kind() Kind

func (Truthy) Paths 

func (c Truthy) Paths() []Path

func (Truthy) String 

func (c Truthy) String() string

func (Truthy) Substitute 

func (c Truthy) Substitute(args []Path) (Constraint, bool)

type UnsatisfiableError 

type UnsatisfiableError struct{}

UnsatisfiableError represents constraint set with concrete type violations.

func (*UnsatisfiableError) Error 

func (e *UnsatisfiableError) Error() string

type Var 

type Var struct {
	Name string
}

Var represents a symbolic variable (e.g., "i", "len_arr").

func V 

func V(name string) Var

V creates a variable expression.

func (Var) Eval 

func (v Var) Eval(env map[string]int64) (int64, bool)

func (Var) String 

func (v Var) String() string

func (Var) Substitute 

func (v Var) Substitute(subst map[string]Expr) Expr

func (Var) Variables 

func (v Var) Variables() []string

Source Files

View all Source files

Directories

Path Synopsis
Package theory provides modular constraint solving theories for SMT-style reasoning.
 Package theory provides modular constraint solving theories for SMT-style reasoning.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.