-- | Possibly infinite sets of integers (but with finitely many consecutive
-- segments). Used for checking guard coverage in int/nat cases in the
-- treeless compiler.
module Agda.Utils.IntSet.Infinite
( IntSet
, empty, full, below, above, singleton
, difference, member, toFiniteList
, invariant )
where
import Control.Arrow (first, second)
import Data.Semigroup hiding (All(..))
import Data.List
import Data.Set (Set)
import qualified Data.Set as Set
-- | Represents a set of integers.
-- Invariants:
-- - All cannot be the argument to `Below` or `Above`
-- - at most one 'IntsBelow'
-- - at most one 'IntsAbove'
-- - if `Below lo` and `Below hi`, then `lo < hi`
-- - if `Below lo .. (Some xs)` then `all (> lo) xs`
-- - if `Above hi .. (Some xs)` then `all (< hi - 1) xs`
data IntSet = All
| Some (Set Integer)
| Below Integer IntSet -- exclusive
| Above Integer IntSet -- inclusive
deriving (Show)
instance Eq IntSet where
r == r' = norm r == norm r'
where
norm All = Nothing
norm (Some xs) = Just (Nothing, Nothing, xs)
norm (Below lo r) = do (_, hi, xs) <- norm r; return (Just lo, hi, xs)
norm (Above hi r) = do (lo, _, xs) <- norm r; return (lo, Just hi, xs)
below' :: Integer -> IntSet -> IntSet
below' _ All = All
below' lo r@(Some xs)
| elem lo xs = below' (lo + 1) r
| otherwise = Below lo $ Some $ Set.filter (>= lo) xs
below' lo r0@(Below lo' r)
| lo' >= lo = r0
| otherwise = below' lo r
below' lo (Above hi r)
| hi <= lo = All
| otherwise = Above hi $ below' lo r
above' :: Integer -> IntSet -> IntSet
above' _ All = All
above' hi r@(Some xs)
| elem (hi - 1) xs = above' (hi - 1) r
| otherwise = Above hi $ Some $ Set.filter (< hi) xs
above' hi r0@(Above hi' r)
| hi' <= hi = r0
| otherwise = above' hi r
above' hi (Below lo r)
| hi <= lo = All
| otherwise = Below lo $ above' hi r
some' :: Set Integer -> IntSet -> IntSet
some' xs r | null xs = r
some' xs (Some ys) = Some (Set.union xs ys)
some' _ All = All
some' xs (Below lo r)
| elem lo xs = some' xs (Below (lo + 1) r)
| otherwise = below' lo $ some' (Set.filter (>= lo) xs) r
some' xs (Above hi r)
| elem (hi - 1) xs = some' xs (Above (hi - 1) r)
| otherwise = above' hi $ some' (Set.filter (< hi) xs) r
difference :: IntSet -> IntSet -> IntSet
difference r All = empty
difference r (Some xs) = subtractSome r xs
difference r (Below lo r') = difference (subtractBelow r lo) r'
difference r (Above hi r') = difference (subtractAbove r hi) r'
subtractSome :: IntSet -> Set Integer -> IntSet
subtractSome r xs | null xs = r
subtractSome All xs = below lo <> above hi <> Some (Set.fromList [lo..hi - 1] `Set.difference` xs)
where lo = minimum xs
hi = maximum xs + 1
subtractSome (Some ys) xs = Some (Set.difference ys xs)
subtractSome (Below lo r) xs = Below (min lo lo') $ subtractSome (Some (Set.fromList [lo'..lo - 1]) <> r) xs
where lo' = minimum xs
subtractSome (Above hi r) xs = Above (max hi hi') $ subtractSome (Some (Set.fromList [hi..hi' - 1]) <> r) xs
where hi' = maximum xs + 1
subtractBelow :: IntSet -> Integer -> IntSet
subtractBelow All lo = above lo
subtractBelow (Below lo' r) lo = some' (Set.fromList [lo..lo' - 1]) (subtractBelow r lo)
subtractBelow (Above hi r) lo = Above (max hi lo) (subtractBelow r lo)
subtractBelow (Some xs) lo = Some $ Set.filter (>= lo) xs
subtractAbove :: IntSet -> Integer -> IntSet
subtractAbove All hi = below hi
subtractAbove (Above hi' r) hi = some' (Set.fromList [hi'..hi - 1]) (subtractAbove r hi)
subtractAbove (Below lo r) hi = Below (min lo hi) (subtractAbove r hi)
subtractAbove (Some xs) hi = Some $ Set.filter (< hi) xs
instance Semigroup IntSet where
Below lo r <> r' = below' lo (r <> r')
Above hi r <> r' = above' hi (r <> r')
Some xs <> r' = some' xs r'
All <> _ = All
instance Monoid IntSet where
mempty = empty
mappend = (<>)
-- | Membership
member :: Integer -> IntSet -> Bool
member _ All = True
member x (Some xs) = Set.member x xs
member x (Below lo s) = x < lo || member x s
member x (Above hi s) = x >= hi || member x s
-- | All integers `< n`
below :: Integer -> IntSet
below lo = Below lo empty
-- | All integers `>= n`
above :: Integer -> IntSet
above hi = Above hi empty
-- | A single integer.
singleton :: Integer -> IntSet
singleton x = fromList [x]
-- | From a list of integers.
fromList :: [Integer] -> IntSet
fromList xs = Some (Set.fromList xs)
-- | No integers.
empty :: IntSet
empty = Some Set.empty
-- | All integers.
full :: IntSet
full = All
-- | If finite, return the list of elements.
toFiniteList :: IntSet -> Maybe [Integer]
toFiniteList (Some xs) = Just $ Set.toList xs
toFiniteList All = Nothing
toFiniteList Above{} = Nothing
toFiniteList Below{} = Nothing
-- | Invariant.
invariant :: IntSet -> Bool
invariant xs =
case xs of
All -> True
Some{} -> True
Below lo ys -> invariant ys && invBelow lo ys
Above hi ys -> invariant ys && invAbove hi ys
where
invBelow lo All = False
invBelow lo (Some xs) = all (> lo) xs
invBelow lo Below{} = False
invBelow lo (Above hi r) = lo < hi && invBelow lo r
invAbove hi All = False
invAbove hi (Some xs) = all (< hi - 1) xs
invAbove hi Above{} = False
invAbove hi (Below lo r) = lo < hi && invAbove hi r