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 ¶
- func IsChildPath(parent, child string) bool
- func SplitPathKey(key constraint.PathKey) (constraint.PathKey, string, bool)
- type AtomClass
- type Domain
- type NumericNarrower
- type ShapeDomain
- func (d *ShapeDomain) ApplyConstraint(c constraint.Constraint, target constraint.PathKey) bool
- func (d *ShapeDomain) Clone() Domain
- func (d *ShapeDomain) IsUnsat() bool
- func (d *ShapeDomain) Join(other Domain) Domain
- func (d *ShapeDomain) NarrowedTypeAt(key constraint.PathKey) typ.Type
- func (d *ShapeDomain) TypeAt(key constraint.PathKey) typ.Type
- type TypeDomain
- func (d *TypeDomain) ApplyAtom(atom constraint.Atom) bool
- func (d *TypeDomain) Clone() Domain
- func (d *TypeDomain) IsUnsat() bool
- func (d *TypeDomain) Join(other Domain) Domain
- func (d *TypeDomain) NarrowedTypeAt(key constraint.PathKey) typ.Type
- func (d *TypeDomain) TypeAt(key constraint.PathKey) typ.Type
- type TypeNarrower
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func IsChildPath ¶
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.
func ClassifyAtom ¶
func ClassifyAtom(atom constraint.Atom) AtomClass
ClassifyAtom determines which domain should handle an atom.
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:
- Look up the base type for the target path
- Apply the constraint via Solver.ApplyToSingle to get a narrowed type
- If narrowed type differs from base, store it in Narrowed map
- 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:
- d.Narrowed[key] - explicitly narrowed type from shape constraints
- 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:
- d.Narrowed[key] - explicitly narrowed type from constraint application
- 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.