0 | ||| Least Recently Used (LRU) Cache Internals
 1 | module Data.LRUCache.Internal
 2 |
 3 | import Data.HashPSQ
 4 | import Derive.Prelude
 5 |
 6 | %default total
 7 | %language ElabReflection
 8 |
 9 | --------------------------------------------------------------------------------
10 | --          Priority
11 | --------------------------------------------------------------------------------
12 |
13 | ||| Logical time at which an element was last accessed.
14 | public export
15 | Priority : Type
16 | Priority = Nat
17 |
18 | --------------------------------------------------------------------------------
19 | --          LRUCache
20 | --------------------------------------------------------------------------------
21 |
22 | ||| Least Recently Used (LRU) Cache based on hashing.
23 | public export
24 | data LRUCache : (k : Type) -> (v : Type) -> Type where
25 |   MkLRUCache :  (capacity : Nat)               -- The maximum number of elements the queue can hold.
26 |              -> (size : Nat)                   -- The current number of elements in the queue.
27 |              -> (tick : Priority)              -- The next logical time.
28 |              -> (queue : HashPSQ k Priority v) -- The underlying priority queue.
29 |              -> LRUCache k v
30 |
31 | %runElab derive "LRUCache" [Eq,Ord,Show]
32 |