Crate tptp

source · [−]

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());
}

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.