domain

package
v1.5.9 Latest Latest
Warning

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

Go to latest
Published: Feb 14, 2026 License: MIT Imports: 5 Imported by: 0

Documentation

Overview

Package domain provides abstract domain interfaces for constraint solving.

The domain package defines the interfaces for type and numeric constraint domains used by the flow solver. Each domain processes constraints relevant to its abstraction level:

  • TypeDomain: Handles type-based constraints (HasType, NotHasType, Truthy, Falsy)
  • NumericDomain: Handles numeric constraints (Lt, Le, Gt, Ge, ModEq, Eq, Ne)

The flow solver routes atoms to the appropriate domain based on ClassifyAtom, which returns AtomClassType, AtomClassNumeric, or AtomClassBoth.

Domain Protocol

Domains implement the Domain interface with three methods:

  • IsUnsat(): Returns true if the domain has reached a contradiction
  • Clone(): Creates an independent copy for speculative narrowing
  • Join(): Merges two domain states (used at phi nodes)

Type and numeric domains extend this with ApplyAtom for constraint application.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func IsChildPath

func IsChildPath(parent, child string) bool

IsChildPath returns true if child is a descendant path of parent.

A path is a child if it extends the parent with one or more path segments (field or index access) under the same canonical root.

Examples:

  • IsChildPath("sym1@1", "sym1@1.foo") -> true
  • IsChildPath("sym1@1", "sym1@1.foo.bar") -> true
  • IsChildPath("sym1@1.foo", "sym1@1.foo.bar") -> true
  • IsChildPath("sym1@1", "sym1@1[0]") -> true
  • IsChildPath("sym1@1", "sym1@1") -> false (not strict descendant)
  • IsChildPath("sym1@1", "sym1@10") -> false (different version, not child)

func SplitPathKey

func SplitPathKey(key constraint.PathKey) (constraint.PathKey, string, bool)

SplitPathKey extracts the parent key and field name from a path key.

Given a key like "sym42@3.field", returns ("sym42@3", "field", true). This is used for parent narrowing: when a field like r.ok is tested, we may need to narrow the parent type r based on the field's value.

The function finds the last '.' not inside brackets and splits there. If no such dot exists (the key has no field segment), returns ("", "", false).

Examples:

  • "sym1@1.foo" -> ("sym1@1", "foo", true)
  • "sym1@1.foo.bar" -> ("sym1@1.foo", "bar", true)
  • "sym1@1[0].x" -> ("sym1@1[0]", "x", true)
  • "sym1@1" -> ("", "", false)
  • "sym1@1[0]" -> ("", "", false)

Types

type AtomClass

type AtomClass int

AtomClass classifies atoms for routing.

const (
	AtomClassNone AtomClass = iota
	AtomClassType
	AtomClassNumeric
	AtomClassBoth
)

func ClassifyAtom

func ClassifyAtom(atom constraint.Atom) AtomClass

ClassifyAtom determines which domain should handle an atom.

type Domain

type Domain interface {
	IsUnsat() bool
	Clone() Domain
	Join(other Domain) Domain
}

Domain represents an abstract domain for constraint solving.

type NumericNarrower

type NumericNarrower interface {
	ApplyAtom(atom constraint.Atom) bool
	IsUnsat() bool
	BoundsFor(key constraint.PathKey) (lower, upper int64, ok bool)
}

NumericNarrower provides numeric constraint results.

type ShapeDomain

type ShapeDomain struct {
	Narrowed map[constraint.PathKey]typ.Type
	Solver   constraint.Solver
	Env      constraint.Env
	Unsat    bool
}

ShapeDomain handles structural narrowing for tables and records.

ShapeDomain is one of the three subdomains in ProductDomain. It handles constraints that affect the structural shape of types, particularly tables:

  • Field presence: HasField constraints proving a table has a field
  • Field types: Narrowing field types based on usage
  • Index constraints: HasIndex proving indexability with a type
  • Metatable constraints: Proving metatable presence or structure

Unlike TypeDomain which handles primitive type predicates, ShapeDomain uses constraint.Solver for sophisticated shape reasoning. The Solver can:

  • Apply constraints to record types, narrowing fields
  • Handle open records (unknown additional fields)
  • Process map component constraints
  • Chain constraints through nested paths

When a constraint targets a nested path (e.g., t.user.name), ShapeDomain propagates narrowings to ancestor paths. If t.user.name is proven to be string, this may narrow t.user and t as well by proving they have the required structure.

The domain maintains a Narrowed map from path keys to narrowed types. Missing keys fall back to env.PathTypeAt for base types.

func NewShapeDomain

func NewShapeDomain(env constraint.Env) *ShapeDomain

NewShapeDomain creates a new ShapeDomain with the given environment.

The Solver is initialized with the same environment, ensuring consistent type resolution for nested constraint application.

func (*ShapeDomain) ApplyConstraint

func (d *ShapeDomain) ApplyConstraint(c constraint.Constraint, target constraint.PathKey) bool

ApplyConstraint applies a structural constraint and propagates to ancestors.

The method performs several steps:

  1. Look up the base type for the target path
  2. Apply the constraint via Solver.ApplyToSingle to get a narrowed type
  3. If narrowed type differs from base, store it in Narrowed map
  4. Walk up ancestor paths and apply the constraint to each

Ancestor propagation is crucial for nested field constraints. Given:

local t = {}  -- t: {}
if t.user.name then
    -- constraint: HasField(t.user, "name")
end

The constraint must propagate to prove t has a "user" field too. The method walks from the deepest path segment up to the root.

Returns false and sets Unsat=true if the constraint proves unsatisfiability.

func (*ShapeDomain) Clone

func (d *ShapeDomain) Clone() Domain

Clone creates a deep copy of the ShapeDomain for speculative evaluation.

The Narrowed map is deep copied; Solver and Env are shared by reference.

func (*ShapeDomain) IsUnsat

func (d *ShapeDomain) IsUnsat() bool

IsUnsat returns true if the domain has proven a structural contradiction.

func (*ShapeDomain) Join

func (d *ShapeDomain) Join(other Domain) Domain

Join computes the least upper bound of two ShapeDomain states.

Join semantics for shape domains:

  • If either domain is unsatisfiable, return a clone of the other
  • For keys in both domains, compute type union (join.Two)
  • Keys only in one domain are dropped (no narrowing survives)

For records, type union preserves only fields present in both types. For example, joining {foo: string, bar: number} with {foo: string} yields {foo: string} (bar is not present in both).

func (*ShapeDomain) NarrowedTypeAt

func (d *ShapeDomain) NarrowedTypeAt(key constraint.PathKey) typ.Type

NarrowedTypeAt returns only the explicitly narrowed type, not the base type.

Unlike TypeAt, this returns nil if there is no shape narrowing, even if the key has a base type. Used to check whether narrowing has occurred.

func (*ShapeDomain) TypeAt

func (d *ShapeDomain) TypeAt(key constraint.PathKey) typ.Type

TypeAt returns the type for a PathKey, preferring narrowed types over base types.

Lookup order:

  1. d.Narrowed[key] - explicitly narrowed type from shape constraints
  2. env.PathTypeAt(key) - base type from declarations

Returns nil if the key has no type in either source.

type TypeDomain

type TypeDomain struct {
	Narrowed map[constraint.PathKey]typ.Type
	Env      constraint.Env
	Unsat    bool
}

TypeDomain handles type narrowing based on type predicates and boolean constraints.

TypeDomain is one of the three subdomains in ProductDomain. It tracks narrowings derived from type-related constraints:

  • HasType: Narrows a union to include only the specified type. Example: HasType(x, "string") on x:string|number yields x:string

  • NotHasType: Removes a type from a union. Example: NotHasType(x, "nil") on x:string|nil yields x:string

  • Truthy: Narrows to values that are truthy (not nil or false). Example: Truthy(x) on x:string|nil yields x:string

  • Falsy: Narrows to values that are falsy (nil or false). Example: Falsy(x) on x:string|nil yields x:nil

  • Eq/Ne with nil: Narrows based on nil equality. Example: x ~= nil on x:string|nil yields x:string

The domain maintains a map of narrowed types keyed by canonical path keys. When no narrowing exists, the domain falls back to env.PathTypeAt for base types.

TypeDomain supports boolean discriminant narrowing: when a field like .ok is tested for truthiness, and the parent type uses .ok as a discriminant, the parent type is also narrowed. This enables result type patterns:

---@type {ok: true, value: T} | {ok: false, error: string}
local result = ...
if result.ok then
    -- result is narrowed to {ok: true, value: T}
end

func NewTypeDomain

func NewTypeDomain(env constraint.Env) *TypeDomain

NewTypeDomain creates a new TypeDomain with the given environment.

The environment provides type resolution functions:

  • env.PathTypeAt: Returns base type for a path key before narrowing
  • env.ResolveType: Resolves type keys to actual types (for HasType atoms)
  • env.Resolver: Field/index access for boolean discriminant narrowing

func (*TypeDomain) ApplyAtom

func (d *TypeDomain) ApplyAtom(atom constraint.Atom) bool

ApplyAtom applies a type-related constraint atom to the domain.

Supported atom kinds:

  • AtomKindHasType: Narrow to include only the specified type
  • AtomKindNotHasType: Exclude the specified type from a union
  • AtomKindTruthy: Narrow to truthy values (excludes nil and false)
  • AtomKindFalsy: Narrow to falsy values (nil or false only)
  • AtomKindEq with nil RHS: Narrow to exactly nil
  • AtomKindNe with nil RHS: Exclude nil from the type
  • AtomKindEq with two vars: No-op (equality tracked in E-graph)
  • AtomKindNe with two vars: Exclude singleton types if applicable

Returns false and sets Unsat=true if the atom proves unsatisfiability (e.g., HasType("string") on a number-only type).

func (*TypeDomain) Clone

func (d *TypeDomain) Clone() Domain

Clone creates a deep copy of the TypeDomain for speculative evaluation.

The Narrowed map is deep copied; the Env is shared by reference.

func (*TypeDomain) IsUnsat

func (d *TypeDomain) IsUnsat() bool

IsUnsat returns true if the domain has proven a contradiction.

func (*TypeDomain) Join

func (d *TypeDomain) Join(other Domain) Domain

Join computes the least upper bound of two TypeDomain states.

Join semantics for type domains:

  • If either domain is unsatisfiable, return a clone of the other
  • For keys in both domains, compute type union (join.Two)
  • Keys only in one domain are dropped (no narrowing survives)

The intuition: after joining branches, we only know facts that hold in BOTH. If one branch has x:string and the other doesn't narrow x at all, the joined result has no narrowing for x (could be anything).

func (*TypeDomain) NarrowedTypeAt

func (d *TypeDomain) NarrowedTypeAt(key constraint.PathKey) typ.Type

NarrowedTypeAt returns only the explicitly narrowed type, not the base type.

Unlike TypeAt, this returns nil if there is no narrowing, even if the key has a base type. Used to check whether narrowing has occurred for a path.

func (*TypeDomain) TypeAt

func (d *TypeDomain) TypeAt(key constraint.PathKey) typ.Type

TypeAt returns the type for a PathKey, preferring narrowed types over base types.

Lookup order:

  1. d.Narrowed[key] - explicitly narrowed type from constraint application
  2. env.PathTypeAt(key) - base type from declarations

Returns nil if the key has no type in either source.

type TypeNarrower

type TypeNarrower interface {
	TypeAt(key constraint.PathKey) typ.Type
	NarrowedTypeAt(key constraint.PathKey) typ.Type
	ApplyAtom(atom constraint.Atom) bool
	IsUnsat() bool
}

TypeNarrower provides type narrowing results.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL