@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.

@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.

@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.

@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.

@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.

@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.

@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.

@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.

@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.

@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.

@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.

@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.