From 271fb5d68ce6eb26436fc970321c1f9f37b2f162 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 23 Apr 2026 14:00:21 -0700 Subject: [PATCH 1/3] feat(core): Add Sequence.empty() syntax for creating empty sequences 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 Resolves #1027 --- .../Core/DDMTransform/FormatCore.lean | 15 +++- .../Languages/Core/DDMTransform/Grammar.lean | 5 +- .../Core/DDMTransform/Translate.lean | 8 +- Strata/Languages/Core/Factory.lean | 4 +- StrataTest/Languages/Core/Examples/Seq.lean | 83 +++++++++++++++++++ 5 files changed, 105 insertions(+), 10 deletions(-) diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean index 772dd94e18..868e8df5e6 100644 --- a/Strata/Languages/Core/DDMTransform/FormatCore.lean +++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean @@ -289,13 +289,21 @@ 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 + | some (.tcons "Sequence" [elemTy]) => + let ety ← lmonoTyToCoreType elemTy + pure (.seq_empty default ety) + | _ => + let ety := CoreType.tvar default unknownTypeVar + pure (.seq_empty default ety) | _ => do ToCSTM.logError "lopToExpr" "0-ary op not found" name pure (.re_none default) @@ -495,6 +503,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 @@ -511,7 +520,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 @@ -549,7 +558,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 => diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean index 70eaa52a05..7f496cce03 100644 --- a/Strata/Languages/Core/DDMTransform/Grammar.lean +++ b/Strata/Languages/Core/DDMTransform/Grammar.lean @@ -101,9 +101,8 @@ 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. +fn seq_empty (A : Type) : Sequence A => + "Sequence.empty" "<" A ">" "(" ")"; 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 => diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 7d4e3d797a..325f6773b3 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -823,6 +823,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)) + return fn -- Unary function applications | .fn _ fni, [xa] => match fni with @@ -888,7 +895,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 := diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index 577f25de5a..d80838a574 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -426,9 +426,7 @@ 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()` returns an empty sequence of element type `A`. -/ def seqEmptyFunc : WFLFunc CoreLParams := polyUneval "Sequence.empty" ["a"] [] (seqTy mty[%a]) (axioms := [ diff --git a/StrataTest/Languages/Core/Examples/Seq.lean b/StrataTest/Languages/Core/Examples/Seq.lean index c7e3c32b8e..69a3368c36 100644 --- a/StrataTest/Languages/Core/Examples/Seq.lean +++ b/StrataTest/Languages/Core/Examples/Seq.lean @@ -305,3 +305,86 @@ Result: ✅ pass #eval verify seqOpsPgm --------------------------------------------------------------------- + +---------------------------------------------------------------------- +-- Tests for Sequence.empty() 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(); + assert [empty_length]: Sequence.length(s) == 0; + + // Build on top of an empty sequence + s := Sequence.build(Sequence.empty(), 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(); + assert [empty_length]: Sequence.length(s) == 0; + s := Sequence.build(Sequence.empty(), 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()) == 0 + +Label: build_on_empty_length +Property: assert +Obligation: +Sequence.length(Sequence.build(Sequence.empty(), 42)) == 1 + +Label: build_on_empty_elem +Property: assert +Obligation: +Sequence.select(Sequence.build(Sequence.empty(), 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 +-/ +#guard_msgs in +#eval verify seqEmptyPgm + +---------------------------------------------------------------------- From b573bb668dbe7de61dbff84fd37375d397c848ed Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 6 May 2026 08:39:00 -0700 Subject: [PATCH 2/3] Update editor syntax files --- editors/emacs/core-st-mode.el | 13 +++++++------ editors/vscode/syntaxes/core-st.tmLanguage.json | 2 +- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/editors/emacs/core-st-mode.el b/editors/emacs/core-st-mode.el index 6bcfb271d4..d34a2792b2 100644 --- a/editors/emacs/core-st-mode.el +++ b/editors/emacs/core-st-mode.el @@ -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 diff --git a/editors/vscode/syntaxes/core-st.tmLanguage.json b/editors/vscode/syntaxes/core-st.tmLanguage.json index 44e4208209..54fd7a90c6 100644 --- a/editors/vscode/syntaxes/core-st.tmLanguage.json +++ b/editors/vscode/syntaxes/core-st.tmLanguage.json @@ -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" } } From f22f601dd035082d9a74a7db3a135968456c48cd Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 7 May 2026 15:59:29 -0700 Subject: [PATCH 3/3] fix(core): Improve Sequence.empty type resolution in DDM transform Fix pattern match in handleZeroaryOps to use Core.seqTy instead of raw tcons string matching for Sequence.empty element type extraction. Add error logging when the op-type annotation is missing or malformed. - Use structured Core.seqTy pattern in FormatCore.lean - Add ToCSTM.logError for the fallback path - Add comment in Grammar.lean explaining why seq_empty needs explicit type syntax - Clarify seqEmptyFunc doc comment in Factory.lean - Add test exercising Sequence.empty with bool, nested Sequence, and Map element types --- .../Core/DDMTransform/FormatCore.lean | 5 +- .../Languages/Core/DDMTransform/Grammar.lean | 2 + Strata/Languages/Core/Factory.lean | 4 +- StrataTest/Languages/Core/Examples/Seq.lean | 83 +++++++++++++++++++ 4 files changed, 91 insertions(+), 3 deletions(-) diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean index fa9c79ebdc..a07bbe6c9b 100644 --- a/Strata/Languages/Core/DDMTransform/FormatCore.lean +++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean @@ -298,10 +298,11 @@ def handleZeroaryOps {M} [Inhabited M] (name : String) | .re .None => pure (.re_none default) | .seq .Empty => do match opTy with - | some (.tcons "Sequence" [elemTy]) => + | 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 pure (.seq_empty default ety) | _ => do diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean index c491cec549..5c8abe4e6f 100644 --- a/Strata/Languages/Core/DDMTransform/Grammar.lean +++ b/Strata/Languages/Core/DDMTransform/Grammar.lean @@ -103,6 +103,8 @@ 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 "]"; +// 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 => "Sequence.empty" "<" A ">" "(" ")"; fn seq_length (A : Type, s : Sequence A) : int => "Sequence.length" "(" s ")"; diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean index 18fc837148..0fedf025c4 100644 --- a/Strata/Languages/Core/Factory.lean +++ b/Strata/Languages/Core/Factory.lean @@ -432,7 +432,9 @@ def seqLengthFunc : WFLFunc CoreLParams := ]) /- An empty `Sequence` constructor with type `∀a. Sequence a`. - `Sequence.empty()` returns an empty sequence of element type `A`. -/ + `Sequence.empty()` returns an empty sequence of element type `A`. + The `` 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 := [ diff --git a/StrataTest/Languages/Core/Examples/Seq.lean b/StrataTest/Languages/Core/Examples/Seq.lean index 69a3368c36..fd1f7b38d3 100644 --- a/StrataTest/Languages/Core/Examples/Seq.lean +++ b/StrataTest/Languages/Core/Examples/Seq.lean @@ -388,3 +388,86 @@ Result: ✅ pass #eval verify seqEmptyPgm ---------------------------------------------------------------------- + +-- Exercise various element types for Sequence.empty(). +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(); + ssi := Sequence.empty(); + smi := Sequence.empty(); + + 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(); + ssi := Sequence.empty(); + smi := Sequence.empty(); + 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()) == 0 + +Label: seq_seq_len +Property: assert +Obligation: +Sequence.length(Sequence.empty()) == 0 + +Label: seq_map_len +Property: assert +Obligation: +Sequence.length(Sequence.empty()) == 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 + +----------------------------------------------------------------------