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