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

Contains functionality to parse a formula in THF syntax with full type
inference. The algorithm uses Hindley-Milner rank-1 polymorphism and
implements algorithm W for type inference. The resulting constraints are
resolved via Robinson's first-order unification algorithm. A context can be
specified to clear up unknown types. If terms still have unknown/polymorphic
type after parsing, it can be specified to unify their type with type o. The
main entry point is the `parse/2` function.

The parser follows the TPTP BNF
(https://tptp.org/UserDocs/TPTPLanguage/SyntaxBNF.html). The binding strength
is listed below from **strongest (tightest binding)** to **weakest**.

    (Strongest)   !, ?, !!, ??, ^     [Quantors/Binders]
                  @                   [Application]
                  =, !=               [Equality]
                  ~                   [Negation]
                  &, ~&               [Conjunction]
                  |, ~|               [Disjunction]
    (Weakest)     =>, <=, <=>, <~>    [Implication]

The TH0 syntax is specified in https://doi.org/10.1007/s10817-017-9407-7 for
reference.

Note that the usage of binders requires special care. A binder scopes over a
single `<thf_unit_formula>` only — an atom, a variable, a parenthesized
formula, another binder, a `~`-prefixed unit formula, or an infix
(in)equation between unitary terms. Application chains and binary connectives
are *not* part of the body; they continue **outside** the binder, as the TPTP
BNF spells out:

    %----@ (denoting apply) is left-associative and lambda is right-associative.
    %----^ [X] : ^ [Y] : f @ g (where f is a <thf_apply_formula> and g is a
    %----<thf_unitary_formula>) should be parsed as: (^ [X] : (^ [Y] : f)) @ g.
    %----That is, g is not in the scope of either lambda.

    iex> parse!("^ [X: $i] : f @ g", ctx: ~e(f: $i>$o, g: $i)) ==
    ...>   parse!("( ^ [X: $i] : f ) @ g", ctx: ~e(f: $i>$o, g: $i))
    true

Likewise a binder never extends across a binary connective, so the following
parses as `"(![X : $o]: $false) => (X => $true)"`:

    iex> parse!("![X : $o]: $false => (X => $true)") ==
    ...>   parse!("(![X : $o]: $false) => (X => $true)")
    true

Parenthesize the body to bind the whole formula, as in
`"![X : $i]: (p @ X)"`.

> #### Note {: .info}
>
> There are also custom sigils available for most parsing functions. These are
> defined in the module `ShotDs.Hol.Sigils`.

# `parse`

```elixir
@spec parse(String.t(), Keyword.t()) ::
  {:ok, ShotDs.Data.Term.term_id()} | {:error, String.t()}
```

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

Returns `{:ok, term_id}` or `{:error, reason}`

## Options:

- `ctx`: a `ShotDs.Data.Context` struct for providing type information
- `force_o?`: identify type variables on the outermost level type o

## Example:

    iex> match?({:ok, _parsed}, parse("X & a"))
    true

    iex> match?({:ok, _parsed}, parse("X &"))
    false

# `parse!`

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

Parses a given string representing a formula in TH0 syntax with full type
inference, raising a `ShotDs.Parser.ParseError` if invalid. 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.

## Options:

- `ctx`: a `ShotDs.Data.Context` struct for providing type information
- `force_o`: identify type variables on the outermost level type o

## Example:

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

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

    iex> parse!("X @ Y", ctx: ~e(X:$i>$i, Y:$i)) |> format_term!(false)
    "(X_i>i Y_i)_i"

# `parse_context`

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

Parses a string into a `ShotDs.Data.Context` struct. Returns `{:ok, ctx}` or
`{:error, reason}`.

## Example

    iex> parse_context("X:$i, c:$o>$o")

# `parse_context!`

```elixir
@spec parse_context!(String.t()) :: ShotDs.Data.Context.t()
```

Parses a string into a `ShotDs.Data.Context` struct, raising on errors.

## Example

    iex> parse_context!("X : $i, c: $o>$o")

# `parse_tokens`

```elixir
@spec parse_tokens(ShotDs.Util.Lexer.tokens(), Keyword.t() | ShotDs.Data.Context.t()) ::
  {:ok, ShotDs.Data.Term.term_id()} | {:error, String.t()}
```

Safely parses a given list of tokens with full type inference. Types which
can't be inferred are assigned type variables. Returns the assigned ID of the
created term.

## Options:

- `ctx`: a `ShotDs.Data.Context` struct for providing type information
- `force_o`: identify type variables on the outermost level type o

Returns `{:ok, term_id}` or `{:error, reason}`.

# `parse_tokens!`

```elixir
@spec parse_tokens!(ShotDs.Util.Lexer.tokens(), Keyword.t()) ::
  ShotDs.Data.Term.term_id()
```

Parses a given list of tokens with full type inference. Types which can't be
inferred are assigned type variables. Returns the assigned ID of the created
term.

## Options:

- `ctx`: a `ShotDs.Data.Context` struct for providing type information
- `force_o`: identify type variables on the outermost level type o

## Example:

    iex> {:ok, tokens, _, _, _, _} = Lexer.tokenize("$false")
    iex> parse_tokens!(tokens) |> format_term!()
    "⊥"

# `parse_type`

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

Parses a HOL type from TPTP syntax into a `ShotDs.Data.Type` struct. Returns
a tuple `{:ok, result}` or `{:error, reason}`.

## Example:

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

# `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, raising
on errors.

## Example:

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

# `parse_type_scheme`

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

Parses a TPTP TH1 type scheme from a string.

Two forms are accepted:

- **Explicit (TH1):** `!>[A:$tType, B:$tType]: t` — every type variable in
  the body must be declared in the binder list. The kind annotation
  `:$tType` is also accepted-without (extension).
- **Implicit:** `t` — every uppercase identifier in `t` is treated as an
  implicitly universally-quantified type variable.

Returns `{:ok, scheme}` or `{:error, reason}`.

## Examples

    iex> match?({:ok, %ShotDs.Data.TypeScheme{vars: [_]}},
    ...>   parse_type_scheme("!>[A:$tType]: (A > A)"))
    true

    iex> match?({:ok, %ShotDs.Data.TypeScheme{vars: [_]}},
    ...>   parse_type_scheme("A > A"))
    true

    iex> match?({:ok, %ShotDs.Data.TypeScheme{vars: []}},
    ...>   parse_type_scheme("$i > $o"))
    true

# `parse_type_scheme!`

```elixir
@spec parse_type_scheme!(String.t()) :: ShotDs.Data.TypeScheme.t()
```

Parses a TPTP TH1 type scheme from a string, raising on errors. See
`parse_type_scheme/1` for the accepted syntax.

# `parse_type_scheme_tokens`

```elixir
@spec parse_type_scheme_tokens(ShotDs.Util.Lexer.tokens()) ::
  {:ok, {ShotDs.Data.TypeScheme.t(), ShotDs.Util.Lexer.tokens()}}
  | {:error, String.t()}
```

Parses a type scheme from a list of tokens. Returns the constructed
`TypeScheme` along with the remaining tokens, or `{:error, reason}`.

# `parse_type_tokens`

```elixir
@spec parse_type_tokens(ShotDs.Util.Lexer.tokens()) ::
  {:ok, {ShotDs.Data.Type.t(), ShotDs.Util.Lexer.tokens()}}
  | {:error, String.t()}
```

Parses a HOL type from a list of tokens into a `ShotDs.Data.Type` struct.
Returns a tuple `{:ok, result}` containing the constructed type as well as the
remaining tokens or `{:error, reason}`.

# `unparse`

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

Converts a HOL term (by its ID) to a maximally-bracketed TPTP THF formula string.
Returns `{:ok, formula_str}` or `{:error, reason}`.

# `unparse_type`

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

Converts a `Type.t()` to a TPTP type string.

The mapping type `α > c` and the type-constructor application `c @ α` share
one representation (`%Type{goal: c, args: [α]}`), so they can only be told
apart by the kind of `c`. The mapping reading is assumed unless `c` has been
declared a type constructor via `with_type_constructors/2`.

# `unparse_type_scheme`

```elixir
@spec unparse_type_scheme(ShotDs.Data.TypeScheme.t()) :: String.t()
```

Converts a `TypeScheme.t()` to a TPTP type string.

# `with_type_constructors`

```elixir
@spec with_type_constructors(Enumerable.t(), (-&gt; result)) :: result when result: var
```

Runs `fun` with `names` (atoms) registered as type constructors, so that
`unparse_type/1` renders their applications as `c @ α` rather than as the
mapping type `α > c`. Returns the result of `fun`.

---

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