In this paper, we present a derivative-based, functional recognizer and parser generator for visibly pushdown grammars. The generated parser accepts ambiguous grammars and produces a parse forest containing all valid parse trees for an input string in linear time. Each parse tree in the forest can then be extracted also in linear time. Besides the parser generator, to allow more flexible forms of the visibly pushdown grammars, we also present a translator that converts a tagged CFG to a visibly pushdown grammar in a sound way, and the parse trees of the tagged CFG are further produced by running the semantic actions embedded in the parse trees of the translated visibly pushdown grammar. The performance of the parser is compared with a popular parsing tool ANTLR and other popular hand-crafted parsers. The correctness of the core parsing algorithm is formally verified in the proof assistant Coq.
翻译:在本文中, 我们为明显下推语法提供了一个基于衍生物的、 功能识别器和剖析器生成器。 生成的剖析器接受模糊的语法, 并生成一个包含所有有效剖析树的剖析林, 用于直线时间的输入线条。 然后, 森林中的每一棵剖析树也可以在线性时间中提取 。 除了剖析器生成器外, 允许更灵活的表推语法形式, 我们还提出一个翻译器, 将贴有标签的 CFG 转换成一个明显推下语法, 并且通过运行被翻译的明显下推语法树的剖析树进一步生成 。 剖析器的性能与流行的剖析工具 ANTRR 和其他流行手工艺的剖析器相比较。 校准助理 Coq 正式验证了核心剖析算法的正确性 。