# `ShotDs.Stt.Semantics`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.2.1/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, and `unfold_defs/2` and `unfold_defs!/2`, which unfold (possibly
polymorphic) constant definitions while instantiating their type variables
according to each occurrence's monotype.

# `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.

# `subst_types`

```elixir
@spec subst_types(
  ShotDs.Data.Term.term_id(),
  ShotDs.Util.TypeInference.type_substitution()
) ::
  {:ok, ShotDs.Data.Term.term_id()} | ShotDs.Stt.TermFactory.lookup_error_t()
```

Applies a type substitution (a map from type-variable references to types) to
every type appearing in the term with the given id, propagating any lookup
errors.

This rewrites the head, the bound and free variables, and the term-level
type, while leaving the term's tree-structure - i.e. its de Bruijn indices
and abstraction nesting - untouched. Subterms whose `:tvars` field shares no
element with the substitution's domain are skipped via short-circuit, so the
cost of `subst_types/2` is proportional to the part of the term that
actually mentions the substituted variables.

# `subst_types!`

```elixir
@spec subst_types!(
  ShotDs.Data.Term.term_id(),
  ShotDs.Util.TypeInference.type_substitution()
) ::
  ShotDs.Data.Term.term_id()
```

Like `subst_types/2`, but raises on invalid IDs.

# `unfold_defs`

```elixir
@spec unfold_defs(ShotDs.Data.Term.term_id(), %{
  required(ShotDs.Data.Declaration.const_t()) => ShotDs.Data.Term.term_id()
}) ::
  {:ok, ShotDs.Data.Term.term_id()}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :incompatible_types}
  | {:error, String.t()}
```

Unfolds occurrences of all defined constants in `target_id` by replacing
each occurrence with a type-instantiated, β-reduced copy of the
corresponding definition body.

The `defs` map associates polymorphic (or monomorphic) constant declarations
with their definition bodies. Polymorphism is implicit: any free type
variables appearing in a declaration's stored type are treated as
universally quantified scheme variables, and the same variables are expected
to occur in the corresponding definition body. At each occurrence of a
defined constant, the declaration's polymorphic type is matched against the
occurrence's instance type to derive a type substitution, which is applied
to the definition body via `subst_types/2` before β-reducing it with the
occurrence's arguments.

Lookup is by constant name: each declaration is keyed in `defs` by its full
struct, but only its `:name` is consulted at occurrences (since the type at
each occurrence is the instance, not the polymorphic, type).

For a monomorphic declaration (no free type variables in its stored type)
this degenerates to constant rewriting analogous to free variable
substitution via `subst/2`.

Returns `{:ok, target_id}` immediately when `defs` is empty.

# `unfold_defs!`

```elixir
@spec unfold_defs!(ShotDs.Data.Term.term_id(), %{
  required(ShotDs.Data.Declaration.const_t()) => ShotDs.Data.Term.term_id()
}) :: ShotDs.Data.Term.term_id()
```

Like `unfold_defs/2`, but raises on invalid IDs or matching failures.

---

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