Laurel Language Enhancements

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,18 +198,21 @@ def toString : SepFormat → String
   | .comma => "commaSepBy"
   | .space => "spaceSepBy"
   | .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
   | _ => none
 
 theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :

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

@@ -1208,6 +1208,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

@@ -318,7 +318,7 @@ private def SyntaxDefAtom.formatArgs (opts : FormatOptions) (args : Array PrecFo
   match stx with
   | .ident lvl prec _ =>
     let ⟨r, innerPrec⟩ := args[lvl]!
-    if prec > 0 ∧ (innerPrec ≤ prec ∨ opts.alwaysParen) then
+    if prec > 0 ∧ (innerPrec < prec ∨ opts.alwaysParen) then
       f!"({r})"
     else
       r
@@ -399,6 +399,9 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
   | .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

@@ -118,27 +118,38 @@ 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 :=
+  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
+
 /-- 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 +190,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 +236,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 +252,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 +319,30 @@ 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 methods (op : OpDecl) :=
     let fields := op.argDecls.toArray.map argDeclToJavaField
-    let (ps, as) := fields.foldl (init := (#[], #[])) fun (ps, as) f =>
+    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})")
-      | .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)
+      | .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 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 +378,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

@@ -666,6 +666,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
@@ -869,6 +872,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
@@ -1101,6 +1106,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
@@ -1396,6 +1403,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
 

Strata/DDM/Parser.lean

@@ -228,16 +228,19 @@ private partial def whitespace : ParserFn := fun c s =>
       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 _ => s
+        | 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 _ => s
+        | some tk => if tk.startsWith "/*" then s
+          else andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j))
         | none =>
-          let j := c.next j
-          andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c j)
+          andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c (c.next j))
       | _ =>
         s
     else s
@@ -897,7 +900,7 @@ partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metad
     assert! cat.args.size = 1
     let isNonempty := q`StrataDDL.nonempty ∈ metadata
     commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]!
-  | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.Seq =>
+  | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.NewlineSepBy | q`Init.Seq =>
     assert! cat.args.size = 1
     let isNonempty := q`StrataDDL.nonempty ∈ metadata
     (if isNonempty then many1Parser else manyParser) <$> catParser ctx cat.args[0]!

Strata/DL/Lambda/LExprEval.lean

@@ -181,7 +181,7 @@ def eval (n : Nat) (σ : LState TBase) (e : (LExpr TBase.mono))
             -- At least one argument in the function call is symbolic.
             new_e
       | none =>
-        -- Not a call of a factory function.
+        -- Not a call of a factory function - go through evalCore
         evalCore n' σ e
 
 def evalCore  (n' : Nat) (σ : LState TBase) (e : LExpr TBase.mono) : LExpr TBase.mono :=