[−][src]Crate tptp
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 fooX
as a lower_word
succeeds, returning the trailing X
to parse next.
However, 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
cnf | the CNF dialect |
common | common syntax across all dialects |
fof | the FOF dialect |
meta | top-level inputs, formula annotations, etc. |
visitor | visitor pattern |
Structs
TPTPIterator | iterator returning |
Traits
Error | an alias for nom's |
Parse | syntax items which have an associated parser |
Type Definitions
Result | an alias for nom's |