module Data.Set.Unique.Properties where
import Data.Set.Unique
import qualified Data.Tree.Braun.Sized as Braun
import qualified Data.Tree.Braun.Sized.Properties as Braun
import Data.Foldable
import Data.List (sortBy)
import Data.Functor.Classes
sizesInBound :: Set a -> Bool
sizesInBound (Set b) = null xs || it && re where
xs = toList b
it = and $ zipWith (\x y -> Braun.size x == szfn y) (safeInit xs) [1..]
safeInit [] = []
safeInit ys = init ys
re = Braun.size (last xs) <= szfn (length xs)
allBraun :: Set a -> Bool
allBraun (Set b) = Braun.isBraun b && all Braun.isBraun b
inOrder :: (a -> a -> Ordering) -> Set a -> Bool
inOrder cmp xs =
liftEq
(\x y ->
cmp x y == EQ)
ys
(sortBy cmp ys)
where
ys = toList xs
allCorrectSizes :: Set a -> Bool
allCorrectSizes (Set b) = Braun.validSize b && all Braun.validSize b
validSize :: Set a -> Bool
validSize s = length s == foldl' (\a _ -> a + 1) 0 s