@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

@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"

@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")

@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")

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

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

@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: []}}

@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: []}

@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

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

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

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

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

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

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

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

@spec with_type_constructors(Enumerable.t(), (-> 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.