Replace the Laurel DDM based grammar with one defined using bidirectional parser combinators

[keyboardDrummer]

Define a syntax combinator library, like what is defined in this paper: https://dl.acm.org/doi/epdf/10.1145/1863523.1863525

And use it to define the Laurel grammar, and then use this grammar definition in the Laurel compilation pipeline to see if you can get the tests in StrataTest/Languages/Laurel to pass. You can leave the existing DDM based Laurel grammar for now.

[keyboardDrummer-bot]

I've read through the codebase and have a few questions before I start implementing:

1. Parser target type: The current DDM pipeline goes Text → Strata.Program (generic AST) → Laurel.Program via ConcreteToAbstractTreeTranslator. Should the new combinator-based parser go directly from String → Laurel.Program, bypassing the generic Strata.Program intermediate representation? That seems like the natural approach for a combinator library, but I want to confirm.

2. Library location: I'm planning to put the combinator library in Strata/Languages/Laurel/Grammar/ alongside the existing grammar files (e.g. SyntaxCombinator.lean or similar). Or would you prefer it in a more general location like Strata/Util/ since it could potentially be reused for other languages?

3. Test integration: The tests in StrataTest/Languages/Laurel/TestExamples.lean use processLaurelFile which calls the DDM parser pipeline. Should I create a parallel processLaurelFileCombinator and update the tests to use it, or replace the existing processLaurelFile implementation?

4. Bidirectionality: The paper describes partial isomorphisms for both parsing and printing. Should I implement the full bidirectional approach (so the same grammar definition can both parse and pretty-print), or is parsing sufficient for now? The existing LaurelFormat.lean already handles printing.

[keyboardDrummer]

Should the new combinator-based parser go directly from String → Laurel.Program

Yes

Library location

In Strata/Util please

Test integration

Replace the existing processLaurelFile

Bidirectionality

The full approach.

[keyboardDrummer-bot]

I've started implementing this and opened a draft PR: #8

What's done

Strata/Util/Syntax.lean — The bidirectional combinator library is complete and compiles. It implements the core abstractions from the Rendel & Ostermann paper:

• Iso a b — partial isomorphisms (forward for parsing, backward for printing)
• Syntax a — a single type that describes both parsing (String → Option (a, PState)) and printing (a → Option String)
• All the standard combinators: seq, alt, map, many, sepBy, optional, plus token-level parsers for identifiers, numbers, strings, keywords

Strata/Languages/Laurel/Grammar/CombinatorGrammar.lean — The Laurel grammar is defined using these combinators, covering the full language: types, expressions with precedence climbing, all statement forms, procedures/functions, composites, constrained types, and datatypes. The grammar goes directly from String → Laurel.Program (and back), bypassing the DDM intermediate representation.

What's left

The grammar file has compilation errors I'm working through:

1. Mutual recursion between expression parsers — Expression parsing is inherently recursive (e.g., if contains sub-expressions, blocks contain statement lists). Lean 4's partial + where clauses don't support the needed pattern where stmtExprAtom references stmtExprPrec0 and vice versa. I need to restructure this, likely by combining all expression parsing into a single partial def with explicit tag-based dispatch.

2. Lean 4.27 String API — String.drop now returns String.Slice instead of String, requiring .toString calls in several places in the grammar file.

Once these are resolved, I'll wire the combinator parser into TestExamples.lean to replace the DDM pipeline and verify the Laurel tests pass.