ShotDs.Stt.Semantics (shot_ds v1.0.0)

Copy Markdown View Source

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.

Summary

Functions

add_subst(substs, new_subst)

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

add_subst!(substs, new_subst)

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

instantiate(term_id, k, replacement_id, cache \\ %{})

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

instantiate!(term_id, k, replacement_id, cache \\ %{})

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(term_id, d, c \\ 0, cache \\ %{})

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

shift!(term_id, d, c \\ 0, cache \\ %{})

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

subst(substitutions, term_id)

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!(substitutions, 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.

Functions

add_subst(substs, new_subst)

@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!(substs, new_subst)

@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(term_id, k, replacement_id, cache \\ %{})

@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!(term_id, k, replacement_id, cache \\ %{})

@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(term_id, d, c \\ 0, cache \\ %{})

@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!(term_id, d, c \\ 0, cache \\ %{})

@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(substitutions, term_id)

@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!(substitutions, term_id)

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