    -- |  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