diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index ecc4e924c3..db6d64896d 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -10,7 +10,7 @@ namespace Expr namespace FindImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean index 4ef9038f05..044b36f30d 100644 --- a/src/Lean/Util/FoldConsts.lean +++ b/src/Lean/Util/FoldConsts.lean @@ -10,7 +10,7 @@ namespace Lean namespace Expr namespace FoldConstsImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where visitedTerms : Array Expr -- Remark: cache based on pointer address. Our "unsafe" implementation relies on the fact that `()` is not a valid Expr diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean index e1c59c87da..853fc717c0 100644 --- a/src/Lean/Util/ReplaceExpr.lean +++ b/src/Lean/Util/ReplaceExpr.lean @@ -10,7 +10,7 @@ namespace Expr namespace ReplaceImpl -@[inline] def cacheSize : USize := 8192 +@[inline] def cacheSize : USize := 8192 - 1 structure Cache where -- First cacheSize elements are the keys. @@ -23,7 +23,7 @@ unsafe def Cache.new : Cache := @[inline] unsafe def Cache.keyIdx (key : Expr) : USize := - (ptrAddrUnsafe key >>> 4) % cacheSize + ptrAddrUnsafe key % cacheSize @[inline] unsafe def Cache.resultIdx (key : Expr) : USize := diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 1185838ad6..df3c57b35a 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -23,7 +23,7 @@ namespace Expr namespace ReplaceLevelImpl -abbrev cacheSize : USize := 8192 +abbrev cacheSize : USize := 8192 - 1 structure State where keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr