# `ShotUn.Matching`
[🔗](https://github.com/jcschuster/ShotUn/blob/v0.2.1/lib/shot_un/matching.ex#L1)

Decidable higher-order matching for the second-order fragment.

Higher-order *matching* is the task of finding a substitution σ such
that σ(s) ≡_βη t for two given terms s and t where t is _ground_
(contains no free variables). General higher-order matching is
decidable (Stirling 2009) but impractical to implement; this module
restricts to Huet's second-order fragment, where every variable and
constant in the problem has a type of order at most 2.

Termination is guaranteed by a structural argument on the multi-set of
right-hand sides: every imitation step strictly decreases the total
size of the targets, and every projection step eliminates a flex
variable without introducing new ones (for order-1 flex arguments) or
introduces strictly-smaller-order metas (for order-2 flex arguments).
No depth bound is needed.

Inputs that violate the second-order or ground-target preconditions
raise `ArgumentError`.

Pass `vis: true` in `opts` to receive a `{stream, %ShotUn.Trace{}}`
tuple instead of a bare stream. Under `vis: true` the stream is
materialised eagerly so the trace is complete on return.

# `match`

```elixir
@spec match(
  [term_pair()] | term_pair(),
  keyword()
) ::
  Enumerable.t(ShotUn.UnifSolution.t())
  | {Enumerable.t(ShotUn.UnifSolution.t()), ShotUn.Trace.t()}
```

Returns the lazy stream of all matchers for the given problem.

Raises `ArgumentError` if any right-hand side has free variables, or if
any type in the problem has order greater than 2.

`opts`:

  * `:vis` — when `true`, returns `{stream, %ShotUn.Trace{}}`. The
    stream is materialised eagerly. Defaults to `false`.

---

*Consult [api-reference.md](api-reference.md) for complete listing*