Infrastructure changes from PR 385

Strata/DDM/AST.lean

@@ -188,6 +188,7 @@ inductive SepFormat where
 | comma          -- Comma separator (CommaSepBy)
 | space          -- Space separator (SpaceSepBy)
 | spacePrefix    -- Space before each element (SpacePrefixSepBy)
+| newline        -- Newline separator (NewlineSepBy)
 deriving Inhabited, Repr, BEq
 
 namespace SepFormat
@@ -197,24 +198,16 @@ def toString : SepFormat → String
   | .comma => "commaSepBy"
   | .space => "spaceSepBy"
   | .spacePrefix => "spacePrefixSepBy"
-
-def toIonName : SepFormat → String
-  | .none => "seq"
-  | .comma => "commaSepList"
-  | .space => "spaceSepList"
-  | .spacePrefix => "spacePrefixedList"
-
-def fromIonName? : String → Option SepFormat
-  | "seq" => some .none
-  | "commaSepList" => some .comma
-  | "spaceSepList" => some .space
-  | "spacePrefixedList" => some .spacePrefix
+  | .newline => "newlineSepBy"
+
+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/BuiltinDialects/Init.lean

@@ -20,6 +20,7 @@ def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.
 def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] }
 def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] }
 def SyntaxCat.mkSpacePrefixSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixSepBy, args := #[c] }
+def SyntaxCat.mkNewlineSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.NewlineSepBy, args := #[c] }
 
 def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident
@@ -56,6 +57,8 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
 
   declareCat q`Init.SpacePrefixSepBy #["a"]
 
+  declareCat q`Init.NewlineSepBy #["a"]
+
   let QualifiedIdent := q`Init.QualifiedIdent
   declareCat QualifiedIdent
   declareOp {

Strata/DDM/Elab.lean

@@ -71,6 +71,11 @@ private partial def runCommand (leanEnv : Lean.Environment) (commands : Array Op
     return commands
   let (some tree, true) ← runChecked <| elabCommand leanEnv
     | return commands
+  -- Prevent infinite loop if parser makes no progress
+  let newPos := (←get).pos
+  if newPos <= iniPos then
+    logError { start := iniPos, stop := iniPos } "Syntax error: unrecognized syntax or unexpected token"
+    return commands
   let cmd := tree.info.asOp!.op
   let dialects := (← read).loader.dialects
   modify fun s => { s with

Strata/DDM/Elab/Core.lean

@@ -1209,6 +1209,8 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
     elabSeqWith c .space "spaceSepBy" (·.getSepArgs)
   | q`Init.SpacePrefixSepBy =>
     elabSeqWith c .spacePrefix "spacePrefixSepBy" (·.getArgs)
+  | q`Init.NewlineSepBy =>
+    elabSeqWith c .newline "newlineSepBy" (·.getArgs)
   | _ =>
     assert! c.args.isEmpty
     elabOperation

Strata/DDM/Format.lean

@@ -408,6 +408,13 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
   | .spacePrefix =>
     .atom <$> entries.foldlM (init := .nil) fun p a =>
       return (p ++ " " ++ (← a.mformatM).format)
+  | .newline =>
+    if z : entries.size = 0 then
+      pure (.atom .nil)
+    else do
+      let f i q s := return s ++ "\n" ++ (← entries[i].mformatM).format
+      let a := (← entries[0].mformatM).format
+      .atom <$> entries.size.foldlM f (start := 1) a
 
 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
@@ -43,7 +44,9 @@ def javaReservedWords : Std.HashSet String := Std.HashSet.ofList [
   -- Literals (cannot be used as identifiers)
   "true", "false", "null",
   -- Underscore (Java 9+)
-  "_"
+  "_",
+  -- Common java.lang classes that would cause ambiguity
+  "String", "Object", "Integer", "Boolean", "Long", "Double", "Float", "Character", "Byte", "Short"
 ]
 
 def escapeJavaName (name : String) : String :=
@@ -118,27 +121,32 @@ partial def syntaxCatToJavaType (cat : SyntaxCat) : JavaType :=
   else if abstractCategories.contains cat.name then
     .simple (abstractJavaName cat.name)
   else match cat.name with
-  | ⟨"Init", "Option"⟩ =>
+  | q`Init.Option =>
     match cat.args[0]? with
     | some inner => .optional (syntaxCatToJavaType inner)
     | none => panic! "Init.Option requires a type argument"
-  | ⟨"Init", "Seq"⟩ | ⟨"Init", "CommaSepBy"⟩ =>
+  | q`Init.Seq | q`Init.CommaSepBy | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy =>
     match cat.args[0]? with
     | some inner => .list (syntaxCatToJavaType inner)
-    | none => panic! "Init.Seq/CommaSepBy requires a type argument"
+    | none => panic! "List category requires a type argument"
   | ⟨"Init", _⟩ => panic! s!"Unknown Init category: {cat.name.name}"
   | ⟨_, name⟩ => .simple (escapeJavaName (toPascalCase name))
 
 def argDeclKindToJavaType : ArgDeclKind → JavaType
   | .type _ => .simple "Expr"
   | .cat c => syntaxCatToJavaType c
 
+/-- Get Ion separator name for a list category, or none if not a list. -/
+def getSeparator (c : SyntaxCat) : Option String :=
+  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 :=
   if primitiveCategories.contains cat.name then none
   else if abstractCategories.contains cat.name then some cat.name
   else match cat.name with
-  | ⟨"Init", "Option"⟩ | ⟨"Init", "Seq"⟩ | ⟨"Init", "CommaSepBy"⟩ =>
+  | q`Init.Option | q`Init.Seq | q`Init.CommaSepBy
+  | q`Init.NewlineSepBy | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy =>
     cat.args[0]?.bind syntaxCatToQualifiedName
   | ⟨"Init", _⟩ => none
   | qid => some qid
@@ -179,8 +187,7 @@ structure NameAssignments where
 /-! ## Code Generation -/
 
 def argDeclToJavaField (decl : ArgDecl) : JavaField :=
-  { name := escapeJavaName decl.ident
-    type := argDeclKindToJavaType decl.kind }
+  { name := escapeJavaName decl.ident, type := argDeclKindToJavaType decl.kind }
 
 def JavaField.toParam (f : JavaField) : String :=
   s!"{f.type.toJava} {f.name}"
@@ -226,8 +233,9 @@ def generateNodeInterface (package : String) (categories : List String) : String
 def generateStubInterface (package : String) (name : String) : String × String :=
   (s!"{name}.java", s!"package {package};\n\npublic non-sealed interface {name} extends Node \{}\n")
 
-def generateSerializer (package : String) : String :=
+def generateSerializer (package : String) (separatorMap : String) : String :=
   serializerTemplate.replace templatePackage package
+    |>.replace "/*SEPARATOR_MAP*/" separatorMap
 
 /-- Assign unique Java names to all generated types -/
 def assignAllNames (d : Dialect) : NameAssignments :=
@@ -241,7 +249,7 @@ def assignAllNames (d : Dialect) : NameAssignments :=
       let cats := if cats.contains op.category then cats else cats.push op.category
       let refs := op.argDecls.toArray.foldl (init := refs) fun refs arg =>
         match arg.kind with
-        | .type _ => refs.insert ⟨"Init", "Expr"⟩
+        | .type _ => refs.insert q`Init.Expr
         | .cat c => match syntaxCatToQualifiedName c with
           | some qid => refs.insert qid
           | none => refs
@@ -308,17 +316,37 @@ def opDeclToJavaRecord (dialectName : String) (names : NameAssignments) (op : Op
     fields := op.argDecls.toArray.map argDeclToJavaField }
 
 def generateBuilders (package : String) (dialectName : String) (d : Dialect) (names : NameAssignments) : String :=
-  let method (op : OpDecl) :=
-    let fields := op.argDecls.toArray.map argDeclToJavaField
-    let (ps, as) := fields.foldl (init := (#[], #[])) fun (ps, as) f =>
-      match f.type with
-      | .simple "java.math.BigInteger" _ => (ps.push s!"long {f.name}", as.push s!"java.math.BigInteger.valueOf({f.name})")
-      | .simple "java.math.BigDecimal" _ => (ps.push s!"double {f.name}", as.push s!"java.math.BigDecimal.valueOf({f.name})")
-      | t => (ps.push s!"{t.toJava} {f.name}", as.push f.name)
+  let methods (op : OpDecl) :=
+    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
-    s!"    public static {names.categories[op.category]!} {methodName}({", ".intercalate ps.toList}) \{ return new {names.operators[(op.category, op.name)]!}(SourceRange.NONE{if as.isEmpty then "" else ", " ++ ", ".intercalate as.toList}); }"
-  let methods := d.declarations.filterMap fun | .op op => some (method op) | _ => none
-  s!"package {package};\n\npublic class {dialectName} \{\n{"\n".intercalate methods.toList}\n}\n"
+    let returnType := names.categories[op.category]!
+    let recordName := names.operators[(op.category, op.name)]!
+    let checksStr := if checks.isEmpty then "" else " ".intercalate checks.toList ++ " "
+    let argsStr := if as.isEmpty then "" else ", " ++ ", ".intercalate as.toList
+    let paramsStr := ", ".intercalate ps.toList
+    -- Overload with SourceRange parameter
+    let srParams := if ps.isEmpty then "SourceRange sourceRange" else s!"SourceRange sourceRange, {paramsStr}"
+    let withSR := s!"    public static {returnType} {methodName}({srParams}) \{ {checksStr}return new {recordName}(sourceRange{argsStr}); }"
+    -- Convenience overload without SourceRange
+    let withoutSR := s!"    public static {returnType} {methodName}({paramsStr}) \{ {checksStr}return new {recordName}(SourceRange.NONE{argsStr}); }"
+    s!"{withSR}\n{withoutSR}"
+  let allMethods := d.declarations.filterMap fun | .op op => some (methods op) | _ => none
+  s!"package {package};\n\npublic class {dialectName} \{\n{"\n\n".intercalate allMethods.toList}\n}\n"
 
 public def generateDialect (d : Dialect) (package : String) : Except String GeneratedFiles := do
   let names := assignAllNames d
@@ -354,13 +382,32 @@ public def generateDialect (d : Dialect) (package : String) : Except String Gene
         sealedInterfaces ++ stubInterfaces
         |>.map (·.1.dropEnd 5 |>.toString)
 
+  -- Generate separator map for list fields
+  let separatorEntries := d.declarations.toList.filterMap fun decl =>
+    match decl with
+    | .op op =>
+      let opName := s!"{d.name}.{op.name}"
+      let fieldEntries := op.argDecls.toArray.toList.filterMap fun arg =>
+        match arg.kind with
+        | .cat c => match getSeparator c with
+          | some sep => some s!"\"{escapeJavaName arg.ident}\", \"{sep}\""
+          | none => none
+        | _ => none
+      if fieldEntries.isEmpty then none
+      else
+        let inner := fieldEntries.map fun e => s!"java.util.Map.entry({e})"
+        some s!"        java.util.Map.entry(\"{opName}\", java.util.Map.ofEntries({", ".intercalate inner}))"
+    | _ => none
+  let separatorMap := if separatorEntries.isEmpty then "java.util.Map.of()"
+    else s!"java.util.Map.ofEntries(\n{",\n".intercalate separatorEntries})"
+
   return {
     sourceRange := generateSourceRange package
     node := generateNodeInterface package allInterfaceNames
     interfaces := sealedInterfaces.toArray ++ stubInterfaces.toArray
     records := records.toArray
     builders := (s!"{names.builders}.java", generateBuilders package names.builders d names)
-    serializer := generateSerializer package
+    serializer := generateSerializer package separatorMap
   }
 
 /-! ## File Output -/

Strata/DDM/Integration/Java/templates/IonSerializer.java

@@ -6,6 +6,8 @@
 public class IonSerializer {
     private final IonSystem ion;
 
+    private static final java.util.Map<String, java.util.Map<String, String>> SEPARATORS = /*SEPARATOR_MAP*/;
+
     public IonSerializer(IonSystem ion) {
         this.ion = ion;
     }
@@ -22,14 +24,17 @@ public IonValue serialize(Node node) {
 
     private IonSexp serializeNode(Node node) {
         IonSexp sexp = ion.newEmptySexp();
-        sexp.add(ion.newSymbol(node.operationName()));
+        String opName = node.operationName();
+        sexp.add(ion.newSymbol(opName));
         sexp.add(serializeSourceRange(node.sourceRange()));
 
+        var fieldSeps = SEPARATORS.getOrDefault(opName, java.util.Map.of());
         for (var component : node.getClass().getRecordComponents()) {
             if (component.getName().equals("sourceRange")) continue;
             try {
                 java.lang.Object value = component.getAccessor().invoke(node);
-                sexp.add(serializeArg(value, component.getType(), component.getGenericType()));
+                String sep = fieldSeps.get(component.getName());
+                sexp.add(serializeArg(value, sep, component.getType()));
             } catch (java.lang.Exception e) {
                 throw new java.lang.RuntimeException("Failed to serialize " + component.getName(), e);
             }
@@ -54,7 +59,7 @@ private IonValue serializeSourceRange(SourceRange sr) {
         return sexp;
     }
 
-    private IonValue serializeArg(java.lang.Object value, java.lang.Class<?> type, java.lang.reflect.Type genericType) {
+    private IonValue serializeArg(java.lang.Object value, String sep, java.lang.Class<?> type) {
         if (value == null) {
             return serializeOption(java.util.Optional.empty());
         }
@@ -80,7 +85,7 @@ private IonValue serializeArg(java.lang.Object value, java.lang.Class<?> type, j
             return serializeOption(opt);
         }
         if (value instanceof java.util.List<?> list) {
-            return serializeSeq(list, genericType);
+            return serializeSeq(list, sep != null ? sep : "seq");
         }
         throw new java.lang.IllegalArgumentException("Unsupported type: " + type);
     }
@@ -129,17 +134,17 @@ private IonValue serializeOption(java.util.Optional<?> opt) {
         sexp.add(ion.newSymbol("option"));
         sexp.add(ion.newNull());
         if (opt.isPresent()) {
-            sexp.add(serializeArg(opt.get(), opt.get().getClass(), opt.get().getClass()));
+            sexp.add(serializeArg(opt.get(), null, opt.get().getClass()));
         }
         return sexp;
     }
 
-    private IonValue serializeSeq(java.util.List<?> list, java.lang.reflect.Type genericType) {
+    private IonValue serializeSeq(java.util.List<?> list, String sepType) {
         IonSexp sexp = ion.newEmptySexp();
-        sexp.add(ion.newSymbol("seq"));
+        sexp.add(ion.newSymbol(sepType));
         sexp.add(ion.newNull());
         for (java.lang.Object item : list) {
-            sexp.add(serializeArg(item, item.getClass(), item.getClass()));
+            sexp.add(serializeArg(item, null, item.getClass()));
         }
         return sexp;
     }

Strata/DDM/Integration/Lean/Gen.lean

@@ -703,6 +703,9 @@ partial def genCatTypeTerm (annType : Ident) (c : SyntaxCat)
   | q`Init.SpacePrefixSepBy, 1 =>
     let inner := mkCApp ``Array #[args[0]]
     return if addAnn then mkCApp ``Ann #[inner, annType] else inner
+  | q`Init.NewlineSepBy, 1 =>
+    let inner := mkCApp ``Array #[args[0]]
+    return if addAnn then mkCApp ``Ann #[inner, annType] else inner
   | q`Init.Option, 1 =>
     let inner := mkCApp ``Option #[args[0]]
     return if addAnn then mkCApp ``Ann #[inner, annType] else inner
@@ -910,6 +913,8 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat)
     toAstApplyArgSeq v cat ``SepFormat.space
   | q`Init.SpacePrefixSepBy => do
     toAstApplyArgSeq v cat ``SepFormat.spacePrefix
+  | q`Init.NewlineSepBy => do
+    toAstApplyArgSeq v cat ``SepFormat.newline
   | q`Init.Seq => do
     toAstApplyArgSeq v cat ``SepFormat.none
   | q`Init.Option => do
@@ -1170,6 +1175,8 @@ partial def genOfAstArgTerm (varName : String) (cat : SyntaxCat)
     genOfAstSeqArgTerm varName cat e ``SepFormat.space
   | q`Init.SpacePrefixSepBy => do
     genOfAstSeqArgTerm varName cat e ``SepFormat.spacePrefix
+  | q`Init.NewlineSepBy => do
+    genOfAstSeqArgTerm varName cat e ``SepFormat.newline
   | q`Init.Seq => do
     genOfAstSeqArgTerm varName cat e ``SepFormat.none
   | q`Init.Option => do
@@ -1485,6 +1492,7 @@ def tryMakeInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor)
         | q`Init.CommaSepBy => true
         | q`Init.SpaceSepBy => true
         | q`Init.SpacePrefixSepBy => true
+        | q`Init.NewlineSepBy => true
         | q`Init.Option => true
         | c => c ∈ inhabited
     if !argsInhabited then

Strata/DDM/Integration/Lean/ToExpr.lean

@@ -40,6 +40,7 @@ instance : ToExpr SepFormat where
     | .comma => mkConst ``SepFormat.comma
     | .space => mkConst ``SepFormat.space
     | .spacePrefix => mkConst ``SepFormat.spacePrefix
+    | .newline => mkConst ``SepFormat.newline
 
 end SepFormat