Add SpaceSepBy and SpacePrefixSepBy constructs + nonempty attribute

Strata/DDM/AST.lean

@@ -141,6 +141,44 @@ termination_by d
 
 end TypeExprF
 
+/-- Separator format for sequence formatting -/
+inductive SepFormat where
+| none           -- No separator (original Seq)
+| comma          -- Comma separator (CommaSepBy)
+| space          -- Space separator (SpaceSepBy)
+| spacePrefix    -- Space before each element (SpacePrefixSepBy)
+deriving Inhabited, Repr, BEq
+
+namespace SepFormat
+
+def toString : SepFormat → String
+  | .none => "seq"
+  | .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
+  | _ => none
+
+theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :
+  fromIonName? (toIonName sep) = some sep := by
+  cases sep <;> rfl
+
+instance : ToString SepFormat where
+  toString := SepFormat.toString
+
+end SepFormat
+
 mutual
 
 inductive ExprF (α : Type) : Type where
@@ -167,8 +205,7 @@ inductive ArgF (α : Type) : Type where
 | strlit (ann : α) (i : String)
 | bytes (ann : α) (a : ByteArray)
 | option (ann : α) (l : Option (ArgF α))
-| seq (ann : α) (l : Array (ArgF α))
-| commaSepList (ann : α) (l : Array (ArgF α))
+| seq (ann : α) (sep : SepFormat) (l : Array (ArgF α))
 deriving Inhabited, Repr
 
 end
@@ -192,8 +229,7 @@ def ArgF.ann {α : Type} : ArgF α → α
 | .bytes ann _ => ann
 | .strlit ann _ => ann
 | .option ann _ => ann
-| .seq ann _ => ann
-| .commaSepList ann _ => ann
+| .seq ann _ _ => ann
 
 end
 
@@ -289,10 +325,8 @@ private def ArgF.beq {α} [BEq α] (a1 a2 : ArgF α) : Bool :=
     | .none, .none => true
     | .some v1, .some v2 => ArgF.beq v1 v2
     | _, _ => false
-  | .seq a1 v1, .seq a2 v2 =>
-    a1 == a2 && ArgF.array_beq v1 v2
-  | .commaSepList a1 v1, .commaSepList a2 v2 =>
-    a1 == a2 && ArgF.array_beq v1 v2
+  | .seq a1 sep1 v1, .seq a2 sep2 v2 =>
+    a1 == a2 && sep1 == sep2 && ArgF.array_beq v1 v2
   | _, _ => false
 termination_by sizeOf a1
 
@@ -1549,8 +1583,7 @@ partial def foldOverArgBindingSpecs {α β}
   | .expr _ | .type _ | .cat _ | .ident .. | .num .. | .decimal .. | .bytes .. | .strlit .. => init
   | .option _ none => init
   | .option _ (some a) => foldOverArgBindingSpecs m f init a
-  | .seq _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
-  | .commaSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
+  | .seq _ _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
 
 /--
 Invoke a function `f` over each of the declaration specifications for an operator.

Strata/DDM/BuiltinDialects/Init.lean

@@ -18,6 +18,8 @@ namespace Strata
 def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Option, args := #[c] }
 def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] }
 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 initDialect : Dialect := BuiltinM.create! "Init" #[] do
   let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident
@@ -50,6 +52,10 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
 
   declareCat q`Init.CommaSepBy #["a"]
 
+  declareCat q`Init.SpaceSepBy #["a"]
+
+  declareCat q`Init.SpacePrefixSepBy #["a"]
+
   let QualifiedIdent := q`Init.QualifiedIdent
   declareCat QualifiedIdent
   declareOp {

Strata/DDM/BuiltinDialects/StrataDDL.lean

@@ -156,6 +156,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
 
   declareMetadata { name := "scope", args := #[.mk "scope" .ident] }
   declareMetadata { name := "unwrap", args := #[] }
+  declareMetadata { name := "nonempty", args := #[] }
   -- Metadata for marking an operation as a constructor definition
   declareMetadata { name := "constructor", args := #[.mk "name" .ident, .mk "fields" .ident] }
   -- Metadata for marking an operation as a constructor list atom (single constructor)

Strata/DDM/Elab/Core.lean

@@ -1165,28 +1165,28 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
     let a := c.args[0]!
     elabOption (catElaborator a)
   |  q`Init.Seq =>
-    assert! c.args.size = 1
-    let a := c.args[0]!
-    let f := elabManyElement (catElaborator a)
-    fun tctx stx => do
-      let some loc := mkSourceRange? stx
-        | panic! "seq missing source location"
-      let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx)
-      let info : SeqInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
-      pure <| .node (.ofSeqInfo info) args
+    elabSeqWith c .none "seq" (·.getArgs)
   | q`Init.CommaSepBy =>
+    elabSeqWith c .comma "commaSepBy" (·.getSepArgs)
+  | q`Init.SpaceSepBy =>
+    elabSeqWith c .space "spaceSepBy" (·.getSepArgs)
+  | q`Init.SpacePrefixSepBy =>
+    elabSeqWith c .spacePrefix "spacePrefixSepBy" (·.getArgs)
+  | _ =>
+    assert! c.args.isEmpty
+    elabOperation
+
+where
+  elabSeqWith (c : SyntaxCat) (sep : SepFormat) (name : String) (getArgsFrom : Syntax → Array Syntax) : TypingContext → Syntax → ElabM Tree :=
     assert! c.args.size = 1
     let a := c.args[0]!
     let f := elabManyElement (catElaborator a)
     fun tctx stx => do
       let some loc := mkSourceRange? stx
-        | panic! s!"commaSepBy missing source location {repr stx}"
-      let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx)
-      let info : CommaSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
-      pure <| .node (.ofCommaSepInfo info) args
-  | _ =>
-    assert! c.args.isEmpty
-    elabOperation
+        | panic! s!"{name} missing source location {repr stx}"
+      let (args, resultCtx) ← (getArgsFrom stx).foldlM f (#[], tctx)
+      let info : SeqInfo := { inputCtx := tctx, loc := loc, sep := sep, args := args.map (·.arg), resultCtx }
+      pure <| .node (.ofSeqInfo info) args
 
 partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
   match stx.getKind with

Strata/DDM/Elab/Tree.lean

@@ -246,11 +246,7 @@ structure OptionInfo extends ElabInfo where
   deriving Inhabited, Repr
 
 structure SeqInfo extends ElabInfo where
-  args : Array Arg
-  resultCtx : TypingContext
-deriving Inhabited, Repr
-
-structure CommaSepInfo extends ElabInfo where
+  sep : SepFormat
   args : Array Arg
   resultCtx : TypingContext
 deriving Inhabited, Repr
@@ -267,7 +263,6 @@ inductive Info
 | ofBytesInfo (info : ConstInfo ByteArray)
 | ofOptionInfo (info : OptionInfo)
 | ofSeqInfo (info : SeqInfo)
-| ofCommaSepInfo (info : CommaSepInfo)
 deriving Inhabited, Repr
 
 namespace Info
@@ -301,7 +296,6 @@ def elabInfo (info : Info) : ElabInfo :=
   | .ofBytesInfo info => info.toElabInfo
   | .ofOptionInfo info => info.toElabInfo
   | .ofSeqInfo info => info.toElabInfo
-  | .ofCommaSepInfo info => info.toElabInfo
 
 def inputCtx (info : Info) : TypingContext := info.elabInfo.inputCtx
 
@@ -347,8 +341,7 @@ def arg : Tree → Arg
       | #[x] => some x.arg
       | _ => panic! "Unexpected option"
     .option info.loc r
-  | .ofSeqInfo info => .seq info.loc info.args
-  | .ofCommaSepInfo info => .commaSepList info.loc info.args
+  | .ofSeqInfo info => .seq info.loc info.sep info.args
 
 theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by
   match t with
@@ -370,7 +363,6 @@ def resultContext (t : Tree) : TypingContext :=
     else
       info.inputCtx
   | .ofSeqInfo info => info.resultCtx
-  | .ofCommaSepInfo info => info.resultCtx
 termination_by t
 
 def isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool :=
@@ -384,14 +376,20 @@ def asOption? (t : Tree) : Option (Option Tree) :=
   | _ => none
 
 def asCommaSepInfo? (t : Tree) : Option (Array Tree) :=
-  if let .ofCommaSepInfo _ := t.info then
-    some t.children
+  if let .ofSeqInfo info := t.info then
+    if info.sep == .comma then
+      some t.children
+    else
+      none
   else
     none
 
 def asCommaSepInfo! (t : Tree) : Array Tree :=
-  if let .ofCommaSepInfo _ := t.info then
-    t.children
+  if let .ofSeqInfo info := t.info then
+    if info.sep == .comma then
+      t.children
+    else
+      panic! "Expected commaSepInfo"
   else
     panic! "Expected commaSepInfo"
 

Strata/DDM/Format.lean

@@ -378,16 +378,28 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
   match ma with
   | none => pure (.atom .nil)
   | some a => a.mformatM
-| .seq _ entries => do
-  .atom <$> entries.foldlM (init := .nil) fun p a =>
-    return (p ++ (← a.mformatM).format)
-| .commaSepList _ entries => do
-  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
+| .seq _ sep entries => do
+  match sep with
+  | .none =>
+    .atom <$> entries.foldlM (init := .nil) fun p a =>
+      return (p ++ (← a.mformatM).format)
+  | .comma =>
+    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
+  | .spacePrefix =>
+    .atom <$> entries.foldlM (init := .nil) fun p a =>
+      return (p ++ " " ++ (← a.mformatM).format)
 
 private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat :=
   if rargs.isEmpty then