Add getIonDeserializer% elaborator for generic Ion deserialization

Strata.lean

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

Strata/DDM/Integration/Java.lean

@@ -6,3 +6,4 @@
 module
 
 public import Strata.DDM.Integration.Java.Gen
+public import Strata.DDM.Integration.Java.GenDDM

StrataMain.lean

@@ -10,6 +10,7 @@ import Lean.Parser.Extension
 import Strata.Backends.CBMC.CollectSymbols
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
 import Strata.DDM.Integration.Java.Gen
+import Strata.DDM.Integration.Java.GenDDM
 import Strata.Languages.Core.Verifier
 import Strata.Languages.Core.SarifOutput
 import Strata.Languages.Core.ProgramEval
@@ -849,10 +850,10 @@ def javaGenCommand : Command where
       match ← Strata.readStrataFile fm v[0] with
       | .dialect d => pure d
       | .program _ => exitFailure "Expected a dialect file, not a program file."
-    match Strata.Java.generateDialect d v[1] with
+    match Strata.Java.DDM.generateDialect d v[1] with
     | .ok files =>
-      Strata.Java.writeJavaFiles v[2] v[1] files
-      IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.packageToPath v[1]}"
+      Strata.Java.DDM.writeJavaFiles v[2] v[1] files
+      IO.println s!"Generated Java files for {d.name} in {v[2]}/{Strata.Java.DDM.packageToPath v[1]}"
     | .error msg =>
       exitFailure s!"Error generating Java: {msg}"
 

StrataTest/Util/IonDeserializer.lean

@@ -0,0 +1,144 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+import Strata.Util.IonDeserializer
+
+-- Test structure
+structure Point where
+  x : Nat
+  y : Nat
+deriving Repr, BEq
+
+-- Verify the elaborator produces a well-typed function
+def deserializePoint : ByteArray → Except Std.Format Point :=
+  getIonDeserializer% Point
+
+-- Test multi-constructor inductive
+inductive Color where
+  | red
+  | green
+  | blue
+deriving Repr, BEq
+
+def deserializeColor : ByteArray → Except Std.Format Color :=
+  getIonDeserializer% Color
+
+-- Test inductive with fields
+inductive Shape where
+  | circle (radius : Nat)
+  | rect (width : Nat) (height : Nat)
+deriving Repr, BEq
+
+def deserializeShape : ByteArray → Except Std.Format Shape :=
+  getIonDeserializer% Shape
+
+-- Test structure with String and Bool
+structure Person where
+  name : String
+  age : Nat
+  active : Bool
+deriving Repr, BEq
+
+def deserializePerson : ByteArray → Except Std.Format Person :=
+  getIonDeserializer% Person
+
+-- Test structure with Int
+structure Offset where
+  dx : Int
+  dy : Int
+deriving Repr, BEq
+
+def deserializeOffset : ByteArray → Except Std.Format Offset :=
+  getIonDeserializer% Offset
+
+-- Test structure with Float
+structure Measurement where
+  value : Float
+  tolerance : Float
+deriving Repr, BEq
+
+def deserializeMeasurement : ByteArray → Except Std.Format Measurement :=
+  getIonDeserializer% Measurement
+
+-- Test nested structure (non-recursive)
+structure Line where
+  start : Point
+  stop : Point
+deriving Repr, BEq
+
+def deserializeLine : ByteArray → Except Std.Format Line :=
+  getIonDeserializer% Line
+
+-- Test recursive type
+inductive Tree where
+  | leaf (value : Nat)
+  | node (left : Tree) (right : Tree)
+deriving Repr, BEq
+
+partial def deserializeTree : ByteArray → Except Std.Format Tree :=
+  getIonDeserializer% Tree
+
+-- Verify type signatures
+#check (deserializePoint : ByteArray → Except Std.Format Point)
+#check (deserializeColor : ByteArray → Except Std.Format Color)
+#check (deserializeShape : ByteArray → Except Std.Format Shape)
+#check (deserializePerson : ByteArray → Except Std.Format Person)
+#check (deserializeOffset : ByteArray → Except Std.Format Offset)
+#check (deserializeMeasurement : ByteArray → Except Std.Format Measurement)
+#check (deserializeLine : ByteArray → Except Std.Format Line)
+#check (deserializeTree : ByteArray → Except Std.Format Tree)
+
+-- Test structure with List fields
+structure Polygon where
+  vertices : List Point
+deriving Repr, BEq
+
+partial def deserializePolygon : ByteArray → Except Std.Format Polygon :=
+  getIonDeserializer% Polygon
+
+#check (deserializePolygon : ByteArray → Except Std.Format Polygon)
+
+-- Test structure with Option fields
+structure Config where
+  name : String
+  timeout : Option Nat
+deriving Repr, BEq
+
+def deserializeConfig : ByteArray → Except Std.Format Config :=
+  getIonDeserializer% Config
+
+#check (deserializeConfig : ByteArray → Except Std.Format Config)
+
+-- Test structure with Decimal fields
+structure Price where
+  amount : Strata.Decimal
+deriving Repr, BEq
+
+def deserializePrice : ByteArray → Except Std.Format Price :=
+  getIonDeserializer% Price
+
+#check (deserializePrice : ByteArray → Except Std.Format Price)
+
+-- Test structure with List of leaf types
+structure Numbers where
+  values : List Nat
+deriving Repr, BEq
+
+def deserializeNumbers : ByteArray → Except Std.Format Numbers :=
+  getIonDeserializer% Numbers
+
+#check (deserializeNumbers : ByteArray → Except Std.Format Numbers)
+
+-- Test structure with Option of compound type
+structure MaybeLine where
+  line : Option Line
+deriving Repr, BEq
+
+partial def deserializeMaybeLine : ByteArray → Except Std.Format MaybeLine :=
+  getIonDeserializer% MaybeLine
+
+#check (deserializeMaybeLine : ByteArray → Except Std.Format MaybeLine)