parsing - Coq的解析器是如何实现的？

Question

我对 Coq 解析器的实现方式感到非常惊讶。例如

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab347

这太疯狂了，解析器似乎可以通过给出符号命令来获取任何词位，并且后续解析器能够按原样解析任何表达式。所以这意味着语法必须是上下文相关的。但这太灵活了，绝对超出了我的理解范围。

有关这种解析器在理论上如何可行的任何指示？应该如何运作？任何 Material 或知识都可以。我只是尝试总体了解这种类型的解析器。谢谢。

请不要让我自己阅读 Coq 的源代码。我想检查一般的想法，而不是具体的实现。

Answer 1

确实，这个符号系统非常强大，这可能是 Coq 成功的原因之一。实际上，这会导致源代码变得非常复杂。我认为 @ejgallego 应该能够告诉您更多相关信息，但这里有一个快速解释:

• 一开始，Coq 的文档由 coqtop 逐句评估(句子之间用点分隔)。某些命令可以定义符号，并在评估时修改解析规则。因此，后面的句子将使用稍微不同的解析器进行评估。

• 从 8.5 版本开始，还有一种机制(STM)来完全评估文档(并行的许多句子)，但是有一些特殊的机制来处理这些符号命令(基本上你必须等待这些命令)在继续解析和评估文档的其余部分之前进行评估)。

因此，与普通的编程语言相反，编译器将获取文档，将其传递给词法分析器，然后传递给解析器(一次性解析完整文档)，然后将 AST 提供给打字机或在其他后期阶段，在 Coq 中，每个命令都被单独解析和评估。因此，没有必要诉诸复杂的上下文语法......