# `ShotDs.Parser`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.2.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 standard TH0 precedence rules. The binding strength is
listed below from **strongest (tightest binding)** to **weakest**.

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

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 when using parentheses.
If the body of the term starts with a parenthesis, the range of the binder is
limited to the next closing parenthesis.

For example, the following parses as `"![X : $o]: ($false => (X => $true))"`:

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

While this will be parsed as `"(![X : $o]: (f @ X)) | (g @ X)"`:

    iex> parse "![X : $o]: (f @ X) | (g @ 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.

# `unparse_type_scheme`

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

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

---

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