Add getIonDeserializer% and getIonSerializer% elaborators for generic Ion serialization

.github/workflows/ci.yml

@@ -91,10 +91,6 @@ jobs:
             StrataDDM/.lake
             StrataBoole/.lake
             StrataPython/.lake
-      - name: Verify Java testdata is up to date
-        run: |
-          StrataTestExtra/Languages/Java/regenerate-testdata.sh
-          git diff --exit-code StrataTestExtra/Languages/Java/testdata/
       - name: Build and run strata verify
         run: lake exe strata verify ../Examples/SimpleProc.core.st
         working-directory: StrataCLI

Scripts/LaurelJavaGen.lean

@@ -0,0 +1,36 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import StrataDDM.Integration.Java.Gen
+import Strata.Languages.Laurel.LaurelAST
+
+/-!
+# Laurel Java AST Generator
+
+Generates Java source files for the Laurel AST types using `getIonSerializer%`.
+The generated Java matches the Ion encoding format used by `getIonDeserializer%`.
+
+Usage:
+  lake exe laurelJavaGen <package> <output-dir>
+
+Example:
+  lake exe laurelJavaGen org.strata.jverify.laurel ../jverify/verifier/src/main/java
+-/
+
+open Strata.Java
+
+/-- Pre-computed Java files for the Laurel `Program` type. -/
+private def laurelFiles : GeneratedFiles := getIonSerializer% Strata.Laurel.Program "___placeholder___"
+
+def main (args : List String) : IO Unit := do
+  match args with
+  | [package, outputDir] =>
+    let files := laurelFiles.files.map fun (name, content) =>
+      (name, content.replace "package ___placeholder___;" s!"package {package};")
+    writeJavaFiles outputDir package { files }
+    IO.println s!"Generated {files.size} Java files in {outputDir}"
+  | _ =>
+    IO.eprintln "Usage: lake exe laurelJavaGen <package> <output-dir>"
+    IO.Process.exit 1

Strata.lean

@@ -17,6 +17,7 @@ import Strata.DL.Lambda
 import Strata.DL.Imperative
 
 /- Utilities -/
+import Strata.Util.IonDeserializer
 import Strata.Util.NameProofs
 import Strata.Util.Sarif
 

Strata/Languages/Laurel.lean

@@ -12,6 +12,7 @@ import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Languages.Laurel.Grammar.LaurelGrammar
 import StrataDDM.Elab
+import Strata.Util.IonDeserializer
 
 /-! ## Strata Laurel API
 
@@ -22,6 +23,11 @@ public section
 
 namespace Strata
 
+/-- Deserializer for the new struct-format Ion encoding of `Laurel.Program`,
+generated by `getIonSerializer%`. -/
+private partial def deserializeLaurelProgram : ByteArray → Except Std.Format Laurel.Program :=
+  getIonDeserializer% Laurel.Program
+
 /-! ### File I/O -/
 
 /--
@@ -64,9 +70,17 @@ def readLaurelIonFiles (bytes : ByteArray)
 /--
 Deserialize Laurel Ion bytes and parse all files into a single
 combined `Laurel.Program`.
+
+Supports both the new struct-format (from `getIonSerializer%`) and the
+legacy DDM-based format. Tries the new format first, falls back to DDM.
 -/
 def readLaurelIonProgram (bytes : ByteArray)
     : IO Laurel.Program := do
+  -- Try new struct-format deserialization first
+  match deserializeLaurelProgram bytes with
+  | .ok program => return program
+  | .error _ => pure ()
+  -- Fall back to legacy DDM path
   let files ← readLaurelIonFiles bytes
   let mut combined : Laurel.Program := {
     staticProcedures := []