ShotDs.Data.Declaration (shot_ds v1.0.0)

Copy Markdown View Source

Represents free and bound variables as well as constants.

Summary

Types

bound_var_t()

Type of a bound variable declaration.

const_name_t()

The name of a constant is given as a string or a reference (indicating a generated fresh constant).

const_t()

Type of a constant declaration.

free_var_t()

Type of a free variable declaration.

t()

The type of a declaration. A declaration represents either a free variable, a bound variable or a constant.

var_name_t()

The name of a free variable is given as a string, a reference (indicating a generated fresh variable) or a positive integer representing its de Bruijn index.

Functions

format(declaration, hide_type \\ true)

Pretty-prints a declaration.

fresh_const(t)

Generates a fresh constant of the given type using Erlang references to ensure uniqueness. Useful for skolemization.

fresh_var(t)

Generates a fresh variable of the given type using Erlang references to ensure uniqueness. Useful for γ-instantiations in tableaux.

new_const(name, type)

Returns a struct representing a constant of the given name and type.

new_free_var(name, type)

Returns a struct representing a free variable of the given name and type.

Types

bound_var_t()

@type bound_var_t() :: %ShotDs.Data.Declaration{
  kind: :bv,
  name: pos_integer(),
  type: ShotDs.Data.Type.t()
}

Type of a bound variable declaration.

const_name_t()

@type const_name_t() :: String.t() | reference()

The name of a constant is given as a string or a reference (indicating a generated fresh constant).

const_t()

@type const_t() :: %ShotDs.Data.Declaration{
  kind: :co,
  name: const_name_t(),
  type: ShotDs.Data.Type.t()
}

Type of a constant declaration.

free_var_t()

@type free_var_t() :: %ShotDs.Data.Declaration{
  kind: :fv,
  name: var_name_t(),
  type: ShotDs.Data.Type.t()
}

Type of a free variable declaration.

t()

@type t() :: free_var_t() | bound_var_t() | const_t()

The type of a declaration. A declaration represents either a free variable, a bound variable or a constant.

var_name_t()

@type var_name_t() :: String.t() | reference() | pos_integer()

The name of a free variable is given as a string, a reference (indicating a generated fresh variable) or a positive integer representing its de Bruijn index.

Functions

format(declaration, hide_type \\ true)

@spec format(t(), boolean()) :: String.t()

Pretty-prints a declaration.

fresh_const(t)

@spec fresh_const(ShotDs.Data.Type.t()) :: const_t()

Generates a fresh constant of the given type using Erlang references to ensure uniqueness. Useful for skolemization.

fresh_var(t)

@spec fresh_var(ShotDs.Data.Type.t()) :: free_var_t()

Generates a fresh variable of the given type using Erlang references to ensure uniqueness. Useful for γ-instantiations in tableaux.

Note

Consider wrapping functions using this to create temporary free variables with ShotDs.Stt.TermFactory.with_scratchpad/1 or ShotDs.Stt.TermFactory.with_scratchpad!/1 for garbage collection.

new_const(name, type)

@spec new_const(const_name_t(), ShotDs.Data.Type.t()) :: const_t()

Returns a struct representing a constant of the given name and type.

new_free_var(name, type)

@spec new_free_var(var_name_t(), ShotDs.Data.Type.t()) :: free_var_t()

Returns a struct representing a free variable of the given name and type.