more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;
authorwenzelm
Wed, 28 Feb 2024 23:50:22 +0100
changeset 79741 513829904beb
parent 79740 ea1913c953ef
child 79742 2e4518e8a36b
more scalable: avoid potentially expensive ordering of underlying key data type, e.g. in MESON.Cache of Naproche;
src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Wed Feb 28 22:11:11 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Wed Feb 28 23:50:22 2024 +0100
@@ -3905,9 +3905,8 @@
 prune (Cache ref) max_size min_timing = do
   atomicModifyIORef' ref (\entries ->
     let
-      trim x e = if _timing e < min_timing then Map.delete x else id
       sort = List.sortBy (\(_, e1) (_, e2) -> compare (_access e2) (_access e1))
-      entries1 = Map.foldrWithKey trim entries entries
+      entries1 = Map.filter (\e -> _timing e >= min_timing) entries
       entries2 =
         if Map.size entries1 <= max_size then entries1
         else Map.fromList $ List.take max_size $ sort $ Map.toList entries1