Idris TyRE：一种依赖类型的正则表达式解析器
摘要：正则表达式（regex）不仅广泛用于验证，也用于解析文本数据。通常，正则表达式解析器输出一种松散的结构，例如一个无结构列表的匹配项，让用户验证输出属性并将其转换为所需的结构。由于正则表达式本身携带有关结构的信息，这种设计导致了不必要的重复。 Radanne引入了类型化正则表达式（TyRE）-一种可以添加到现有的正则表达式引擎之上的类型索引组合器层。我们扩展了Radanne的设计，并实现了一个解析器，该解析器在所有层次中保持类型安全性：面向用户的正则表达式、其内部的去糖表示、已编译的有限状态自动机，以及用于构建解析树的自动机的相关指令集。我们在依赖类型的语言Idris 2中实现了TyRE。
作者：Ohad Kammar and Katarzyna Marek
论文ID：2305.04480
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-09