{-
Copyright (C) 2010 Andrejs Sisojevs <andrejs.sisojevs@nextmail.ru>

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.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