Lay-it-out: Interactive Design of Layout-Sensitive Grammars

TL;DR

Lay-it-out is an interactive framework that helps design layout-sensitive grammars by refining ambiguous grammars with user input and automatically generating example sentences, supported by formal proofs.

Contribution

It introduces a novel interactive approach for designing layout-sensitive grammars with SMT-based synthesis and formal verification in Coq.

Findings

Successfully refines ambiguous grammars with user interaction.

Automatically generates example sentences using SMT solving.

Demonstrates practicality and scalability on real grammars.

Abstract

Layout-sensitive grammars have been adopted in many modern programming languages. However, tool support for this kind of grammars still remains limited and immature. In this paper, we present Lay-it-out, an interactive framework for layout-sensitive grammar design. Beginning with a user-defined ambiguous grammar, our framework refines it by synthesizing layout constraints through user interaction. For ease of interaction, a shortest nonempty ambiguous sentence (if exists) is automatically generated by our bounded ambiguity checker via SMT solving. The soundness and completeness of our SMT encoding are mechanized in the Coq proof assistant. Case studies on real grammars, including a full grammar, demonstrate the practicality and scalability of our approach.