-- | Maps containing non-overlapping intervals.

module Agda.Utils.RangeMap
  ( IsBasicRangeMap(..)
  , several
  , RangeMap(..)
  , rangeMapInvariant
  , fromNonOverlappingNonEmptyAscendingList
  , insert
  , splitAt
  , insideAndOutside
  , restrictTo
  , PairInt(..)
  )
  where

import Prelude hiding (null, splitAt)

import Control.DeepSeq

import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

import Agda.Utils.Range
import Agda.Utils.List
import Agda.Utils.Null

------------------------------------------------------------------------
-- An abstraction

-- | A class that is intended to make it easy to swap between
-- different range map implementations.
--
-- Note that some 'RangeMap' operations are not included in this
-- class.

class IsBasicRangeMap a m | m -> a where

  -- | The map @'singleton' rs x@ contains the ranges from @rs@, and
  -- every position in those ranges is associated with @x@.

  singleton :: Ranges -> a -> m

  -- | Converts range maps to 'IntMap's from positions to values.

  toMap :: m -> IntMap a

  -- | Converts the map to a list. The ranges are non-overlapping and
  -- non-empty, and earlier ranges precede later ones in the list.

  toList :: m -> [(Range, a)]

  -- | Returns the smallest range covering everything in the map (or
  -- 'Nothing', if the range would be empty).
  --
  -- Note that the default implementation of this operation might be
  -- inefficient.

  coveringRange :: m -> Maybe Range
  coveringRange m
f = do
    min <- (Int, a) -> Int
forall a b. (a, b) -> a
fst ((Int, a) -> Int) -> Maybe (Int, a) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap a -> Maybe (Int, a)
forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMin IntMap a
m
    max <- fst <$> IntMap.lookupMax m
    return (Range { from = min, to = max + 1 })
    where
    m :: IntMap a
m = m -> IntMap a
forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap m
f

-- | Like 'singleton', but with several 'Ranges' instead of only one.

several ::
  (IsBasicRangeMap a hl, Monoid hl) =>
  [Ranges] -> a -> hl
several :: forall a hl.
(IsBasicRangeMap a hl, Monoid hl) =>
[Ranges] -> a -> hl
several [Ranges]
rss a
m = [hl] -> hl
forall a. Monoid a => [a] -> a
mconcat ([hl] -> hl) -> [hl] -> hl
forall a b. (a -> b) -> a -> b
$ (Ranges -> hl) -> [Ranges] -> [hl]
forall a b. (a -> b) -> [a] -> [b]
map ((Ranges -> a -> hl) -> a -> Ranges -> hl
forall a b c. (a -> b -> c) -> b -> a -> c
flip Ranges -> a -> hl
forall a m. IsBasicRangeMap a m => Ranges -> a -> m
singleton a
m) [Ranges]
rss

-- We use strict pairs.
data PairInt a = !Int :!: !a
  deriving (Int -> PairInt a -> ShowS
[PairInt a] -> ShowS
PairInt a -> String
(Int -> PairInt a -> ShowS)
-> (PairInt a -> String)
-> ([PairInt a] -> ShowS)
-> Show (PairInt a)
forall a. Show a => Int -> PairInt a -> ShowS
forall a. Show a => [PairInt a] -> ShowS
forall a. Show a => PairInt a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> PairInt a -> ShowS
showsPrec :: Int -> PairInt a -> ShowS
$cshow :: forall a. Show a => PairInt a -> String
show :: PairInt a -> String
$cshowList :: forall a. Show a => [PairInt a] -> ShowS
showList :: [PairInt a] -> ShowS
Show)

instance NFData a => NFData (PairInt a) where
  rnf :: PairInt a -> ()
rnf (Int
_ :!: a
b) = a -> ()
forall a. NFData a => a -> ()
rnf a
b

pair :: Int -> a -> PairInt a
pair :: forall a. Int -> a -> PairInt a
pair = Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
(:!:)

------------------------------------------------------------------------
-- The type

-- | Maps containing non-overlapping intervals.
--
-- The implementation does not use IntMap, because IntMap does not
-- come with a constant-time size function.
--
-- Note the invariant which 'RangeMap's should satisfy
-- ('rangeMapInvariant').

newtype RangeMap a = RangeMap
  { forall a. RangeMap a -> Map Int (PairInt a)
rangeMap :: Map Int (PairInt a)
    -- ^ The keys are starting points of ranges, and the pairs contain
    -- endpoints and values.
  }
  deriving (Int -> RangeMap a -> ShowS
[RangeMap a] -> ShowS
RangeMap a -> String
(Int -> RangeMap a -> ShowS)
-> (RangeMap a -> String)
-> ([RangeMap a] -> ShowS)
-> Show (RangeMap a)
forall a. Show a => Int -> RangeMap a -> ShowS
forall a. Show a => [RangeMap a] -> ShowS
forall a. Show a => RangeMap a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RangeMap a -> ShowS
showsPrec :: Int -> RangeMap a -> ShowS
$cshow :: forall a. Show a => RangeMap a -> String
show :: RangeMap a -> String
$cshowList :: forall a. Show a => [RangeMap a] -> ShowS
showList :: [RangeMap a] -> ShowS
Show, RangeMap a -> ()
(RangeMap a -> ()) -> NFData (RangeMap a)
forall a. NFData a => RangeMap a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => RangeMap a -> ()
rnf :: RangeMap a -> ()
NFData)

-- | Invariant for 'RangeMap'.
--
-- The ranges must not be empty, and they must not overlap.

rangeMapInvariant :: RangeMap a -> Bool
rangeMapInvariant :: forall a. RangeMap a -> Bool
rangeMapInvariant RangeMap a
f = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Range -> Bool
rangeInvariant [Range]
rs
  , (Range -> Bool) -> [Range] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Range -> Bool) -> Range -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Bool
forall a. Null a => a -> Bool
null) [Range]
rs
  , [Range] -> Bool -> (Range -> [Range] -> Bool) -> Bool
forall a b. [a] -> b -> (a -> [a] -> b) -> b
caseList [Range]
rs Bool
True ((Range -> [Range] -> Bool) -> Bool)
-> (Range -> [Range] -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ Range
r [Range]
rs' ->
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Bool) -> [Int] -> [Int] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(<=) ((Range -> Int) -> [Range] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
to ([Range] -> [Int]) -> [Range] -> [Int]
forall a b. (a -> b) -> a -> b
$ Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
init1 Range
r [Range]
rs') ((Range -> Int) -> [Range] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Int
from [Range]
rs')
  ]
  where
  rs :: [Range]
rs = ((Range, a) -> Range) -> [(Range, a)] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (Range, a) -> Range
forall a b. (a, b) -> a
fst ([(Range, a)] -> [Range]) -> [(Range, a)] -> [Range]
forall a b. (a -> b) -> a -> b
$ RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList RangeMap a
f

------------------------------------------------------------------------
-- Construction, conversion and inspection

instance Null (RangeMap a) where
  empty :: RangeMap a
empty = RangeMap { rangeMap :: Map Int (PairInt a)
rangeMap = Map Int (PairInt a)
forall k a. Map k a
Map.empty }
  null :: RangeMap a -> Bool
null  = Map Int (PairInt a) -> Bool
forall k a. Map k a -> Bool
Map.null (Map Int (PairInt a) -> Bool)
-> (RangeMap a -> Map Int (PairInt a)) -> RangeMap a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap

instance IsBasicRangeMap a (RangeMap a) where
  singleton :: Ranges -> a -> RangeMap a
singleton (Ranges [Range]
rs) a
m =
    RangeMap { rangeMap :: Map Int (PairInt a)
rangeMap = [(Int, PairInt a)] -> Map Int (PairInt a)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(Int, PairInt a)]
rms }
    where
    rms :: [(Int, PairInt a)]
rms =
      [ (Range -> Int
from Range
r, Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m)
      | Range
r <- [Range]
rs
      , Bool -> Bool
not (Range -> Bool
forall a. Null a => a -> Bool
null Range
r)
      ]

  toMap :: RangeMap a -> IntMap a
toMap RangeMap a
f =
    [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
      [ (Int
p, a
m)
      | (Range
r, a
m) <- RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList RangeMap a
f
      , Int
p <- Range -> [Int]
rangeToPositions Range
r
      ]

  toList :: RangeMap a -> [(Range, a)]
toList =
    ((Int, PairInt a) -> (Range, a))
-> [(Int, PairInt a)] -> [(Range, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Int
f, Int
t :!: a
a) -> (Range{ from :: Int
from = Int
f, to :: Int
to = Int
t }, a
a)) ([(Int, PairInt a)] -> [(Range, a)])
-> (RangeMap a -> [(Int, PairInt a)]) -> RangeMap a -> [(Range, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Map Int (PairInt a) -> [(Int, PairInt a)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map Int (PairInt a) -> [(Int, PairInt a)])
-> (RangeMap a -> Map Int (PairInt a))
-> RangeMap a
-> [(Int, PairInt a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap

  coveringRange :: RangeMap a -> Maybe Range
coveringRange RangeMap a
f = do
    min <- (Int, PairInt a) -> Int
forall a b. (a, b) -> a
fst ((Int, PairInt a) -> Int) -> Maybe (Int, PairInt a) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Int (PairInt a) -> Maybe (Int, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMin (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
f)
    max <- (\ (Int
_, Int
p :!: a
_) -> Int
p) <$> Map.lookupMax (rangeMap f)
    return (Range { from = min, to = max })

-- | Converts a list of pairs of ranges and values to a 'RangeMap'.
-- The ranges have to be non-overlapping and non-empty, and earlier
-- ranges have to precede later ones.

fromNonOverlappingNonEmptyAscendingList :: [(Range, a)] -> RangeMap a
fromNonOverlappingNonEmptyAscendingList :: forall a. [(Range, a)] -> RangeMap a
fromNonOverlappingNonEmptyAscendingList =
  Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> ([(Range, a)] -> Map Int (PairInt a))
-> [(Range, a)]
-> RangeMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  [(Int, PairInt a)] -> Map Int (PairInt a)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(Int, PairInt a)] -> Map Int (PairInt a))
-> ([(Range, a)] -> [(Int, PairInt a)])
-> [(Range, a)]
-> Map Int (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ((Range, a) -> (Int, PairInt a))
-> [(Range, a)] -> [(Int, PairInt a)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Range
r, a
m) -> (Range -> Int
from Range
r, Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m))

-- | The number of ranges in the map.
--
-- This function should not be exported.

size :: RangeMap a -> Int
size :: forall a. RangeMap a -> Int
size = Map Int (PairInt a) -> Int
forall k a. Map k a -> Int
Map.size (Map Int (PairInt a) -> Int)
-> (RangeMap a -> Map Int (PairInt a)) -> RangeMap a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap

------------------------------------------------------------------------
-- Merging

-- | Inserts a value, along with a corresponding 'Range', into a
-- 'RangeMap'. No attempt is made to merge adjacent ranges with equal
-- values.
--
-- The function argument is used to combine values. The inserted value
-- is given as the first argument to the function.

insert :: (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert :: forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
combine Range
r a
m (RangeMap Map Int (PairInt a)
f)
  | Range -> Bool
forall a. Null a => a -> Bool
null Range
r    = Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap Map Int (PairInt a)
f
  | Bool
otherwise =
    case Maybe (PairInt a)
equal of
      Just (Int
p :!: a
m') ->
        case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Int
to Range
r) Int
p of
          Ordering
EQ ->
            -- The range r matches exactly.
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') Map Int (PairInt a)
f
          Ordering
LT ->
            -- The range r is strictly shorter.
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
to Range
r) (Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') Map Int (PairInt a)
f
          Ordering
GT ->
            -- The range r is strictly longer. Continue recursively.
            (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
combine (Range { from :: Int
from = Int
p, to :: Int
to = Range -> Int
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') Map Int (PairInt a)
f
      Maybe (PairInt a)
Nothing ->
        -- Find the part of r that does not overlap with anything in
        -- smaller or larger, if any.
        case (Maybe (Int, PairInt a)
overlapLeft, Maybe Int
overlapRight) of
          (Maybe (Int, PairInt a)
Nothing, Maybe Int
Nothing) ->
            -- No overlap.
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m) Map Int (PairInt a)
f
          (Maybe (Int, PairInt a)
Nothing, Just Int
p) ->
            -- Overlap on the right. Continue recursively.
            (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
combine (Range { from :: Int
from = Int
p, to :: Int
to = Range -> Int
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m) Map Int (PairInt a)
f
          (Just (Int
p1, Int
p2 :!: a
m'), Just Int
p3) ->
            -- Overlap on both sides. Continue recursively.
            (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
combine (Range { from :: Int
from = Int
p3, to :: Int
to = Range -> Int
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            (if Int
p2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
p3 then
               -- The left range ends exactly where the right range
               -- starts.
               Map Int (PairInt a) -> Map Int (PairInt a)
forall a. a -> a
id
             else
               -- There is something between the left and right
               -- ranges.
               Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p2 (Int
p3 Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m)) (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Int
p2 Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p1 (Range -> Int
from Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') Map Int (PairInt a)
f
          (Just (Int
p1, Int
p2 :!: a
m'), Maybe Int
Nothing) ->
            case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
p2 (Range -> Int
to Range
r) of
              Ordering
LT ->
                -- Overlap on the left, the left range ends before r.
                Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p2 (Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m) (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Int
p2 Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p1 (Range -> Int
from Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') Map Int (PairInt a)
f
              Ordering
EQ ->
                -- Overlap on the left, the left range ends where r
                -- ends.
                Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p1 (Range -> Int
from Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') Map Int (PairInt a)
f
              Ordering
GT ->
                -- Overlap on the left, the left range ends after r.
                Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
to Range
r) (Int
p2 Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Int
from Range
r) (Range -> Int
to Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a -> a -> a
combine a
m a
m') (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p1 (Range -> Int
from Range
r Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m') Map Int (PairInt a)
f
    where
    (Map Int (PairInt a)
smaller, Maybe (PairInt a)
equal, Map Int (PairInt a)
larger) = Int
-> Map Int (PairInt a)
-> (Map Int (PairInt a), Maybe (PairInt a), Map Int (PairInt a))
forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup (Range -> Int
from Range
r) Map Int (PairInt a)
f

    overlapRight :: Maybe Int
overlapRight = case Map Int (PairInt a) -> Maybe (Int, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMin Map Int (PairInt a)
larger of
      Maybe (Int, PairInt a)
Nothing -> Maybe Int
forall a. Maybe a
Nothing
      Just (Int
from, PairInt a
_)
        | Int
from Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Range -> Int
to Range
r -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
from
        | Bool
otherwise   -> Maybe Int
forall a. Maybe a
Nothing

    overlapLeft :: Maybe (Int, PairInt a)
overlapLeft = case Map Int (PairInt a) -> Maybe (Int, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map Int (PairInt a)
smaller of
      Maybe (Int, PairInt a)
Nothing -> Maybe (Int, PairInt a)
forall a. Maybe a
Nothing
      Just s :: (Int, PairInt a)
s@(Int
_, Int
to :!: a
_)
        | Range -> Int
from Range
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
to -> (Int, PairInt a) -> Maybe (Int, PairInt a)
forall a. a -> Maybe a
Just (Int, PairInt a)
s
        | Bool
otherwise   -> Maybe (Int, PairInt a)
forall a. Maybe a
Nothing

-- | Merges 'RangeMap's by inserting every \"piece\" of the smaller
-- one into the larger one.

instance Semigroup a => Semigroup (RangeMap a) where
  RangeMap a
f1 <> :: RangeMap a -> RangeMap a -> RangeMap a
<> RangeMap a
f2
    | RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
f1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
f2 =
      ((Range, a) -> RangeMap a -> RangeMap a)
-> RangeMap a -> [(Range, a)] -> RangeMap a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Range -> a -> RangeMap a -> RangeMap a)
-> (Range, a) -> RangeMap a -> RangeMap a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Range -> a -> RangeMap a -> RangeMap a)
 -> (Range, a) -> RangeMap a -> RangeMap a)
-> (Range -> a -> RangeMap a -> RangeMap a)
-> (Range, a)
-> RangeMap a
-> RangeMap a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)) RangeMap a
f2 (RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList RangeMap a
f1)
    | Bool
otherwise =
      ((Range, a) -> RangeMap a -> RangeMap a)
-> RangeMap a -> [(Range, a)] -> RangeMap a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Range -> a -> RangeMap a -> RangeMap a)
-> (Range, a) -> RangeMap a -> RangeMap a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Range -> a -> RangeMap a -> RangeMap a)
 -> (Range, a) -> RangeMap a -> RangeMap a)
-> (Range -> a -> RangeMap a -> RangeMap a)
-> (Range, a)
-> RangeMap a
-> RangeMap a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert ((a -> a -> a) -> a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>))) RangeMap a
f1 (RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList RangeMap a
f2)

-- | Merges 'RangeMap's by inserting every \"piece\" of the smaller
-- one into the larger one.

instance Semigroup a => Monoid (RangeMap a) where
  mempty :: RangeMap a
mempty  = RangeMap a
forall a. Null a => a
empty
  mappend :: RangeMap a -> RangeMap a -> RangeMap a
mappend = RangeMap a -> RangeMap a -> RangeMap a
forall a. Semigroup a => a -> a -> a
(<>)

------------------------------------------------------------------------
-- Splitting

-- | The value of @'splitAt' p f@ is a pair @(f1, f2)@ which contains
-- everything from @f@. All the positions in @f1@ are less than @p@,
-- and all the positions in @f2@ are greater than or equal to @p@.

splitAt :: Int -> RangeMap a -> (RangeMap a, RangeMap a)
splitAt :: forall a. Int -> RangeMap a -> (RangeMap a, RangeMap a)
splitAt Int
p RangeMap a
f = (RangeMap a
before, RangeMap a
after)
  where
  (RangeMap a
before, Maybe ((Int, PairInt a), (Int, PairInt a))
_, RangeMap a
after) = Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
forall a.
Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
splitAt' Int
p RangeMap a
f

-- | A variant of 'splitAt'. If a range in the middle was split into
-- two pieces, then those two pieces are returned.

splitAt' ::
  Int -> RangeMap a ->
  ( RangeMap a
  , Maybe ((Int, PairInt a), (Int, PairInt a))
  , RangeMap a
  )
splitAt' :: forall a.
Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
splitAt' Int
p (RangeMap Map Int (PairInt a)
f) =
  case Maybe (PairInt a)
equal of
    Just PairInt a
r  -> ( Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap Map Int (PairInt a)
maybeOverlapping
               , Maybe ((Int, PairInt a), (Int, PairInt a))
forall a. Maybe a
Nothing
               , Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p PairInt a
r Map Int (PairInt a)
larger)
               )
    Maybe (PairInt a)
Nothing ->
      -- Check if maybeOverlapping overlaps with p.
      case Map Int (PairInt a)
-> Maybe ((Int, PairInt a), Map Int (PairInt a))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey Map Int (PairInt a)
maybeOverlapping of
        Maybe ((Int, PairInt a), Map Int (PairInt a))
Nothing ->
          (RangeMap a
forall a. Null a => a
empty, Maybe ((Int, PairInt a), (Int, PairInt a))
forall a. Maybe a
Nothing, Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap Map Int (PairInt a)
larger)
        Just ((Int
from, Int
to :!: a
m), Map Int (PairInt a)
smaller)
          | Int
to Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
p ->
            ( Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap Map Int (PairInt a)
maybeOverlapping
            , Maybe ((Int, PairInt a), (Int, PairInt a))
forall a. Maybe a
Nothing
            , Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap Map Int (PairInt a)
larger
            )
          | Bool
otherwise ->
            -- Here from < p < to.
            ( Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
from (Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m) Map Int (PairInt a)
smaller)
            , ((Int, PairInt a), (Int, PairInt a))
-> Maybe ((Int, PairInt a), (Int, PairInt a))
forall a. a -> Maybe a
Just ((Int
from, Int
p Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m), (Int
p, Int
to Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m))
            , Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
p (Int
to Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
:!: a
m) Map Int (PairInt a)
larger)
            )
  where
  (Map Int (PairInt a)
maybeOverlapping, Maybe (PairInt a)
equal, Map Int (PairInt a)
larger) = Int
-> Map Int (PairInt a)
-> (Map Int (PairInt a), Maybe (PairInt a), Map Int (PairInt a))
forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup Int
p Map Int (PairInt a)
f

-- | Returns a 'RangeMap' overlapping the given range, as well as the
-- rest of the map.

insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
insideAndOutside :: forall a. Range -> RangeMap a -> (RangeMap a, RangeMap a)
insideAndOutside Range
r RangeMap a
f
  | Range -> Int
from Range
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Range -> Int
to Range
r = (RangeMap a
forall a. Null a => a
empty, RangeMap a
f)
  | Bool
otherwise      =
    ( RangeMap a
middle
    , -- Because it takes so long to recompile Agda with all
      -- optimisations and run a benchmark no experimental
      -- verification has been made that the code below is better than
      -- reasonable variants. Perhaps it would make sense to benchmark
      -- RangeMap independently of Agda.
      if RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
before Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
middle Bool -> Bool -> Bool
|| RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
after Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< RangeMap a -> Int
forall a. RangeMap a -> Int
size RangeMap a
middle then
        Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$ Map Int (PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
before) (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
after)
      else
        -- If the number of pieces in the middle is "small", remove
        -- the pieces from f instead of merging before and after.
        Map Int (PairInt a) -> RangeMap a
forall a. Map Int (PairInt a) -> RangeMap a
RangeMap (Map Int (PairInt a) -> RangeMap a)
-> Map Int (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
        (Map Int (PairInt a) -> Map Int (PairInt a))
-> (((Int, PairInt a), (Int, PairInt a))
    -> Map Int (PairInt a) -> Map Int (PairInt a))
-> Maybe ((Int, PairInt a), (Int, PairInt a))
-> Map Int (PairInt a)
-> Map Int (PairInt a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map Int (PairInt a) -> Map Int (PairInt a)
forall a. a -> a
id ((Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a))
-> (Int, PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((Int, PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a))
-> (((Int, PairInt a), (Int, PairInt a)) -> (Int, PairInt a))
-> ((Int, PairInt a), (Int, PairInt a))
-> Map Int (PairInt a)
-> Map Int (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, PairInt a), (Int, PairInt a)) -> (Int, PairInt a)
forall a b. (a, b) -> b
snd) Maybe ((Int, PairInt a), (Int, PairInt a))
split1 (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
        (Map Int (PairInt a) -> Map Int (PairInt a))
-> (((Int, PairInt a), (Int, PairInt a))
    -> Map Int (PairInt a) -> Map Int (PairInt a))
-> Maybe ((Int, PairInt a), (Int, PairInt a))
-> Map Int (PairInt a)
-> Map Int (PairInt a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map Int (PairInt a) -> Map Int (PairInt a)
forall a. a -> a
id ((Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a))
-> (Int, PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> PairInt a -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((Int, PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a))
-> (((Int, PairInt a), (Int, PairInt a)) -> (Int, PairInt a))
-> ((Int, PairInt a), (Int, PairInt a))
-> Map Int (PairInt a)
-> Map Int (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, PairInt a), (Int, PairInt a)) -> (Int, PairInt a)
forall a b. (a, b) -> a
fst) Maybe ((Int, PairInt a), (Int, PairInt a))
split2 (Map Int (PairInt a) -> Map Int (PairInt a))
-> Map Int (PairInt a) -> Map Int (PairInt a)
forall a b. (a -> b) -> a -> b
$
        Map Int (PairInt a) -> Map Int (PairInt a) -> Map Int (PairInt a)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
f) (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
middle)
    )
  where
  (RangeMap a
beforeMiddle, Maybe ((Int, PairInt a), (Int, PairInt a))
split1, RangeMap a
after) = Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
forall a.
Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
splitAt' (Range -> Int
to Range
r) RangeMap a
f
  (RangeMap a
before, Maybe ((Int, PairInt a), (Int, PairInt a))
split2, RangeMap a
middle)      = Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
forall a.
Int
-> RangeMap a
-> (RangeMap a, Maybe ((Int, PairInt a), (Int, PairInt a)),
    RangeMap a)
splitAt' (Range -> Int
from Range
r) RangeMap a
beforeMiddle

-- | Restricts the 'RangeMap' to the given range.

restrictTo :: Range -> RangeMap a -> RangeMap a
restrictTo :: forall a. Range -> RangeMap a -> RangeMap a
restrictTo Range
r = (RangeMap a, RangeMap a) -> RangeMap a
forall a b. (a, b) -> a
fst ((RangeMap a, RangeMap a) -> RangeMap a)
-> (RangeMap a -> (RangeMap a, RangeMap a))
-> RangeMap a
-> RangeMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> RangeMap a -> (RangeMap a, RangeMap a)
forall a. Range -> RangeMap a -> (RangeMap a, RangeMap a)
insideAndOutside Range
r