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

instance Eq IntSet where
  IntSet
r == :: IntSet -> IntSet -> Bool
== 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 IntSet
All          = Maybe (Maybe Integer, Maybe Integer, Set Integer)
forall a. Maybe a
Nothing
      norm (Some 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 Integer
lo IntSet
r) = do (Maybe Integer
_, Maybe Integer
hi, 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 a. a -> Maybe a
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 Integer
hi IntSet
r) = do (Maybe Integer
lo, Maybe Integer
_, 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 a. a -> Maybe a
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' Integer
_  IntSet
All = IntSet
All
below' Integer
lo r :: IntSet
r@(Some 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
+ Integer
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' Integer
lo r0 :: IntSet
r0@(Below Integer
lo' 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' Integer
lo (Above Integer
hi 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' Integer
_  IntSet
All = IntSet
All
above' Integer
hi r :: IntSet
r@(Some Set Integer
xs)
  | (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
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
- Integer
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' Integer
hi r0 :: IntSet
r0@(Above Integer
hi' 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' Integer
hi (Below Integer
lo 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' Set Integer
xs IntSet
r | Set Integer -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Integer
xs = IntSet
r
some' Set Integer
xs (Some 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' Set Integer
_  IntSet
All = IntSet
All
some' Set Integer
xs (Below Integer
lo 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
+ Integer
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' Set Integer
xs (Above Integer
hi IntSet
r)
  | (Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
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
- Integer
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 IntSet
r IntSet
All           = IntSet
empty
difference IntSet
r (Some Set Integer
xs)     = IntSet -> Set Integer -> IntSet
subtractSome IntSet
r Set Integer
xs
difference IntSet
r (Below Integer
lo IntSet
r') = IntSet -> IntSet -> IntSet
difference (IntSet -> Integer -> IntSet
subtractBelow IntSet
r Integer
lo) IntSet
r'
difference IntSet
r (Above Integer
hi 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 IntSet
r Set Integer
xs | Set Integer -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Integer
xs = IntSet
r
subtractSome IntSet
All 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
- Integer
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 a. Ord a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Set Integer
xs
        hi :: Integer
hi = Set Integer -> Integer
forall a. Ord a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Set Integer
xs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
subtractSome (Some Set Integer
ys) 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 Integer
lo IntSet
r) 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
- Integer
1]) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r) Set Integer
xs
  where lo' :: Integer
lo' = Set Integer -> Integer
forall a. Ord a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Set Integer
xs
subtractSome (Above Integer
hi IntSet
r) 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
- Integer
1]) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r) Set Integer
xs
  where hi' :: Integer
hi' = Set Integer -> Integer
forall a. Ord a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Set Integer
xs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1

subtractBelow :: IntSet -> Integer -> IntSet
subtractBelow :: IntSet -> Integer -> IntSet
subtractBelow IntSet
All           Integer
lo = Integer -> IntSet
above Integer
lo
subtractBelow (Below Integer
lo' IntSet
r) 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
- Integer
1]) (IntSet -> Integer -> IntSet
subtractBelow IntSet
r Integer
lo)
subtractBelow (Above Integer
hi IntSet
r)  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 Set Integer
xs)     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 IntSet
All           Integer
hi = Integer -> IntSet
below Integer
hi
subtractAbove (Above Integer
hi' IntSet
r) 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
- Integer
1]) (IntSet -> Integer -> IntSet
subtractAbove IntSet
r Integer
hi)
subtractAbove (Below Integer
lo IntSet
r)  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 Set Integer
xs)     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 Integer
lo IntSet
r <> :: IntSet -> IntSet -> IntSet
<> IntSet
r' = Integer -> IntSet -> IntSet
below' Integer
lo (IntSet
r IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r')
  Above Integer
hi IntSet
r <> IntSet
r' = Integer -> IntSet -> IntSet
above' Integer
hi (IntSet
r IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
r')
  Some Set Integer
xs    <> IntSet
r' = Set Integer -> IntSet -> IntSet
some' Set Integer
xs IntSet
r'
  IntSet
All        <> IntSet
_  = 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 Integer
_ IntSet
All          = Bool
True
member Integer
x (Some Set Integer
xs)    = Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Integer
x Set Integer
xs
member Integer
x (Below Integer
lo 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 Integer
x (Above Integer
hi 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 Integer
lo = Integer -> IntSet -> IntSet
Below Integer
lo IntSet
empty

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

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

-- | From a list of integers.
fromList :: [Integer] -> IntSet
fromList :: [Integer] -> IntSet
fromList [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 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 IntSet
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 IntSet
xs =
  case IntSet
xs of
    IntSet
All         -> Bool
True
    Some{}      -> Bool
True
    Below Integer
lo IntSet
ys -> IntSet -> Bool
invariant IntSet
ys Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invBelow Integer
lo IntSet
ys
    Above Integer
hi IntSet
ys -> IntSet -> Bool
invariant IntSet
ys Bool -> Bool -> Bool
&& Integer -> IntSet -> Bool
invAbove Integer
hi IntSet
ys
  where
    invBelow :: Integer -> IntSet -> Bool
invBelow Integer
lo IntSet
All          = Bool
False
    invBelow Integer
lo (Some 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 Integer
lo Below{}      = Bool
False
    invBelow Integer
lo (Above Integer
hi 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 Integer
hi IntSet
All          = Bool
False
    invAbove Integer
hi (Some 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
- Integer
1) Set Integer
xs
    invAbove Integer
hi Above{}      = Bool
False
    invAbove Integer
hi (Below Integer
lo 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