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

Contains functionality to parse a formula in TH0 syntax with full type
inference. The algorithm is similar to Hindley-Milner type systems but for
simplicity reasons without the optimizations found in algorithms J or W.
Uses Robinson's first-order unification algorithm for type inference. A
context can be specified to clear up unknown types. If terms still have
unknown type after parsing, unifies 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(), ShotDs.Data.Context.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}`

## Example:

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

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

# `parse!`

```elixir
@spec parse!(String.t(), ShotDs.Data.Context.t()) :: 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.

## Example:

    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"

    iex> parse!("X @ Y", ~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(), 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. 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}`.

# `parse_tokens!`

```elixir
@spec parse_tokens!(ShotDs.Util.Lexer.tokens(), ShotDs.Data.Context.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. Variables on the outermost level are
identified with type o. Returns the assigned ID of the created term.

## 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_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}`.

---

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