kirancodes.me
To Proof Maintenance & Beyond!

Compiling regular patterns

Michael Y. Levin

Abstract

Pattern matching mechanisms based on regular expressions feature in a number of recent languages for processing tree-structured data such as XML. A compiler for such a language must address not only the familiar problems of pattern optimization for ML-style algebraic datatypes and pattern matching, but also some new ones, arising principally from the use of recursion in patterns. We identify several factors playing a significant role in the quality of the generated code, propose two pattern compilers---one generating backtracking target programs, the other non-backtracking---and sketch proofs of their correctness.

DOI 10.1145/944705.944712

Related papers