Crate dedukti_parse

Expand description

Parser for the Dedukti file format

This crate serves to parse Dedukti theory files. The syntax of Dedukti theories is documented here.

One of the main targets of this crate is speed: An evaluation of an older version of this crate in the article Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting showed that this parser can be more than 4x faster than the parser in Dedukti. This is relevant because the runtime of parsing can make up for nearly half the total runtime of Dedukti.

This crate currently does not support the complete Dedukti syntax; in particular, commands starting with #, such as #EVAL and #REQUIRE are not supported. Still, the supported subset of the syntax suffices to parse many large proof corpora, such as those produced from Matita, HOL Light, and Isabelle/HOL.

Usage

Lazy / Strict

This crate supports several modes of operation:

Strict parsing: The whole content of the file is in memory before parsing.
Lazy parsing: The file is read bit by bit during parsing.

Strict parsing of a whole file is faster than lazy parsing; however, it consumes more memory than lazy parsing and takes longer to get the first command.

Scoping

One important operation that is performed during parsing is scoping. This operation decides how to store symbols occurring in a term. There are currently two options:

All symbols are unconditionally stored using strings.
Symbols are distinguished into atoms that are either constants and variables, where constants are saved using strings and variables as de Bruijn indices (natural numbers that refer to the position of the binder of the variable).

The first option can use String and &str as string type. However, &str can be only used in conjunction with strict parsing, because lazy parsing “forgets” the input string and therefore does not allow references into the input string. The second option can be used regardless of strict or lazy parsing.

When to use what?

Use lazy parsing if you want to wait as little as possible to get each command or minimise your memory consumption.
Use strict parsing if you parse a whole file and wish to reduce the total runtime of parsing.
Store symbols unconditionally using strings if you do not care whether a symbol is a variable or not. In that case, when doing strict parsing, prefer &str over String as string type to reduce String allocations.

Example

use dedukti_parse::{term, Command, Error, Lazy, Scoped, Strict, Symb};

let cmds = r#"
    prop: Type.
    def proof : prop -> Type.
"#;

// strict parsing with `&str` symbols
let parse = Strict::<_, Symb<&str>, &str>::new(&cmds);
let parse: Result<Vec<_>, _> = parse.collect();
assert_eq!(parse?.len(), 2);

// strict parsing with atoms
let parse = Strict::<_, term::Atom<Symb<String>>, String>::new(cmds);
let parse: Result<Vec<_>, _> = parse.collect();
assert_eq!(parse?.len(), 2);

// lazy parsing with `String` symbols
let parse = Lazy::<_, Symb<String>, String>::new(cmds.lines());
let parse: Result<Vec<_>, _> = parse.collect();
assert_eq!(parse?.len(), 2);

// lazy parsing with atoms
let parse = Lazy::<_, term::Atom<Symb<String>>, String>::new(cmds.lines());
let parse: Result<Vec<_>, _> = parse.collect();
assert_eq!(parse?.len(), 2);