module Data.Cardinality (
PreciseCardinality
, CurrentNotFinalPreciseCardinality
, BoundaryPreciseCardinality
, ContinueCounting_DoWe
, ContinueRefiningCardinalityUntil
, CardinalityRefinementState
, LazyCardinality
, infiniteC
, preciseC
, refinableC
, lazyIsZeroLC
, refinementState
, addPCToLC
, addLCToLC
, sumLCs
, refineCRS_Till
, refineCRS_TillOneAbove
, refineCRS_TillOneBelow
, crsRefinementStep
, refineCRS_TillEnd
, refineTill
, refineTillOneAbove
, refineTillOneBelow
, refinementStep
, refineTillEnd
, equalize2Refinements
, compare2Refinements
, almostStrictCompare2LCs
, lazyCompare2LCs
, showLazy
, showStrict
, HasCard(..)
, HasCardT(..)
, cardOf_Unity
, cardOf_EmptySet
, cardOf_Identity1
, cardOf_Maybe
, cardOf_List
, cardOf_Map
, cardOf_NeverEmptyList
, length2
) where
import Data.EmptySet
import Data.NeverEmptyList
import qualified Data.Map as M
import Data.Map (Map, (!))
import Data.Word
import Data.Typeable
import Control.Monad.Identity
type PreciseCardinality = Integer
type CurrentNotFinalPreciseCardinality = PreciseCardinality
type BoundaryPreciseCardinality = CurrentNotFinalPreciseCardinality
type ContinueCounting_DoWe = Bool
type ContinueRefiningCardinalityUntil = CurrentNotFinalPreciseCardinality -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -> LazyCardinality
type CardinalityRefinementState = (CurrentNotFinalPreciseCardinality, ContinueRefiningCardinalityUntil)
data LazyCardinality =
InfiniteC
| PreciseC PreciseCardinality
| RefinableC CardinalityRefinementState
deriving (Typeable)
infiniteC :: LazyCardinality
infiniteC = InfiniteC
preciseC :: PreciseCardinality -> LazyCardinality
preciseC c = case c < 0 of { True -> error ("Can't construct negative cardinality '" ++ show c ++ "' "); False -> PreciseC c }
refinableC :: CardinalityRefinementState -> LazyCardinality
refinableC = RefinableC
lcIsInfinite :: LazyCardinality -> Bool
lcIsInfinite InfiniteC = True
lcIsInfinite _ = False
preciseOfLC :: LazyCardinality -> Maybe PreciseCardinality
preciseOfLC (PreciseC c) = Just c
preciseOfLC _ = Nothing
lazyIsZeroLC :: LazyCardinality -> Maybe Bool
lazyIsZeroLC (PreciseC c) = Just (c == 0)
lazyIsZeroLC InfiniteC = Just False
lazyIsZeroLC (RefinableC (c, _)) = case c `compare` 0 of { EQ -> Nothing; _ -> Just False }
refinementState :: LazyCardinality -> Maybe CardinalityRefinementState
refinementState (RefinableC rs) = Just rs
refinementState _ = Nothing
infixr 6 `addPCToLC`
addPCToLC :: PreciseCardinality -> LazyCardinality -> LazyCardinality
addPCToLC n lc =
case lc of
InfiniteC -> lc
PreciseC m -> preciseC (m + n)
RefinableC (c, ref_while) -> refinableC (c + n, ref_while)
infixr 6 `addLCToLC`
addLCToLC :: LazyCardinality -> LazyCardinality -> LazyCardinality
addLCToLC lc_1 lc_2 =
case (lc_1, lc_2) of
(InfiniteC, _) -> InfiniteC
(_, InfiniteC) -> InfiniteC
(PreciseC m, PreciseC n) -> preciseC (m + n)
(PreciseC m, RefinableC (c, ref_while)) -> refinableC (c + m, ref_while)
(RefinableC (c, ref_while), PreciseC m) -> refinableC (c + m, ref_while)
(RefinableC (c, ref_while_1), RefinableC (d, ref_while_2)) -> refinableC (c + d, refWhileSyn ref_while_1 ref_while_2)
where
refWhileSyn :: ContinueRefiningCardinalityUntil -> ContinueRefiningCardinalityUntil -> ContinueRefiningCardinalityUntil
refWhileSyn ref_while_1 ref_while_2 =
(\ sofar stop_cond ->
case ref_while_1 sofar stop_cond of
InfiniteC -> InfiniteC
RefinableC (sofar_2, ref_while_1_2) -> RefinableC (sofar_2, refWhileSyn ref_while_1_2 ref_while_2)
PreciseC c ->
case ref_while_1 (sofar + c) stop_cond of
InfiniteC -> InfiniteC
RefinableC (sofar_3, ref_while_2_2) -> RefinableC (sofar_3, ref_while_2_2)
PreciseC final_c -> PreciseC final_c
)
sumLCs :: [LazyCardinality] -> LazyCardinality
sumLCs = foldl addLCToLC (preciseC 0)
refineCRS_Till :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_Till crs@(c, ref_while) n =
case c >= n of
True -> refinableC crs
False -> ref_while c (<= n)
refineCRS_TillOneAbove :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_TillOneBelow :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_TillOneAbove crs n = refineCRS_Till crs (n + 1)
refineCRS_TillOneBelow crs n = refineCRS_Till crs (n 1)
crsRefinementStep :: CardinalityRefinementState -> LazyCardinality
crsRefinementStep crs@(c, ref_while) = ref_while c (<= (c + 1))
refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinality
refineCRS_TillEnd crs@(c, ref_while) = ref_while c (const True)
refineTill :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
refineTill lc n =
case lc of
RefinableC crs -> refineCRS_Till crs n
_ -> lc
refineTillOneAbove :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
refineTillOneBelow :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
refineTillOneAbove lc n = case lc of { RefinableC crs -> refineCRS_Till crs (n + 1); _ -> lc }
refineTillOneBelow lc n = case lc of { RefinableC crs -> refineCRS_Till crs (n 1); _ -> lc }
refinementStep :: LazyCardinality -> LazyCardinality
refinementStep lc = case lc of { RefinableC crs -> crsRefinementStep crs ; _ -> lc }
refineTillEnd :: LazyCardinality -> LazyCardinality
refineTillEnd lc = case lc of { RefinableC crs -> refineCRS_TillEnd crs ; _ -> lc }
equalize2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (LazyCardinality, LazyCardinality)
equalize2Refinements crs1@(m, ref_f_1) crs2@(n, ref_f_2) =
case m `compare` n of
LT -> let lc_of_crs1_refined = ref_f_1 m (<= n)
in case refinementState lc_of_crs1_refined of
Nothing -> (lc_of_crs1_refined, refinableC crs2)
Just crs1_refined -> equalize2Refinements crs1_refined crs2
EQ -> (refinableC crs1, refinableC crs2)
GT -> let lc_of_crs2_refined = ref_f_2 n (<= m)
in case refinementState lc_of_crs2_refined of
Nothing -> (refinableC crs1, lc_of_crs2_refined)
Just crs2_refined -> equalize2Refinements crs1 crs2_refined
compare2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (Ordering, LazyCardinality, LazyCardinality)
compare2Refinements crs1@(m, _) crs2@(n, _) =
let cards = equalize2Refinements crs1 crs2
in case cards of
(lc1_2@(RefinableC crs1_2), lc2_2@(RefinableC crs2_2)) ->
let lc1_3 = crsRefinementStep crs1_2
in case lc1_3 of
RefinableC crs1_3 ->
let lc2_3 = crsRefinementStep crs2_2
in case lc2_3 of
RefinableC crs2_3 -> compare2Refinements crs1_3 crs2_3
_ -> almostStrictCompare2LCs lc1_3 lc2_3
_ -> almostStrictCompare2LCs lc1_3 lc2_2
_ -> uncurry almostStrictCompare2LCs cards
infixr 9 `almostStrictCompare2LCs`
almostStrictCompare2LCs :: LazyCardinality -> LazyCardinality -> (Ordering, LazyCardinality, LazyCardinality)
almostStrictCompare2LCs a b =
let reverseOrdering :: (Ordering, LazyCardinality, LazyCardinality) -> (Ordering, LazyCardinality, LazyCardinality)
reverseOrdering (GT, a, b) = (LT, b, a)
reverseOrdering (LT, a, b) = (GT, b, a)
reverseOrdering (EQ, a, b) = (EQ, b, a)
in case (a,b) of
(InfiniteC , InfiniteC) -> (EQ, a, b)
(InfiniteC , _ ) -> (GT, a, b)
(_ , InfiniteC) -> (LT, a, b)
(PreciseC m, PreciseC n) -> (m `compare` n, a, b)
(RefinableC crs@(m, _), PreciseC n) -> case m > n of { True -> (GT, a, b); False -> almostStrictCompare2LCs (refineCRS_TillOneAbove crs n) b }
(RefinableC crs1, RefinableC crs2) -> compare2Refinements crs1 crs2
(_ , RefinableC _) -> reverseOrdering $ almostStrictCompare2LCs b a
instance Eq LazyCardinality where
lc1 == lc2 = (fst3 $ almostStrictCompare2LCs lc1 lc2) == EQ
instance Ord LazyCardinality where
lc1 `compare` lc2 = fst3 $ almostStrictCompare2LCs lc1 lc2
infixr 9 `lazyCompare2LCs`
lazyCompare2LCs :: LazyCardinality -> LazyCardinality -> Maybe Ordering
lazyCompare2LCs a b =
let reverseOrdering :: Maybe Ordering -> Maybe Ordering
reverseOrdering (Just GT) = (Just LT)
reverseOrdering (Just LT) = (Just GT)
reverseOrdering (Just EQ) = (Just EQ)
reverseOrdering Nothing = Nothing
in case (a,b) of
(InfiniteC , InfiniteC) -> Just EQ
(InfiniteC , _ ) -> Just GT
(_ , InfiniteC) -> Just LT
(PreciseC m, PreciseC n) -> Just (m `compare` n)
(RefinableC crs@(m, _), PreciseC n) -> case m > n of { True -> Just GT; False -> Nothing }
(PreciseC n, RefinableC crs@(m, _)) -> case m > n of { True -> Just LT; False -> Nothing }
_ -> Nothing
showLazy :: LazyCardinality -> String
showLazy lc =
case lc of
InfiniteC -> "infiniteC"
PreciseC c -> "preciseC " ++ show c
RefinableC (c, _) -> "Refinable (" ++ show c ++ ", refine_f)"
showStrict :: LazyCardinality -> String
showStrict lc =
case lc of
InfiniteC -> "infiniteC"
PreciseC c -> "preciseC " ++ show c
RefinableC crs -> show $ refineCRS_TillEnd crs
instance Show LazyCardinality where
show = showLazy
class HasCard a where
cardOf :: a -> LazyCardinality
class HasCardT t where
cardOfT :: t elem -> LazyCardinality
cardOf_Unity :: () -> LazyCardinality
cardOf_Unity _ = preciseC 0
instance HasCard () where
cardOf = cardOf_Unity
cardOf_EmptySet :: EmptySet a -> LazyCardinality
cardOf_EmptySet _ = preciseC 0
instance HasCard (EmptySet a) where
cardOf = cardOf_EmptySet
instance HasCardT EmptySet where
cardOfT = cardOf_EmptySet
cardOf_Identity1 :: Identity a -> LazyCardinality
cardOf_Identity1 _ = preciseC 1
instance HasCard (Identity a) where
cardOf = cardOf_Identity1
instance HasCardT Identity where
cardOfT = cardOf_Identity1
cardOf_Maybe :: Maybe a -> LazyCardinality
cardOf_Maybe Nothing = preciseC 0
cardOf_Maybe (Just _) = preciseC 1
instance HasCard (Maybe a) where
cardOf = cardOf_Maybe
instance HasCardT Maybe where
cardOfT = cardOf_Maybe
cardOf_List :: [a] -> LazyCardinality
cardOf_List l = refinableC (0, \ sofar refine_while -> length2 l sofar refine_while)
instance HasCard [a] where
cardOf = cardOf_List
instance HasCardT ([]) where
cardOfT = cardOf_List
cardOf_Map :: Map k e -> LazyCardinality
cardOf_Map = preciseC . fromIntegral . M.size
instance HasCard (Map k e) where
cardOf = cardOf_Map
instance HasCardT (Map k) where
cardOfT = cardOf_Map
cardOf_NeverEmptyList :: NeverEmptyList k -> LazyCardinality
cardOf_NeverEmptyList (NEL _ l) = 1 `addPCToLC` cardOf l
instance HasCard (NeverEmptyList a) where
cardOf = cardOf_NeverEmptyList
instance HasCardT NeverEmptyList where
cardOfT = cardOf_NeverEmptyList
instance HasCardT ((,) key) where { cardOfT _ = preciseC 1 }
instance HasCard (a,a) where { cardOf _ = preciseC 2 }
instance HasCard (a,a,a) where { cardOf _ = preciseC 3 }
instance HasCard (a,a,a,a) where { cardOf _ = preciseC 4 }
instance HasCard (a,a,a,a,a) where { cardOf _ = preciseC 5 }
instance HasCard (a,a,a,a,a,a) where { cardOf _ = preciseC 6 }
instance HasCard (a,a,a,a,a,a,a) where { cardOf _ = preciseC 7 }
instance HasCard (a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 8 }
instance HasCard (a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 9 }
instance HasCard (a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 10 }
instance HasCard (a,a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 11 }
instance HasCard (a,a,a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 12 }
length2 :: [a] -> ContinueRefiningCardinalityUntil
length2 l !sofar p =
case _length2 l sofar of
(i, Nothing) -> preciseC i
(i, Just new_ref_while) -> RefinableC (i, new_ref_while)
where
_length2 :: [a] -> CurrentNotFinalPreciseCardinality
-> ( BoundaryPreciseCardinality
, Maybe ContinueRefiningCardinalityUntil
)
_length2 [] !_sofar = (_sofar, Nothing)
_length2 l@(_:t) !_sofar =
let next_sofar = _sofar + 1
in case p next_sofar of
False -> (_sofar, Just (length2 l))
True -> _length2 t next_sofar
fst3 :: (a,b,c) -> a
snd3 :: (a,b,c) -> b
thrd3 :: (a,b,c) -> c
fst3 (a,_,_) = a
snd3 (_,b,_) = b
thrd3 (_,_,c) = c