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

Question

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

通过给出notation命令并且后续解析器能够解析任何表达式,解析器似乎可以接受任何lexeme.所以这意味着语法必须是上下文敏感的.但这非常灵活,绝对超出了我的理解范围.

关于这种解析器在理论上如何可行的任何指针？它应该如何工作？任何材料或知识都可行.我只是试着了解一下这种类型的解析器.谢谢.

请不要让我自己阅读Coq的来源.我想检查一般的想法,但不是具体的实现.

Answer 1

实际上,这种符号系统非常强大,这可能是Coq成功的原因之一.实际上,这是源代码中复杂化的一个原因.我认为@ejgallego应该可以告诉你更多关于它的信息,但这里有一个简单的解释:

最初,Coq的文件逐句评估(句子用点分隔)coqtop.某些命令可以定义符号,这些命令在评估时会修改解析规则.因此,稍后的句子用稍微不同的解析器来评估.
从版本8.5开始,还有一个机制(STM)来完全评估文档(并行多个句子),但是有一些特殊的机制来处理这些符号命令(基本上你必须等待这些评估才能继续解析和评估文档的其余部分).

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

Answer 2

我会放弃我的两分钱来补充@ Zimmi48的优秀答案.

Coq确实具有可扩展的解析器,TTBOMK主要是Hugo Herbelin的工作,它基于Daniel de Rauglaudre的CAMLP4/CAMLP5可扩展解析系统.两者都是有关解析器信息的规范来源,我将尝试总结我所知道的内容,但请注意我对系统的体验很短.

CAMLPX系统基本上支持任何LL1语法.Coq向用户公开整套语法规则,允许用户重新定义它们.这是构建可扩展语法的基本机制.符号在Metasyntax模块中编译为解析规则,并在后一个后处理阶段展开.这真的是AFAICT.

系统本身在整个8.x系列中没有太大变化,@ Zimmi48的注释与解析后的命令内部处理更相关.我最近了解到Coq v7有一个更强大的系统来修改解析器.

用Hugo Herbelin的话说"可扩展解析的艺术是一个微妙的解决方案",事实上确实如此,但Coq实现了它的非常好的实现.