Dedukti 文件格式的解析器

此crate的作用是解析Dedukti理论文件。Dedukti理论的语法在此处有文档说明。

此crate的主要目标之一是速度：文章Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting中关于此crate旧版本的评估表明，此解析器比Dedukti中的解析器快4倍以上。这很重要，因为解析的时间可以占据Dedukti总运行时间的一半左右。

此crate目前不支持完整的Dedukti语法；特别是，以下命令不支持：以#开头的命令，例如 #EVAL 和 #REQUIRE。尽管如此，支持的语法子集足以解析许多大型证明集合，例如从Matita、HOL Light和Isabelle/HOL生成的证明。

使用方法

惰性/严格

此crate支持几种操作模式

• [严格] 解析：在解析之前，整个文件内容都在内存中。
• [惰性] 解析：在解析过程中逐位读取文件。

严格解析整个文件比惰性解析快，但它消耗的内存比惰性解析多，并且获取第一个命令的时间更长。

作用域

解析过程中执行的一项重要操作是 作用域。此操作决定如何存储出现在项中的符号。目前有两种选项

1. 无条件地使用字符串存储所有符号。
2. 符号被区分成原子，这些原子是常量和变量，其中常量用字符串保存，变量用de Bruijn索引（表示变量绑定位置的自然数）保存。

第一个选项可以使用 String 和 &str 作为字符串类型。然而，&str 只能在严格解析的情况下使用，因为懒解析“忘记”了输入字符串，因此不允许对输入字符串的引用。第二个选项无论是否使用严格解析都可以使用。

何时使用什么？

• 如果你想要尽可能少地等待以获取每个命令或最小化内存消耗，请使用懒解析。
• 如果你解析整个文件并希望减少解析的总运行时间，请使用严格解析。
• 如果你不关心一个符号是否是变量，请无条件使用字符串存储符号。在这种情况下，在进行严格解析时，为了减少 String 分配，优先使用 &str 而不是 String 作为字符串类型。

示例

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