@spec format(
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Substitution.t()
  | ShotDs.Data.Problem.t(),
  boolean()
) ::
  {:ok, String.t()}
  | ShotDs.Stt.TermFactory.lookup_error_t()
  | {:error, :unknown_argument}

Pretty-prints the given HOL object taking the ETS cache into accout for recursively traversing term DAGs. This is implemented for singular types, declarations, terms (via ID or struct), substitutions and TPTP proof problems. Returns a tuple {:ok, result} or {:error, reason}.

@spec format!(
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Substitution.t()
  | ShotDs.Data.Problem.t(),
  boolean()
) :: String.t()

Pretty-prints the given HOL object taking the ETS cache into accout for recursively traversing term DAGs. This is implemented for singular types, declarations, terms (via ID or struct), substitutions and TPTP proof problems. Raises on errors (for terms, substitutions and problems).

@spec format_problem(ShotDs.Data.Problem.t(), boolean()) ::
  {:ok, String.t()} | {:error, term()}

Pretty-prints a TPTP proof problem. Returns a tuple {:ok, result} or {:error, reason}.

@spec format_problem!(ShotDs.Data.Problem.t(), boolean()) :: String.t()

Pretty-prints a TPTP proof problem, raising on errors.

@spec format_substitution(ShotDs.Data.Substitution.t(), boolean()) ::
  {:ok, String.t()} | ShotDs.Stt.TermFactory.lookup_error_t()

Pretty-prints a substitution. Returns a tuple {:ok, result} or {:error, reason}.

@spec format_substitution!(ShotDs.Data.Substitution.t(), boolean()) :: String.t()

Pretty-prints a substitution, raising on errors.

@spec format_term(ShotDs.Data.Term.term_id() | ShotDs.Data.Term.t(), boolean()) ::
  {:ok, String.t()} | ShotDs.Stt.TermFactory.lookup_error_t()

Recursively traverses the term DAG to build a pretty-printed string representation with minimal bracketing. Type annotations may be enabled.

Returns a tuple {:ok, result} or {:error, reason}.

@spec format_term!(ShotDs.Data.Term.term_id() | ShotDs.Data.Term.t(), boolean()) ::
  String.t()

Recursively traverses the term DAG to build a pretty-printed string representation with minimal bracketing, raising on errors. Type annotations may be enabled.

@spec short_ref(reference()) :: String.t()

Shortens Erlang references by hashing it and converting it to base 36 for display purposes.

Example:

iex> make_ref() |> short_ref
"1PO9GZ"