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


-- | Collection of widely reimplemented type families
--   
--   Collection of widely reimplemented type families
@package type-fun
@version 0.1.2

module TypeFun.Constraint

-- | Apply constraint for each element of list
type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint

module TypeFun.Data.Eq
type family Equal (a :: k) (b :: k) :: Bool

module TypeFun.Data.Maybe
type family MaybeCase (a :: Maybe k) (nothing :: r) (just :: k -> r) :: r
type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint
type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint

-- | Like <tt>catMaybes</tt> for type lists
type family CatMaybes (l :: [Maybe k]) :: [k]
type family FromJust (a :: Maybe k) :: k

module TypeFun.Data.Peano
data N
Z :: N
S :: N -> N

class KnownPeano (p :: N)
peanoVal :: KnownPeano p => proxy p -> Integer
type family ToNat (a :: N) :: Nat
type family FromNat (a :: Nat) :: N
type family (:+:) (a :: N) (b :: N) :: N
type family (:-:) (a :: N) (b :: N) :: N
type family (:*:) (a :: N) (b :: N) :: N
instance GHC.Generics.Generic TypeFun.Data.Peano.N
instance GHC.Show.Show TypeFun.Data.Peano.N
instance GHC.Read.Read TypeFun.Data.Peano.N
instance GHC.Classes.Ord TypeFun.Data.Peano.N
instance GHC.Classes.Eq TypeFun.Data.Peano.N
instance TypeFun.Data.Peano.KnownPeano 'TypeFun.Data.Peano.Z
instance TypeFun.Data.Peano.KnownPeano n => TypeFun.Data.Peano.KnownPeano ('TypeFun.Data.Peano.S n)


-- | Collection of type families on type lists. This module differs from
--   <b>Data.Singletons.Prelude.List</b> because works with <b>[*]</b> and
--   relies on GHC's type equality (~). The rest of required operations
--   like <tt>Reverse</tt> or '(:++:)' you could find in singletons
module TypeFun.Data.List
type family Length (a :: [k]) :: N
type family Drop (c :: N) (s :: [k]) :: [k]
type family Take (c :: N) (s :: [k]) :: [k]

-- | Remove first argument type from anywhere in a list.
type family Delete (a :: k) (s :: [k]) :: [k]

-- | Remove index from the list
type family Remove (i :: N) (a :: [k]) :: [k]
type family (:++:) (a :: [k]) (b :: [k]) :: [k]
type IndexOf a s = FromJust (IndexOfMay a s)
type IndexOfMay a s = IndexOfMay' Z a s
type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N
type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N]
type family IndicesOf (a :: [k]) (b :: [k]) :: [N]
type Index idx s = FromJust (IndexMay idx s)
type family IndexMay (idx :: N) (s :: [k]) :: Maybe k
type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k]
type family Indices (idxs :: [N]) (a :: [k]) :: [k]

-- | Generates unresolvable constraint if fists element is not contained
--   inside of second
type Elem a s = NothingToConstr (IndexOfMay a s) (ElementNotFoundInList a s)

-- | Reverse of <a>Elem</a>
type NotElem a s = JustToConstr (IndexOfMay a s) (ElementIsInList a s)

-- | Count elements in a list
type family Count (a :: k) (s :: [k]) :: N

-- | Constanints that first argument is a sublist of second. Reduces to
--   <b>(Elem a1 b, Elem a2 b, Elem a3 b, ...)</b>
type family SubList (a :: [k]) (b :: [k]) :: Constraint
type family NotSubList (a :: [k]) (b :: [k]) :: Constraint
type IsPrefixOf a b = (If (IsPrefixOfBool a b) (() :: Constraint) (ListIsNotPrefixOf a b), SubList a b)
type IsNotPrefixOf a b = If (IsPrefixOfBool a b) (ListIsPrefixOf a b) (() :: Constraint)

-- | First argument is prefix of second
type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool

-- | Appends elements from first list to second if they are not presented
--   in.
type family Union (a :: [k]) (b :: [k]) :: [k]
type family UnionList (l :: [[k]]) :: [k]

-- | Append element to list if element is not already presented in
type family AppendUniq (a :: k) (s :: [k]) :: [k]

-- | Calculates intersection between two lists. Order of elements is taken
--   from first list
type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)

-- | Removes from first list all elements occured in second
type family Substract (a :: [k]) (b :: [k]) :: [k]

-- | Checks that element <tt>a</tt> occurs in a list just once
type ElementIsUniq a s = If (Equal (S Z) (Count a s)) (() :: Constraint) (ElementIsNotUniqInList a s)

-- | Checks that all elements in list are unique
type UniqElements a = UniqElements' a a
type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint
appendId :: forall proxy l r. proxy l -> (l ~ (l :++: '[]) => r) -> r
subListId :: forall proxy l r. proxy l -> (SubList l l => r) -> r