{- Copyright (C) 2010 Andrejs Sisojevs All rights reserved. For license and copyright information, see the file COPYRIGHT -} -------------------------------------------------------------------------- -------------------------------------------------------------------------- {-# LANGUAGE BangPatterns, FlexibleInstances #-} -- | Two main assumptions (and constraints) of this module: -- -- (1) Cardinality can't be negative. -- -- (2) For @'refinableC'@ construction it is always refined by growing. F.e., -- if @'refinableC' (7, ref_f_1)@ refines to @'refinableC' (x, ref_f_2)@, then -- @x@ SHOULD NEVER be less then @7@. -- On this assumption relies heavily functions @'lazyIsZeroLC'@, -- @'lazyCompare2LCs'@, @'addLCToLC'@ and also almost every refinement routine. module Data.Cardinality ( -- * Core 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 -- * Application , HasCard(..) , HasCardT(..) -- * Instances -- ** Cardinality = 0 , cardOf_Unity , cardOf_EmptySet -- ** Cardinality = 1 -- , cardOf_Identity0 , cardOf_Identity1 -- ** Cardinality = 0..1 , cardOf_Maybe -- ** Cardinality = 0..Inf , cardOf_List , cardOf_Map -- ** Cardinality = 1..Inf , cardOf_NeverEmptyList -- * Helpers , 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 -------------------------------------------------------------- -- * Core -- | Count of elements in container. It's always positive or zero. -- -- It would be best here to use @'Word32'@ instead, however, with @Integer@ -- it's easier to catch the error of going down below zero (in case -- of @'Word32' 0-1==4294967295@ ). -- -- However it is decided not to allow the direct use of @'PreciseC'@ data -- constructor, but to wrap it into function @'preciseC'@, which guards from -- the attemts to conctruct negative cardinality (by throwing an error). type PreciseCardinality = Integer type CurrentNotFinalPreciseCardinality = PreciseCardinality type BoundaryPreciseCardinality = CurrentNotFinalPreciseCardinality type ContinueCounting_DoWe = Bool -- | An example of this is @'length2'@ function. type ContinueRefiningCardinalityUntil = CurrentNotFinalPreciseCardinality -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -> LazyCardinality type CardinalityRefinementState = (CurrentNotFinalPreciseCardinality, ContinueRefiningCardinalityUntil) -- | In other words: count of elements in a container, -- with an opportunity not to refine the whole content of the container -- (and the container's structure). -- -- Constructors: -- -- * @'infiniteC'@ -- -- * @'preciseC' 'PreciseCardinality'@ -- -- * @'refinableC' 'CardinalityRefinementState'@ data LazyCardinality = InfiniteC | PreciseC PreciseCardinality | RefinableC CardinalityRefinementState deriving (Typeable) -- | @'LazyCardinality'@ constructor. -- -- F.e., @[1..]@ list has such cardinality. infiniteC :: LazyCardinality infiniteC = InfiniteC -- | @'LazyCardinality'@ constructor. If given negative value, raises error. -- -- F.e., the tuple @(5,6)@ has a precise cardinality 2. preciseC :: PreciseCardinality -> LazyCardinality preciseC c = case c < 0 of { True -> error ("Can't construct negative cardinality '" ++ show c ++ "' "); False -> PreciseC c } -- | @'LazyCardinality'@ constructor. -- -- For lists it happens, that we do not want to count all the elements -- of a container, -- but want to count them until some lower boundary. For example, -- I do not want to know the length of the list (which involves taking -- each element of it, and counting it in) to reason about whether -- it's content fit into the @(,,)@ data constructor. For this -- case I only need to count till 3rd element and check, if list is -- continued. It's actual especially, when dealing with infinite lists -- or with lists, whose reading may block. -- -- For @(refinableC (x0, refine_f))@ important rules: -- -- 1. If @(refine_f x0 (<= 5))@ evaluates to another @refinableC@, then -- it is not fully refined, but (at least) @5@ is achieved (the precise -- cardinality is @>= 5@). -- -- 2. If @x0@ is @10@ and @(refine_f 10 (<= 15))@ returned -- @(refinableC (17, refine_f_2))@, then it is known, that precise -- cardinality is already >= @10 + 7@. In sight of @refine_f@ there -- SHOULD be everything except for what's already counted in @x0@ -- (which is @10@), and in sight of @refine_f_2@ there should be even -- less by @7@ elements comparing to @refine_f@. So if total cardinality was -- @25@, then @(refine_f_2 17 (<= 30))@ MUST return @preciseC 25@, to make -- @10 + 7 + 8 = 25@. -- -- 3. The theatment of the first argument of refinement function @refine_f@ -- must be relative. For example, given total count of elements @= 25@ , -- and @x0 = 20@ - these 20 elements are already counted, and in sight of -- @refine_f@ there are only 5 last elements. -- Then @refine_f 20 (<= 26)@ will result in @preciseC 25@, but(!) -- @refine_f 10 (<= 16)@ MUST result in @preciseC 15@. -- -- Recomendations: -- -- 1. If subject has infinite cardinality, it's best to determine -- it's cardinality as @'infiniteC'@ at early stages and -- avoid using @refinableC@ for it. refinableC :: CardinalityRefinementState -> LazyCardinality refinableC = RefinableC lcIsInfinite :: LazyCardinality -> Bool lcIsInfinite InfiniteC = True lcIsInfinite _ = False preciseOfLC :: LazyCardinality -> Maybe PreciseCardinality preciseOfLC (PreciseC c) = Just c preciseOfLC _ = Nothing -- | Returns @Nothing@, ONLY if LC is @'refinableC' (0, _)@ -- (according to 2nd assumption of the module). Returns @Just True@ -- only for @'preciseC' 0@. 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` -- Throws an error if @'preciseC'@ is attempted to construct with negative -- resulting cardinality. 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` -- | For case when adding up 2 refinables, if both of them sooner or later -- refines to @'infiniteC'@, then one that returns infinity earlier is -- recommended to put as a first term. Infinity + any LazyCardinality -- = infinity. Another recommendation would be to put -- refinable that's easier to compute as a first term. 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 ) -- | @foldl 'addLCToLC'@ -- -- See recommendations by @'addLCToLC'@. 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) -- [1,2,3,4,5,6,7,8,9,10] -- refineCRS_Till (refinableC (5, ref_while)) 8 -- ref_while sees [6,7,8,9,10] -- ref_while (<= 8 - 5) -> ref_while (<= 3) -> refinableC (8, ref_while')) -- ref_while' sees [9, 10] 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)) -- | Don't use it on infinite refinables not measured with 'infiniteC'. refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinality refineCRS_TillEnd crs@(c, ref_while) = ref_while c (const True) -- | Wrapper around @'refineCRS_Till'@. refineTill :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality refineTill lc n = case lc of RefinableC crs -> refineCRS_Till crs n _ -> lc -- | Wrapper around @'refineTillOneAbove'@. refineTillOneAbove :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality -- | Wrapper around @'refineTillOneBelow'@. 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 } -- | Wrapper around @'crsRefinementStep'@. refinementStep :: LazyCardinality -> LazyCardinality refinementStep lc = case lc of { RefinableC crs -> crsRefinementStep crs ; _ -> lc } -- | Wrapper around @'refineCRS_TillEnd'@. refineTillEnd :: LazyCardinality -> LazyCardinality refineTillEnd lc = case lc of { RefinableC crs -> refineCRS_TillEnd crs ; _ -> lc } -- | For @equalize2Refinements (m, ref_f_1) (n, ref_f_2)@ finishes when m == n. -- Else refines them. Another termination condition is when in result of -- refinement one of cardinalities becomes final (not @'refinableC'@). 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)) -> -- m == n let lc1_3 = crsRefinementStep crs1_2 in case lc1_3 of -- I could have made crsRefinementStep for both in tuple here, but let's keep it as lazy as possible 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` -- | Used for instance of Ord typeclass. -- -- Together with @'Ordering'@ returns also probably refined cardinalities -- for reuse. -- -- WARNING!!! When comparing @'refinableC'@ with @'infiniteC'@ -- , it results in @'LT'@ (less than)! -- While comparing @'infiniteC' \`almostStrictCompare2LCs\` 'infiniteC' == -- 'EQ'@. -- That's the reason for an /almost-/ prefix in function name. -- If there is a probability that refinement of -- @'refinableC'@ may evaluate to @'infiniteC'@, and it's important to you, -- that infinities are equal, then before comparing this refinable, -- use 'refineCRS_TillEnd' on it. That's laziness. -- -- Trying to compare 2 @'refinableC'@s that are actually infinite, but don't -- use @'infiniteC'@ will hang -- the system (the same as if you try to determine length of an infinite -- list). 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) -- !!! even though 'refinableC' may return 'infiniteC' !!! (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` -- | Won't refine refinables. According to 2nd assumption of the module: -- -- @'refinableC' (m, _) \`lazyCompare2LCs\` 'preciseC' n@ -- -- equals to @Just GT@ if @m > n@ , and @Nothing@ otherwise. 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 -- !!! even though 'refinableC' may return 'infiniteC' !!! (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 -- | Used for Show typeclass instaniation. Here @'refinableC'@ isn't refined. showLazy :: LazyCardinality -> String showLazy lc = case lc of InfiniteC -> "infiniteC" PreciseC c -> "preciseC " ++ show c RefinableC (c, _) -> "Refinable (" ++ show c ++ ", refine_f)" -- | Here @ 'refineCRS_TillEnd'@ is applied to @'refinableC'@ argument. 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 -------------------------------------------------------------- -- * Application -- | @HasCard@ = \"Has cardinality\". In other words, \"it's possible to measure -- current count of elements for this container\" class HasCard a where cardOf :: a -> LazyCardinality -- | @HasCardT@ = \"Has cardinality (for container types of kind @(* -> *)@)\". -- In other words, \"it's possible to measure -- current count of elements for this container (for container types of -- kind @(* -> *)@)\" class HasCardT t where cardOfT :: t elem -> LazyCardinality -------------------------------------------------------------- -------------------------------------------------------------- -- * Instances -- ** Cardinality = 0 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 -- ** Cardinality = 1 {- cardOf_Identity0 :: a -> LazyCardinality cardOf_Identity0 _ = preciseC 1 instance HasCard a where cardOf = cardOf_Identity0 -} cardOf_Identity1 :: Identity a -> LazyCardinality cardOf_Identity1 _ = preciseC 1 instance HasCard (Identity a) where cardOf = cardOf_Identity1 instance HasCardT Identity where cardOfT = cardOf_Identity1 -- ** Cardinality = 0..1 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 -- ** Cardinality = 0..N -- | Refinable starting from 0, uses @'length2'@ 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 -- | Not refinable, since @'Data.Map.Map'@ is a strict structure. 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 -- ** Cardinality = 1..N -- | Refinable starting from 1. 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 -- Other instances instance HasCardT ((,) key) where { cardOfT _ = preciseC 1 } -- this messes up things, in the context of HasCard (a,a) instance... 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 } -------------------------------------------------------------- -- * Helpers -- type ContinueRefiningCardinalityUntil = -- CurrentNotFinalPreciseCardinality -- -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -- -> LazyCardinality -- | List length of controlable greediness. 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