feat(core): Add Sequence.empty<T>() syntax for creating empty sequences

[atomb]

Enable parsing Sequence.empty from .st files by adding a DDM fn declaration with an explicit type parameter. Previously, the 0-ary polymorphic function could not be parsed because the DDM grammar had no value arguments to infer the type parameter from.

Users now write Sequence.empty() instead of the workaround of declaring a variable and assuming its length is zero.

• Grammar.lean: Add fn seq_empty with explicit Type argument
• Translate.lean: Add translation case for seq_empty
• FormatCore.lean: Format Sequence.empty back to () syntax
• Factory.lean: Update seqEmptyFunc comment (now parseable)
• Seq.lean: Add verification tests for the new syntax

Addresses but does not completely resolve #1027

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

[tautschnig]

See comment above.

[tautschnig]

Nice, focused fix that lifts a real user-facing restriction on Sequence.empty. The happy path is well exercised via the #eval verify test (parse → translate → format → typecheck → VC → SMT).

Before approving I'd like to see:

• Tighter behavior in handleZeroaryOps for the .seq .Empty fallback (see inline).
• Slightly decoupled pattern match using the existing seqTy match_pattern helper.
• Broader test coverage: non-int element types (bool, string), nested sequences, and Sequence.empty<Map _ _>(). I verified manually that all three work with the current code, but the regressions would slip past CI with only the current int test.
• A few tiny doc / commit-message nits (commit says "Resolves #1027", PR body / issue scope say it only addresses half of it).
• Some proof / #guard coverage of the translation shape (see inline on Translate.lean).

Refactoring notes:

• handleZeroaryOps is now asymmetric — only one of four cases consumes opTy. If we ever gain another 0-ary polymorphic op, growing this match further will get ugly. Worth a small helper that normalizes opTy → element type where relevant.
• The silent CoreType.tvar default unknownTypeVar fallback mirrors the other unknown-type paths in this file, but elsewhere those paths call ToCSTM.logError. Sticking to that convention here would help catch well-typed-but-malformed inputs.

[tautschnig]

Would you consider adding a small #guard-style test (in StrataTest/Languages/Core/Tests/ — CoreOpTests.lean or a new TranslateTests.lean) that exercises the expected structural shape of this translation for a couple of element types? Something along the lines of:

/-- The translation of `Sequence.empty<T>()` produces a `.seq .Empty` operator
    annotated with `Sequence T`. -/
#guard
  match translateExpr (mkTestPgm "Sequence.empty<int>()") with
  | .ok (.op _ name (.some ty)) =>
    name.name == "Sequence.empty" && ty == Core.seqTy .int
  | _ => false

The #eval verify test in Seq.lean exercises this path end-to-end, but a direct structural test would catch regressions (missing seqTy wrapper, wrong kind tag, etc.) without relying on an SMT call.

For an actual theorem, the nice property to prove is the round-trip with FormatCore: for any T in the Core grammar, format ∘ translate on Sequence.empty<T>() is the identity (up to formatting whitespace). That would tie the three pieces of this PR together.

[tautschnig]

Test coverage is narrow — only Sequence.empty<int>(). I verified manually that each of the following also works end-to-end with the PR as-is, so please extend the test to include them (otherwise we have no regression protection for these cases):

1. Non-int primitive element: Sequence.empty<bool>()
2. Nested sequences: Sequence.empty<Sequence int>()
3. Compound element type: Sequence.empty<Map int bool>()

Example follow-up test (feel free to consolidate into one procedure):

Suggested change

	-/
	#eval verify seqEmptyPgm
	----------------------------------------------------------------------
	-- Exercise various element types for Sequence.empty<T>().
	private def seqEmptyTypesPgm :=
	#strata
	program Core;
	procedure SeqEmptyTypes()
	{
	var sb : Sequence bool;
	var sss : Sequence (Sequence int);
	var smi : Sequence (Map int bool);
	sb := Sequence.empty<bool>();
	sss := Sequence.empty<Sequence int>();
	smi := Sequence.empty<Map int bool>();
	assert [bool_len]: Sequence.length(sb) == 0;
	assert [seq_seq_len]: Sequence.length(sss) == 0;
	assert [seq_map_len]: Sequence.length(smi) == 0;
	};
	#end
	/-- info: true -/
	#guard_msgs in
	#eval TransM.run Inhabited.default (translateProgram seqEmptyTypesPgm) |>.snd |>.isEmpty

Also worth adding: a negative test showing that Sequence.empty() (no type argument) is rejected at parse time, so we can't silently regress to the old polymorphism-inference behavior if the grammar rule is ever weakened.

Related proof suggestion for SeqModel.lean: you already prove length_empty : ([] : List α).length = 0. It would be nice to extend the axiom-model block with a short lemma tying Sequence.build(Sequence.empty, v) to [v], matching the build_on_empty_* obligations this PR's test introduces.

[tautschnig]

Note that the PR-description / commit-message wording is inconsistent with the actual scope: the commit message on 271fb5d68 says "Resolves #1027", but the PR body correctly says "Addresses but does not completely resolve #1027" (the Map part of the issue is not touched). Would you mind amending the commit message to match, so that squash-merging the PR doesn't auto-close #1027?

[atomb]

Doesn't squash-merging use the PR description as the commit message? I don't think it includes messages from the intermediate commits on the branch.

[MikaelMayer]

We need also the roundtrip of pretty-printing it that way

[MikaelMayer]

This PR's functionality is also implemented in #1100 but could be merged before.

[MikaelMayer]

Everything unique in this PR was imported into #1100 which was just merged