3847 err_lines = drop n lines |
3847 err_lines = drop n lines |
3848 in return $ Process_Result.make rc out_lines err_lines timing |
3848 in return $ Process_Result.make rc out_lines err_lines timing |
3849 _ -> err |
3849 _ -> err |
3850 \<close> |
3850 \<close> |
3851 |
3851 |
|
3852 generate_file "Isabelle/Cache.hs" = \<open> |
|
3853 {- Title: Isabelle/Cache.hs |
|
3854 Author: Makarius |
|
3855 LICENSE: BSD 3-clause (Isabelle) |
|
3856 |
|
3857 Cache for slow computations. |
|
3858 -} |
|
3859 |
|
3860 module Isabelle.Cache ( |
|
3861 T, init, apply, prune |
|
3862 ) |
|
3863 where |
|
3864 |
|
3865 import Prelude hiding (init) |
|
3866 import Control.Exception (evaluate) |
|
3867 import Data.IORef |
|
3868 import Data.Map.Strict (Map) |
|
3869 import qualified Data.Map.Strict as Map |
|
3870 import qualified Data.List as List |
|
3871 |
|
3872 import Isabelle.Time (Time) |
|
3873 import qualified Isabelle.Time as Time |
|
3874 |
|
3875 |
|
3876 data Entry v = Entry {_value :: v, _access :: Time, _timing :: Time} |
|
3877 |
|
3878 newtype T k v = Cache (IORef (Map k (Entry v))) |
|
3879 |
|
3880 init :: IO (T k v) |
|
3881 init = Cache <$> newIORef Map.empty |
|
3882 |
|
3883 commit :: Ord k => T k v -> k -> Entry v -> IO v |
|
3884 commit (Cache ref) x e = do |
|
3885 atomicModifyIORef' ref (\entries -> |
|
3886 let |
|
3887 entry = |
|
3888 case Map.lookup x entries of |
|
3889 Just e' | _access e' > _access e -> e' |
|
3890 _ -> e |
|
3891 in (Map.insert x entry entries, _value entry)) |
|
3892 |
|
3893 apply :: Ord k => T k v -> (k -> v) -> k -> IO v |
|
3894 apply cache@(Cache ref) f x = do |
|
3895 start <- Time.now |
|
3896 entries <- readIORef ref |
|
3897 case Map.lookup x entries of |
|
3898 Just entry -> do |
|
3899 commit cache x (entry {_access = start}) |
|
3900 Nothing -> do |
|
3901 y <- evaluate $ f x |
|
3902 stop <- Time.now |
|
3903 commit cache x (Entry y start (stop - start)) |
|
3904 |
|
3905 prune :: Ord k => T k v -> Int -> Time -> IO () |
|
3906 prune (Cache ref) max_size min_timing = do |
|
3907 atomicModifyIORef' ref (\entries -> |
|
3908 let |
|
3909 trim x e = if _timing e < min_timing then Map.delete x else id |
|
3910 sort = List.sortBy (\(_, e1) (_, e2) -> compare (_access e2) (_access e1)) |
|
3911 entries1 = Map.foldrWithKey trim entries entries |
|
3912 entries2 = |
|
3913 if Map.size entries1 <= max_size then entries1 |
|
3914 else Map.fromList $ List.take max_size $ sort $ Map.toList entries1 |
|
3915 in (entries2, ())) |
|
3916 \<close> |
|
3917 |
3852 export_generated_files _ |
3918 export_generated_files _ |
3853 |
3919 |
3854 end |
3920 end |