BeHOLd.Parser (behold v1.1.3)

View Source

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. The type unification algorithm is documented in BeHOLd.Util.TypeInference). 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)"

Summary

Functions

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

Parses a given string representing a formula in TH0 syntax to a HOL.Data.hol_term() with respect to the given context. Types are inferred if they are not present in the given context. Types that can't be inferred will be handled as unknown types which are constructed by BeHOLd.Util.TypeInference.mk_new_unknown_type/0. Top level unknown types will be unified with type o.

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

Parses a given list of tokens tokenized by BeHOLd.Util.Lexer.tokenize/1 representing a formula in TH0 syntax to a HOL.Data.hol_term() with respect to the given context. Types are inferred if they are not present in the given context. Types that can't be inferred will be handled as unknown types which are constructed by BeHOLd.Util.TypeInference.mk_new_unknown_type/0.

parse_type(type_str)

Parses a given string representing a type in TH0 syntax to a HOL.Data.type().

parse_type_tokens(tokens)

Parses the next tokens in tokens as type and returns the constructed type as well as the remaining tokens from tokens.

Functions

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

@spec parse(String.t(), BeHOLd.Data.Context.t()) :: HOL.Data.hol_term()

Parses a given string representing a formula in TH0 syntax to a HOL.Data.hol_term() with respect to the given context. Types are inferred if they are not present in the given context. Types that can't be inferred will be handled as unknown types which are constructed by BeHOLd.Util.TypeInference.mk_new_unknown_type/0. Top level unknown types will be unified with type o.

The parsing proceeds in two steps: a constraining phase and an unification phase. This is different to algorithms J and W on Hindley-Milner type systems which immediately unify constraints as they are generated. This however introduces unnecessary complexity. This function doesn't need to be heavily optimized since input problems are always reasonably small.

Examples

iex> parse "$true"
{:term, [], {:decl, :co, "⊤", {:type, :o, []}}, [], {:type, :o, []}, [], 0}

iex> parse "X & Y"
{:term, [], {:decl, :co, "∧", {:type, :o, [{:type, :o, []}, {:type, :o, []}]}},
[
  {:term, [], {:decl, :fv, "X", {:type, :o, []}}, [], {:type, :o, []},
    [{:decl, :fv, "X", {:type, :o, []}}], 0},
  {:term, [], {:decl, :fv, "Y", {:type, :o, []}}, [], {:type, :o, []},
    [{:decl, :fv, "Y", {:type, :o, []}}], 0}
], {:type, :o, []}, [{:decl, :fv, "Y", {:type, :o, []}}, {:decl, :fv, "X", {:type, :o, []}}], 0}

iex> parse "X"
{:term, [], {:decl, :fv, "X", {:type, :o, []}}, [], {:type, :o, []}, [{:decl, :fv, "X", {:type, :o, []}}], 0}

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

@spec parse_tokens(BeHOLd.Util.Lexer.tokens(), BeHOLd.Data.Context.t()) ::
  HOL.Data.hol_term()

Parses a given list of tokens tokenized by BeHOLd.Util.Lexer.tokenize/1 representing a formula in TH0 syntax to a HOL.Data.hol_term() with respect to the given context. Types are inferred if they are not present in the given context. Types that can't be inferred will be handled as unknown types which are constructed by BeHOLd.Util.TypeInference.mk_new_unknown_type/0.

Example

iex> {:ok, tokens, _, _, _, _} = Lexer.tokenize "$false"
iex> parse_tokens(tokens)
{:term, [], {:decl, :co, "⊥", {:type, :o, []}}, [], {:type, :o, []}, [], 0}

parse_type(type_str)

@spec parse_type(String.t()) :: HOL.Data.type()

Parses a given string representing a type in TH0 syntax to a HOL.Data.type().

Examples

iex> parse_type("$i>$o")
{:type, :o, [{:type, :i, []}]}

iex> parse_type("($i>$i)>$o")
{:type, :o, [{:type, :i, []}, {:type, :i, []}]}

iex> parse_type("($i>$o)>$o")
{:type, :o, [{:type, :o, [{:type, :i, []}]}]}

parse_type_tokens(tokens)

@spec parse_type_tokens(BeHOLd.Util.Lexer.tokens()) ::
  {HOL.Data.type(), BeHOLd.Util.Lexer.tokens()}

Parses the next tokens in tokens as type and returns the constructed type as well as the remaining tokens from tokens.

Example

iex> {:ok, tokens, _, _, _, _} = Lexer.tokenize "$i>$o"
iex> parse_type_tokens(tokens)
{{:type, :o, [{:type, :i, []}]}, []}