Fix #1146: require command_datatypes to be non-empty (#1155)

The Core grammar declared command_datatypes as

op command_datatypes (datatypes : NewlineSepBy DatatypeDecl) : Command
=>
    datatypes ";\\n";

Without @[nonempty] on the field, NewlineSepBy compiles to a
zero-or-more parser, so the trailing ";\\n" production alone matched any
stray ";" in the input. This is particularly easy to trip accidentally:
command_fndef's surface syntax has no trailing semicolon, so a user
writing "};" at the end of a function body (by analogy with procedures,
whose grammar does end in ";") silently produced a phantom
command_datatypes op with zero datatypes.

The phantom later tripped an explicit assertion in translateDatatypes:

  "Datatype block must contain at least one datatype"

which calls panic!, producing a large backtrace at gen_smt_vcs time with
no useful source location.

Mark the datatypes field @[nonempty]. The stray ";" now surfaces as a
parse error at the point it actually appears, and the original repro
elaborates cleanly.

Add a regression test
(StrataTest/Languages/Core/Tests/Issue1146Test.lean) that pins the
canonical form: a program mixing a datatype and a function can run
through gen_smt_vcs without panicking.

Fixes: #1146

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>

Author: 3 people

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -461,8 +461,11 @@ op datatype_decl (name : Ident,
 
 // Unified datatype command: one or more datatype declarations separated by
 // newlines, ending with a semicolon.
+//
+// `@[nonempty]` is load-bearing: see
+// https://github.com/strata-org/Strata/issues/1146.
 @[scope(datatypes), preRegisterTypes(datatypes)]
-op command_datatypes (datatypes : NewlineSepBy DatatypeDecl) : Command =>
+op command_datatypes (@[nonempty] datatypes : NewlineSepBy DatatypeDecl) : Command =>
   datatypes ";\n";
 
 #end

StrataTest/Languages/Core/Tests/Issue1146Test.lean

@@ -0,0 +1,56 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Core.DDMTransform.Translate
+
+/-!
+# Regression test for https://github.com/strata-org/Strata/issues/1146
+
+A trailing `;` after a `function` body must not be silently accepted as an
+empty `command_datatypes` block (which would later panic in
+`translateDatatypes`), and a program mixing a datatype and a function must
+translate cleanly.
+-/
+
+namespace Strata.Issue1146Test
+
+/-! ## Canonical form: datatype + function translates without error -/
+
+private def datatypeAndFunction : Strata.Program :=
+#strata
+program Core;
+
+datatype List () { Nil() };
+
+function Len (xs : List) : int
+{
+  0
+}
+#end
+
+/-- info: true -/
+#guard_msgs in
+#eval TransM.run Inhabited.default (translateProgram datatypeAndFunction) |>.snd |>.isEmpty
+
+/-! ## Stray trailing `;` after a function body is a parse error -/
+
+/--
+error: unexpected token ';'; expected 'function', Core.Block or expected at least one element
+-/
+#guard_msgs in
+def strayTrailingSemi : Strata.Program :=
+#strata
+program Core;
+
+datatype List () { Nil() };
+
+function Len (xs : List) : int
+{
+  0
+};
+#end
+
+end Strata.Issue1146Test