Coq 的解析器是如何实现的？
How is Coq's parser implemented?
我对 Coq 解析器的实现方式感到非常惊讶。例如
https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab347
这太疯狂了，解析器似乎可以通过给出符号命令来获取任何词位，并且后续解析器能够按原样解析任何表达式。所以这意味着语法必须是上下文相关的。但这太灵活了，完全超出了我的理解范围。
关于这种解析器在理论上如何可行的任何指示？它应该如何工作？任何材料或知识都可以。我只是尝试大致了解这种类型的解析器。谢谢
请不要让我自己阅读 Coq 的源代码。我想检查一般的想法而不是具体的实现。
的确，这个符号系统非常强大，这可能是 Coq 成功的原因之一。实际上，这是源代码中很多复杂性的来源。我认为 @ejgallego 应该能够告诉您更多相关信息，但这里有一个快速解释：
一开始，Coq的文档都是由coqtop逐句求值（句子之间用点隔开）。一些命令可以定义符号，这些符号在评估时会修改解析规则。因此，后面的句子使用略有不同的解析器进行评估。
从 8.5 版本开始，还有一种机制 (STM) 可以对文档进行全面评估（许多句子并行），但是有一些特殊的机制来处理这些符号命令（基本上你必须等待这些被评估，然后才能继续解析和评估文档的其余部分。
因此，与普通的编程语言相反，编译器将获取文档，将其传递给词法分析器，然后传递给解析器（一次性解析完整文档），然后将 AST 提供给typer 或其他后期阶段，在 Coq 中，每个命令都被单独解析和评估。因此，无需求助于复杂的上下文语法...
我会拿出我的两分钱来补充@Zimmi48 的出色回答。
Coq 确实具有可扩展的解析器，TTBOMK 主要是 Hugo Herbelin 的作品，建立在 Daniel de Rauglaudre 的 CAMLP4/CAMLP5 可扩展解析系统之上。两者都是关于解析器信息的规范来源，我将尝试总结我所知道的，但请注意，我对系统的经验确实很短。
CAMLPX系统基本支持任何LL1语法。 Coq 向用户公开了整套语法规则，允许用户重新定义它们。这是构建可扩展语法的基本机制。符号在 Metasyntax 模块中被编译成解析规则，并在后面的 post 处理阶段展开。这真的是 AFAICT。
系统本身在整个8.x系列中并没有太大的变化，@Zimmi48的评论更多的是关于命令after解析后的内部处理。我最近了解到 Coq v7 有一个更强大的系统来修改解析器。
用 Hugo Herbelin 的话说 "the art of extensible parsing is a delicate one" 确实如此，但 Coq 实现了它的一个非常好的实现。
我对 Coq 解析器的实现方式感到非常惊讶。例如
https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab347
这太疯狂了，解析器似乎可以通过给出符号命令来获取任何词位，并且后续解析器能够按原样解析任何表达式。所以这意味着语法必须是上下文相关的。但这太灵活了，完全超出了我的理解范围。
关于这种解析器在理论上如何可行的任何指示？它应该如何工作？任何材料或知识都可以。我只是尝试大致了解这种类型的解析器。谢谢
请不要让我自己阅读 Coq 的源代码。我想检查一般的想法而不是具体的实现。
的确，这个符号系统非常强大，这可能是 Coq 成功的原因之一。实际上，这是源代码中很多复杂性的来源。我认为 @ejgallego 应该能够告诉您更多相关信息，但这里有一个快速解释：
一开始，Coq的文档都是由
coqtop逐句求值（句子之间用点隔开）。一些命令可以定义符号，这些符号在评估时会修改解析规则。因此，后面的句子使用略有不同的解析器进行评估。从 8.5 版本开始，还有一种机制 (STM) 可以对文档进行全面评估（许多句子并行），但是有一些特殊的机制来处理这些符号命令（基本上你必须等待这些被评估，然后才能继续解析和评估文档的其余部分。
因此，与普通的编程语言相反，编译器将获取文档，将其传递给词法分析器，然后传递给解析器（一次性解析完整文档），然后将 AST 提供给typer 或其他后期阶段，在 Coq 中，每个命令都被单独解析和评估。因此，无需求助于复杂的上下文语法...
我会拿出我的两分钱来补充@Zimmi48 的出色回答。
Coq 确实具有可扩展的解析器，TTBOMK 主要是 Hugo Herbelin 的作品，建立在 Daniel de Rauglaudre 的 CAMLP4/CAMLP5 可扩展解析系统之上。两者都是关于解析器信息的规范来源，我将尝试总结我所知道的，但请注意，我对系统的经验确实很短。
CAMLPX系统基本支持任何LL1语法。 Coq 向用户公开了整套语法规则，允许用户重新定义它们。这是构建可扩展语法的基本机制。符号在 Metasyntax 模块中被编译成解析规则，并在后面的 post 处理阶段展开。这真的是 AFAICT。
系统本身在整个8.x系列中并没有太大的变化，@Zimmi48的评论更多的是关于命令after解析后的内部处理。我最近了解到 Coq v7 有一个更强大的系统来修改解析器。
用 Hugo Herbelin 的话说 "the art of extensible parsing is a delicate one" 确实如此，但 Coq 实现了它的一个非常好的实现。