# `ShotDs.Stt.Semantics`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.0/lib/shot_ds/stt/semantics.ex#L1)

Implements the semantics of Church's simple type theory. The most important
functions are `subst/2` and `subst!/2`, which apply substitutions to a given
term.

# `add_subst`

```elixir
@spec add_subst([ShotDs.Data.Substitution.t()], ShotDs.Data.Substitution.t()) ::
  {:ok, [ShotDs.Data.Substitution.t()]}
  | ShotDs.Stt.TermFactory.lookup_error_t()
```

Adds a new substitution to a list of substitutions by applying it to every
member and prepending it, propagating errors.

# `add_subst!`

```elixir
@spec add_subst!([ShotDs.Data.Substitution.t()], ShotDs.Data.Substitution.t()) :: [
  ShotDs.Data.Substitution.t()
]
```

Adds a new substitution to a list of substitutions by applying it to every
member and prepending it, raising on errors.

# `instantiate`

```elixir
@spec instantiate(
  ShotDs.Data.Term.term_id(),
  pos_integer(),
  ShotDs.Data.Term.term_id(),
  map()
) ::
  {:ok, {ShotDs.Data.Term.term_id(), map()}}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :incompatible_types}
```

Instantiates the bound variable with index *k* with the replacement term
corresponding to the given id, safely propagating errors.

# `instantiate!`

```elixir
@spec instantiate!(
  ShotDs.Data.Term.term_id(),
  pos_integer(),
  ShotDs.Data.Term.term_id(),
  map()
) ::
  {ShotDs.Data.Term.term_id(), map()}
```

Instantiates the bound variable with index *k* with the replacement term
corresponding to the given id, raising on errors. Uses caching for efficient
computation.

# `shift`

```elixir
@spec shift(ShotDs.Data.Term.term_id(), integer(), non_neg_integer(), map()) ::
  {:ok, {ShotDs.Data.Term.term_id(), map()}}
  | ShotDs.Stt.TermFactory.lookup_error_t()
```

Applies a *d*-shift above cutoff *c* to the term with the given id.

# `shift!`

```elixir
@spec shift!(ShotDs.Data.Term.term_id(), integer(), non_neg_integer(), map()) ::
  {ShotDs.Data.Term.term_id(), map()}
```

Applies a *d*-shift above cutoff *c* to the term with the given id, raising on
invalid IDs.

# `subst`

```elixir
@spec subst(
  [ShotDs.Data.Substitution.t()] | ShotDs.Data.Substitution.t(),
  ShotDs.Data.Term.term_id()
) ::
  {:ok, ShotDs.Data.Term.term_id()}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :incompatible_types}
```

Applies a singular substitution or a list of substitutions left to right to
the term with the given id, propagating any lookup or type errors.

# `subst!`

```elixir
@spec subst!(
  [ShotDs.Data.Substitution.t()] | ShotDs.Data.Substitution.t(),
  ShotDs.Data.Term.term_id()
) ::
  ShotDs.Data.Term.term_id()
```

Applies a singular substitution or a list of substitutions left to right to
the term with the given id, erroring out if it encounters an invalid ID.

---

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