
   0 | ||| Specialized implementation of an interval map with finger trees [1].
   1 | ||| This data structure is meant to get efficiently data with a correlated NonEmptyFC.
   2 | ||| The element data type must implement the `Measure` interface. An implementation
   3 | ||| is provided already for NonEmptyFC and tuples with NonEmptyFC as first element.
   4 | |||
   5 | ||| [1] https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf
   6 | module Libraries.Data.PosMap
   7 | 
   8 | import Core.FC
   9 | 
  10 | %hide Prelude.Ops.infixr.(<|)
  11 | %hide Prelude.Ops.infixl.(|>)
  12 | 
  13 | %default total
  14 | 
  15 | export infixr 5 <|, <:
  16 | export infixl 5 |>, :>
  17 | 
  18 | public export
  19 | FileRange : Type
  20 | FileRange = (FilePos, FilePos)
  21 | 
  22 | ||| Type for rightmost intervals, ordered by their low endpoints and annotated
  23 | ||| with the maximum of the high endpoints.
  24 | data RMFileRange = MkRange FileRange FilePos
  25 | 
  26 | Eq RMFileRange where
  27 |   (MkRange low high) == (MkRange low' high') = low == low' && high == high'
  28 | 
  29 | Show RMFileRange where
  30 |   showPrec p (MkRange low high) = showCon p "MkRange" $ showArg low ++ showArg high
  31 | 
  32 | Semigroup RMFileRange where
  33 |   -- The semigroup operation on righmost intervals is the composition of two
  34 |   -- monoids applied to each component:
  35 |   -- 1) the operation on low endpoints always returns the last key it contains,
  36 |   --    assuming the keys are ordered (enforced by the insertion function), the
  37 |   --    FingerTree behaves as a store of ordered sequences, with measures
  38 |   --    serving as signpost keys.
  39 |   -- 2) the operation on high endpoints returns the maximum of the endpoints,
  40 |   --    thus the FingerTree behaves as a max-priority queue.
  41 |   (MkRange low high) <+> (MkRange low' high') = MkRange low' (max high high')
  42 | 
  43 | data Interval = MkInterval RMFileRange | NoInterval
  44 | 
  45 | Eq Interval where
  46 |   (MkInterval range) == (MkInterval range') = range == range'
  47 |   NoInterval == NoInterval = True
  48 |   _ == _ = False
  49 | 
  50 | Show Interval where
  51 |   showPrec p (MkInterval range) = showCon p "MkInterval" $ showArg range
  52 |   showPrec p NoInterval = "NoInterval"
  53 | 
  54 | Semigroup Interval where
  55 |   NoInterval <+> i = i
  56 |   i <+> NoInterval = i
  57 |   (MkInterval range) <+> (MkInterval range') = MkInterval (range <+> range')
  58 | 
  59 | Monoid Interval where
  60 |   neutral = NoInterval
  61 | 
  62 | Cast FileRange RMFileRange where
  63 |   cast (l, h) = MkRange (l, h) h
  64 | 
  65 | Cast FileRange Interval where
  66 |   cast (l, h) = MkInterval (MkRange (l, h) h)
  67 | 
  68 | Cast RMFileRange Interval where
  69 |   cast = MkInterval
  70 | 
  71 | ||| Things that have an associated interval in the source files.
  72 | public export
  73 | interface Measure a where
  74 |   measure : a -> FileRange
  75 | 
  76 | interface MeasureRM a where
  77 |   measureRM : a -> RMFileRange
  78 | 
  79 | public export
  80 | Measure a => MeasureRM a where
  81 |   measureRM = cast . measure
  82 | 
  83 | measureInterval : Measure a => a -> Interval
  84 | measureInterval = cast . measure
  85 | 
  86 | data Digit : Type -> Type where
  87 |   One : a -> Digit a
  88 |   Two : a -> a -> Digit a
  89 |   Three : a -> a -> a -> Digit a
  90 |   Four : a -> a -> a -> a -> Digit a
  91 | 
  92 | Eq a => Eq (Digit a) where
  93 |   (One x) == (One x') = x == x'
  94 |   (Two x y) == (Two x' y') = x == x' && y == y'
  95 |   (Three x y z) == (Three x' y' z') = x == x' && y == y' && z == z'
  96 |   (Four x y z w) == (Four x' y' z' w') = x == x' && y == y' && z == z' && w == w'
  97 |   _ == _ = False
  98 | 
  99 | Show a => Show (Digit a) where
 100 |   showPrec p (One x) = showCon p "One" $ showArg x
 101 |   showPrec p (Two x y) = showCon p "Two" $ showArg x ++ showArg y
 102 |   showPrec p (Three x y z) = showCon p "Three" $ showArg x ++ showArg y ++ showArg z
 103 |   showPrec p (Four x y z w) = showCon p "Four" $ showArg x ++ showArg y ++ showArg z ++ showArg w
 104 | 
 105 | Functor Digit where
 106 |   map f (One x) = One (f x)
 107 |   map f (Two x y) = Two (f x) (f y)
 108 |   map f (Three x y z) = Three (f x) (f y) (f z)
 109 |   map f (Four x y z w) = Four (f x) (f y) (f z) (f w)
 110 | 
 111 | Foldable Digit where
 112 |   foldr f init (One a) = f a init
 113 |   foldr f init (Two a b) = f a (f b init)
 114 |   foldr f init (Three a b c) = f a (f b (f c init))
 115 |   foldr f init (Four a b c d) = f a (f b (f c (f d init)))
 116 | 
 117 |   foldl f init (One a) = f init a
 118 |   foldl f init (Two a b) = f (f init a) b
 119 |   foldl f init (Three a b c) = f (f (f init a) b) c
 120 |   foldl f init (Four a b c d) = f (f (f (f init a) b) c) d
 121 | 
 122 |   null _ = False
 123 | 
 124 | Traversable Digit where
 125 |   traverse f (One x) = [| One (f x) |]
 126 |   traverse f (Two x y) = [| Two (f x) (f y) |]
 127 |   traverse f (Three x y z) = [| Three (f x) (f y) (f z) |]
 128 |   traverse f (Four x y z w) = [| Four (f x) (f y) (f z) (f w) |]
 129 | 
 130 | MeasureRM a => MeasureRM (Digit a) where
 131 |   measureRM (One x) = measureRM x
 132 |   measureRM (Two x y) = measureRM x <+> measureRM y
 133 |   measureRM (Three x y z) = measureRM x <+> measureRM y <+> measureRM z
 134 |   measureRM (Four x y z w) = measureRM x <+> measureRM y <+> measureRM z <+> measureRM w
 135 | 
 136 | data Node : Type -> Type where
 137 |   Node2 : RMFileRange -> a -> a -> Node a
 138 |   Node3 : RMFileRange -> a -> a -> a -> Node a
 139 | 
 140 | node2 : MeasureRM a => a -> a -> Node a
 141 | node2 x y = Node2 (measureRM x <+> measureRM y) x y
 142 | 
 143 | node3 : MeasureRM a => a -> a -> a -> Node a
 144 | node3 x y z = Node3 (measureRM x <+> measureRM y <+> measureRM z) x y z
 145 | 
 146 | Foldable Node where
 147 |   foldr f init (Node2 _ x y) = f x (f y init)
 148 |   foldr f init (Node3 _ x y z) = f x (f y (f z init))
 149 | 
 150 |   foldl f init (Node2 v a b) = f (f init a) b
 151 |   foldl f init (Node3 v a b c) = f (f (f init a) b) c
 152 | 
 153 | MeasureRM (Node a) where
 154 |   measureRM (Node2 v {}) = v
 155 |   measureRM (Node3 v {}) = v
 156 | 
 157 | namespace Node
 158 |   export
 159 |   map : MeasureRM b => (a -> b) -> Node a -> Node b
 160 |   map f (Node2 _ x y) = node2 (f x) (f y)
 161 |   map f (Node3 _ x y z) = node3 (f x) (f y) (f z)
 162 | 
 163 |   export
 164 |   traverse : (Applicative f, MeasureRM b) => (a -> f b) -> Node a -> f (Node b)
 165 |   traverse f (Node2 _ x y) = [| node2 (f x) (f y) |]
 166 |   traverse f (Node3 _ x y z) = [| node3 (f x) (f y) (f z) |]
 167 | 
 168 | nodeToDigit : MeasureRM a => Node a -> Digit a
 169 | nodeToDigit (Node2 _ x y) = Two x y
 170 | nodeToDigit (Node3 _ x y z) = Three x y z
 171 | 
 172 | export
 173 | data PosMap : Type -> Type where
 174 |   Empty : PosMap a
 175 |   Single : a -> PosMap a
 176 |   Deep : RMFileRange -> Digit a -> PosMap (Node a) -> Digit a -> PosMap a
 177 | 
 178 | measureTree : MeasureRM a => PosMap a -> Interval
 179 | measureTree Empty = neutral
 180 | measureTree (Single x) = cast (measureRM x)
 181 | measureTree (Deep v {}) = cast v
 182 | 
 183 | addIntervalRight : RMFileRange -> Interval -> RMFileRange
 184 | addIntervalRight range (MkInterval range') = range <+> range'
 185 | addIntervalRight range NoInterval = range
 186 | 
 187 | addIntervalLeft : Interval -> RMFileRange -> RMFileRange
 188 | addIntervalLeft (MkInterval range) range' = range <+> range'
 189 | addIntervalLeft NoInterval range' = range'
 190 | 
 191 | deep : MeasureRM a => Digit a -> PosMap (Node a) -> Digit a -> PosMap a
 192 | deep pr t sf = Deep value pr t sf
 193 |   where value : RMFileRange
 194 |         value = case measureTree t of
 195 |                      MkInterval range => measureRM pr <+> range <+> measureRM sf
 196 |                      NoInterval => measureRM pr <+> measureRM sf
 197 | 
 198 | digitToTree : MeasureRM a => Digit a -> PosMap a
 199 | digitToTree (One a) = Single a
 200 | digitToTree (Two a b) = deep (One a) Empty (One b)
 201 | digitToTree (Three a b c) = deep (Two a b) Empty (One c)
 202 | digitToTree (Four a b c d) = deep (Two a b) Empty (Two c d)
 203 | 
 204 | (<|) : MeasureRM a => a -> PosMap a -> PosMap a
 205 | a <| Empty                        = Single a
 206 | a <| (Single b)                   = deep (One a) Empty (One b)
 207 | a <| (Deep _ (One b) m sf)        = deep (Two a b) m sf
 208 | a <| (Deep _ (Two b c) m sf)      = deep (Three a b c) m sf
 209 | a <| (Deep _ (Three b c d) m sf)  = deep (Four a b c d) m sf
 210 | a <| (Deep _ (Four b c d e) m sf) = deep (Two a b) (node3 c d e <| m) sf
 211 | 
 212 | (|>) : MeasureRM a => PosMap a -> a -> PosMap a
 213 | Empty                        |> a = Single a
 214 | (Single b)                   |> a = deep (One b) Empty (One a)
 215 | (Deep _ pr m (One b))        |> a = deep pr m (Two b a)
 216 | (Deep _ pr m (Two c b))      |> a = deep pr m (Three c b a)
 217 | (Deep _ pr m (Three d c b))  |> a = deep pr m (Four d c b a)
 218 | (Deep _ pr m (Four e d c b)) |> a = deep pr (m |> node3 e d c) (Two b a)
 219 | 
 220 | export
 221 | Foldable PosMap where
 222 |   foldr f init Empty = init
 223 |   foldr f init (Single x) = f x init
 224 |   foldr f init (Deep _ pr m sf) = foldr f (foldr (flip (foldr f)) (foldr f init sf) m) pr
 225 | 
 226 |   foldl f init Empty = init
 227 |   foldl f init (Single x) = f init x
 228 |   foldl f init (Deep _ pr m sf) = foldl f (foldl (foldl f) (foldl f init pr) m) sf
 229 | 
 230 |   null Empty = True
 231 |   null (Single {}) = False
 232 |   null (Deep {}) = False
 233 | 
 234 | export
 235 | empty : PosMap a
 236 | empty = Empty
 237 | 
 238 | export
 239 | singleton : a -> PosMap a
 240 | singleton x = Single x
 241 | 
 242 | toTree : (Foldable f, MeasureRM a) => f a -> PosMap a
 243 | toTree xs = foldr (<|) empty xs
 244 | 
 245 | data ViewL : Type -> Type where
 246 |   EmptyL : ViewL a
 247 |   (<:) : a -> PosMap a -> ViewL a
 248 | 
 249 | rotl : MeasureRM a => PosMap (Node a) -> Digit a -> PosMap a
 250 | viewl : MeasureRM a => PosMap a -> ViewL a
 251 | 
 252 | rotl t sf =
 253 |   case viewl t of
 254 |        EmptyL => digitToTree sf
 255 |        a <: t' => case measureTree t of
 256 |                        MkInterval range => Deep (range <+> measureRM sf) (nodeToDigit a) t' sf
 257 |                        NoInterval => Deep (measureRM sf) (nodeToDigit a) t' sf
 258 | 
 259 | viewl Empty = EmptyL
 260 | viewl (Single x) = x <: Empty
 261 | viewl (Deep _ (One x) t sf) = x <: rotl t sf
 262 | viewl (Deep _ (Two x y) t sf) = x <: deep (One y) t sf
 263 | viewl (Deep _ (Three x y z) t sf) = x <: deep (Two y z) t sf
 264 | viewl (Deep _ (Four x y z w) t sf) = x <: deep (Three y z w) t sf
 265 | 
 266 | data ViewR : Type -> Type where
 267 |   EmptyR : ViewR a
 268 |   (:>) : PosMap a -> a -> ViewR a
 269 | 
 270 | rotr : MeasureRM a => Digit a -> PosMap (Node a) -> PosMap a
 271 | viewr : MeasureRM a => PosMap a -> ViewR a
 272 | 
 273 | rotr pr t =
 274 |   case viewr t of
 275 |        EmptyR => digitToTree pr
 276 |        t' :> a => case measureTree t of
 277 |                        MkInterval range => Deep (measureRM pr <+> range) pr t' (nodeToDigit a)
 278 |                        NoInterval => Deep (measureRM pr) pr t' (nodeToDigit a)
 279 | 
 280 | viewr Empty = EmptyR
 281 | viewr (Single x) = Empty :> x
 282 | viewr (Deep _ pr t (One x)) = rotr pr t :> x
 283 | viewr (Deep _ pr t (Two x y)) = deep pr t (One x) :> y
 284 | viewr (Deep _ pr t (Three x y z)) = deep pr t (Two x y) :> z
 285 | viewr (Deep _ pr t (Four x y z w)) = deep pr t (Three x y z) :> w
 286 | 
 287 | appendTree0 : MeasureRM a => PosMap a -> PosMap a -> PosMap a
 288 | appendTree1 : MeasureRM a => PosMap a -> a -> PosMap a -> PosMap a
 289 | appendTree2 : MeasureRM a => PosMap a -> a -> a -> PosMap a -> PosMap a
 290 | appendTree3 : MeasureRM a => PosMap a -> a -> a -> a -> PosMap a -> PosMap a
 291 | appendTree4 : MeasureRM a => PosMap a -> a -> a -> a -> a -> PosMap a -> PosMap a
 292 | addDigits0  : MeasureRM a => PosMap (Node a) -> Digit a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
 293 | addDigits1  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
 294 | addDigits2  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
 295 | addDigits3  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
 296 | addDigits4  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
 297 | 
 298 | appendTree0 Empty xs = xs
 299 | appendTree0 xs Empty = xs
 300 | appendTree0 (Single x) xs = x <| xs
 301 | appendTree0 xs (Single x) = xs |> x
 302 | appendTree0 (Deep _ pr1 t1 sf1) (Deep _ pr2 t2 sf2) = deep pr1 (addDigits0 t1 sf1 pr2 t2) sf2
 303 | 
 304 | appendTree1 Empty a xs = a <| xs
 305 | appendTree1 xs a Empty = xs |> a
 306 | appendTree1 (Single x) a xs = x <| a <| xs
 307 | appendTree1 xs a (Single x) = xs |> a |> x
 308 | appendTree1 (Deep _ pr1 t1 sf1) a (Deep _ pr2 t2 sf2) = deep pr1 (addDigits1 t1 sf1 a pr2 t2) sf2
 309 | 
 310 | appendTree2 Empty a b xs = a <| b <| xs
 311 | appendTree2 xs a b Empty = xs |> a |> b
 312 | appendTree2 (Single x) a b xs = x <| a <| b <| xs
 313 | appendTree2 xs a b (Single x) = xs |> a |> b |> x
 314 | appendTree2 (Deep _ pr1 t1 sf1) a b (Deep _ pr2 t2 sf2) = deep pr1 (addDigits2 t1 sf1 a b pr2 t2) sf2
 315 | 
 316 | appendTree3 Empty a b c xs = a <| b <| c <| xs
 317 | appendTree3 xs a b c Empty = xs |> a |> b |> c
 318 | appendTree3 (Single x) a b c xs = x <| a <| b <| c <| xs
 319 | appendTree3 xs a b c (Single x) = xs |> a |> b |> c |> x
 320 | appendTree3 (Deep _ pr1 t1 sf1) a b c (Deep _ pr2 t2 sf2) = deep pr1 (addDigits3 t1 sf1 a b c pr2 t2) sf2
 321 | 
 322 | appendTree4 Empty a b c d xs = a <| b <| c <| d <| xs
 323 | appendTree4 xs a b c d Empty = xs |> a |> b |> c |> d
 324 | appendTree4 (Single x) a b c d xs = a <| b <| c <| d <| x <| xs
 325 | appendTree4 xs a b c d (Single x) = xs |> a |> b |> c |> d |> x
 326 | appendTree4 (Deep _ pr1 m1 sf1) a b c d (Deep _ pr2 m2 sf2) = deep pr1 (addDigits4 m1 sf1 a b c d pr2 m2) sf2
 327 | 
 328 | addDigits0 t1 (One a)        (One b)        t2 = appendTree1 t1 (node2 a b) t2
 329 | addDigits0 t1 (One a)        (Two b c)      t2 = appendTree1 t1 (node3 a b c) t2
 330 | addDigits0 t1 (One a)        (Three b c d)  t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 331 | addDigits0 t1 (One a)        (Four b c d e) t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 332 | addDigits0 t1 (Two a b)      (One c)        t2 = appendTree1 t1 (node3 a b c) t2
 333 | addDigits0 t1 (Two a b)      (Two c d)      t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 334 | addDigits0 t1 (Two a b)      (Three c d e)  t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 335 | addDigits0 t1 (Two a b)      (Four c d e f) t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 336 | addDigits0 t1 (Three a b c)  (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 337 | addDigits0 t1 (Three a b c)  (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 338 | addDigits0 t1 (Three a b c)  (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 339 | addDigits0 t1 (Three a b c)  (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 340 | addDigits0 t1 (Four a b c d) (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 341 | addDigits0 t1 (Four a b c d) (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 342 | addDigits0 t1 (Four a b c d) (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 343 | addDigits0 t1 (Four a b c d) (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 344 | 
 345 | addDigits1 t1 (One a)        b (One c)        t2 = appendTree1 t1 (node3 a b c) t2
 346 | addDigits1 t1 (One a)        b (Two c d)      t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 347 | addDigits1 t1 (One a)        b (Three c d e)  t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 348 | addDigits1 t1 (One a)        b (Four c d e f) t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 349 | addDigits1 t1 (Two a b)      c (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 350 | addDigits1 t1 (Two a b)      c (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 351 | addDigits1 t1 (Two a b)      c (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 352 | addDigits1 t1 (Two a b)      c (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 353 | addDigits1 t1 (Three a b c)  d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 354 | addDigits1 t1 (Three a b c)  d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 355 | addDigits1 t1 (Three a b c)  d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 356 | addDigits1 t1 (Three a b c)  d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 357 | addDigits1 t1 (Four a b c d) e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 358 | addDigits1 t1 (Four a b c d) e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 359 | addDigits1 t1 (Four a b c d) e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 360 | addDigits1 t1 (Four a b c d) e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 361 | 
 362 | addDigits2 t1 (One a)        b c (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
 363 | addDigits2 t1 (One a)        b c (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 364 | addDigits2 t1 (One a)        b c (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 365 | addDigits2 t1 (One a)        b c (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 366 | addDigits2 t1 (Two a b)      c d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 367 | addDigits2 t1 (Two a b)      c d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 368 | addDigits2 t1 (Two a b)      c d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 369 | addDigits2 t1 (Two a b)      c d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 370 | addDigits2 t1 (Three a b c)  d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 371 | addDigits2 t1 (Three a b c)  d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 372 | addDigits2 t1 (Three a b c)  d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 373 | addDigits2 t1 (Three a b c)  d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 374 | addDigits2 t1 (Four a b c d) e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 375 | addDigits2 t1 (Four a b c d) e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 376 | addDigits2 t1 (Four a b c d) e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 377 | addDigits2 t1 (Four a b c d) e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 378 | 
 379 | addDigits3 t1 (One a)        b c d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
 380 | addDigits3 t1 (One a)        b c d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 381 | addDigits3 t1 (One a)        b c d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 382 | addDigits3 t1 (One a)        b c d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 383 | addDigits3 t1 (Two a b)      c d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 384 | addDigits3 t1 (Two a b)      c d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 385 | addDigits3 t1 (Two a b)      c d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 386 | addDigits3 t1 (Two a b)      c d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 387 | addDigits3 t1 (Three a b c)  d e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 388 | addDigits3 t1 (Three a b c)  d e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 389 | addDigits3 t1 (Three a b c)  d e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 390 | addDigits3 t1 (Three a b c)  d e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 391 | addDigits3 t1 (Four a b c d) e f g (One h)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 392 | addDigits3 t1 (Four a b c d) e f g (Two h i)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 393 | addDigits3 t1 (Four a b c d) e f g (Three h i j)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 394 | addDigits3 t1 (Four a b c d) e f g (Four h i j k) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2
 395 | 
 396 | addDigits4 t1 (One a)        b c d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
 397 | addDigits4 t1 (One a)        b c d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 398 | addDigits4 t1 (One a)        b c d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 399 | addDigits4 t1 (One a)        b c d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 400 | addDigits4 t1 (Two a b)      c d e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
 401 | addDigits4 t1 (Two a b)      c d e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 402 | addDigits4 t1 (Two a b)      c d e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 403 | addDigits4 t1 (Two a b)      c d e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 404 | addDigits4 t1 (Three a b c)  d e f g (One h)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
 405 | addDigits4 t1 (Three a b c)  d e f g (Two h i)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 406 | addDigits4 t1 (Three a b c)  d e f g (Three h i j)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 407 | addDigits4 t1 (Three a b c)  d e f g (Four h i j k) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2
 408 | addDigits4 t1 (Four a b c d) e f g h (One i)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
 409 | addDigits4 t1 (Four a b c d) e f g h (Two i j)      t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
 410 | addDigits4 t1 (Four a b c d) e f g h (Three i j k)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2
 411 | addDigits4 t1 (Four a b c d) e f g h (Four i j k l) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node3 j k l) t2
 412 | 
 413 | Split : Type -> Type -> Type
 414 | Split t a = (t, a, t)
 415 | 
 416 | data SearchResult : Type -> Type where
 417 |   Position : PosMap a -> a -> PosMap a -> SearchResult a
 418 |   OnLeft : SearchResult a
 419 |   OnRight : SearchResult a
 420 |   Nowhere : SearchResult a
 421 | 
 422 | searchDigit : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> Digit a -> Interval -> Split (Maybe (Digit a)) a
 423 | searchDigit p vl (One a) vr = (Nothing, a, Nothing)
 424 | searchDigit p vl (Two a b) vr =
 425 |   let va = vl <+> cast (measureRM a)
 426 |       vb = cast (measureRM b) <+> vr in
 427 |       if p va vb
 428 |          then (Nothing, a, Just (One b))
 429 |          else (Just (One a), b, Nothing)
 430 | searchDigit p vl (Three a b c) vr =
 431 |   let va  = vl <+> cast (measureRM a)
 432 |       vab = va <+> cast (measureRM b)
 433 |       vc  = cast (measureRM c) <+> vr
 434 |       vbc = cast (measureRM b) <+> vc in
 435 |       if p va vbc
 436 |          then (Nothing, a, Just (Two b c))
 437 |          else if p vab vc
 438 |                  then (Just (One a), b, Just (One c))
 439 |                  else (Just (Two a b), c, Nothing)
 440 | searchDigit p vl (Four a b c d) vr =
 441 |   let va   = vl <+> cast (measureRM a)
 442 |       vab  = va <+> cast (measureRM b)
 443 |       vabc = vab <+> cast (measureRM c)
 444 |       vd   = cast (measureRM d) <+> vr
 445 |       vcd  = cast (measureRM c) <+> vd
 446 |       vbcd = cast (measureRM b) <+> vcd in
 447 |       if p va vbcd
 448 |          then (Nothing, a, Just (Three b c d))
 449 |          else if p vab vcd
 450 |                  then (Just (One a), b, Just (Two c d))
 451 |                  else if p vabc vd
 452 |                          then (Just (Two a b), c, Just (One d))
 453 |                          else (Just (Three a b c), d, Nothing)
 454 | 
 455 | deepl : MeasureRM a => Maybe (Digit a) -> PosMap (Node a) -> Digit a -> PosMap a
 456 | deepl Nothing m sf = rotl m sf
 457 | deepl (Just pr) m sf = deep pr m sf
 458 | 
 459 | deepr : MeasureRM a => Digit a -> PosMap (Node a) -> Maybe (Digit a) -> PosMap a
 460 | deepr pr m Nothing = rotr pr m
 461 | deepr pr m (Just sf) = deep pr m sf
 462 | 
 463 | searchNode : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> Node a -> Interval -> Split (Maybe (Digit a)) a
 464 | searchNode p vl x vr = searchDigit p vl (nodeToDigit x) vr
 465 | 
 466 | searchTree : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> PosMap a -> Interval -> Maybe (Split (PosMap a) a)
 467 | searchTree p vl Empty vr = Nothing
 468 | searchTree p vl (Single x) vr = Just (Empty, x, Empty)
 469 | searchTree p vl (Deep _ pr m sf) vr =
 470 |   let vm   = measureTree m
 471 |       vsr  = cast (measureRM sf) <+> vr
 472 |       vmsr = vm <+> vsr
 473 |       vlp  = vl <+> cast (measureRM pr)
 474 |       vlpm = vlp <+> vm in
 475 |       if p vlp vmsr
 476 |          then let (l, x, r) = searchDigit p vl pr vmsr in
 477 |                   Just (maybe Empty digitToTree l, x, deepl r m sf)
 478 |          else if p vlpm vsr
 479 |                  then do (ml, xs, mr) <- searchTree p vlp m vsr
 480 |                          let (l, x, r) = searchNode p (vlp <+> measureTree ml) xs (measureTree mr <+> vsr)
 481 |                          Just (deepr pr ml l, x, deepl r mr sf)
 482 |                  else let (l, x, r) = searchDigit p vlpm sf vr in
 483 |                           Just (deepr pr m l, x, maybe Empty digitToTree r)
 484 | 
 485 | search' : MeasureRM a => (Interval -> Interval -> Bool) -> PosMap a -> SearchResult a
 486 | search' p t =
 487 |   let vt     = measureTree t
 488 |       pLeft  = p neutral vt
 489 |       pRight = p vt neutral in
 490 |       case (pLeft, pRight) of
 491 |            (True,  True)  => OnLeft
 492 |            (False, True)  => case searchTree p neutral t neutral of
 493 |                                   Just (l, x, r) => Position l x r
 494 |                                   Nothing => Nowhere
 495 |            (False, False) => OnRight
 496 |            (True,  False) => Nowhere
 497 | 
 498 | split : MeasureRM a => (Interval -> Bool) -> PosMap a -> (PosMap a, PosMap a)
 499 | split p Empty = (Empty, Empty)
 500 | split p xs =
 501 |   case searchTree (\a, _ => p a) neutral xs neutral of
 502 |        Just (l, x, r) => if p (measureTree xs)
 503 |                             then (l, x <| r)
 504 |                             else (xs, Empty)
 505 |        Nothing => (xs, Empty)
 506 | 
 507 | (++) : MeasureRM a => PosMap a -> PosMap a -> PosMap a
 508 | xs ++ ys = appendTree0 xs ys
 509 | 
 510 | export
 511 | map : MeasureRM b => (a -> b) -> PosMap a -> PosMap b
 512 | map f Empty = Empty
 513 | map f (Single x) = Single (f x)
 514 | map f (Deep _ pr t sf) = deep (map f pr) (map (map f) t) (map f sf)
 515 | 
 516 | export
 517 | traverse : (Applicative f, MeasureRM b) => (a -> f b) -> PosMap a -> f (PosMap b)
 518 | traverse f Empty = [| Empty |]
 519 | traverse f (Single x) = [| Single (f x) |]
 520 | traverse f (Deep _ pr t sf) = [| deep (traverse f pr) (traverse (traverse f) t) (traverse f sf) |]
 521 | 
 522 | export
 523 | takeUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a
 524 | takeUntil p = fst . split p
 525 | 
 526 | export
 527 | dropUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a
 528 | dropUntil p = snd . split p
 529 | 
 530 | export
 531 | Show a => Show (PosMap a) where
 532 |   showPrec p xs = showCon p "fromList" $ showArg (foldr (::) [] xs)
 533 | 
 534 | larger : FileRange -> Interval -> Bool
 535 | larger i (MkInterval (MkRange k _)) = k >= i
 536 | larger i NoInterval = False
 537 | 
 538 | larger' : FileRange -> Interval -> Bool
 539 | larger' i (MkInterval (MkRange k _)) = k > i
 540 | larger' i NoInterval = False
 541 | 
 542 | ||| Inserts a new element in the map, in lexicographical order.
 543 | export
 544 | insert : Measure a => a -> PosMap a -> PosMap a
 545 | insert v m = let (l, r) = split (larger (measure v)) m in l ++ (v <| r)
 546 | 
 547 | ||| Builds a new map from a list of measurable elements, inserting in
 548 | ||| lexicographical order.
 549 | export
 550 | fromList : Measure a => List a -> PosMap a
 551 | fromList = foldr insert empty
 552 | 
 553 | merge1 : Measure a => PosMap a -> PosMap a -> PosMap a
 554 | merge2 : Measure a => PosMap a -> PosMap a -> PosMap a
 555 | 
 556 | merge1 xs ys =
 557 |   case viewl xs of
 558 |        EmptyL => ys
 559 |        a <: as' => let (l, r) = split (larger (measure a)) ys in
 560 |                        l ++ (a <| assert_total (merge2 as' r))
 561 | 
 562 | merge2 xs ys =
 563 |   case viewl ys of
 564 |        EmptyL => xs
 565 |        b <: bs' => let (l, r) = split (larger' (measure b)) xs in
 566 |                        l ++ (b <| assert_total (merge1 r bs'))
 567 | 
 568 | ||| Merges two interval maps.
 569 | export
 570 | union : Measure a => PosMap a -> PosMap a -> PosMap a
 571 | union xs ys = merge1 xs ys
 572 | 
 573 | atleast : FilePos -> Interval -> Bool
 574 | atleast k (MkInterval (MkRange _ high)) = k <= high
 575 | atleast k NoInterval = False
 576 | 
 577 | greater : FilePos -> Interval -> Bool
 578 | greater k (MkInterval (MkRange low _)) = fst low > k
 579 | greater k NoInterval = False
 580 | 
 581 | ||| Finds all the intervals that overlap with the given interval.
 582 | export
 583 | inRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a
 584 | inRange low high t = matches (takeUntil (greater high) t)
 585 |   -- takeUntil selects all the intervals within the given upper bound,
 586 |   -- however the remaining interval are not necessarily adjacent in
 587 |   -- the sequence, thus it drops elements until the next intersecting
 588 |   -- interval with dropUntil.
 589 |   where matches : PosMap a -> List a
 590 |         matches xs = case viewl (dropUntil (atleast low) xs) of
 591 |                           EmptyL => []
 592 |                           x <: xs' => x :: assert_total (matches xs')
 593 | 
 594 | ||| Finds the values matching the exact interval input
 595 | export
 596 | exactRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a
 597 | exactRange low high t = flip List.mapMaybe (inRange low high t) $ \ a =>
 598 |   do let (MkRange rng _) = measureRM a
 599 |      guard (rng == (low, high))
 600 |      pure a
 601 | 
 602 | ||| Returns all the interval that contains the given point.
 603 | export
 604 | searchPos : MeasureRM a => FilePos -> PosMap a -> List a
 605 | searchPos p = inRange p p
 606 | 
 607 | ||| Returns all the intervals that intersect the given interval.
 608 | export
 609 | intersections : MeasureRM a => FileRange -> PosMap a -> List a
 610 | intersections i = inRange (fst i) (snd i)
 611 | 
 612 | ||| Returns all the intervals that contain the given interval.
 613 | export
 614 | dominators : MeasureRM a => FileRange -> PosMap a -> List a
 615 | dominators i = inRange (snd i) (fst i)
 616 | 
 617 | ||| Returns the extreme boundaries of the map, if non empty.
 618 | export
 619 | bounds : Measure a => PosMap a -> Maybe FileRange
 620 | bounds t =
 621 |   case measureTree t of
 622 |        NoInterval => Nothing
 623 |        MkInterval (MkRange _ high) =>
 624 |          case viewl t of
 625 |               EmptyL => Nothing
 626 |               x <: _ => Just (fst (measure x), high)
 627 | 
 628 | public export
 629 | Measure NonEmptyFC where
 630 |   measure = snd
 631 | 
 632 | public export
 633 | Measure (NonEmptyFC, a) where
 634 |   measure = measure . fst
 635 |