-- | 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
    Int
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
    Int
max <- (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.lookupMax IntMap a
m
    Range -> Maybe Range
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Range { from :: Int
from = Int
min, to :: Int
to = Int
max Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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

------------------------------------------------------------------------
-- 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 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 (PairInt (Int
_ :!: a
y)) = a -> ()
forall a. NFData a => a -> ()
rnf a
y

-- | Constructs a pair.

pair :: Int -> a -> PairInt a
pair :: forall a. Int -> a -> PairInt a
pair Int
x a
y = Pair Int a -> PairInt a
forall a. Pair Int a -> PairInt a
PairInt (Int
x Int -> a -> Pair Int 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
  { 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, Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
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 =
    [(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, PairInt (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
    Int
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)
    Int
max <- (\(Int
_, PairInt (Int
p :!: a
_)) -> Int
p) ((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.lookupMax (RangeMap a -> Map Int (PairInt a)
forall a. RangeMap a -> Map Int (PairInt a)
rangeMap RangeMap a
f)
    Range -> Maybe Range
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Range { from :: Int
from = Int
min, to :: Int
to = Int
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, Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) 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 (PairInt (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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p (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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) (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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p (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) (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p a
m) Map Int (PairInt a)
f
          (Just (Int
p1, PairInt (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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p3 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p2 (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 (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
from Range
r) a
m') Map Int (PairInt a)
f
          (Just (Int
p1, PairInt (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 (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p2 (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 (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
from Range
r) 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) (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) (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 (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
from Range
r) 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p2 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
to Range
r) (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 (Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair (Range -> Int
from Range
r) 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
_, PairInt (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, PairInt (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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
p a
m), (Int
p, Int -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
to 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 -> a -> PairInt a
forall a. Int -> a -> PairInt a
pair Int
to 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