0 | ||| Linear Least Recently Used (LRU) Cache Internals
 1 | module Data.LRUCache1.Internal
 2 |
 3 | import Data.HashPSQ
 4 | import Data.LRUCache.Internal
 5 |
 6 | import Derive.Prelude
 7 | import Data.Linear.Ref1
 8 |
 9 | %default total
10 | %language ElabReflection
11 |
12 | --------------------------------------------------------------------------------
13 | --          LRUCache1
14 | --------------------------------------------------------------------------------
15 |
16 | ||| Linear Least Recently Used (LRU) Cache based on hashing.
17 | public export
18 | data LRUCache1 : (s : Type) -> (k : Type) -> (v : Type) -> Type where
19 |   MkLRUCache1 :  (lrucache : Ref s (LRUCache k v))
20 |               -> LRUCache1 s k v
21 |