LFSC的Rust实现

安装说明

1. 使用Rustup安装Rust工具链。
   • 确保将Cargo的bin目录添加到您的路径中
     • 例如，通过将以下代码添加到您的rc文件中：export PATH="$HOME/.cargo/bin/:$PATH"
2. 运行 cargo install rlfsc

相对于原始LFSC的可能改进

• 标记器和检查器是分开的。
• 标记器不是按字符逐个进行
  • 它使用logos库实现。
• 使用std::rc::Rc自动引用计数表达式。
• 没有goto/疯狂的东西

形势与政策

在我们的小型测试证明（pf）中，在我的机器上，我们比LFSC慢30%（10.8ms vs 8.0ms）。

在CVC4签名（sig）中，在我的机器上，我们比LFSC快30%（3.0ms vs 4.4ms）。

这表明我们的标记化确实更好，但我们的检查速度较慢。

我们做了很多递归，没有尾递归，导致我们吹小栈。

类型检查算法

它基于Aaron 2008年的手稿，“Satisfiability Modulo Theories的证明检查技术”，但总体上没有优化。

值得注意的是

• 我们始终为检查的项构建一个AST。
• 作用域内的标识符保存在全局映射中
• 当一个抽象表达式被实例化时，我们替换提供值
  • 例如，(\x t) v 变为 t[v / x]，字面意思。也就是说，我们将 t 分解，寻找所有的 x，将它们替换为 v，然后重建 t。
• 在代码表达式中，我们不做这件事。
  • 例如，当我们评估 (let x v t) 时，我们将 x -> v 放入环境，并评估 t，而不是替换。

待办事项

• 尾递归
  • C 语言在尾递归方面一直支持得不好，这也是为什么原始的 LFSC 手动使用 gotos 实现。
  • 我们不能（也不会）在 Rust 中这样做。
  • 我们应该实现一个基于 trampoline 的方法
• 项销毁
  • 在销毁项（自动实现）时，我们会进入深层次的递归。
  • 我们应该手动实现一些析构函数来防止这种情况。
• 实现一个流式标记化程序。
  • 目前我们需要在标记化之前将整个输入加载到内存中。
  • 选项 1：修改 logos，通过实现 logos::Source 为 std::io::Read 来允许这样做。
    • 这并不完全奏效。我们需要稍微修改 Source 的要求。
  • 选项 2：切换到不同的标记化库。
    • 也许 nom？它通常用于解析，但它也支持流式处理。
  • 选项 3：自己编写。
    • 我认为这是一个糟糕的想法。如果 这篇博客文章 教给我的任何东西，那就是高性能文本处理比大多数人想象的要复杂。我认为要匹配像 logos 或 nom 这样的专用库的性能非常困难。