Address review feedback: simplify parser, Java codegen, and formatting

- Parser.lean: use Id.run do + early return for comment parsing, replace
  startsWith with utf8ByteSize check (comment 6)
- Java/Gen.lean: match on DDM category name (Init.Num/Init.Decimal) instead
  of Java type string for builder parameter generation (comment 7)
- Format.lean: collapse comma/space/newline seq formatting into single
  sepBy arm, eliminating duplication (comment 8)
- Java/Gen.lean: consolidate getSeparator with SepFormat.toIonName by
  adding fromCategoryName? and moving Ion-specific functions to
  Strata.DDM.Ion (comment 9)

Author: fabiomadge

Strata/DDM/AST.lean

@@ -200,25 +200,14 @@ def toString : SepFormat → String
   | .spacePrefix => "spacePrefixSepBy"
   | .newline => "newlineSepBy"
 
-def toIonName : SepFormat → String
-  | .none => "seq"
-  | .comma => "commaSepList"
-  | .space => "spaceSepList"
-  | .spacePrefix => "spacePrefixedList"
-  | .newline => "newlineSepList"
-
-def fromIonName? : String → Option SepFormat
-  | "seq" => some .none
-  | "commaSepList" => some .comma
-  | "spaceSepList" => some .space
-  | "spacePrefixedList" => some .spacePrefix
-  | "newlineSepList" => some .newline
+def fromCategoryName? : QualifiedIdent → Option SepFormat
+  | q`Init.Seq => some .none
+  | q`Init.CommaSepBy => some .comma
+  | q`Init.SpaceSepBy => some .space
+  | q`Init.SpacePrefixSepBy => some .spacePrefix
+  | q`Init.NewlineSepBy => some .newline
   | _ => none
 
-theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :
-  fromIonName? (toIonName sep) = some sep := by
-  cases sep <;> rfl
-
 instance : ToString SepFormat where
   toString := SepFormat.toString
 

Strata/DDM/Format.lean

@@ -382,26 +382,16 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
   | .none =>
     .atom <$> entries.foldlM (init := .nil) fun p a =>
       return (p ++ (← a.mformatM).format)
-  | .comma =>
+  | .comma | .space | .newline =>
+    let sepStr := match sep with | .comma => ", " | .space => " " | .newline => "\n" | _ => ""
     if z : entries.size = 0 then
       pure (.atom .nil)
     else do
-      let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format
       let a := (← entries[0].mformatM).format
-      .atom <$> entries.size.foldlM f (start := 1) a
-  | .space =>
-    if z : entries.size = 0 then
-      pure (.atom .nil)
-    else do
-      let f i q s := return s ++ " " ++ (← entries[i].mformatM).format
-      let a := (← entries[0].mformatM).format
-      .atom <$> entries.size.foldlM f (start := 1) a
+      .atom <$> entries.size.foldlM (fun i q s => return s ++ sepStr ++ (← entries[i].mformatM).format) (start := 1) a
   | .spacePrefix =>
     .atom <$> entries.foldlM (init := .nil) fun p a =>
       return (p ++ " " ++ (← a.mformatM).format)
-  | .newline =>
-    .atom <$> entries.foldlM (init := .nil) fun p a =>
-      return (if p.isEmpty then p else p ++ "\n") ++ (← a.mformatM).format
 
 private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat :=
   if rargs.isEmpty then

Strata/DDM/Integration/Java/Gen.lean

@@ -6,6 +6,7 @@
 module
 
 public import Strata.DDM.AST
+import Strata.DDM.Ion
 import Strata.DDM.Integration.Categories
 
 namespace Strata.Java
@@ -137,13 +138,7 @@ def argDeclKindToJavaType : ArgDeclKind → JavaType
 
 /-- Get Ion separator name for a list category, or none if not a list. -/
 def getSeparator (c : SyntaxCat) : Option String :=
-  match c.name with
-  | q`Init.Seq => some "seq"
-  | q`Init.CommaSepBy => some "commaSepList"
-  | q`Init.NewlineSepBy => some "newlineSepList"
-  | q`Init.SpaceSepBy => some "spaceSepList"
-  | q`Init.SpacePrefixSepBy => some "spacePrefixedList"
-  | _ => none
+  SepFormat.fromCategoryName? c.name |>.map SepFormat.toIonName
 
 /-- Extract the QualifiedIdent for categories that need Java interfaces, or none for primitives. -/
 partial def syntaxCatToQualifiedName (cat : SyntaxCat) : Option QualifiedIdent :=
@@ -322,15 +317,22 @@ def opDeclToJavaRecord (dialectName : String) (names : NameAssignments) (op : Op
 
 def generateBuilders (package : String) (dialectName : String) (d : Dialect) (names : NameAssignments) : String :=
   let methods (op : OpDecl) :=
-    let fields := op.argDecls.toArray.map argDeclToJavaField
-    let (ps, as, checks) := fields.foldl (init := (#[], #[], #[])) fun (ps, as, checks) f =>
-      match f.type with
-      | .simple "java.math.BigInteger" _ =>
-        (ps.push s!"long {f.name}",
-         as.push s!"java.math.BigInteger.valueOf({f.name})",
-         checks.push s!"if ({f.name} < 0) throw new IllegalArgumentException(\"{f.name} must be non-negative\");")
-      | .simple "java.math.BigDecimal" _ => (ps.push s!"double {f.name}", as.push s!"java.math.BigDecimal.valueOf({f.name})", checks)
-      | t => (ps.push s!"{t.toJava} {f.name}", as.push f.name, checks)
+    let (ps, as, checks) := op.argDecls.toArray
+        |>.foldl (init := (#[], #[], #[])) fun (ps, as, checks) decl =>
+      let name := escapeJavaName decl.ident
+      let cat := decl.kind.categoryOf.name
+      if cat == q`Init.Num then
+        -- Long parameter must be non-negative.
+        (ps.push s!"long {name}",
+         as.push s!"java.math.BigInteger.valueOf({name})",
+         checks.push s!"if ({name} < 0) throw new IllegalArgumentException(\"{name} must be non-negative\");")
+      else if cat == q`Init.Decimal then
+        (ps.push s!"double {name}",
+         as.push s!"java.math.BigDecimal.valueOf({name})",
+         checks)
+      else
+        let t := (argDeclKindToJavaType decl.kind).toJava
+        (ps.push s!"{t} {name}", as.push name, checks)
     let methodName := escapeJavaName op.name
     let returnType := names.categories[op.category]!
     let recordName := names.operators[(op.category, op.name)]!

Strata/DDM/Ion.lean

@@ -82,6 +82,29 @@ end Ion.Ion
 
 namespace Strata
 
+namespace SepFormat
+
+def toIonName : SepFormat → String
+  | .none => "seq"
+  | .comma => "commaSepList"
+  | .space => "spaceSepList"
+  | .spacePrefix => "spacePrefixedList"
+  | .newline => "newlineSepList"
+
+def fromIonName? : String → Option SepFormat
+  | "seq" => some .none
+  | "commaSepList" => some .comma
+  | "spaceSepList" => some .space
+  | "spacePrefixedList" => some .spacePrefix
+  | "newlineSepList" => some .newline
+  | _ => none
+
+theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :
+  fromIonName? (toIonName sep) = some sep := by
+  cases sep <;> rfl
+
+end SepFormat
+
 /--
 Represents an Ion value that is either a symbol/string or a non-empty
 s-expression. The size proof ensures termination in recursive deserialization.

Strata/DDM/Parser.lean

@@ -227,20 +227,19 @@ private partial def whitespace : ParserFn := fun c s =>
       let j    := c.next' i h
       let curr := c.get j
       match curr with
-      | '/' =>
-        -- Treat as comment unless a token starting with "//" exists (e.g., //@pre)
-        match c.tokens.matchPrefix c.inputString i with
-        | some tk => if tk.startsWith "//" then s
-          else andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j)
-        | none =>
-          andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j)
-      | '*' =>
-        -- Treat as comment unless a token starting with "/*" exists
-        match c.tokens.matchPrefix c.inputString i with
-        | some tk => if tk.startsWith "/*" then s
-          else andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j))
-        | none =>
-          andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j))
+      | '/' => Id.run do
+        -- Treat // as comment unless a token covering both chars exists (e.g., //@pre)
+        if let some tk := c.tokens.matchPrefix c.inputString i then
+          if tk.utf8ByteSize >= 2 then
+            return s
+        andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j)
+      | '*' => Id.run do
+        -- Treat /* as comment unless a token covering both chars exists
+        if let some tk := c.tokens.matchPrefix c.inputString i then
+          if tk.utf8ByteSize >= 2 then
+            return s
+        andthenFn (finishCommentBlock (pushMissingOnError := false))
+          whitespace c (s.next c (c.next j))
       | _ =>
         s
     else s