Expand description
A collection of parsers for the TFX*/FOF/CNF dialects of the TPTP format, expressed as functions from byte slices to syntax trees.
Most users will want to use the TPTPIterator
interface to stream <TPTP_input>
s from TPTP problems, but it is also possible to use parsers individually for more exotic formats.
Quickstart
use tptp::TPTPIterator;
use tptp::visitor::Visitor;
struct MyVisitor;
impl<'a> Visitor<'a> for MyVisitor {}
fn example(bytes: &[u8]) {
let mut visitor = MyVisitor;
let mut parser = TPTPIterator::<()>::new(bytes);
for result in &mut parser {
let input = result.expect("syntax error");
println!("{}", &input);
visitor.visit_tptp_input(&input);
}
assert!(parser.remaining.is_empty());
}
Design Points
Parser Combinators
Parsers are built with the nom parser combinator library, and this implementation detail is kept deliberately transparent. If you need them, you can use nom’s facilities such as error handling or streaming.
Parsers as Functions
All parsers are functions from byte slices to Result<T, E>
type, representing either parsed syntax T
or a nom error E
.
Parsers are zero-copy, which typically means T
will borrow from the input slice.
Parsers are invoked as T::parse
via the Parse
trait.
Syntax Trees
Explicit, strongly-typed syntax trees are constructed during parsing.
After you have some parsed syntax, you can either manipulate it manually, or use the Visitor
interface if you only need to handle certain parts of the syntax.
Flexible Parsing
Individual parsers for each item of the TPTP BNF are available.
This can be useful to parse unusual or ‘hybrid’ formats such as DeepMath.
Generally parsers and BNF are a one-to-one map, but for efficiency/sanity reasons items like integer
are not split into signed_integer
and unsigned_integer
.
Whitespace/comments are handled inside invidual BNF items, but not outside, as the caller should handle it.
For example, parsing fof ( 1 , axiom , /* comment */ $true ) .
as a fof_annotated
is OK, but ␣fof(1,axiom,$true).␣
is an error.
Naturally, TPTPIterator
handles whitespace and comments between <TPTP_input>
s.
Streaming
Parsers are streaming, so they will signal “incomplete” on EOF, rather than success or failure, until the outcome is known.
Most of the time this is obvious, but the behaviour can be surprising.
For example, parsing foo$
as a lower_word
succeeds, returning the trailing $
to parse next (which will fail).
However, parsing foo
is “incomplete” as there might be more input coming.
#![no_std]
The crate is #![no_std]
, but recursive syntax trees must allocate so the alloc
crate is required.
Serialisation
Support for serde
can be switched on with a feature flag as usual.
Structures can then be serialised, but not deseralised due to ownership issues.
*currently partial support, notably missing $let
, $ite
and tuples
Modules
the CNF dialect
common syntax across all dialects
the FOF dialect
the TFX dialect
top-level inputs, formula annotations, etc.
visitor pattern
Structs
iterator returning TPTP_input
s from a byte slice
Traits
Type Definitions
an alias for nom’s IResult