From eb20c07b4a900c9ae9e7328aa9a95f9c3f07a170 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 15 Dec 2025 10:35:42 +0100
Subject: [PATCH] fix: fix broken benchmarks from #11446 (#11681)

This PR fixes benchmarks that were broken by #11446.
---
 tests/bench/hashmap.lean       |  2 +-
 tests/bench/phashmap.lean      |  2 +-
 tests/bench/sigmaIterator.lean | 14 +++++++-------
 tests/bench/treemap.lean       |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/tests/bench/hashmap.lean b/tests/bench/hashmap.lean
index 588588f328..a68bd7d038 100644
--- a/tests/bench/hashmap.lean
+++ b/tests/bench/hashmap.lean
@@ -25,7 +25,7 @@ def iterRandM (seed : UInt64) : Std.IterM (α := RandomIterator) m UInt64 :=
 def iterRand (seed : UInt64) : Std.Iter (α := RandomIterator) UInt64 :=
   { internalState := RandomIterator.mk seed }
 
-instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
+instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
   IsPlausibleStep it
     | .yield it' out => True -- fake it for now
     | .skip _ => False
diff --git a/tests/bench/phashmap.lean b/tests/bench/phashmap.lean
index d2443d643e..bbc7ec134c 100644
--- a/tests/bench/phashmap.lean
+++ b/tests/bench/phashmap.lean
@@ -23,7 +23,7 @@ def iterRandM (seed : UInt64) : Std.IterM (α := RandomIterator) m UInt64 :=
 def iterRand (seed : UInt64) : Std.Iter (α := RandomIterator) UInt64 :=
   { internalState := RandomIterator.mk seed }
 
-instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
+instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
   IsPlausibleStep it
     | .yield it' out => True -- fake it for now
     | .skip _ => False
diff --git a/tests/bench/sigmaIterator.lean b/tests/bench/sigmaIterator.lean
index df27e5de02..461d436218 100644
--- a/tests/bench/sigmaIterator.lean
+++ b/tests/bench/sigmaIterator.lean
@@ -26,7 +26,7 @@ structure SigmaIterator (γ : Type w) (α : γ → Type w) where
 def SigmaIterator.Monadic.modifyStep {β γ : Type w} {α : γ → Type w} {m : Type w → Type w'}
     [∀ x : γ, Iterator (α := α x) m β]
     (it : IterM (α := SigmaIterator γ α) m β)
-    (step : (toIterM it.internalState.inner m β).Step) :
+    (step : (IterM.mk it.internalState.inner m β).Step) :
     IterStep (IterM (α := SigmaIterator γ α) m β) β :=
   match step.val with
   | .yield it' out =>
@@ -41,7 +41,7 @@ instance SigmaIterator.instIterator {γ : Type w} {α : γ → Type w}
   IsPlausibleStep it step := ∃ step', Monadic.modifyStep it step' = step
   step it :=
     (fun step => .deflate ⟨Monadic.modifyStep it step.inflate, step.inflate, rfl⟩) <$>
-      (toIterM it.internalState.inner m β).step
+      (IterM.mk it.internalState.inner m β).step
 
 private structure SigmaIteratorWF (γ : Type w) (α : γ → Type w) (m : Type w → Type w) (β : Type w) where
   parameter : γ
@@ -54,7 +54,7 @@ private def SigmaIterator.instFinitenessRelation {γ : Type w} {α : γ → Type
     (PSigma.Lex emptyRelation
       (β := fun param : γ => IterM (α := α param) m β)
       (fun _ => InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps))
-    (fun it => ⟨it.internalState.parameter, toIterM it.internalState.inner m β⟩)
+    (fun it => ⟨it.internalState.parameter, IterM.mk it.internalState.inner m β⟩)
   wf := by
     apply InvImage.wf
     refine ⟨fun ⟨param, it⟩ => ?_⟩
@@ -84,7 +84,7 @@ private def SigmaIterator.instProductivenessRelation {γ : Type w} {α : γ →
     (PSigma.Lex emptyRelation
       (β := fun param : γ => IterM (α := α param) m β)
       (fun _ => InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips))
-    (fun it => ⟨it.internalState.parameter, toIterM it.internalState.inner m β⟩)
+    (fun it => ⟨it.internalState.parameter, IterM.mk it.internalState.inner m β⟩)
   wf := by
     apply InvImage.wf
     refine ⟨fun ⟨param, it⟩ => ?_⟩
@@ -131,14 +131,14 @@ dependency at the cost of storing the parameter in a structure field at runtime.
 def IterM.sigma {γ : Type w} {α : γ → Type w}
     [∀ x : γ, Iterator (α x) m β] {param : γ} (it : IterM (α := α param) m β) :
     IterM (α := Types.SigmaIterator γ α) m β :=
-  toIterM ⟨param, it.internalState⟩ m β
+  IterM.mk ⟨param, it.internalState⟩ m β
 
 end Std.Iterators
 
-open Std.Iterators Std.Iterators.Types
+open Std Std.Iterators Std.Iterators.Types
 
 @[always_inline, inline, expose]
-def Std.Iterators.Iter.sigma {γ : Type w} {α : γ → Type w}
+def Std.Iter.sigma {γ : Type w} {α : γ → Type w}
     [∀ x : γ, Iterator (α x) Id β] {param : γ} (it : Iter (α := α param) β):
     Iter (α := SigmaIterator γ α) β :=
   ⟨param, it.internalState⟩
diff --git a/tests/bench/treemap.lean b/tests/bench/treemap.lean
index 07246ea510..000454f570 100644
--- a/tests/bench/treemap.lean
+++ b/tests/bench/treemap.lean
@@ -20,7 +20,7 @@ def iterRandM (seed : UInt64) : Std.IterM (α := RandomIterator) m UInt64 :=
 def iterRand (seed : UInt64) : Std.Iter (α := RandomIterator) UInt64 :=
   { internalState := RandomIterator.mk seed }
 
-instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
+instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
   IsPlausibleStep it
     | .yield it' out => True -- fake it for now
     | .skip _ => False