# `ShotDs`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.0.4/lib/shot_ds.ex#L1)

This module collects the most important functions from the library. These
include parsing functions as well as simple term construction.

# `app`

```elixir
@spec app(
  ShotDs.Data.Term.term_id(),
  [ShotDs.Data.Term.term_id()] | ShotDs.Data.Term.term_id()
) ::
  ShotDs.Data.Term.term_id()
```

Applies a term to a single argument term or list of argument terms.

Delegates the function call to `ShotDs.Util.Builder.app/2`.

# `format!`

```elixir
@spec format!(
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Substitution.t()
) :: 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 and substitutions.

Delegates the function call to `ShotDs.Util.Formatter.format!/1`.

# `format!`

```elixir
@spec format!(
  ShotDs.Data.Type.t()
  | ShotDs.Data.Declaration.t()
  | ShotDs.Data.Term.t()
  | ShotDs.Data.Substitution.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 and substitutions. Type annotations may be displayed by
setting the second field to `false`.

Delegates the function call to `ShotDs.Util.Formatter.format!/1`.

# `lambda`

```elixir
@spec lambda([ShotDs.Data.Type.t()] | ShotDs.Data.Type.t(), (... ->
                                                         ShotDs.Data.Term.term_id())) ::
  ShotDs.Data.Term.term_id()
```

Constructs a lambda abstraction over a list of variable types. Temporary
fresh free variables will be generated corresponding to the types. Passes the
generated variable term IDs to the provided `body_fn`. The arity of `body_fn`
must correspond to the number of given variables.

Delegates the function call to `ShotDs.Util.Builder.lambda/2`.

## Examples:

    iex> lambda(Type.new(:i), fn x -> ... end)

    iex> lambda([Type.new(:o), Type.new(:o), Type.new(:o)], fn x, y, z -> ... end)

# `make_const_term`

```elixir
@spec make_const_term(String.t() | reference(), ShotDs.Data.Type.t()) ::
  ShotDs.Data.Term.term_id()
```

Basic construction of a constant with the corresponding name and type and
returns the ID for its term representation. While unique constants can be
created by giving an Erlang reference as name, it is recommended to use
`ShotDs.Stt.TermFactory.make_fresh_const_term/1` instead for that purpose.

Delegates the function call to `ShotDs.Stt.TermFactory.make_const_term/2`.

## Example:

    iex> import ShotDs.Hol.Definitions # shorthand type defs etc.
    iex> make_const_term("f", type_io())

# `make_free_var_term`

```elixir
@spec make_free_var_term(String.t() | reference(), ShotDs.Data.Type.t()) ::
  ShotDs.Data.Term.term_id()
```

Basic construction of a free variable with the corresponding name and type
and returns the ID for its term representation. While unique variables can be
created by giving an Erlang reference as name, it is recommended to use
`ShotDs.Stt.TermFactory.make_fresh_var_term/1` instead for that purpose.

Delegates the function call to `ShotDs.Stt.TermFactory.make_free_var_term/2`.

## Example:

    iex> import ShotDs.Hol.Definitions # shorthand type defs etc.
    iex> make_free_var_term("X", type_o())

# `parse!`

```elixir
@spec parse!(String.t()) :: ShotDs.Data.Term.term_id()
```

Parses a given string representing a formula in TH0 syntax with full type
inference. Types which can't be inferred are assigned type variables.
Variables on the outermost level are identified with type o. Returns the
assigned ID of the created term.

Delegates the function call to `ShotDs.Parser.parse!/1`.

## Examples:

    iex> parse!("X & a") |> format_term()
    "X ∧ a"

    iex> parse!("X @ Y") |> format_term(_hide_types = false)
    "(X_T[OUFDH]>o Y_T[OUFDH])_o"

# `parse_tptp_file`

```elixir
@spec parse_tptp_file(String.t()) ::
  {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
```

Parses a TPTP file in TH0 syntax at the provided path into a
`ShotDs.Data.Problem` struct. Returns `{:error, reason}` if a problem
occurred.

Delegates the function call to `ShotDs.Tptp.parse_tptp_file/1`.

# `parse_tptp_file`

```elixir
@spec parse_tptp_file(String.t(), :tptp_problem | :tptp_relative | :custom) ::
  {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
```

Parses a TPTP file in TH0 syntax at the provided path into a
`ShotDs.Data.Problem` struct. Returns `{:error, reason}` if a problem
occurred.

`origin` indicates whether it is a file from the TPTP problem library and can
be accessed via the environment variable `TPTP_ROOT` pointing to the root
directory of the TPTP library.

Delegates the function call to `ShotDs.Tptp.parse_tptp_file/1`.

# `parse_tptp_string`

```elixir
@spec parse_tptp_string(String.t()) ::
  {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
```

Parses a string representing a full problem file in TPTP's TH0 syntax into a
`ShotDs.Data.Problem` struct.

Delegates the function call to `ShotDs.Tptp.parse_tptp_string/1`.

# `parse_type!`

```elixir
@spec parse_type!(String.t()) :: ShotDs.Data.Type.t()
```

Parses a HOL type from TPTP syntax into a `ShotDs.Data.Type` struct.

Delegates the function call to `ShotDs.Parser.parse_type!/1`.

## Example:

    iex> parse_type!("$i")
    %ShotDs.Data.Type{goal: :i, args: []}

---

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