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