0 | ||| Least Recently Used (LRU) Cache
  1 | module Data.LRUCache
  2 |
  3 | import public Data.HashPSQ
  4 | import public Data.LRUCache.Internal
  5 |
  6 | import Data.List
  7 | import Data.Hashable
  8 | import Data.Maybe
  9 | import Data.Zippable
 10 |
 11 | %default total
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Construction
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Create an empty LRUCache of the given size.
 18 | export
 19 | empty :  Nat
 20 |       -> LRUCache k v
 21 | empty capacity =
 22 |   case capacity < 1 of
 23 |     True  =>
 24 |       assert_total $ idris_crash "Data.LRUCache.empty: capacity < 1"
 25 |     False =>
 26 |       MkLRUCache capacity
 27 |                  0
 28 |                  0
 29 |                  empty
 30 |
 31 | --------------------------------------------------------------------------------
 32 | --          Insertion
 33 | --------------------------------------------------------------------------------
 34 |
 35 | private
 36 | compress :  List (k, Priority, v)
 37 |          -> List (k, Priority, v)
 38 | compress q =
 39 |   let sortedq = sortBy compareByPriority q
 40 |     in zipWith (\(k, _, v), p => (k, p, v))
 41 |                sortedq
 42 |                [1..(length sortedq)]
 43 |   where
 44 |     compareByPriority :  (k, Priority, v)
 45 |                       -> (k, Priority, v)
 46 |                       -> Ordering
 47 |     compareByPriority (_, p, _) (_, p', _) =
 48 |       compare p p'
 49 |
 50 | ||| Restore LRUCache invariants.
 51 | ||| For performance reasons this is not snd . trim'.
 52 | private
 53 | trim :  Hashable k
 54 |      => Ord k
 55 |      => LRUCache k v
 56 |      -> LRUCache k v
 57 | trim cache@(MkLRUCache c s t q) =
 58 |   case s > c of
 59 |     True  =>
 60 |       MkLRUCache c
 61 |                  (s `minus` 1)
 62 |                  t
 63 |                  (deleteMin q)
 64 |     False =>
 65 |       cache
 66 |
 67 | ||| Insert an element into the LRUCache.
 68 | export
 69 | insert :  Hashable k
 70 |        => Ord k
 71 |        => k
 72 |        -> v
 73 |        -> LRUCache k v
 74 |        -> LRUCache k v
 75 | insert key val (MkLRUCache c s t q) =
 76 |   let (mboldval, queue) = HashPSQ.insertView key t val q
 77 |     in case isNothing mboldval of
 78 |          True  =>
 79 |            trim $
 80 |              MkLRUCache c
 81 |                         (s `plus` 1)
 82 |                         (t `plus` 1)
 83 |                         queue
 84 |          False =>
 85 |            trim $
 86 |              MkLRUCache c
 87 |                         s
 88 |                         (t `plus` 1)
 89 |                         queue
 90 |
 91 | --------------------------------------------------------------------------------
 92 | --          Views
 93 | --------------------------------------------------------------------------------
 94 |
 95 | ||| Restore LRUCache invariants returning the evicted element if any.
 96 | private
 97 | trim' :  Hashable k
 98 |       => Ord k
 99 |       => LRUCache k v
100 |       -> (Maybe (k, v), LRUCache k v)
101 | trim' cache@(MkLRUCache c s t q) =
102 |   case s > c of
103 |     True  =>
104 |       case HashPSQ.findMin q of
105 |         Nothing        =>
106 |           assert_total $ idris_crash "Data.LRUCache.trim': internal error"
107 |         Just (k, _, v) =>
108 |           let c' = MkLRUCache c
109 |                               (s `minus` 1)
110 |                               t
111 |                               (HashPSQ.deleteMin q)
112 |             in (Just (k, v), c')
113 |     False =>
114 |       (Nothing, cache)
115 |
116 | ||| Insert an element into the LRUCache returning the evicted element if any.
117 | ||| When the logical clock reaches its maximum value and all values are
118 | ||| evicted Nothing is returned.
119 | export
120 | insertView :  Hashable k
121 |            => Ord k
122 |            => k
123 |            -> v
124 |            -> LRUCache k v
125 |            -> (Maybe (k, v), LRUCache k v)
126 | insertView key val (MkLRUCache c s t q) =
127 |   let (mboldval, queue) = HashPSQ.insertView key t val q
128 |     in case isNothing mboldval of
129 |          True  =>
130 |            trim' $
131 |              MkLRUCache c
132 |                         (s `plus` 1)
133 |                         (t `plus` 1)
134 |                         queue
135 |          False =>
136 |             trim' $
137 |               MkLRUCache c
138 |                          s
139 |                          (t `plus` 1)
140 |                          queue
141 |
142 | --------------------------------------------------------------------------------
143 | --          Query
144 | --------------------------------------------------------------------------------
145 |
146 | ||| Lookup an element in an LRUCache and mark it as the least recently accessed.
147 | export
148 | lookup :  Hashable k
149 |        => Ord k
150 |        => k
151 |        -> LRUCache k v
152 |        -> Maybe (v, LRUCache k v)
153 | lookup k cache@(MkLRUCache c s t q) =
154 |   case HashPSQ.alter lookupAndBump k q of
155 |     (Nothing, _) =>
156 |       Nothing
157 |     (Just x, q)  =>
158 |       let c' = trim $
159 |                  MkLRUCache c
160 |                             s
161 |                             (t `plus` 1)
162 |                             q
163 |         in Just (x, c')
164 |   where
165 |     lookupAndBump :  Maybe (a, b)
166 |                   -> (Maybe b, Maybe (Priority, b))
167 |     lookupAndBump Nothing       =
168 |       (Nothing, Nothing)
169 |     lookupAndBump (Just (_, x)) =
170 |       (Just x, Just (t, x))
171 |