-- | Maps containing non-overlapping intervals.

module Agda.Utils.RangeMap
  ( IsBasicRangeMap(..)
  , several
  , PairInt(..)
  , RangeMap(..)
  , rangeMapInvariant
  , fromNonOverlappingNonEmptyAscendingList
  , insert
  , splitAt
  , insideAndOutside
  , restrictTo
  )
  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 Data.Semigroup

import Data.Strict.Tuple (Pair(..))

import Agda.Interaction.Highlighting.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
    Key
min <- (Key, a) -> Key
forall a b. (a, b) -> a
fst ((Key, a) -> Key) -> Maybe (Key, a) -> Maybe Key
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap a -> Maybe (Key, a)
forall a. IntMap a -> Maybe (Key, a)
IntMap.lookupMin IntMap a
m
    Key
max <- (Key, a) -> Key
forall a b. (a, b) -> a
fst ((Key, a) -> Key) -> Maybe (Key, a) -> Maybe Key
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntMap a -> Maybe (Key, a)
forall a. IntMap a -> Maybe (Key, a)
IntMap.lookupMax IntMap a
m
    Range -> Maybe Range
forall (m :: * -> *) a. Monad m => a -> m a
return (Range :: Key -> Key -> Range
Range { from :: Key
from = Key
min, to :: Key
to = Key
max Key -> Key -> Key
forall a. Num a => a -> a -> a
+ Key
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 :: [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

------------------------------------------------------------------------
-- A strict pair type

-- | A strict pair type where the first argument must be an 'Int'.
--
-- This type is included because there is no 'NFData' instance for
-- 'Pair' in the package @strict@ before version 4.

newtype PairInt a = PairInt (Pair Int a)
  deriving Key -> PairInt a -> ShowS
[PairInt a] -> ShowS
PairInt a -> String
(Key -> PairInt a -> ShowS)
-> (PairInt a -> String)
-> ([PairInt a] -> ShowS)
-> Show (PairInt a)
forall a. Show a => Key -> PairInt a -> ShowS
forall a. Show a => [PairInt a] -> ShowS
forall a. Show a => PairInt a -> String
forall a.
(Key -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PairInt a] -> ShowS
$cshowList :: forall a. Show a => [PairInt a] -> ShowS
show :: PairInt a -> String
$cshow :: forall a. Show a => PairInt a -> String
showsPrec :: Key -> PairInt a -> ShowS
$cshowsPrec :: forall a. Show a => Key -> PairInt a -> ShowS
Show

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

-- | Constructs a pair.

pair :: Int -> a -> PairInt a
pair :: Key -> a -> PairInt a
pair Key
x a
y = Pair Key a -> PairInt a
forall a. Pair Key a -> PairInt a
PairInt (Key
x Key -> a -> Pair Key a
forall a b. a -> b -> Pair a b
:!: a
y)

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

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

rangeMapInvariant :: RangeMap a -> Bool
rangeMapInvariant :: 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
$ (Key -> Key -> Bool) -> [Key] -> [Key] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
(<=) ((Range -> Key) -> [Range] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Key
to ([Range] -> [Key]) -> [Range] -> [Key]
forall a b. (a -> b) -> a -> b
$ Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
init1 Range
r [Range]
rs') ((Range -> Key) -> [Range] -> [Key]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Key
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 :: forall a. Map Key (PairInt a) -> RangeMap a
RangeMap { rangeMap :: Map Key (PairInt a)
rangeMap = Map Key (PairInt a)
forall k a. Map k a
Map.empty }
  null :: RangeMap a -> Bool
null  = Map Key (PairInt a) -> Bool
forall k a. Map k a -> Bool
Map.null (Map Key (PairInt a) -> Bool)
-> (RangeMap a -> Map Key (PairInt a)) -> RangeMap a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap

instance IsBasicRangeMap a (RangeMap a) where
  singleton :: Ranges -> a -> RangeMap a
singleton (Ranges [Range]
rs) a
m =
    RangeMap :: forall a. Map Key (PairInt a) -> RangeMap a
RangeMap { rangeMap :: Map Key (PairInt a)
rangeMap = [(Key, PairInt a)] -> Map Key (PairInt a)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(Key, PairInt a)]
rms }
    where
    rms :: [(Key, PairInt a)]
rms =
      [ (Range -> Key
from Range
r, Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) 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 =
    [(Key, a)] -> IntMap a
forall a. [(Key, a)] -> IntMap a
IntMap.fromList
      [ (Key
p, a
m)
      | (Range
r, a
m) <- RangeMap a -> [(Range, a)]
forall a m. IsBasicRangeMap a m => m -> [(Range, a)]
toList RangeMap a
f
      , Key
p <- Range -> [Key]
rangeToPositions Range
r
      ]

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

  coveringRange :: RangeMap a -> Maybe Range
coveringRange RangeMap a
f = do
    Key
min <- (Key, PairInt a) -> Key
forall a b. (a, b) -> a
fst ((Key, PairInt a) -> Key) -> Maybe (Key, PairInt a) -> Maybe Key
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Key (PairInt a) -> Maybe (Key, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMin (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap RangeMap a
f)
    Key
max <- (\(Key
_, PairInt (Key
p :!: a
_)) -> Key
p) ((Key, PairInt a) -> Key) -> Maybe (Key, PairInt a) -> Maybe Key
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Key (PairInt a) -> Maybe (Key, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap RangeMap a
f)
    Range -> Maybe Range
forall (m :: * -> *) a. Monad m => a -> m a
return (Range :: Key -> Key -> Range
Range { from :: Key
from = Key
min, to :: Key
to = Key
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 :: [(Range, a)] -> RangeMap a
fromNonOverlappingNonEmptyAscendingList =
  Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> ([(Range, a)] -> Map Key (PairInt a))
-> [(Range, a)]
-> RangeMap a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  [(Key, PairInt a)] -> Map Key (PairInt a)
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(Key, PairInt a)] -> Map Key (PairInt a))
-> ([(Range, a)] -> [(Key, PairInt a)])
-> [(Range, a)]
-> Map Key (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ((Range, a) -> (Key, PairInt a))
-> [(Range, a)] -> [(Key, PairInt a)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Range
r, a
m) -> (Range -> Key
from Range
r, Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) a
m))

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

size :: RangeMap a -> Int
size :: RangeMap a -> Key
size = Map Key (PairInt a) -> Key
forall k a. Map k a -> Key
Map.size (Map Key (PairInt a) -> Key)
-> (RangeMap a -> Map Key (PairInt a)) -> RangeMap a -> Key
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (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 :: (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
insert a -> a -> a
combine Range
r a
m (RangeMap Map Key (PairInt a)
f)
  | Range -> Bool
forall a. Null a => a -> Bool
null Range
r    = Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap Map Key (PairInt a)
f
  | Bool
otherwise =
    case Maybe (PairInt a)
equal of
      Just (PairInt (Key
p :!: a
m')) ->
        case Key -> Key -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Key
to Range
r) Key
p of
          Ordering
EQ ->
            -- The range r matches exactly.
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p (a -> a -> a
combine a
m a
m')) Map Key (PairInt a)
f
          Ordering
LT ->
            -- The range r is strictly shorter.
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
to Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p a
m') (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) (a -> a -> a
combine a
m a
m')) Map Key (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 :: Key -> Key -> Range
Range { from :: Key
from = Key
p, to :: Key
to = Range -> Key
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p (a -> a -> a
combine a
m a
m')) Map Key (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 (Key, PairInt a)
overlapLeft, Maybe Key
overlapRight) of
          (Maybe (Key, PairInt a)
Nothing, Maybe Key
Nothing) ->
            -- No overlap.
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) a
m) Map Key (PairInt a)
f
          (Maybe (Key, PairInt a)
Nothing, Just Key
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 :: Key -> Key -> Range
Range { from :: Key
from = Key
p, to :: Key
to = Range -> Key
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p a
m) Map Key (PairInt a)
f
          (Just (Key
p1, PairInt (Key
p2 :!: a
m')), Just Key
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 :: Key -> Key -> Range
Range { from :: Key
from = Key
p3, to :: Key
to = Range -> Key
to Range
r }) a
m (RangeMap a -> RangeMap a) -> RangeMap a -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
            (if Key
p2 Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
p3 then
               -- The left range ends exactly where the right range
               -- starts.
               Map Key (PairInt a) -> Map Key (PairInt a)
forall a. a -> a
id
             else
               -- There is something between the left and right
               -- ranges.
               Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p2 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p3 a
m)) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p2 (a -> a -> a
combine a
m a
m')) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
            Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p1 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
from Range
r) a
m') Map Key (PairInt a)
f
          (Just (Key
p1, PairInt (Key
p2 :!: a
m')), Maybe Key
Nothing) ->
            case Key -> Key -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Key
p2 (Range -> Key
to Range
r) of
              Ordering
LT ->
                -- Overlap on the left, the left range ends before r.
                Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p2 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) a
m) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p2 (a -> a -> a
combine a
m a
m')) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p1 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
from Range
r) a
m') Map Key (PairInt a)
f
              Ordering
EQ ->
                -- Overlap on the left, the left range ends where r
                -- ends.
                Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) (a -> a -> a
combine a
m a
m')) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p1 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
from Range
r) a
m') Map Key (PairInt a)
f
              Ordering
GT ->
                -- Overlap on the left, the left range ends after r.
                Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
to Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p2 a
m') (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Range -> Key
from Range
r) (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
to Range
r) (a -> a -> a
combine a
m a
m')) (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
                Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p1 (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair (Range -> Key
from Range
r) a
m') Map Key (PairInt a)
f
    where
    (Map Key (PairInt a)
smaller, Maybe (PairInt a)
equal, Map Key (PairInt a)
larger) = Key
-> Map Key (PairInt a)
-> (Map Key (PairInt a), Maybe (PairInt a), Map Key (PairInt a))
forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup (Range -> Key
from Range
r) Map Key (PairInt a)
f

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

    overlapLeft :: Maybe (Key, PairInt a)
overlapLeft = case Map Key (PairInt a) -> Maybe (Key, PairInt a)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map Key (PairInt a)
smaller of
      Maybe (Key, PairInt a)
Nothing -> Maybe (Key, PairInt a)
forall a. Maybe a
Nothing
      Just s :: (Key, PairInt a)
s@(Key
_, PairInt (Key
to :!: a
_))
        | Range -> Key
from Range
r Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
< Key
to -> (Key, PairInt a) -> Maybe (Key, PairInt a)
forall a. a -> Maybe a
Just (Key, PairInt a)
s
        | Bool
otherwise   -> Maybe (Key, 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 -> Key
forall a. RangeMap a -> Key
size RangeMap a
f1 Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
<= RangeMap a -> Key
forall a. RangeMap a -> Key
size RangeMap a
f2 =
      ((Range, a) -> RangeMap a -> RangeMap a)
-> RangeMap a -> [(Range, a)] -> RangeMap a
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 (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 :: Key -> RangeMap a -> (RangeMap a, RangeMap a)
splitAt Key
p RangeMap a
f = (RangeMap a
before, RangeMap a
after)
  where
  (RangeMap a
before, Maybe ((Key, PairInt a), (Key, PairInt a))
_, RangeMap a
after) = Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
forall a.
Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
splitAt' Key
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' :: Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
splitAt' Key
p (RangeMap Map Key (PairInt a)
f) =
  case Maybe (PairInt a)
equal of
    Just PairInt a
r  -> ( Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap Map Key (PairInt a)
maybeOverlapping
               , Maybe ((Key, PairInt a), (Key, PairInt a))
forall a. Maybe a
Nothing
               , Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p PairInt a
r Map Key (PairInt a)
larger)
               )
    Maybe (PairInt a)
Nothing ->
      -- Check if maybeOverlapping overlaps with p.
      case Map Key (PairInt a)
-> Maybe ((Key, PairInt a), Map Key (PairInt a))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey Map Key (PairInt a)
maybeOverlapping of
        Maybe ((Key, PairInt a), Map Key (PairInt a))
Nothing ->
          (RangeMap a
forall a. Null a => a
empty, Maybe ((Key, PairInt a), (Key, PairInt a))
forall a. Maybe a
Nothing, Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap Map Key (PairInt a)
larger)
        Just ((Key
from, PairInt (Key
to :!: a
m)), Map Key (PairInt a)
smaller)
          | Key
to Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
<= Key
p ->
            ( Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap Map Key (PairInt a)
maybeOverlapping
            , Maybe ((Key, PairInt a), (Key, PairInt a))
forall a. Maybe a
Nothing
            , Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap Map Key (PairInt a)
larger
            )
          | Bool
otherwise ->
            -- Here from < p < to.
            ( Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
from (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p a
m) Map Key (PairInt a)
smaller)
            , ((Key, PairInt a), (Key, PairInt a))
-> Maybe ((Key, PairInt a), (Key, PairInt a))
forall a. a -> Maybe a
Just ((Key
from, Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
p a
m), (Key
p, Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
to a
m))
            , Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Key
p (Key -> a -> PairInt a
forall a. Key -> a -> PairInt a
pair Key
to a
m) Map Key (PairInt a)
larger)
            )
  where
  (Map Key (PairInt a)
maybeOverlapping, Maybe (PairInt a)
equal, Map Key (PairInt a)
larger) = Key
-> Map Key (PairInt a)
-> (Map Key (PairInt a), Maybe (PairInt a), Map Key (PairInt a))
forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup Key
p Map Key (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 :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
insideAndOutside Range
r RangeMap a
f
  | Range -> Key
from Range
r Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Range -> Key
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 -> Key
forall a. RangeMap a -> Key
size RangeMap a
before Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
< RangeMap a -> Key
forall a. RangeMap a -> Key
size RangeMap a
middle Bool -> Bool -> Bool
|| RangeMap a -> Key
forall a. RangeMap a -> Key
size RangeMap a
after Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
< RangeMap a -> Key
forall a. RangeMap a -> Key
size RangeMap a
middle then
        Map Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$ Map Key (PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap RangeMap a
before) (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (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 Key (PairInt a) -> RangeMap a
forall a. Map Key (PairInt a) -> RangeMap a
RangeMap (Map Key (PairInt a) -> RangeMap a)
-> Map Key (PairInt a) -> RangeMap a
forall a b. (a -> b) -> a -> b
$
        (Map Key (PairInt a) -> Map Key (PairInt a))
-> (((Key, PairInt a), (Key, PairInt a))
    -> Map Key (PairInt a) -> Map Key (PairInt a))
-> Maybe ((Key, PairInt a), (Key, PairInt a))
-> Map Key (PairInt a)
-> Map Key (PairInt a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map Key (PairInt a) -> Map Key (PairInt a)
forall a. a -> a
id ((Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a))
-> (Key, PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((Key, PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a))
-> (((Key, PairInt a), (Key, PairInt a)) -> (Key, PairInt a))
-> ((Key, PairInt a), (Key, PairInt a))
-> Map Key (PairInt a)
-> Map Key (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Key, PairInt a), (Key, PairInt a)) -> (Key, PairInt a)
forall a b. (a, b) -> b
snd) Maybe ((Key, PairInt a), (Key, PairInt a))
split1 (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
        (Map Key (PairInt a) -> Map Key (PairInt a))
-> (((Key, PairInt a), (Key, PairInt a))
    -> Map Key (PairInt a) -> Map Key (PairInt a))
-> Maybe ((Key, PairInt a), (Key, PairInt a))
-> Map Key (PairInt a)
-> Map Key (PairInt a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map Key (PairInt a) -> Map Key (PairInt a)
forall a. a -> a
id ((Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a))
-> (Key, PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Key -> PairInt a -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ((Key, PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a))
-> (((Key, PairInt a), (Key, PairInt a)) -> (Key, PairInt a))
-> ((Key, PairInt a), (Key, PairInt a))
-> Map Key (PairInt a)
-> Map Key (PairInt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Key, PairInt a), (Key, PairInt a)) -> (Key, PairInt a)
forall a b. (a, b) -> a
fst) Maybe ((Key, PairInt a), (Key, PairInt a))
split2 (Map Key (PairInt a) -> Map Key (PairInt a))
-> Map Key (PairInt a) -> Map Key (PairInt a)
forall a b. (a -> b) -> a -> b
$
        Map Key (PairInt a) -> Map Key (PairInt a) -> Map Key (PairInt a)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap RangeMap a
f) (RangeMap a -> Map Key (PairInt a)
forall a. RangeMap a -> Map Key (PairInt a)
rangeMap RangeMap a
middle)
    )
  where
  (RangeMap a
beforeMiddle, Maybe ((Key, PairInt a), (Key, PairInt a))
split1, RangeMap a
after) = Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
forall a.
Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
splitAt' (Range -> Key
to Range
r) RangeMap a
f
  (RangeMap a
before, Maybe ((Key, PairInt a), (Key, PairInt a))
split2, RangeMap a
middle)      = Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
forall a.
Key
-> RangeMap a
-> (RangeMap a, Maybe ((Key, PairInt a), (Key, PairInt a)),
    RangeMap a)
splitAt' (Range -> Key
from Range
r) RangeMap a
beforeMiddle

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

restrictTo :: Range -> RangeMap a -> RangeMap a
restrictTo :: 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