feat(DDM): Java code generator for dialects #292

fabiomadge · 2025-12-23T02:34:12Z

Java Code Generator for DDM Dialects

Generates Java source files from DDM dialect definitions for Java tooling to build ASTs that Lean can consume.

Generated:

Sealed interfaces for categories
Record classes for operators
Static factory methods (num(1) vs new Num(SourceRange.NONE, ...))
Ion serializer for Lean interop

Usage:

lake exe strata javaGen dialect.st com.example.pkg output/

Tests: 12 tests including javac compilation and Java→Ion→Lean roundtrip.

keyboardDrummer · 2025-12-24T16:18:37Z

StrataTest/DDM/Integration/Java/TestGen.lean

+  let files := generateDialect simple "com.test"
+
+  let dir := "/tmp/strata-java-test"
+  IO.FS.createDirAll (dir ++ "/com/test")


Could this use writeJavaFiles instead of generateDialect, to prevent needing this awkward part?

keyboardDrummer · 2025-12-24T16:20:52Z

StrataTest/DDM/Integration/Java/TestGen.lean

+
+#testCompile
+
+elab "#testRoundtrip" : command => do


Could you explain this test relies on comprehensive.ion and point to the README for updating that file? I can even imagine inlining that README.md here, because it only seems relevant for this test.

keyboardDrummer · 2025-12-24T16:25:43Z

StrataTest/DDM/Integration/Java/TestGen.lean

+#testBoogie
+
+-- Test 11: Generated Java compiles (requires javac)
+-- Test 12: Roundtrip - verify Lean can read Java-generated Ion


Shouldn't -- Test 12: Roundtrip - verify Lean can read Java-generated Ion occur after the body of test 11 ? The tests are independent right?

keyboardDrummer · 2025-12-24T16:32:03Z

StrataTest/DDM/Integration/Java/TestGen.lean

@@ -0,0 +1,302 @@
+/-


Test 11 seems problematic since it uses javac. Is that even available in CI? I don't see it being installed in the CI script. How it is possible that this test passes in CI?

I think it would be better to have generated .java files checked into source and have a test compare those against what's currently generated.

joehendrix · 2025-12-24T16:42:36Z

Strata/DDM/Integration/Java/Gen.lean

+  | ⟨"Init", "Option"⟩ =>
+    match cat.args[0]? with
+    | some inner => .optional (syntaxCatToJavaType inner)
+    | none => .optional (.simple "java.lang.Object")


The none case here (and with "Seq") would be an malformed SyntaxCat. I'd recommend using panic!.

Strata/DDM/Integration/Java/Gen.lean

joehendrix · 2025-12-24T16:51:00Z

Strata/DDM/Integration/Java/Gen.lean

+"
+
+/-- Assign unique Java names to all generated types -/
+def assignAllNames (d : Dialect) : NameAssignments :=


I noticed this isn't (yet) supporting functions or types. I think that's ok if they aren't needed now, but I'd recommend adding a check that they are empty in the dialect.

The Laurel grammar is using them at the moment, for which this PR is intended. I think we can refactor the Laurel grammar not to use functions or types. Despite reading the DDM documentation their purpose isn't entirely clear to me. I don't think we need any type checking features for Laurel.

- Use writeJavaFiles helper in Test 11 (keyboardDrummer) - Document Test 12's dependency on comprehensive.ion (keyboardDrummer) - Fail if javac not found instead of skip (keyboardDrummer) - Use panic! for malformed SyntaxCat (joehendrix) - Add doc comments to GeneratedFiles and NameAssignments (joehendrix) - Collect warnings for unsupported type/function declarations (joehendrix)

fabiomadge · 2025-12-24T21:26:49Z

Strata/DDM/Elab/Core.lean

+    let name := name.stripPrefix "«" |>.stripSuffix "»"
+    match name.splitOn "." with
+    | [dialect, rest] => .qid { dialect, name := rest }
+    | _ => .name name


@MikaelMayer your PR (#293) broke my Simple.dialect.st‎. Does this fix look reasonable to you?

PR strata-org#293 added dots to valid identifier characters, which broke qualified name resolution (e.g., 'Simple.Expr' was parsed as one identifier instead of dialect 'Simple' + name 'Expr'). Fix: In translateQualifiedIdent, split dotted identifiers on the first dot to extract dialect and name components. Also strip guillemets that the parser adds around special identifiers.

keyboardDrummer · 2026-01-02T09:43:59Z

As a follow-up, could you enable the Laurel grammer, which is currently in a .lean file, to be consumed by the command that this PR adds? I think it would mean moving that grammar into a .dialect.st file, with some of the surrounding code stripped, and updating references to LaurelGrammar so they load that dialect file instead of loading a lean module.

fabiomadge · 2026-01-02T10:48:35Z

@keyboardDrummer Would it just take the first grammar it finds? Could you use generateDialect in the .lean instead?

keyboardDrummer · 2026-01-05T12:12:25Z

Could you add a test related to source locations? Note that the original program will have sources divided across different files, and each AST node except for the root will have a start and an end location, where each location is a line and column. My impression is that this PR doesn't support the above.

joehendrix · 2026-01-06T07:41:14Z

Strata/DDM/Integration/Java/Gen.lean

+    | some inner => .list (syntaxCatToJavaType inner)
+    | none => panic! "Init.Seq/CommaSepBy requires a type argument"
+  | ⟨"Init", "Expr"⟩ => .simple "Expr"
+  | ⟨"Init", "TypeExpr"⟩ => .simple "TypeExpr"


I've been treating Init.TypeExpr as a implementation detail that I don't think dialects should directly use. It essentially exists for the parser, and they should use Init.Type. It essentially is a type or category expression and I think dialects should be Init.Type or Init.TypeP.

I'd like to better codify this, but the Lean generator code has a notion of forbidden categories.

In short, I think if the generator sees references to Init.TypeExpr, it should issue a warning.

joehendrix · 2026-01-06T07:43:08Z

Strata/DDM/Integration/Java/Gen.lean

+  | ⟨"Init", "TypeExpr"⟩ => .simple "TypeExpr"
+  | ⟨"Init", "Type"⟩ => .simple "Type_"
+  | ⟨"Init", "TypeP"⟩ => .simple "TypeP"
+  | ⟨_, name⟩ => .simple (escapeJavaName (toPascalCase name))


Right now the DDM would allow two dialects to have categories with the same name (e.g., A.Num and B.Num) but would need them to be qualified in the source. I think this code won't handle that case. The Lean generator has a some additional code for this here.

keyboardDrummer · 2026-01-06T15:14:59Z

Tools/Java/regenerate-testdata.sh

+(cd "$STRATA_ROOT" && lake exe strata javaGen "$TESTDATA/Simple.dialect.st" com.strata.simple "$STRATA_ROOT/Tools/Java/src/main/java")
+
+echo "=== Building and running test data generator ==="
+./gradlew run -PmainClass=com.strata.test.GenerateTestData --args="$TESTDATA/comprehensive.ion" --quiet


Which gradlew is this referring to? Is that checked in somewhere? This script is not run in CI right? How do we know that it runs?

- Fail on Init.TypeExpr (internal DDM machinery) - Fail on type/function declarations instead of warning - Remove warnings mechanism from GeneratedFiles - Fix cross-dialect category collision (A.Num vs B.Num) - Track QualifiedIdent instead of String for refs - Prefix with dialect name when names collide - Replace gradle with plain javac/java in regenerate script - Add test for cross-dialect name collision

joehendrix · 2026-01-08T17:44:52Z

Strata/DDM/Integration/Java/Gen.lean

+  match cat.name with
+  -- Primitives map to Java types, no interface needed
+  | ⟨"Init", "Ident"⟩ | ⟨"Init", "Num"⟩ | ⟨"Init", "Decimal"⟩
+  | ⟨"Init", "Str"⟩ | ⟨"Init", "ByteArray"⟩ | ⟨"Init", "Bool"⟩ => none


In the Lean generator, I call these "declaredCategories" and define a set here.

Maybe it should be a separate PR, but I suspect this and some of the other Init category handling could be shared.

joehendrix · 2026-01-08T17:47:10Z

Strata/DDM/Integration/Java/Gen.lean

+        return sexp;
+    }
+}
+"


I wonder if some of these functions could be moved into a fixed file with a Java extension (e.g., for syntax highlighting)?

If it needs to ship in the Strata executable we could have a custom elaborator read it in from a file.

joehendrix

I had a couple comments, but didn't see anything that would block merging.

I didn't look at the tests in as much detail as Remy, but I'd recommend making sure they run in CI in this or a future PR.

- Add Strata/DDM/Integration/Categories.lean with shared: - primitiveCategories (Init types mapping to primitives) - forbiddenCategories (internal DDM machinery) - abstractCategories (dialect extension points) - Extract Java templates to .java files for syntax highlighting: - templates/SourceRange.java - templates/Node.java - templates/IonSerializer.java - Update both generators to use shared categories: - Java Gen.lean uses all three directly - Lean Gen.lean uses forbiddenCategories and abstractCategories, with guard to verify declaredCategories matches primitiveCategories

fabiomadge added 4 commits December 23, 2025 03:33

feat(DDM): Java code generator for dialects

613fec6

Merge remote-tracking branch 'origin/main' into feat/java-codegen

e18f450

docs: update module docstring to mention builders

f99ea87

test: verify deserialized AST structure

780c78e

fabiomadge force-pushed the feat/java-codegen branch from d002a4d to 780c78e Compare December 23, 2025 02:55

fabiomadge added 6 commits December 23, 2025 03:57

chore: remove redundant inline comments

e0b2bb5

refactor: use #load_dialect instead of inline dialect definition

da67291

fix: correct test 2 title

67c170d

test: use Simple dialect for compile test, include builders

8731075

fix: disambiguate builders filename to avoid collisions

98c3a4a

refactor: use get! and alter for cleaner lookups

b36929a

fabiomadge marked this pull request as ready for review December 23, 2025 04:01

fabiomadge requested review from a team, aqjune-aws, joehendrix and shigoel as code owners December 23, 2025 04:01

fix: escape builder method names for Java reserved words

1404ab0

keyboardDrummer reviewed Dec 24, 2025

View reviewed changes

joehendrix reviewed Dec 24, 2025

View reviewed changes

fabiomadge added 2 commits December 24, 2025 21:51

Merge remote-tracking branch 'origin/main' into feat/java-codegen

be0acbf

fabiomadge force-pushed the feat/java-codegen branch 3 times, most recently from f0fbfb2 to 0a43cda Compare December 24, 2025 21:23

fabiomadge commented Dec 24, 2025

View reviewed changes

fabiomadge force-pushed the feat/java-codegen branch from 0a43cda to 58e2510 Compare December 24, 2025 21:30

fabiomadge force-pushed the feat/java-codegen branch from 58e2510 to 775600c Compare December 24, 2025 21:38

joehendrix reviewed Jan 6, 2026

View reviewed changes

keyboardDrummer reviewed Jan 6, 2026

View reviewed changes

fabiomadge and others added 2 commits January 7, 2026 19:30

Merge branch 'main' into feat/java-codegen

a3e9ec9

This was referenced Jan 8, 2026

Changes to enable communication with JVerify fabiomadge/Strata#1

Open

Changes to enable communication with JVerify #308

Open

chore: retrigger CI

a246dbb

joehendrix reviewed Jan 8, 2026

View reviewed changes

joehendrix previously approved these changes Jan 8, 2026

View reviewed changes

fabiomadge dismissed joehendrix’s stale review via 0915788 January 8, 2026 18:21


		#testCompile

		elab "#testRoundtrip" : command => do

feat(DDM): Java code generator for dialects #292

Are you sure you want to change the base?

feat(DDM): Java code generator for dialects #292

Uh oh!

Conversation

fabiomadge commented Dec 23, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Dec 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer commented Jan 2, 2026

Uh oh!

fabiomadge commented Jan 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

keyboardDrummer commented Jan 5, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joehendrix left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

keyboardDrummer Dec 24, 2025 •

edited

Loading

fabiomadge commented Jan 2, 2026 •

edited

Loading