
  0 | ||| Hash Priority Search Queue Internals
  1 | module Data.HashPSQ.Internal
  2 | 
  3 | import Data.NatPSQ.Internal as NatPSQI
  4 | import Data.OrdPSQ          as OrdPSQ
  5 | import Data.OrdPSQ.Internal as OrdPSQI
  6 | 
  7 | import Data.List
  8 | import Data.String
  9 | import Derive.Prelude
 10 | 
 11 | %default total
 12 | %language ElabReflection
 13 | 
 14 | --------------------------------------------------------------------------------
 15 | --          Bucket
 16 | --------------------------------------------------------------------------------
 17 | 
 18 | public export
 19 | data Bucket : (k : Type) -> (p : Type) -> (v : Type) -> Type where
 20 |   MkBucket :  k
 21 |            -> v
 22 |            -> OrdPSQI.OrdPSQ k p v
 23 |            -> Bucket k p v
 24 | 
 25 | %runElab derive "Bucket" [Eq,Ord,Show]
 26 | 
 27 | export
 28 | toBucket :  Ord k
 29 |          => Ord p
 30 |          => OrdPSQI.OrdPSQ k p v
 31 |          -> Maybe (p, Bucket k p v)
 32 | toBucket opsq =
 33 |   case OrdPSQ.minView opsq of
 34 |     Just (k, p, x, opsq') =>
 35 |       Just (p, MkBucket k x opsq')
 36 |     Nothing               =>
 37 |       Nothing
 38 | 
 39 | ||| Smart constructor which takes care of placing the minimum element directly
 40 | ||| in the Bucket.
 41 | export
 42 | mkBucket :  Ord k
 43 |          => Ord p
 44 |          => k
 45 |          -> p
 46 |          -> v
 47 |          -> OrdPSQI.OrdPSQ k p v
 48 |          -> (p, Bucket k p v)
 49 | mkBucket k p x opsq =
 50 |   case toBucket (OrdPSQ.insert k p x opsq) of
 51 |     Just bucket =>
 52 |       bucket
 53 |     Nothing     =>
 54 |       assert_total $ idris_crash "Data.HashPSQ.Internal.mkBucket: internal error"
 55 | 
 56 | --------------------------------------------------------------------------------
 57 | --          HashPSQ
 58 | --------------------------------------------------------------------------------
 59 | 
 60 | ||| A priority search queue with keys of type k and priorities of type p
 61 | ||| and values of type v.
 62 | ||| A HashPSQ offers very similar performance to NatPSQ.
 63 | ||| In case of collisions, it uses an OrdPSQ locally to solve those.
 64 | ||| This means worst case complexity is usually given by O(min(n,W), log n), where W is the number of bits in an Int.
 65 | ||| This simplifies to O(min(n, W)) since log n is always smaller than W on current machines.
 66 | public export
 67 | data HashPSQ : (k : Type) -> (p : Type) -> (v : Type) -> Type where
 68 |   MkHashPSQ :  NatPSQI.NatPSQ p (Bucket k p v)
 69 |             -> HashPSQ k p v
 70 | 
 71 | %runElab derive "HashPSQ" [Eq,Ord,Show]
 72 |