{-# LANGUAGE CPP #-}
-- |  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

#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup hiding (All(..))
#endif

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 (Int -> IntSet -> ShowS
[IntSet] -> ShowS
IntSet -> String
(Int -> IntSet -> ShowS)
-> (IntSet -> String) -> ([IntSet] -> ShowS) -> Show IntSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IntSet] -> ShowS
$cshowList :: [IntSet] -> ShowS
show :: IntSet -> String
$cshow :: IntSet -> String
showsPrec :: Int -> IntSet -> ShowS
$cshowsPrec :: Int -> IntSet -> ShowS
Show)

instance Eq IntSet where
  r :: IntSet
r == :: IntSet -> IntSet -> Bool
== r' :: IntSet
r' = IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r Maybe (Maybe Integer, Maybe Integer, Set Integer)
-> Maybe (Maybe Integer, Maybe Integer, Set Integer) -> Bool
forall a. Eq a => a -> a -> Bool
== IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r'
    where
      norm :: IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm All          = Maybe (Maybe Integer, Maybe Integer, Set Integer)
forall a. Maybe a
Nothing
      norm (Some xs :: Set Integer
xs)    = (Maybe Integer, Maybe Integer, Set Integer)
-> Maybe (Maybe Integer, Maybe Integer, Set Integer)
forall a. a -> Maybe a
Just (Maybe Integer
forall a. Maybe a
Nothing, Maybe Integer
forall a. Maybe a
Nothing, Set Integer
xs)
      norm (Below lo :: Integer
lo r :: IntSet
r) = do (_, hi :: Maybe Integer
hi, xs :: Set Integer
xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r; (Maybe Integer, Maybe Integer, Set Integer)
-> Maybe (Maybe Integer, Maybe Integer, Set Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
lo, Maybe Integer
hi, Set Integer
xs)
      norm (Above hi :: Integer
hi r :: IntSet
r) = do (lo :: Maybe Integer
lo, _, xs :: Set Integer
xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r; (Maybe Integer, Maybe Integer, Set Integer)
-> Maybe (Maybe Integer, Maybe Integer, Set Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
lo, Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
hi, Set Integer
xs)

below' :: Integer -> IntSet -> IntSet
below' :: Integer -> IntSet -> IntSet
below' _  All = IntSet
All
below' lo :: Integer
lo r :: IntSet
r@(Some xs :: Set Integer
xs)
  | Integer
lo Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Integer
xs = Integer -> IntSet -> IntSet
below' (Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) IntSet
r
  | Bool
otherwise  = Integer -> IntSet -> IntSet
Below Integer
lo (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Set Integer -> IntSet
Some (Set Integer -> IntSet) -> Set Integer -> IntSet
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
lo) Set Integer
xs
below' lo :: Integer
lo r0 :: IntSet
r0@(Below lo' :: Integer
lo' r :: IntSet
r)
  | Integer
lo' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
lo = IntSet
r0
  | Bool
otherwise = Integer -> IntSet -> IntSet
below' Integer
lo IntSet
r
below' lo :: Integer
lo (Above hi :: Integer
hi r :: IntSet
r)
  | Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lo  = IntSet
All
  | Bool
otherwise = Integer -> IntSet -> IntSet
Above Integer
hi (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Integer -> IntSet -> IntSet
below' Integer
lo IntSet
r

above' :: Integer -> IntSet -> IntSet
above' :: Integer -> IntSet -> IntSet
above' _  All = IntSet
All
above' hi :: Integer
hi r :: IntSet
r@(Some xs :: Set Integer
xs)
  | (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Integer
xs = Integer -> IntSet -> IntSet
above' (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) IntSet
r
  | Bool
otherwise        = Integer -> IntSet -> IntSet
Above Integer
hi (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Set Integer -> IntSet
Some (Set Integer -> IntSet) -> Set Integer -> IntSet
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi) Set Integer
xs
above' hi :: Integer
hi r0 :: IntSet
r0@(Above hi' :: Integer
hi' r :: IntSet
r)
  | Integer
hi' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
hi = IntSet
r0
  | Bool
otherwise = Integer -> IntSet -> IntSet
above' Integer
hi IntSet
r
above' hi :: Integer
hi (Below lo :: Integer
lo r :: IntSet
r)
  | Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lo  = IntSet
All
  | Bool
otherwise = Integer -> IntSet -> IntSet
Below Integer
lo (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Integer -> IntSet -> IntSet
above' Integer
hi IntSet
r

some' :: Set Integer -> IntSet -> IntSet
some' :: Set Integer -> IntSet -> IntSet
some' xs :: Set Integer
xs r :: IntSet
r | Set Integer -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Integer
xs = IntSet
r
some' xs :: Set Integer
xs (Some ys :: Set Integer
ys) = Set Integer -> IntSet
Some (Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Integer
xs Set Integer
ys)
some' _  All = IntSet
All
some' xs :: Set Integer
xs (Below lo :: Integer
lo r :: IntSet
r)
  | Integer
lo Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Integer
xs = Set Integer -> IntSet -> IntSet
some' Set Integer
xs (Integer -> IntSet -> IntSet
Below (Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1) IntSet
r)
  | Bool
otherwise  = Integer -> IntSet -> IntSet
below' Integer
lo (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Set Integer -> IntSet -> IntSet
some' ((Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
lo) Set Integer
xs) IntSet
r
some' xs :: Set Integer
xs (Above hi :: Integer
hi r :: IntSet
r)
  | (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Integer
xs = Set Integer -> IntSet -> IntSet
some' Set Integer
xs (Integer -> IntSet -> IntSet
Above (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) IntSet
r)
  | Bool
otherwise        = Integer -> IntSet -> IntSet
above' Integer
hi (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ Set Integer -> IntSet -> IntSet
some' ((Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi) Set Integer
xs) IntSet
r

difference :: IntSet -> IntSet -> IntSet
difference :: IntSet -> IntSet -> IntSet
difference r :: IntSet
r All           = IntSet
empty
difference r :: IntSet
r (Some xs :: Set Integer
xs)     = IntSet -> Set Integer -> IntSet
subtractSome IntSet
r Set Integer
xs
difference r :: IntSet
r (Below lo :: Integer
lo r' :: IntSet
r') = IntSet -> IntSet -> IntSet
difference (IntSet -> Integer -> IntSet
subtractBelow IntSet
r Integer
lo) IntSet
r'
difference r :: IntSet
r (Above hi :: Integer
hi r' :: IntSet
r') = IntSet -> IntSet -> IntSet
difference (IntSet -> Integer -> IntSet
subtractAbove IntSet
r Integer
hi) IntSet
r'

subtractSome :: IntSet -> Set Integer -> IntSet
subtractSome :: IntSet -> Set Integer -> IntSet
subtractSome r :: IntSet
r xs :: Set Integer
xs | Set Integer -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Integer
xs = IntSet
r
subtractSome All xs :: Set Integer
xs = Integer -> IntSet
below Integer
lo IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> Integer -> IntSet
above Integer
hi IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> Set Integer -> IntSet
Some ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
lo..Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1] Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Integer
xs)
  where lo :: Integer
lo = Set Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Set Integer
xs
        hi :: Integer
hi = Set Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Set Integer
xs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1
subtractSome (Some ys :: Set Integer
ys) xs :: Set Integer
xs = Set Integer -> IntSet
Some (Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Integer
ys Set Integer
xs)
subtractSome (Below lo :: Integer
lo r :: IntSet
r) xs :: Set Integer
xs = Integer -> IntSet -> IntSet
Below (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
lo Integer
lo') (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ IntSet -> Set Integer -> IntSet
subtractSome (Set Integer -> IntSet
Some ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
lo'..Integer
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1]) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r) Set Integer
xs
  where lo' :: Integer
lo' = Set Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Set Integer
xs
subtractSome (Above hi :: Integer
hi r :: IntSet
r) xs :: Set Integer
xs = Integer -> IntSet -> IntSet
Above (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
hi Integer
hi') (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ IntSet -> Set Integer -> IntSet
subtractSome (Set Integer -> IntSet
Some ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
hi..Integer
hi' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1]) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r) Set Integer
xs
  where hi' :: Integer
hi' = Set Integer -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Set Integer
xs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1

subtractBelow :: IntSet -> Integer -> IntSet
subtractBelow :: IntSet -> Integer -> IntSet
subtractBelow All           lo :: Integer
lo = Integer -> IntSet
above Integer
lo
subtractBelow (Below lo' :: Integer
lo' r :: IntSet
r) lo :: Integer
lo = Set Integer -> IntSet -> IntSet
some' ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
lo..Integer
lo' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1]) (IntSet -> Integer -> IntSet
subtractBelow IntSet
r Integer
lo)
subtractBelow (Above hi :: Integer
hi r :: IntSet
r)  lo :: Integer
lo = Integer -> IntSet -> IntSet
Above (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
hi Integer
lo) (IntSet -> Integer -> IntSet
subtractBelow IntSet
r Integer
lo)
subtractBelow (Some xs :: Set Integer
xs)     lo :: Integer
lo = Set Integer -> IntSet
Some (Set Integer -> IntSet) -> Set Integer -> IntSet
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
lo) Set Integer
xs

subtractAbove :: IntSet -> Integer -> IntSet
subtractAbove :: IntSet -> Integer -> IntSet
subtractAbove All           hi :: Integer
hi = Integer -> IntSet
below Integer
hi
subtractAbove (Above hi' :: Integer
hi' r :: IntSet
r) hi :: Integer
hi = Set Integer -> IntSet -> IntSet
some' ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
hi'..Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1]) (IntSet -> Integer -> IntSet
subtractAbove IntSet
r Integer
hi)
subtractAbove (Below lo :: Integer
lo r :: IntSet
r)  hi :: Integer
hi = Integer -> IntSet -> IntSet
Below (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
lo Integer
hi) (IntSet -> Integer -> IntSet
subtractAbove IntSet
r Integer
hi)
subtractAbove (Some xs :: Set Integer
xs)     hi :: Integer
hi = Set Integer -> IntSet
Some (Set Integer -> IntSet) -> Set Integer -> IntSet
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi) Set Integer
xs

instance Semigroup IntSet where
  Below lo :: Integer
lo r :: IntSet
r <> :: IntSet -> IntSet -> IntSet
<> r' :: IntSet
r' = Integer -> IntSet -> IntSet
below' Integer
lo (IntSet
r IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r')
  Above hi :: Integer
hi r :: IntSet
r <> r' :: IntSet
r' = Integer -> IntSet -> IntSet
above' Integer
hi (IntSet
r IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r')
  Some xs :: Set Integer
xs    <> r' :: IntSet
r' = Set Integer -> IntSet -> IntSet
some' Set Integer
xs IntSet
r'
  All        <> _  = IntSet
All

instance Monoid IntSet where
  mempty :: IntSet
mempty  = IntSet
empty
  mappend :: IntSet -> IntSet -> IntSet
mappend = IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
(<>)

-- | Membership
member :: Integer -> IntSet -> Bool
member :: Integer -> IntSet -> Bool
member _ All          = Bool
True
member x :: Integer
x (Some xs :: Set Integer
xs)    = Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Integer
x Set Integer
xs
member x :: Integer
x (Below lo :: Integer
lo s :: IntSet
s) = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
lo  Bool -> Bool -> Bool
|| Integer -> IntSet -> Bool
member Integer
x IntSet
s
member x :: Integer
x (Above hi :: Integer
hi s :: IntSet
s) = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
hi Bool -> Bool -> Bool
|| Integer -> IntSet -> Bool
member Integer
x IntSet
s

-- | All integers `< n`
below :: Integer -> IntSet
below :: Integer -> IntSet
below lo :: Integer
lo = Integer -> IntSet -> IntSet
Below Integer
lo IntSet
empty

-- | All integers `>= n`
above :: Integer -> IntSet
above :: Integer -> IntSet
above hi :: Integer
hi = Integer -> IntSet -> IntSet
Above Integer
hi IntSet
empty

-- | A single integer.
singleton :: Integer -> IntSet
singleton :: Integer -> IntSet
singleton x :: Integer
x = [Integer] -> IntSet
fromList [Integer
x]

-- | From a list of integers.
fromList :: [Integer] -> IntSet
fromList :: [Integer] -> IntSet
fromList xs :: [Integer]
xs = Set Integer -> IntSet
Some ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer]
xs)

-- | No integers.
empty :: IntSet
empty :: IntSet
empty = Set Integer -> IntSet
Some Set Integer
forall a. Set a
Set.empty

-- | All integers.
full :: IntSet
full :: IntSet
full = IntSet
All

-- | If finite, return the list of elements.
toFiniteList :: IntSet -> Maybe [Integer]
toFiniteList :: IntSet -> Maybe [Integer]
toFiniteList (Some xs :: Set Integer
xs) = [Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just ([Integer] -> Maybe [Integer]) -> [Integer] -> Maybe [Integer]
forall a b. (a -> b) -> a -> b
$ Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
xs
toFiniteList All       = Maybe [Integer]
forall a. Maybe a
Nothing
toFiniteList Above{}   = Maybe [Integer]
forall a. Maybe a
Nothing
toFiniteList Below{}   = Maybe [Integer]
forall a. Maybe a
Nothing

-- | Invariant.
invariant :: IntSet -> Bool
invariant :: IntSet -> Bool
invariant xs :: IntSet
xs =
  case IntSet
xs of
    All         -> Bool
True
    Some{}      -> Bool
True
    Below lo :: Integer
lo ys :: IntSet
ys -> IntSet -> Bool
invariant IntSet
ys Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invBelow Integer
lo IntSet
ys
    Above hi :: Integer
hi ys :: IntSet
ys -> IntSet -> Bool
invariant IntSet
ys Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invAbove Integer
hi IntSet
ys
  where
    invBelow :: Integer -> IntSet -> Bool
invBelow lo :: Integer
lo All          = Bool
False
    invBelow lo :: Integer
lo (Some xs :: Set Integer
xs)    = (Integer -> Bool) -> Set Integer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
lo) Set Integer
xs
    invBelow lo :: Integer
lo Below{}      = Bool
False
    invBelow lo :: Integer
lo (Above hi :: Integer
hi r :: IntSet
r) = Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invBelow Integer
lo IntSet
r

    invAbove :: Integer -> IntSet -> Bool
invAbove hi :: Integer
hi All          = Bool
False
    invAbove hi :: Integer
hi (Some xs :: Set Integer
xs)    = (Integer -> Bool) -> Set Integer -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1) Set Integer
xs
    invAbove hi :: Integer
hi Above{}      = Bool
False
    invAbove hi :: Integer
hi (Below lo :: Integer
lo r :: IntSet
r) = Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
hi Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invAbove Integer
hi IntSet
r