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; - the arithmetic
<defined_functor>s and<defined_predicate>s ($less,$sum,$to_real, …), which are ad-hoc polymorphic in the numeric sort, so that a problem may use them at$int,$ratand$realalike.
Binders scope over a single <thf_unit_formula>; an application chain or a
binary connective following the body belongs to the enclosing formula, not to
the binder. See ShotDs.Parser for details.
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}.