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


-- | Nat and Fin
--   
--   This package provides two simple types, and some tools to work with
--   them. Also on type level as <tt>DataKinds</tt>.
--   
--   <pre>
--   data Nat = Z | S Nat
--   data Fin (n :: Nat) where
--   Z :: Fin ('Nat.S n)
--   S :: Fin n -&gt; Fin ('Nat.S n)
--   </pre>
--   
--   The <a>Data.Fin.Enum</a> module let's work generically with
--   enumerations.
--   
--   Differences to other packages:
--   
--   <ul>
--   <li><a>type-natural</a> depends on <tt>singletons</tt> package.
--   <a>fin</a> will try to stay light on the dependencies, and support as
--   many GHC versions as practical.</li>
--   <li><a>peano</a> is very incomplete</li>
--   <li><a>nat</a> as well.</li>
--   <li><a>PeanoWitnesses</a> doesn't use <tt>DataKinds</tt>.</li>
--   <li><a>type-combinators</a> is big package too.</li>
--   </ul>
@package fin
@version 0


-- | <a>Nat</a> numbers.
--   
--   This module is designed to be imported qualified.
module Data.Nat

-- | Nat natural numbers.
--   
--   Better than GHC's built-in <a>Nat</a> for some use cases.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Convert <a>Nat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 2
--   2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural $ S $ S $ Z
--   2
--   </pre>
toNatural :: Nat -> Natural

-- | Convert <a>Natural</a> to <a>Nat</a>
--   
--   <pre>
--   &gt;&gt;&gt; fromNatural 4
--   4
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--   </pre>
fromNatural :: Natural -> Nat

-- | Fold <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; cata [] ('x' :) 2
--   "xx"
--   </pre>
cata :: a -> (a -> a) -> Nat -> a

-- | <a>show</a> displaying a structure of <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 0
--   "Z"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 2
--   "S (S Z)"
--   </pre>
explicitShow :: Nat -> String

-- | <a>showsPrec</a> displaying a structure of <a>Nat</a>.
explicitShowsPrec :: Int -> Nat -> ShowS
nat0 :: Nat
nat1 :: Nat
nat2 :: Nat
nat3 :: Nat
nat4 :: Nat
nat5 :: Nat
nat6 :: Nat
nat7 :: Nat
nat8 :: Nat
nat9 :: Nat
instance Data.Data.Data Data.Nat.Nat
instance GHC.Classes.Ord Data.Nat.Nat
instance GHC.Classes.Eq Data.Nat.Nat
instance GHC.Show.Show Data.Nat.Nat
instance GHC.Num.Num Data.Nat.Nat
instance GHC.Real.Real Data.Nat.Nat
instance GHC.Real.Integral Data.Nat.Nat
instance GHC.Enum.Enum Data.Nat.Nat
instance Control.DeepSeq.NFData Data.Nat.Nat
instance Data.Hashable.Class.Hashable Data.Nat.Nat


-- | <a>Nat</a> numbers. <tt>DataKinds</tt> stuff.
--   
--   This module re-exports <a>Data.Nat</a>, and adds type-level things.
module Data.Type.Nat

-- | Nat natural numbers.
--   
--   Better than GHC's built-in <a>Nat</a> for some use cases.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Convert <a>Nat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 2
--   2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural $ S $ S $ Z
--   2
--   </pre>
toNatural :: Nat -> Natural

-- | Convert <a>Natural</a> to <a>Nat</a>
--   
--   <pre>
--   &gt;&gt;&gt; fromNatural 4
--   4
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--   </pre>
fromNatural :: Natural -> Nat

-- | Fold <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; cata [] ('x' :) 2
--   "xx"
--   </pre>
cata :: a -> (a -> a) -> Nat -> a

-- | <a>show</a> displaying a structure of <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 0
--   "Z"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 2
--   "S (S Z)"
--   </pre>
explicitShow :: Nat -> String

-- | <a>showsPrec</a> displaying a structure of <a>Nat</a>.
explicitShowsPrec :: Int -> Nat -> ShowS

-- | Singleton of <a>Nat</a>.
data SNat (n :: Nat)
[SZ] :: SNat Z
[SS] :: SNatI n => SNat (S n)

-- | Convert <a>SNat</a> to <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; snatToNat (snat :: SNat Nat1)
--   1
--   </pre>
snatToNat :: forall n. SNat n -> Nat

-- | Convert <a>SNat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; snatToNatural (snat :: SNat Nat0)
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; snatToNatural (snat :: SNat Nat2)
--   2
--   </pre>
snatToNatural :: forall n. SNat n -> Natural

-- | Convenience class to get <a>SNat</a>.
class SNatI (n :: Nat)
snat :: SNatI n => SNat n

-- | Reify <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; reify nat3 reflect
--   3
--   </pre>
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r

-- | Reflect type-level <a>Nat</a> to the term level.
reflect :: forall n proxy. SNatI n => proxy n -> Nat

-- | As <a>reflect</a> but with any <a>Num</a>.
reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m

-- | Decide equality of type-level numbers.
--   
--   <pre>
--   &gt;&gt;&gt; eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
--   Just Refl
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
--   Nothing
--   </pre>
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)

-- | Type family used to implement <a>==</a> from <a>Data.Type.Equality</a>
--   module.

-- | Induction on <a>Nat</a>.
--   
--   Useful in proofs or with GADTs, see source of <a>proofPlusNZero</a>.
induction :: forall n f. SNatI n => f Z -> (forall m. SNatI m => f m -> f (S m)) -> f n

-- | Induction on <a>Nat</a>, functor form. Useful for computation.
--   
--   <pre>
--   &gt;&gt;&gt; induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int
--   Tagged 6
--   </pre>
induction1 :: forall n f a. SNatI n => f Z a -> (forall m. SNatI m => f m a -> f (S m) a) -> f n a

-- | The induction will be fully inlined.
--   
--   See <tt>test/Inspection.hs</tt>.
class SNatI n => InlineInduction (n :: Nat)
inlineInduction1 :: InlineInduction n => f Z a -> (forall m. InlineInduction m => f m a -> f (S m) a) -> f n a

-- | See <a>InlineInduction</a>.
inlineInduction :: forall n f. InlineInduction n => f Z -> (forall m. InlineInduction m => f m -> f (S m)) -> f n

-- | Unfold <tt>n</tt> steps of a general recursion.
--   
--   <i>Note:</i> Always <b>benchmark</b>. This function may give you both
--   <i>bad</i> properties: a lot of code (increased binary size), and
--   worse performance.
--   
--   For known <tt>n</tt> <a>unfoldedFix</a> will unfold recursion, for
--   example
--   
--   <pre>
--   <a>unfoldedFix</a> (<a>Proxy</a> :: <a>Proxy</a> <a>Nat3</a>) f = f (f (f (fix f)))
--   </pre>
unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a

-- | Addition.
--   
--   <pre>
--   &gt;&gt;&gt; reflect (snat :: SNat (Plus Nat1 Nat2))
--   3
--   </pre>

-- | Multiplication.
--   
--   <pre>
--   &gt;&gt;&gt; reflect (snat :: SNat (Mult Nat2 Nat3))
--   6
--   </pre>

-- | Convert to GHC <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! ToGHC Nat5
--   ToGHC Nat5 :: GHC.Nat
--   = 5
--   </pre>

-- | Convert from GHC <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! FromGHC 7
--   FromGHC 7 :: Nat
--   = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
--   </pre>
nat0 :: Nat
nat1 :: Nat
nat2 :: Nat
nat3 :: Nat
nat4 :: Nat
nat5 :: Nat
nat6 :: Nat
nat7 :: Nat
nat8 :: Nat
nat9 :: Nat
type Nat0 = Z
type Nat1 = S Nat0
type Nat2 = S Nat1
type Nat3 = S Nat2
type Nat4 = S Nat3
type Nat5 = S Nat4
type Nat6 = S Nat5
type Nat7 = S Nat6
type Nat8 = S Nat7
type Nat9 = S Nat8

-- | <pre>
--   0 + n = n
--   </pre>
proofPlusZeroN :: Plus Nat0 n :~: n

-- | <pre>
--   n + 0 = n
--   </pre>
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n

-- | <pre>
--   0 * n = 0
--   </pre>
proofMultZeroN :: Mult Nat0 n :~: Nat0

-- | <pre>
--   n * 0 = n
--   </pre>
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0

-- | <pre>
--   1 * n = n
--   </pre>
proofMultOneN :: SNatI n => Mult Nat1 n :~: n

-- | <pre>
--   n * 1 = n
--   </pre>
proofMultNOne :: SNatI n => Mult n Nat1 :~: n
instance GHC.Show.Show a => GHC.Show.Show (Data.Type.Nat.Tagged n a)
instance GHC.Show.Show (Data.Type.Nat.SNat p)
instance Data.Type.Nat.SNatI 'Data.Nat.Z
instance Data.Type.Nat.SNatI n => Data.Type.Nat.SNatI ('Data.Nat.S n)
instance Data.Type.Equality.TestEquality Data.Nat.Nat Data.Type.Nat.SNat
instance Data.Type.Nat.InlineInduction 'Data.Nat.Z
instance Data.Type.Nat.InlineInduction n => Data.Type.Nat.InlineInduction ('Data.Nat.S n)


-- | Finite numbers.
--   
--   This module is designed to be imported qualified.
module Data.Fin

-- | Finite Numbers up to <tt>n</tt>.
data Fin (n :: Nat)
[Z] :: Fin (S n)
[S] :: Fin n -> Fin (S n)

-- | Fold <a>Fin</a>.
cata :: forall a n. a -> (a -> a) -> Fin n -> a

-- | <a>show</a> displaying a structure of <a>Fin</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (0 :: Fin N.Nat1)
--   "Z"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (2 :: Fin N.Nat3)
--   "S (S Z)"
--   </pre>
explicitShow :: Fin n -> String

-- | <a>showsPrec</a> displaying a structure of <a>Fin</a>.
explicitShowsPrec :: Int -> Fin n -> ShowS

-- | Convert to <tt>Nat</tt>.
toNat :: Fin n -> Nat

-- | Convert from <tt>Nat</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; fromNat N.nat1 :: Maybe (Fin N.Nat2)
--   Just 1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; fromNat N.nat1 :: Maybe (Fin N.Nat1)
--   Nothing
--   </pre>
fromNat :: SNatI n => Nat -> Maybe (Fin n)

-- | Convert to <a>Natural</a>.
toNatural :: Fin n -> Natural

-- | conversion to <a>Integer</a>
toInteger :: Integral a => a -> Integer

-- | Multiplicative inverse.
--   
--   Works for <tt><a>Fin</a> n</tt> where <tt>n</tt> is coprime with an
--   argument, i.e. in general when <tt>n</tt> is prime.
--   
--   <pre>
--   &gt;&gt;&gt; map inverse universe :: [Fin N.Nat5]
--   [0,1,3,2,4]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
--   [0,1,1,1,1]
--   </pre>
--   
--   Adaptation of <a>pseudo-code in Wikipedia</a>
inverse :: forall n. SNatI n => Fin n -> Fin n

-- | All values. <tt>[minBound .. maxBound]</tt> won't work for
--   <tt><a>Fin</a> <a>Nat0</a></tt>.
--   
--   <pre>
--   &gt;&gt;&gt; universe :: [Fin N.Nat3]
--   [0,1,2]
--   </pre>
universe :: SNatI n => [Fin n]

-- | <a>universe</a> which will be fully inlined, if <tt>n</tt> is known at
--   compile time.
--   
--   <pre>
--   &gt;&gt;&gt; inlineUniverse :: [Fin N.Nat3]
--   [0,1,2]
--   </pre>
inlineUniverse :: InlineInduction n => [Fin n]

-- | Like <a>universe</a> but <a>NonEmpty</a>.
--   
--   <pre>
--   &gt;&gt;&gt; universe1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--   </pre>
universe1 :: SNatI n => NonEmpty (Fin (S n))

-- | <pre>
--   &gt;&gt;&gt; inlineUniverse1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--   </pre>
inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))

-- | <tt><a>Fin</a> <a>Nat0</a></tt> is inhabited.
absurd :: Fin Nat0 -> b

-- | Counting to one is boring.
--   
--   <pre>
--   &gt;&gt;&gt; boring
--   0
--   </pre>
boring :: Fin Nat1
fin0 :: Fin (Plus Nat0 (S n))
fin1 :: Fin (Plus Nat1 (S n))
fin2 :: Fin (Plus Nat2 (S n))
fin3 :: Fin (Plus Nat3 (S n))
fin4 :: Fin (Plus Nat4 (S n))
fin5 :: Fin (Plus Nat5 (S n))
fin6 :: Fin (Plus Nat6 (S n))
fin7 :: Fin (Plus Nat7 (S n))
fin8 :: Fin (Plus Nat8 (S n))
fin9 :: Fin (Plus Nat9 (S n))
instance GHC.Classes.Eq (Data.Fin.Fin n)
instance GHC.Classes.Ord (Data.Fin.Fin n)
instance GHC.Show.Show (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Num.Num (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Real.Real (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Real.Integral (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Enum.Enum (Data.Fin.Fin n)
instance (n ~ 'Data.Nat.S m, Data.Type.Nat.SNatI m) => GHC.Enum.Bounded (Data.Fin.Fin n)
instance Control.DeepSeq.NFData (Data.Fin.Fin n)
instance Data.Hashable.Class.Hashable (Data.Fin.Fin n)


-- | This module is designed to be imported qualified:
--   
--   <pre>
--   import qualified Data.Fin.Enum as E
--   </pre>
module Data.Fin.Enum

-- | Generic enumerations.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; from ()
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; to 0 :: ()
--   ()
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; to 0 :: Bool
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; map to F.universe :: [Bool]
--   [False,True]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic
--   [EQ,GT,LT]
--   </pre>
class Enum a where type EnumSize a :: Nat type EnumSize a = GEnumSize a from = gfrom to = gto where {
    type family EnumSize a :: Nat;
    type EnumSize a = GEnumSize a;
}

-- | Converts a value to its index.
from :: Enum a => a -> Fin (EnumSize a)

-- | Converts a value to its index.
from :: (Enum a, Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)

-- | Converts from index to the original value.
to :: Enum a => Fin (EnumSize a) -> a

-- | Converts from index to the original value.
to :: (Enum a, Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a

-- | Generic version of <a>from</a>.
gfrom :: (Generic a, GFrom a) => a -> Fin (GEnumSize a)

-- | Constraint for the class that computes <a>gfrom</a>.
type GFrom a = GFromRep (Rep a)

-- | Generic version of <a>to</a>.
gto :: (Generic a, GTo a) => Fin (GEnumSize a) -> a

-- | Constraint for the class that computes <a>gto</a>.
type GTo a = GToRep (Rep a)

-- | Compute the size from the type.
type GEnumSize a = EnumSizeRep (Rep a) Nat0
instance Data.Fin.Enum.Enum Data.Void.Void
instance Data.Fin.Enum.Enum ()
instance Data.Fin.Enum.Enum GHC.Types.Bool
instance Data.Fin.Enum.Enum GHC.Types.Ordering
instance (Data.Fin.Enum.GFromRep a, Data.Fin.Enum.GFromRep b) => Data.Fin.Enum.GFromRep (a GHC.Generics.:+: b)
instance Data.Fin.Enum.GFromRep a => Data.Fin.Enum.GFromRep (GHC.Generics.M1 d c a)
instance Data.Fin.Enum.GFromRep GHC.Generics.V1
instance Data.Fin.Enum.GFromRep GHC.Generics.U1
instance (Data.Fin.Enum.GToRep a, Data.Fin.Enum.GToRep b) => Data.Fin.Enum.GToRep (a GHC.Generics.:+: b)
instance Data.Fin.Enum.GToRep a => Data.Fin.Enum.GToRep (GHC.Generics.M1 d c a)
instance Data.Fin.Enum.GToRep GHC.Generics.V1
instance Data.Fin.Enum.GToRep GHC.Generics.U1