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

Contains utility to parse files from the TPTP problem library
(https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.

For reference, the TH0 language is defined in
https://doi.org/10.1007/s10817-017-9407-7.

## Coverage of the TPTP syntax BNF

The parser accepts the THF fragment of the TPTP syntax BNF
(https://tptp.org/UserDocs/TPTPLanguage/SyntaxBNF.html), including

- `<thf_annotated>` with an arbitrary `<name>` (`<atomic_word>` or
  `<integer>`), any `<formula_role>` — also in its `<lower_word>-<general_term>`
  form — and optional `<annotations>`, which are accepted and discarded;
- `<thf_atom_typing>` in both its plain and its (arbitrarily nested)
  parenthesised form;
- `<include>` with an optional `<formula_selection>`, applied recursively;
- `<th1_quantified_type>` (`!>`), type application, `$ite`, the choice and
  description binders `@+`/`@-` together with their constant forms
  `@@+`/`@@-`, `@=`, and `<identical>` (`==`), which is read as an equality;
- the full lexical layer: line and block comments, `<single_quoted>` words
  with escapes, `<distinct_object>`s, `<dollar_word>`s and
  `<dollar_dollar_word>`s, and `<integer>`/`<rational>`/`<real>` literals,
  which become constants of type `$int`/`$rat`/`$real`;
- the arithmetic `<defined_functor>`s and `<defined_predicate>`s (`$less`,
  `$sum`, `$to_real`, …), which are ad-hoc polymorphic in the numeric sort,
  so that a problem may use them at `$int`, `$rat` and `$real` alike.

Binders scope over a single `<thf_unit_formula>`; an application chain or a
binary connective following the body belongs to the enclosing formula, not to
the binder. See `ShotDs.Parser` for details.

Some TPTP constructs have no counterpart in Church's simple type theory and
are rejected with a descriptive error rather than silently mis-parsed:
`<thf_tuple>`, `<thf_sequent>`, `<thf_subtype>`, `<thf_xprod_type>`,
`<thf_union_type>`, `<th1_quantified_type>` with `?*`, and `$let`.

Formulas whose role carries no logical content (`plain`, `interpretation`,
`unknown`, and any unrecognised `<lower_word>`) are parsed — so that syntax
and type errors still surface — but are not stored in the `ShotDs.Data.Problem`.

# `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 a tuple `{:ok, result}` or
`{:error, reason}`.

This function serves two purposes: parsing a file from the TPTP problem
library (https://tptp.org/TPTP/) or a custom problem file given by the user.

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

# `parse_tptp_file!`

```elixir
@spec parse_tptp_file!(String.t(), :tptp_problem | :tptp_relative | :custom) ::
  ShotDs.Data.Problem.t()
```

Parses a TPTP file in TH0 syntax at the provided path into a
`ShotDs.Data.Problem` struct. Raises on errors.

This function serves two purposes: parsing a file from the TPTP problem
library (https://tptp.org/TPTP/) or a custom problem file given by the user.

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

# `parse_tptp_string`

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

Parses a string representing full a problem file in TPTP's TH0 syntax into a
`ShotDs.Data.Problem` struct. Returns a tuple `{:ok, result}` or
`{:error, reason}`.

> #### Info {: .info}
>
> The parsing of `content` only supports including files from the TPTP problem
> library. If such includes are present, make sure that the `TPTP_ROOT`
> environment variable is set.

# `parse_tptp_string!`

```elixir
@spec parse_tptp_string!(String.t(), String.t()) :: ShotDs.Data.Problem.t()
```

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

> #### Info {: .info}
>
> The parsing of `content` only supports including files from the TPTP problem
> library. If such includes are present, make sure that the `TPTP_ROOT`
> environment variable is set.

# `unparse_problem`

```elixir
@spec unparse_problem(ShotDs.Data.Term.term_id() | ShotDs.Data.Problem.t()) ::
  {:ok, String.t()} | ShotDs.Stt.TermFactory.lookup_error_t() | {:error, term()}
```

Converts a HOL term or a `ShotDs.Data.Problem` struct to a TPTP problem
string with `thf(...)` annotations.
Returns `{:ok, tptp_str}` or `{:error, reason}`.

---

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