max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: fix broken benchmarks from #11446 (#11681)

Browse source 
This PR fixes benchmarks that were broken by #11446.
This commit is contained in:
Paul Reichert 2025-12-15 10:35:42 +01:00 • committed by GitHub
parent 3fdde57e7b
commit eb20c07b4a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/hashmap.lean
View file

@ -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

2
tests/bench/phashmap.lean
View file

@ -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

14
tests/bench/sigmaIterator.lean
View file

@ -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⟩

2
tests/bench/treemap.lean
View file

@ -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