{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.IntSet.Infinite
( IntSet
, empty, full, below, above, singleton
, difference, member, toFiniteList
, invariant )
where
import Data.Set (Set)
import qualified Data.Set as Set
data IntSet = All
| Some (Set Integer)
| Below Integer IntSet
| Above Integer IntSet
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 (_, hi, xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r; return (Just lo, hi, xs)
norm (Above Integer
hi IntSet
r) = do (lo, _, xs) <- IntSet -> Maybe (Maybe Integer, Maybe Integer, Set Integer)
norm IntSet
r; return (lo, Just hi, 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
(<>)
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
below :: Integer -> IntSet
below :: Integer -> IntSet
below Integer
lo = Integer -> IntSet -> IntSet
Below Integer
lo IntSet
empty
above :: Integer -> IntSet
above :: Integer -> IntSet
above Integer
hi = Integer -> IntSet -> IntSet
Above Integer
hi IntSet
empty
singleton :: Integer -> IntSet
singleton :: Integer -> IntSet
singleton Integer
x = [Integer] -> IntSet
fromList [Integer
x]
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)
empty :: IntSet
empty :: IntSet
empty = Set Integer -> IntSet
Some Set Integer
forall a. Set a
Set.empty
full :: IntSet
full :: IntSet
full = IntSet
All
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 :: 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