Higher-order unification for the data structures and semantics of ShotDs.
Three algorithms are available:
unify/3(default) — depth-bounded pre-unification (Huet 1975): handles arbitrary higher-order problems but is a semi-decision procedure; flex-flex pairs are returned as constraints.pattern_unify/1— Miller pattern unification (Miller 1991): a decidable, unitary fragment in which every flex variable is applied only to distinct bound variables. Returns at most one MGU.match/2— Huet second-order matching: the right-hand side is ground, every variable in the problem has type of order ≤ 2. Returns the complete (lazy) stream of matchers without a depth bound.
unify/3 accepts a :strategy option (:pre_unification, :auto,
:pattern, :matching). With :auto, the problem is inspected and
routed to the most specific decidable algorithm it falls into:
- if every pair is a pattern →
pattern_unify/1, - otherwise if it satisfies the matching precondition →
match/2, - otherwise pre-unification.
See ShotUn.Pattern, ShotUn.Matching and ShotUn.Fragment for
details on the individual algorithms and the fragment classifiers.
Summary
Functions
Returns the (lazy) stream of all matchers σ such that σ(s) ≡_βη t for
each pair {s, t}. Equivalent to ShotUn.Matching.match/1.
Returns {:ok, %UnifSolution{}} (or :error) for a problem in
Miller's pattern fragment. Equivalent to ShotUn.Pattern.unify/1.
Solves a higher-order unification problem.
Types
Functions
@spec match([term_pair()] | term_pair()) :: Enumerable.t(ShotUn.UnifSolution.t())
Returns the (lazy) stream of all matchers σ such that σ(s) ≡_βη t for
each pair {s, t}. Equivalent to ShotUn.Matching.match/1.
@spec pattern_unify([term_pair()] | term_pair()) :: {:ok, ShotUn.UnifSolution.t()} | :error
Returns {:ok, %UnifSolution{}} (or :error) for a problem in
Miller's pattern fragment. Equivalent to ShotUn.Pattern.unify/1.
@spec unify([term_pair()] | term_pair(), non_neg_integer(), keyword()) :: Enumerable.t(ShotUn.UnifSolution.t())
Solves a higher-order unification problem.
Accepts a single term pair {l, r} or a list of pairs. depth is
the search-depth budget for the pre-unification fragment; it is
ignored by the matching and pattern strategies. opts accepts:
:strategy— one of:pre_unification(default),:auto,:pattern,:matching. See module docs for dispatch rules.
Returns a lazy Stream of ShotUn.UnifSolution structs. The
:pattern strategy yields zero or one solution; the other strategies
may yield more (or none).