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

Higher-order pattern unification (Miller 1991).

A higher-order *pattern* is a βη-normal term in which every free
variable F occurs only in applications of the form
$F(x_1, \dots, x_n)$ where the arguments $x_1, \dots, x_n$ are
pairwise distinct bound variables. Unification over the pattern
fragment is decidable and *unitary*: when a unifier exists it is
unique up to α-renaming, so this entry point returns either a single
most-general unifier or `:error`.

The implementation realises Miller's algorithm with four rules:

  * *decomposition* of rigid-rigid pairs whose heads agree,
  * *inversion* of a flex–rigid pair $F(\bar x) \overset{?}{=} t$,
    with *pruning* of any nested flex application whose arguments
    would otherwise reach a binder outside $\{\bar x\}$,
  * *alias* for flex–flex pairs with the same head — bind the
    variable to a fresh meta over the positions on which the two
    argument lists agree,
  * *intersection* for flex–flex pairs with distinct heads — bind
    both variables to a fresh meta applied to the bound variables
    they share.

Termination is by structural recursion on the work-list; no depth
bound is needed.

Use `ShotUn.pattern_unify/2` as the public entry point. Inputs
containing non-pattern terms raise `ArgumentError`. Pass `vis: true`
in `opts` to receive a `{result, %ShotUn.Trace{}}` tuple.

# `unify`

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

Returns `{:ok, %UnifSolution{}}` (whose `flex_pairs` are always empty)
when an MGU exists, otherwise `:error`. Raises `ArgumentError` when
the input is not a higher-order pattern.

`opts`:

  * `:vis` — when `true`, returns `{result, %ShotUn.Trace{}}` instead
    of `result`. Defaults to `false`.

---

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