1-- | Maps containing non-overlapping intervals.
2
3module Agda.Utils.RangeMap
4  ( IsBasicRangeMap(..)
5  , several
6  , PairInt(..)
7  , RangeMap(..)
8  , rangeMapInvariant
9  , fromNonOverlappingNonEmptyAscendingList
10  , insert
11  , splitAt
12  , insideAndOutside
13  , restrictTo
14  )
15  where
16
17import Prelude hiding (null, splitAt)
18
19import Control.DeepSeq
20
21import Data.IntMap (IntMap)
22import qualified Data.IntMap as IntMap
23
24import Data.Map.Strict (Map)
25import qualified Data.Map.Strict as Map
26
27import Data.Semigroup
28
29import Data.Strict.Tuple (Pair(..))
30
31import Agda.Interaction.Highlighting.Range
32import Agda.Utils.List
33import Agda.Utils.Null
34
35------------------------------------------------------------------------
36-- An abstraction
37
38-- | A class that is intended to make it easy to swap between
39-- different range map implementations.
40--
41-- Note that some 'RangeMap' operations are not included in this
42-- class.
43
44class IsBasicRangeMap a m | m -> a where
45
46  -- | The map @'singleton' rs x@ contains the ranges from @rs@, and
47  -- every position in those ranges is associated with @x@.
48
49  singleton :: Ranges -> a -> m
50
51  -- | Converts range maps to 'IntMap's from positions to values.
52
53  toMap :: m -> IntMap a
54
55  -- | Converts the map to a list. The ranges are non-overlapping and
56  -- non-empty, and earlier ranges precede later ones in the list.
57
58  toList :: m -> [(Range, a)]
59
60  -- | Returns the smallest range covering everything in the map (or
61  -- 'Nothing', if the range would be empty).
62  --
63  -- Note that the default implementation of this operation might be
64  -- inefficient.
65
66  coveringRange :: m -> Maybe Range
67  coveringRange f = do
68    min <- fst <$> IntMap.lookupMin m
69    max <- fst <$> IntMap.lookupMax m
70    return (Range { from = min, to = max + 1 })
71    where
72    m = toMap f
73
74-- | Like 'singleton', but with several 'Ranges' instead of only one.
75
76several ::
77  (IsBasicRangeMap a hl, Monoid hl) =>
78  [Ranges] -> a -> hl
79several rss m = mconcat $ map (flip singleton m) rss
80
81------------------------------------------------------------------------
82-- A strict pair type
83
84-- | A strict pair type where the first argument must be an 'Int'.
85--
86-- This type is included because there is no 'NFData' instance for
87-- 'Pair' in the package @strict@ before version 4.
88
89newtype PairInt a = PairInt (Pair Int a)
90  deriving Show
91
92instance NFData a => NFData (PairInt a) where
93  rnf (PairInt (_ :!: y)) = rnf y
94
95-- | Constructs a pair.
96
97pair :: Int -> a -> PairInt a
98pair x y = PairInt (x :!: y)
99
100------------------------------------------------------------------------
101-- The type
102
103-- | Maps containing non-overlapping intervals.
104--
105-- The implementation does not use IntMap, because IntMap does not
106-- come with a constant-time size function.
107--
108-- Note the invariant which 'RangeMap's should satisfy
109-- ('rangeMapInvariant').
110
111newtype RangeMap a = RangeMap
112  { rangeMap :: Map Int (PairInt a)
113    -- ^ The keys are starting points of ranges, and the pairs contain
114    -- endpoints and values.
115  }
116  deriving (Show, NFData)
117
118-- | Invariant for 'RangeMap'.
119--
120-- The ranges must not be empty, and they must not overlap.
121
122rangeMapInvariant :: RangeMap a -> Bool
123rangeMapInvariant f = and
124  [ all rangeInvariant rs
125  , all (not . null) rs
126  , caseList rs True $ \ r rs' ->
127      and $ zipWith (<=) (map to $ init1 r rs') (map from rs')
128  ]
129  where
130  rs = map fst $ toList f
131
132------------------------------------------------------------------------
133-- Construction, conversion and inspection
134
135instance Null (RangeMap a) where
136  empty = RangeMap { rangeMap = Map.empty }
137  null  = Map.null . rangeMap
138
139instance IsBasicRangeMap a (RangeMap a) where
140  singleton (Ranges rs) m =
141    RangeMap { rangeMap = Map.fromDistinctAscList rms }
142    where
143    rms =
144      [ (from r, pair (to r) m)
145      | r <- rs
146      , not (null r)
147      ]
148
149  toMap f =
150    IntMap.fromList
151      [ (p, m)
152      | (r, m) <- toList f
153      , p <- rangeToPositions r
154      ]
155
156  toList =
157    map (\(f, PairInt (t :!: a)) -> (Range { from = f, to = t } , a)) .
158    Map.toAscList .
159    rangeMap
160
161  coveringRange f = do
162    min <- fst <$> Map.lookupMin (rangeMap f)
163    max <- (\(_, PairInt (p :!: _)) -> p) <$> Map.lookupMax (rangeMap f)
164    return (Range { from = min, to = max })
165
166-- | Converts a list of pairs of ranges and values to a 'RangeMap'.
167-- The ranges have to be non-overlapping and non-empty, and earlier
168-- ranges have to precede later ones.
169
170fromNonOverlappingNonEmptyAscendingList :: [(Range, a)] -> RangeMap a
171fromNonOverlappingNonEmptyAscendingList =
172  RangeMap .
173  Map.fromDistinctAscList .
174  map (\(r, m) -> (from r, pair (to r) m))
175
176-- | The number of ranges in the map.
177--
178-- This function should not be exported.
179
180size :: RangeMap a -> Int
181size = Map.size . rangeMap
182
183------------------------------------------------------------------------
184-- Merging
185
186-- | Inserts a value, along with a corresponding 'Range', into a
187-- 'RangeMap'. No attempt is made to merge adjacent ranges with equal
188-- values.
189--
190-- The function argument is used to combine values. The inserted value
191-- is given as the first argument to the function.
192
193insert :: (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
194insert combine r m (RangeMap f)
195  | null r    = RangeMap f
196  | otherwise =
197    case equal of
198      Just (PairInt (p :!: m')) ->
199        case compare (to r) p of
200          EQ ->
201            -- The range r matches exactly.
202            RangeMap $
203            Map.insert (from r) (pair p (combine m m')) f
204          LT ->
205            -- The range r is strictly shorter.
206            RangeMap $
207            Map.insert (to r) (pair p m') $
208            Map.insert (from r) (pair (to r) (combine m m')) f
209          GT ->
210            -- The range r is strictly longer. Continue recursively.
211            insert combine (Range { from = p, to = to r }) m $
212            RangeMap $
213            Map.insert (from r) (pair p (combine m m')) f
214      Nothing ->
215        -- Find the part of r that does not overlap with anything in
216        -- smaller or larger, if any.
217        case (overlapLeft, overlapRight) of
218          (Nothing, Nothing) ->
219            -- No overlap.
220            RangeMap $
221            Map.insert (from r) (pair (to r) m) f
222          (Nothing, Just p) ->
223            -- Overlap on the right. Continue recursively.
224            insert combine (Range { from = p, to = to r }) m $
225            RangeMap $
226            Map.insert (from r) (pair p m) f
227          (Just (p1, PairInt (p2 :!: m')), Just p3) ->
228            -- Overlap on both sides. Continue recursively.
229            insert combine (Range { from = p3, to = to r }) m $
230            RangeMap $
231            (if p2 == p3 then
232               -- The left range ends exactly where the right range
233               -- starts.
234               id
235             else
236               -- There is something between the left and right
237               -- ranges.
238               Map.insert p2 (pair p3 m)) $
239            Map.insert (from r) (pair p2 (combine m m')) $
240            Map.insert p1 (pair (from r) m') f
241          (Just (p1, PairInt (p2 :!: m')), Nothing) ->
242            case compare p2 (to r) of
243              LT ->
244                -- Overlap on the left, the left range ends before r.
245                RangeMap $
246                Map.insert p2 (pair (to r) m) $
247                Map.insert (from r) (pair p2 (combine m m')) $
248                Map.insert p1 (pair (from r) m') f
249              EQ ->
250                -- Overlap on the left, the left range ends where r
251                -- ends.
252                RangeMap $
253                Map.insert (from r) (pair (to r) (combine m m')) $
254                Map.insert p1 (pair (from r) m') f
255              GT ->
256                -- Overlap on the left, the left range ends after r.
257                RangeMap $
258                Map.insert (to r) (pair p2 m') $
259                Map.insert (from r) (pair (to r) (combine m m')) $
260                Map.insert p1 (pair (from r) m') f
261    where
262    (smaller, equal, larger) = Map.splitLookup (from r) f
263
264    overlapRight = case Map.lookupMin larger of
265      Nothing -> Nothing
266      Just (from, _)
267        | from < to r -> Just from
268        | otherwise   -> Nothing
269
270    overlapLeft = case Map.lookupMax smaller of
271      Nothing -> Nothing
272      Just s@(_, PairInt (to :!: _))
273        | from r < to -> Just s
274        | otherwise   -> Nothing
275
276-- | Merges 'RangeMap's by inserting every \"piece\" of the smaller
277-- one into the larger one.
278
279instance Semigroup a => Semigroup (RangeMap a) where
280  f1 <> f2
281    | size f1 <= size f2 =
282      foldr (uncurry $ insert (<>)) f2 (toList f1)
283    | otherwise =
284      foldr (uncurry $ insert (flip (<>))) f1 (toList f2)
285
286-- | Merges 'RangeMap's by inserting every \"piece\" of the smaller
287-- one into the larger one.
288
289instance Semigroup a => Monoid (RangeMap a) where
290  mempty  = empty
291  mappend = (<>)
292
293------------------------------------------------------------------------
294-- Splitting
295
296-- | The value of @'splitAt' p f@ is a pair @(f1, f2)@ which contains
297-- everything from @f@. All the positions in @f1@ are less than @p@,
298-- and all the positions in @f2@ are greater than or equal to @p@.
299
300splitAt :: Int -> RangeMap a -> (RangeMap a, RangeMap a)
301splitAt p f = (before, after)
302  where
303  (before, _, after) = splitAt' p f
304
305-- | A variant of 'splitAt'. If a range in the middle was split into
306-- two pieces, then those two pieces are returned.
307
308splitAt' ::
309  Int -> RangeMap a ->
310  ( RangeMap a
311  , Maybe ((Int, PairInt a), (Int, PairInt a))
312  , RangeMap a
313  )
314splitAt' p (RangeMap f) =
315  case equal of
316    Just r  -> ( RangeMap maybeOverlapping
317               , Nothing
318               , RangeMap (Map.insert p r larger)
319               )
320    Nothing ->
321      -- Check if maybeOverlapping overlaps with p.
322      case Map.maxViewWithKey maybeOverlapping of
323        Nothing ->
324          (empty, Nothing, RangeMap larger)
325        Just ((from, PairInt (to :!: m)), smaller)
326          | to <= p ->
327            ( RangeMap maybeOverlapping
328            , Nothing
329            , RangeMap larger
330            )
331          | otherwise ->
332            -- Here from < p < to.
333            ( RangeMap (Map.insert from (pair p m) smaller)
334            , Just ((from, pair p m), (p, pair to m))
335            , RangeMap (Map.insert p (pair to m) larger)
336            )
337  where
338  (maybeOverlapping, equal, larger) = Map.splitLookup p f
339
340-- | Returns a 'RangeMap' overlapping the given range, as well as the
341-- rest of the map.
342
343insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
344insideAndOutside r f
345  | from r == to r = (empty, f)
346  | otherwise      =
347    ( middle
348    , -- Because it takes so long to recompile Agda with all
349      -- optimisations and run a benchmark no experimental
350      -- verification has been made that the code below is better than
351      -- reasonable variants. Perhaps it would make sense to benchmark
352      -- RangeMap independently of Agda.
353      if size before < size middle || size after < size middle then
354        RangeMap $ Map.union (rangeMap before) (rangeMap after)
355      else
356        -- If the number of pieces in the middle is "small", remove
357        -- the pieces from f instead of merging before and after.
358        RangeMap $
359        maybe id (uncurry Map.insert . snd) split1 $
360        maybe id (uncurry Map.insert . fst) split2 $
361        Map.difference (rangeMap f) (rangeMap middle)
362    )
363  where
364  (beforeMiddle, split1, after) = splitAt' (to r) f
365  (before, split2, middle)      = splitAt' (from r) beforeMiddle
366
367-- | Restricts the 'RangeMap' to the given range.
368
369restrictTo :: Range -> RangeMap a -> RangeMap a
370restrictTo r = fst . insideAndOutside r
371