-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A type inhabited by finitely many values, indexed by type-level naturals.
--   
--   A type inhabited by finitely many values, indexed by type-level
--   naturals.
@package finite-typelits
@version 0.1.2.0


module Data.Finite.Internal

-- | Finite number type. <tt><a>Finite</a> n</tt> is inhabited by exactly
--   <tt>n</tt> values. Invariants:
--   
--   <pre>
--   getFinite x &lt; natVal x
--   </pre>
--   
--   <pre>
--   getFinite x &gt;= 0
--   </pre>
newtype Finite (n :: Nat)
Finite :: Integer -> Finite

-- | Convert an <a>Integer</a> into a <a>Finite</a>, throwing an error if
--   the input is out of bounds.
finite :: KnownNat n => Integer -> Finite n

-- | Convert a <a>Finite</a> into the corresponding <a>Integer</a>.
getFinite :: Finite n -> Integer
instance GHC.Generics.Generic (Data.Finite.Internal.Finite n)
instance GHC.Classes.Ord (Data.Finite.Internal.Finite n)
instance GHC.Classes.Eq (Data.Finite.Internal.Finite n)
instance GHC.TypeLits.KnownNat n => GHC.Enum.Bounded (Data.Finite.Internal.Finite n)
instance GHC.TypeLits.KnownNat n => GHC.Enum.Enum (Data.Finite.Internal.Finite n)
instance GHC.Show.Show (Data.Finite.Internal.Finite n)
instance GHC.TypeLits.KnownNat n => GHC.Num.Num (Data.Finite.Internal.Finite n)
instance GHC.TypeLits.KnownNat n => GHC.Real.Real (Data.Finite.Internal.Finite n)
instance GHC.TypeLits.KnownNat n => GHC.Real.Integral (Data.Finite.Internal.Finite n)
instance Control.DeepSeq.NFData (Data.Finite.Internal.Finite n)


module Data.Finite

-- | Finite number type. <tt><a>Finite</a> n</tt> is inhabited by exactly
--   <tt>n</tt> values. Invariants:
--   
--   <pre>
--   getFinite x &lt; natVal x
--   </pre>
--   
--   <pre>
--   getFinite x &gt;= 0
--   </pre>
data Finite (n :: Nat)

-- | Convert an <a>Integer</a> into a <a>Finite</a>, returning
--   <a>Nothing</a> if the input is out of bounds.
packFinite :: KnownNat n => Integer -> Maybe (Finite n)

-- | Same as <a>packFinite</a> but with a proxy argument to avoid type
--   signatures.
packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe (Finite n)

-- | Convert an <a>Integer</a> into a <a>Finite</a>, throwing an error if
--   the input is out of bounds.
finite :: KnownNat n => Integer -> Finite n

-- | Same as <a>finite</a> but with a proxy argument to avoid type
--   signatures.
finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n

-- | Convert a <a>Finite</a> into the corresponding <a>Integer</a>.
getFinite :: Finite n -> Integer

-- | Generate a list of length <tt>n</tt> of all elements of
--   <tt><a>Finite</a> n</tt>.
finites :: KnownNat n => [Finite n]

-- | Same as <a>finites</a> but with a proxy argument to avoid type
--   signatures.
finitesProxy :: KnownNat n => proxy n -> [Finite n]

-- | Test two different types of finite numbers for equality.
equals :: Finite n -> Finite m -> Bool
infix 4 `equals`

-- | Compare two different types of finite numbers.
cmp :: Finite n -> Finite m -> Ordering

-- | Convert a type-level literal into a <a>Finite</a>.
natToFinite :: (KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m

-- | Add one inhabitant in the end.
weaken :: Finite n -> Finite (n + 1)

-- | Remove one inhabitant from the end. Returns <a>Nothing</a> if the
--   input was the removed inhabitant.
strengthen :: KnownNat n => Finite (n + 1) -> Maybe (Finite n)

-- | Add one inhabitant in the beginning, shifting everything up by one.
shift :: Finite n -> Finite (n + 1)

-- | Remove one inhabitant from the beginning, shifting everything down by
--   one. Returns <a>Nothing</a> if the input was the removed inhabitant.
unshift :: Finite (n + 1) -> Maybe (Finite n)

-- | Add multiple inhabitants in the end.
weakenN :: (n <= m) => Finite n -> Finite m

-- | Remove multiple inhabitants from the end. Returns <a>Nothing</a> if
--   the input was one of the removed inhabitants.
strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)

-- | Add multiple inhabitant in the beginning, shifting everything up by
--   the amount of inhabitants added.
shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m

-- | Remove multiple inhabitants from the beginning, shifting everything
--   down by the amount of inhabitants removed. Returns <a>Nothing</a> if
--   the input was one of the removed inhabitants.
unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n)
weakenProxy :: proxy k -> Finite n -> Finite (n + k)
strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)
shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k)
unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n)

-- | Add two <a>Finite</a>s.
add :: Finite n -> Finite m -> Finite (n + m)

-- | Subtract two <a>Finite</a>s. Returns <a>Left</a> for negative results,
--   and <a>Right</a> for positive results. Note that this function never
--   returns <tt><a>Left</a> 0</tt>.
sub :: Finite n -> Finite m -> Either (Finite m) (Finite n)

-- | Multiply two <a>Finite</a>s.
multiply :: Finite n -> Finite m -> Finite (n * m)

-- | <a>Left</a>-biased (left values come first) disjoint union of finite
--   sets.
combineSum :: KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m)

-- | <a>fst</a>-biased (fst is the inner, and snd is the outer iteratee)
--   product of finite sets.
combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n * m)

-- | Take a <a>Left</a>-biased disjoint union apart.
separateSum :: KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m)

-- | Take a <a>fst</a>-biased product apart.
separateProduct :: KnownNat n => Finite (n * m) -> (Finite n, Finite m)

-- | Verifies that a given <a>Finite</a> is valid. Should always return
--   <a>True</a> unles you bring the <tt>Data.Finite.Internal.Finite</tt>
--   constructor into the scope, or use <a>unsafeCoerce</a> or other nasty
--   hacks
isValidFinite :: KnownNat n => Finite n -> Bool
