0 | ||| Ordered Nat Priority Search Queue Internals
  1 | module Data.NatPSQ.Internal
  2 |
  3 | import Data.Bits
  4 | import Derive.Prelude
  5 |
  6 | %default total
  7 | %language ElabReflection
  8 |
  9 | --------------------------------------------------------------------------------
 10 | --          Internal Utility
 11 | --------------------------------------------------------------------------------
 12 |
 13 | ||| Convenience interface for bitSize that doesn't use an implicit parameter.
 14 | private
 15 | bitSizeOf :  (ty : Type)
 16 |           -> FiniteBits ty
 17 |           => Nat
 18 | bitSizeOf ty =
 19 |   bitSize {a = ty}
 20 |
 21 | --------------------------------------------------------------------------------
 22 | --          Internals
 23 | --------------------------------------------------------------------------------
 24 |
 25 | ||| Size is a natural machine word
 26 | ||| (Bits32/Bits64 or the size of an unsigned Int on the host system).
 27 | public export
 28 | Size : Type
 29 | Size =
 30 |   case bitSizeOf Int of
 31 |     32 =>
 32 |       Bits32
 33 |     _  =>
 34 |       Bits64
 35 |
 36 | ||| The Nat type are keys for the queue (Ordered Nat Priority Search Queue).
 37 | public export
 38 | Key : Type
 39 | Key = Nat
 40 |
 41 | ||| We store Masks as the index of the bit that determines the branching.
 42 | public export
 43 | Mask : Type
 44 | Mask = Nat
 45 |
 46 | --------------------------------------------------------------------------------
 47 | --          Bit Manipulation
 48 | --------------------------------------------------------------------------------
 49 |
 50 | private
 51 | natFromBits :  Key
 52 |             -> Size
 53 | natFromBits =
 54 |   cast
 55 |
 56 | private
 57 | bitsFromNat :  Size
 58 |             -> Key
 59 | bitsFromNat =
 60 |   cast
 61 |
 62 | export
 63 | zero :  Key
 64 |      -> Mask
 65 |      -> Bool
 66 | zero i m =
 67 |   (natFromBits i) .&. (natFromBits m) == 0
 68 |
 69 | private
 70 | maskW :  Size
 71 |       -> Size
 72 | maskW m =
 73 |   complement (m - 1) `xor` m
 74 |
 75 | export
 76 | noMatch :  Key
 77 |         -> Key
 78 |         -> Mask
 79 |         -> Bool
 80 | noMatch k1 k2 m =
 81 |   natFromBits k1 .&. m' /= natFromBits k2 .&. m'
 82 |   where
 83 |     m' = maskW (natFromBits m)
 84 |
 85 | private
 86 | highestBitMask :  Size
 87 |                -> Size
 88 | highestBitMask x1 =
 89 |   let x2 = x1 .|. x1 `shiftR` 1
 90 |       x3 = x2 .|. x2 `shiftR` 2
 91 |       x4 = x3 .|. x3 `shiftR` 4
 92 |       x5 = x4 .|. x4 `shiftR` 8
 93 |       x6 = x5 .|. x5 `shiftR` 16
 94 |       x7 = case bitSizeOf Int of
 95 |              32 =>
 96 |                x6
 97 |              _  =>
 98 |                x6 .|. x6 `shiftR` 32
 99 |     in x7 `xor` (x7 `shiftR` 1)
100 |
101 | export
102 | branchMask :  Key
103 |            -> Key
104 |            -> Mask
105 | branchMask k1 k2 =
106 |   bitsFromNat (highestBitMask (natFromBits k1 `xor` natFromBits k2))
107 |
108 | --------------------------------------------------------------------------------
109 | --          NatPSQ
110 | --------------------------------------------------------------------------------
111 |
112 | ||| A priority search queue with Nat keys
113 | ||| and priorities of type p and values of type v.
114 | ||| Many operations have a worst-case complexity of O(min(n,W)).
115 | ||| This means that the operation can become linear in the number of elements with a maximum of W
116 | ||| (the number of bits in an Int (32 or 64)).
117 | ||| It is generally much faster than an OrdPSQ.
118 | public export
119 | data NatPSQ : (p : Type) -> (v : Type) -> Type where
120 |   Bin :  Key
121 |       -> p
122 |       -> v
123 |       -> Mask
124 |       -> NatPSQ p v
125 |       -> NatPSQ p v
126 |       -> NatPSQ p v
127 |   Tip :  Key
128 |       -> p
129 |       -> v
130 |       -> NatPSQ p v
131 |   Nil : NatPSQ p v
132 |
133 | %runElab derive "NatPSQ" [Eq,Ord,Show]
134 |