diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean
index 639c5f355f..a07bbe6c9b 100644
--- a/Strata/Languages/Core/DDMTransform/FormatCore.lean
+++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean
@@ -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
+ | 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
ToCSTM.logError "lopToExpr" "0-ary op not found" name
pure (.re_none default)
@@ -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
@@ -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
@@ -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 =>
diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean
index 0374322193..5c8abe4e6f 100644
--- a/Strata/Languages/Core/DDMTransform/Grammar.lean
+++ b/Strata/Languages/Core/DDMTransform/Grammar.lean
@@ -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 =>
+ "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 aa088ca54f..bfc33f6de1 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -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))
+ return fn
-- Unary function applications
| .fn _ fni, [xa] =>
match fni with
@@ -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 :=
diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean
index ef99656a5b..0fedf025c4 100644
--- a/Strata/Languages/Core/Factory.lean
+++ b/Strata/Languages/Core/Factory.lean
@@ -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()` 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 c7e3c32b8e..fd1f7b38d3 100644
--- a/StrataTest/Languages/Core/Examples/Seq.lean
+++ b/StrataTest/Languages/Core/Examples/Seq.lean
@@ -305,3 +305,169 @@ 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
+
+----------------------------------------------------------------------
+
+-- 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