Crate tptp[−][src]
Expand description
A crate for reading files in the TPTP format.
Most users will want to use the TPTPIterator
interface to parse statements from a TPTP file.
After you have a parsed statement, you can either manipulate it manually, or use the Visitor
interface to ease writing traversals.
Individual parsers for each item of the TPTP BNF are available: generally this is a one-to-one map, but for efficiency/sanity reasons items like integer
are not split into signed_integer
and unsigned_integer
.
Parsers are built with nom, and this implementation detail is kept deliberately transparent.
If you need it, you can use nom’s facilities such as error handling or streaming.
All parsers are a function from byte slices to Result
.
The input will never be copied, only references made.
The crate is #![no_std]
, but syntax trees must allocate with the current design so the alloc
crate is required.
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.
However, parsing foo
is “incomplete” as there might be more input coming.
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.
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());
}
Modules
the CNF dialect
common syntax across all dialects
the FOF 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