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

Higher-order unification for the data structures and semantics of
[ShotDs](https://hexdocs.pm/shot_ds/readme.html).

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/2` — *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/2`,
  * 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.

## Visualisation

Every public entry point accepts a `vis: true` option that wraps the
result in a `{result, %ShotUn.Trace{}}` tuple. The trace is a tree of
`ShotUn.Trace.Node` records covering only the paths from the initial
state to a `:solution` leaf — failed branches and dead-end steps are
pruned out before the tuple is returned. Render with
`ShotUn.Trace.Mermaid.render/2`. When `vis: true` the search is
materialised eagerly (the lazy `Stream` is consumed before the call
returns) so that the trace is complete.

# `strategy`

```elixir
@type strategy() :: :pre_unification | :auto | :pattern | :matching
```

# `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 σ such that σ(s) ≡_βη t for
each pair `{s, t}`. With `vis: true`, returns `{stream, trace}`.
Equivalent to `ShotUn.Matching.match/2`.

# `pattern_unify`

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

Returns `{:ok, %UnifSolution{}}` (or `:error`) for a problem in
Miller's pattern fragment. With `vis: true`, returns
`{result, trace}`. Equivalent to `ShotUn.Pattern.unify/2`.

# `unify`

```elixir
@spec unify([term_pair()] | term_pair(), non_neg_integer(), keyword()) ::
  Enumerable.t(ShotUn.UnifSolution.t())
  | {Enumerable.t(ShotUn.UnifSolution.t()), ShotUn.Trace.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.
  * `:vis` — when `true`, returns `{stream, %ShotUn.Trace{}}` instead
    of a bare stream. Defaults to `false`.

Returns a lazy `Stream` of `ShotUn.UnifSolution` structs, or — under
`vis: true` — a `{stream, trace}` tuple in which the stream contains
the same solutions but is fully materialised before the call returns.

---

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