ML-Lex and ML-Yacc for Isabelle

Developing concrete syntax and parsers for Domain-Specific Languages (DSLs) within interactive theorem provers, such as Isabelle, is a common task. Isabelle supports this through rich, yet often brittle to configure, mixfix annotations and syntax translations. Moreover, Isabelle provides parser combinators that can be used to build parsers for the content of cartouches. An alternative to the latter are traditional parser generators, e.g., Lex and Yacc, that take a formal grammar description as input and generate a parser. Traditionally, the use of parser generators for defining DSLs in Isabelle relies on invoking the lexer and parser as external tools, often modifying the generated source code, and importing the generated files. This requires users to manage complex external preprocessing toolchains. In this AFP entry, we address this challenge by providing a native integration of standard ML-Lex and ML-Yacc into Isabelle/HOL. In more detail, we introduce an Isar-level interface, ml_lex_yacc, that allows users to write lexical and grammatical specifications directly within theory files. The framework compiles these specifications into Standard ML structures on-the-fly, links them, and loads them into the current theory context. Moreover, the integration automatically hooks into Isabelle’s Prover IDE (PIDE), empowering users to provide real-time syntax highlighting, semantic tooltips, and precise error localization for their custom languages.