Contains utility to parse files from the TPTP problem library (https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.
For reference, the TH0 language is defined in https://doi.org/10.1007/s10817-017-9407-7.
Coverage of the TPTP syntax BNF
The parser accepts the THF fragment of the TPTP syntax BNF (https://tptp.org/UserDocs/TPTPLanguage/SyntaxBNF.html), including
<thf_annotated>with an arbitrary<name>(<atomic_word>or<integer>), any<formula_role>— also in its<lower_word>-<general_term>form — and optional<annotations>, which are accepted and discarded;<thf_atom_typing>in both its plain and its (arbitrarily nested) parenthesised form;<include>with an optional<formula_selection>, applied recursively;<th1_quantified_type>(!>), type application,$ite, the choice and description binders@+/@-together with their constant forms@@+/@@-,@=, and<identical>(==), which is read as an equality;- the full lexical layer: line and block comments,
<single_quoted>words with escapes,<distinct_object>s,<dollar_word>s and<dollar_dollar_word>s, and<integer>/<rational>/<real>literals, which become constants of type$int/$rat/$real.
Some TPTP constructs have no counterpart in Church's simple type theory and
are rejected with a descriptive error rather than silently mis-parsed:
<thf_tuple>, <thf_sequent>, <thf_subtype>, <thf_xprod_type>,
<thf_union_type>, <th1_quantified_type> with ?*, and $let.
Formulas whose role carries no logical content (plain, interpretation,
unknown, and any unrecognised <lower_word>) are parsed — so that syntax
and type errors still surface — but are not stored in the ShotDs.Data.Problem.
Summary
Functions
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Raises on errors.
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Raises on errors.
Converts a HOL term or a ShotDs.Data.Problem struct to a TPTP problem
string with thf(...) annotations.
Returns {:ok, tptp_str} or {:error, reason}.
Functions
@spec parse_tptp_file(String.t(), :tptp_problem | :tptp_relative | :custom) :: {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
This function serves two purposes: parsing a file from the TPTP problem library (https://tptp.org/TPTP/) or a custom problem file given by the user.
origin indicates whether it is a file from the TPTP problem library and can
be accessed via the environment variable TPTP_ROOT pointing to the root
directory of the TPTP library.
@spec parse_tptp_file!(String.t(), :tptp_problem | :tptp_relative | :custom) :: ShotDs.Data.Problem.t()
Parses a TPTP file in TH0 syntax at the provided path into a
ShotDs.Data.Problem struct. Raises on errors.
This function serves two purposes: parsing a file from the TPTP problem library (https://tptp.org/TPTP/) or a custom problem file given by the user.
origin indicates whether it is a file from the TPTP problem library and can
be accessed via the environment variable TPTP_ROOT pointing to the root
directory of the TPTP library.
@spec parse_tptp_string(String.t(), String.t()) :: {:ok, ShotDs.Data.Problem.t()} | {:error, String.t()}
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Returns a tuple {:ok, result} or
{:error, reason}.
Info
The parsing of content only supports including files from the TPTP problem
library. If such includes are present, make sure that the TPTP_ROOT
environment variable is set.
@spec parse_tptp_string!(String.t(), String.t()) :: ShotDs.Data.Problem.t()
Parses a string representing full a problem file in TPTP's TH0 syntax into a
ShotDs.Data.Problem struct. Raises on errors.
Info
The parsing of content only supports including files from the TPTP problem
library. If such includes are present, make sure that the TPTP_ROOT
environment variable is set.
@spec unparse_problem(ShotDs.Data.Term.term_id() | ShotDs.Data.Problem.t()) :: {:ok, String.t()} | ShotDs.Stt.TermFactory.lookup_error_t() | {:error, term()}
Converts a HOL term or a ShotDs.Data.Problem struct to a TPTP problem
string with thf(...) annotations.
Returns {:ok, tptp_str} or {:error, reason}.