ShotDs.Parser (shot_ds v1.0.0)

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

There are also custom sigils available for most parsing functions. These are defined in the module ShotDs.Hol.Sigils.

Summary

Functions

parse(formula_str, context \\ Context.new())

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.

parse!(formula_str, context \\ Context.new())

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.

parse_context(context_str)

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

parse_context!(context_str)

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

parse_tokens(tokens, context \\ Context.new())

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.

parse_tokens!(tokens, context \\ Context.new())

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.

parse_type(type_str)

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

parse_type!(type_str)

Parses a HOL type from TPTP syntax into a ShotDs.Data.Type struct, raising on errors.

parse_type_tokens(tokens)

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

Functions

parse(formula_str, context \\ Context.new())

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

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

Example:

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

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

parse!(formula_str, context \\ Context.new())

@spec parse!(String.t(), ShotDs.Data.Context.t()) :: ShotDs.Data.Term.term_id()

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(context_str)

@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!(context_str)

@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(tokens, context \\ Context.new())

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

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

parse_tokens!(tokens, context \\ Context.new())

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

Example:

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

parse_type(type_str)

@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!(type_str)

@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(tokens)

@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}.