Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
atomb wants to merge 4 commits into from
Closed

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
271fb5d
feat(core): Add Sequence.empty<T>() syntax for creating empty sequences
atomb Apr 23, 2026
bdba95d
Merge branch 'main' into atomb/fix-issue-1027
atomb May 6, 2026
b573bb6
Update editor syntax files
atomb May 6, 2026
f22f601
fix(core): Improve Sequence.empty type resolution in DDM transform
atomb May 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 13 additions & 3 deletions Strata/Languages/Core/DDMTransform/FormatCore.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -289,13 +289,22 @@ def lconstToExpr {M} [Inhabited M] (c : Lambda.LConst) :

/-- Handle 0-ary operations -/
def handleZeroaryOps {M} [Inhabited M] (name : String)
(opTy : Option Lambda.LMonoTy := none)
: ToCSTM M (CoreDDM.Expr M) :=
open Core in
match CoreOp.ofString name with
| .re .All => pure (.re_all default)
| .re .AllChar => pure (.re_allchar default)
| .re .None => pure (.re_none default)
-- TODO: seq_empty is not yet parseable (see Grammar.lean); handle here when added.
| .seq .Empty => do
match opTy with
Comment thread
atomb marked this conversation as resolved.
| some (Core.seqTy elemTy) =>
let ety ← lmonoTyToCoreType elemTy
pure (.seq_empty default ety)
| _ => do
ToCSTM.logError "handleZeroaryOps" "Sequence.empty missing or malformed op-type annotation" name
let ety := CoreType.tvar default unknownTypeVar
Comment thread
atomb marked this conversation as resolved.
pure (.seq_empty default ety)
| _ => do
ToCSTM.logError "lopToExpr" "0-ary op not found" name
pure (.re_none default)
Expand Down Expand Up @@ -497,6 +506,7 @@ def handleTernaryOps {M} [Inhabited M] (name : String)

def lopToExpr {M} [Inhabited M]
(name : String) (args : List (CoreDDM.Expr M))
(opTy : Option Lambda.LMonoTy := none)
: ToCSTM M (CoreDDM.Expr M) := do
let ctx ← get
-- User-defined functions: check bound vars first (local funcDecl via
Expand All @@ -513,7 +523,7 @@ def lopToExpr {M} [Inhabited M]
| none =>
-- Either a built-in or an invalid operation.
match args with
| [] => handleZeroaryOps name
| [] => handleZeroaryOps name opTy
| [arg] => handleUnaryOps name arg
| [arg1, arg2] => handleBinaryOps name arg1 arg2
| [arg1, arg2, arg3] => handleTernaryOps name arg1 arg2 arg3
Expand Down Expand Up @@ -551,7 +561,7 @@ partial def lexprToExpr {M} [Inhabited M]
pure (.fvar default (ctx.allFreeVars.size))
| .ite _ c t f => liteToExpr c t f qLevel
| .eq _ e1 e2 => leqToExpr e1 e2 qLevel
| .op _ name _ => lopToExpr name.name []
| .op _ name ty => lopToExpr name.name [] ty
| .app _ _ _ => lappToExpr e qLevel
| .abs _ prettyName ty body => labsToExpr prettyName ty body (qLevel + 1)
| .quant _ qkind _ ty trigger body =>
Expand Down
7 changes: 4 additions & 3 deletions Strata/Languages/Core/DDMTransform/Grammar.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,9 +103,10 @@ fn map_get (K : Type, V : Type, m : Map K V, k : K) : V => m "[" k "]";
fn map_set (K : Type, V : Type, m : Map K V, k : K, v : V) : Map K V =>
m "[" k ":=" v "]";

// TODO: seq_empty is not yet supported in the grammar because the DDM parser
// cannot currently handle 0-ary polymorphic functions (no arguments to infer
// the type parameter from). The Factory definition exists for programmatic use.
// Unlike other seq_* ops, seq_empty has no value arguments from which DDM can
// infer the element type, so the type argument must be explicit in surface syntax.
fn seq_empty (A : Type) : Sequence A =>

@MikaelMayer MikaelMayer May 15, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

"Sequence.empty" "<" A ">" "(" ")";
Comment thread
atomb marked this conversation as resolved.

@MikaelMayer MikaelMayer May 15, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

fn seq_length (A : Type, s : Sequence A) : int => "Sequence.length" "(" s ")";
fn seq_select (A : Type, s : Sequence A, i : int) : A => "Sequence.select" "(" s ", " i ")";
fn seq_append (A : Type, s1 : Sequence A, s2 : Sequence A) : Sequence A =>
Expand Down
8 changes: 7 additions & 1 deletion Strata/Languages/Core/DDMTransform/Translate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -848,6 +848,13 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
| .fn _ q`Core.re_all, [] =>
let fn ← translateFn .none q`Core.re_all
return fn
-- Sequence.empty (0-ary polymorphic, takes only a type argument)
| .fn _ q`Core.seq_empty, [_atp] =>
let ety ← translateLMonoTy bindings _atp
let fn : LExpr Core.CoreLParams.mono :=
Core.coreOpExpr (.seq .Empty)
(.some (Core.seqTy ety))

@tautschnig tautschnig May 6, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

return fn
-- Unary function applications
| .fn _ fni, [xa] =>
match fni with
Expand Down Expand Up @@ -913,7 +920,6 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
let x ← translateExpr p bindings xa
return .mkApp () fn [m, i, x]
-- Seq operations
-- TODO: seq_empty is not yet parseable (see Grammar.lean); handle here when added.
| .fn _ q`Core.seq_length, [_atp, sa] =>
let ety ← translateLMonoTy bindings _atp
let fn : LExpr Core.CoreLParams.mono :=
Expand Down
6 changes: 3 additions & 3 deletions Strata/Languages/Core/Factory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -432,9 +432,9 @@ def seqLengthFunc : WFLFunc CoreLParams :=
])

/- An empty `Sequence` constructor with type `∀a. Sequence a`.
NOTE: This is registered in the Factory for programmatic use, but is not yet
parseable from `.st` files because the DDM grammar cannot currently handle
0-ary polymorphic functions (no arguments to infer the type parameter from). -/
`Sequence.empty<A>()` returns an empty sequence of element type `A`.
The `<A>` is surface syntax produced by Grammar.lean and consumed by
Translate.lean; this function itself takes no value parameters. -/
def seqEmptyFunc : WFLFunc CoreLParams :=
polyUneval "Sequence.empty" ["a"] [] (seqTy mty[%a])
(axioms := [
Expand Down
166 changes: 166 additions & 0 deletions StrataTest/Languages/Core/Examples/Seq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -305,3 +305,169 @@ Result: ✅ pass
#eval verify seqOpsPgm

---------------------------------------------------------------------

@tautschnig tautschnig May 6, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 atomb May 7, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

----------------------------------------------------------------------
-- Tests for Sequence.empty<T>() syntax (issue #1027)
----------------------------------------------------------------------

private def seqEmptyPgm :=
#strata
program Core;

procedure SeqEmpty()
{
var s : Sequence int;

// Create an empty sequence using the new syntax
s := Sequence.empty<int>();
assert [empty_length]: Sequence.length(s) == 0;

// Build on top of an empty sequence
s := Sequence.build(Sequence.empty<int>(), 42);
assert [build_on_empty_length]: Sequence.length(s) == 1;
assert [build_on_empty_elem]: Sequence.select(s, 0) == 42;
};
#end

/-- info: true -/
#guard_msgs in
-- No errors in translation.
#eval TransM.run Inhabited.default (translateProgram seqEmptyPgm) |>.snd |>.isEmpty

/--
info: program Core;

procedure SeqEmpty ()
{
var s : (Sequence int);
s := Sequence.empty<int>();
assert [empty_length]: Sequence.length(s) == 0;
s := Sequence.build(Sequence.empty<int>(), 42);
assert [build_on_empty_length]: Sequence.length(s) == 1;
assert [build_on_empty_elem]: Sequence.select(s, 0) == 42;
};
-/
#guard_msgs in
#eval TransM.run Inhabited.default (translateProgram seqEmptyPgm) |>.fst

/--
info: [Strata.Core] Type checking succeeded.


VCs:
Label: empty_length
Property: assert
Obligation:
Sequence.length(Sequence.empty<int>()) == 0

Label: build_on_empty_length
Property: assert
Obligation:
Sequence.length(Sequence.build(Sequence.empty<int>(), 42)) == 1

Label: build_on_empty_elem
Property: assert
Obligation:
Sequence.select(Sequence.build(Sequence.empty<int>(), 42), 0) == 42

---
info:
Obligation: empty_length
Property: assert
Result: ✅ pass

Obligation: build_on_empty_length
Property: assert
Result: ✅ pass

Obligation: build_on_empty_elem
Property: assert
Result: ✅ pass
-/

@tautschnig tautschnig May 6, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

#guard_msgs in
#eval verify seqEmptyPgm

----------------------------------------------------------------------

-- Exercise various element types for Sequence.empty<T>().
private def seqEmptyTypesPgm :=
#strata
program Core;

procedure SeqEmptyTypes()
{
var sb : Sequence bool;
var ssi : Sequence (Sequence int);
var smi : Sequence (Map int bool);

sb := Sequence.empty<bool>();
ssi := Sequence.empty<Sequence int>();
smi := Sequence.empty<Map int bool>();

assert [bool_len]: Sequence.length(sb) == 0;
assert [seq_seq_len]: Sequence.length(ssi) == 0;
assert [seq_map_len]: Sequence.length(smi) == 0;
};
#end

/-- info: true -/
#guard_msgs in
#eval TransM.run Inhabited.default (translateProgram seqEmptyTypesPgm) |>.snd |>.isEmpty

/--
info: program Core;

procedure SeqEmptyTypes ()
{
var sb : (Sequence bool);
var ssi : (Sequence (Sequence int));
var smi : (Sequence (Map int bool));
sb := Sequence.empty<bool>();
ssi := Sequence.empty<Sequence int>();
smi := Sequence.empty<Map int bool>();
assert [bool_len]: Sequence.length(sb) == 0;
assert [seq_seq_len]: Sequence.length(ssi) == 0;
assert [seq_map_len]: Sequence.length(smi) == 0;
};
-/
#guard_msgs in
#eval TransM.run Inhabited.default (translateProgram seqEmptyTypesPgm) |>.fst

/--
info: [Strata.Core] Type checking succeeded.


VCs:
Label: bool_len
Property: assert
Obligation:
Sequence.length(Sequence.empty<bool>()) == 0

Label: seq_seq_len
Property: assert
Obligation:
Sequence.length(Sequence.empty<Sequence int>()) == 0

Label: seq_map_len
Property: assert
Obligation:
Sequence.length(Sequence.empty<Map int bool>()) == 0

---
info:
Obligation: bool_len
Property: assert
Result: ✅ pass

Obligation: seq_seq_len
Property: assert
Result: ✅ pass

Obligation: seq_map_len
Property: assert
Result: ✅ pass
-/
#guard_msgs in
#eval verify seqEmptyTypesPgm

----------------------------------------------------------------------
13 changes: 7 additions & 6 deletions editors/emacs/core-st-mode.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,13 @@
'( "div" "mod" "sdiv" "smod" "safesdiv" "safesmod"))

(defvar core-st-builtins
'( "Sequence.length" "Sequence.select" "Sequence.append"
"Sequence.build" "Sequence.update" "Sequence.contains"
"Sequence.take" "Sequence.drop" "str.len" "str.concat" "str.substr"
"str.to.re" "str.in.re" "str.prefixof" "str.suffixof" "re.allchar"
"re.all" "re.range" "re.concat" "re.*" "re.+" "re.loop" "re.union"
"re.inter" "re.comp" "re.none" "Int.DivT" "Int.ModT"))
'( "Sequence.empty" "Sequence.length" "Sequence.select"
"Sequence.append" "Sequence.build" "Sequence.update"
"Sequence.contains" "Sequence.take" "Sequence.drop" "str.len"
"str.concat" "str.substr" "str.to.re" "str.in.re" "str.prefixof"
"str.suffixof" "re.allchar" "re.all" "re.range" "re.concat" "re.*"
"re.+" "re.loop" "re.union" "re.inter" "re.comp" "re.none"
"Int.DivT" "Int.ModT"))

;; Font-lock rules
(defvar core-st-font-lock-keywords
Expand Down
2 changes: 1 addition & 1 deletion editors/vscode/syntaxes/core-st.tmLanguage.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@
]
},
"function-call": {
"match": "\\b(Sequence\\.length|Sequence\\.select|Sequence\\.append|Sequence\\.build|Sequence\\.update|Sequence\\.contains|Sequence\\.take|Sequence\\.drop|str\\.len|str\\.concat|str\\.substr|str\\.to\\.re|str\\.in\\.re|str\\.prefixof|str\\.suffixof|re\\.allchar|re\\.all|re\\.range|re\\.concat|re\\.\\*|re\\.\\+|re\\.loop|re\\.union|re\\.inter|re\\.comp|re\\.none|Int\\.DivT|Int\\.ModT|bvconcat\\{[0-9]+\\}\\{[0-9]+\\}|bvextract\\{[0-9]+\\}\\{[0-9]+\\}\\{[0-9]+\\})\\b",
"match": "\\b(Sequence\\.empty|Sequence\\.length|Sequence\\.select|Sequence\\.append|Sequence\\.build|Sequence\\.update|Sequence\\.contains|Sequence\\.take|Sequence\\.drop|str\\.len|str\\.concat|str\\.substr|str\\.to\\.re|str\\.in\\.re|str\\.prefixof|str\\.suffixof|re\\.allchar|re\\.all|re\\.range|re\\.concat|re\\.\\*|re\\.\\+|re\\.loop|re\\.union|re\\.inter|re\\.comp|re\\.none|Int\\.DivT|Int\\.ModT|bvconcat\\{[0-9]+\\}\\{[0-9]+\\}|bvextract\\{[0-9]+\\}\\{[0-9]+\\}\\{[0-9]+\\})\\b",
"captures": {
"1": { "name": "support.function.builtin.core-st" }
}
Expand Down
Loading