A Menhir for Edit-Incremental Parsing: Sound Reuse, a Verified Predicate, and Localized Cost-Optimal Recovery for Pratt Parsers

Jeff Pickhardt

Loading document…

A Menhir for Edit-Incremental Parsing: Sound Reuse, a Verified Predicate, and Localized Cost-Optimal Recovery for Pratt Parsers

Abstract

Production compilers ship hand-written recursive-descent parsers with Pratt expression cores. In order for tooling to keep the parse current on every edit, three approaches exist: reparse from scratch (linear in file size); run a separate incremental parser (tree-sitter, Lezer), with a second grammar and a tree that is not the compiler’s; or use a Roslyn-like parser (Roslyn, SwiftSyntax, TypeScript) to make the hand-written parser itself incremental, via a span+lookahead reuse predicate that needs per-construct lookahead bookkeeping and is silently wrong on ~1–2 % of edits without it. We put the Roslyn approach on a firmer footing by implementing a reuse predicate read directly off the structure of Pratt parsing, sound by construction from Pratt’s right-boundary property, two integer comparisons and a boundary check. This is both generatable and verifiable: a one- page operator grammar yields an edit-incremental parser plus a machine-checked certificate that the reuse predicate meets its four-condition specification, panic- and UB-free (bounded via Kani, unbounded via Creusot for single-byte grammars). The soundness argument that those conditions imply correct reuse is a paper proof (§3), corroborated across four grammars by a 400k-edit differential oracle, with the parser itself outside the mechanized boundary; the reuse composes from expressions through a generated statement host into one tree. The same precedence-bounded region localizes error recovery with cost-optimal repair confined to the break; when the error is locally contained this local repair is globally optimal — which we prove for our mechanized grammar and for the boundary regime of the general class, and conjecture in full — addressing a composition gap Diekmann named. Finally, a downstream pass memoized on node identity reuses results exactly where the parser reuses subtrees, lifting parse-level soundness one layer (identity alone is unsound under a binding change; tracking the context a value reads restores it). The result is a “Menhir for edit-incremental parsing” for the operator-expression fragment: grammar in, parser plus certificate out.

File Details

v1 paper3.pdf