{-# OPTIONS -fno-warn-orphans #-}

module Data.Type.Witness.General.Finite where

import Data.Type.Witness.General.AllConstraint
import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.All
import Data.Type.Witness.Specific.Some
import Import

type FiniteWitness :: forall k. (k -> Type) -> Constraint
class FiniteWitness (w :: k -> Type) where
    assembleAllFor ::
           forall (m :: Type -> Type) (f :: k -> Type). Applicative m
        => (forall (t :: k). w t -> m (f t))
        -> m (AllFor f w)

instance FiniteWitness ((:~:) t) where
    assembleAllFor :: forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). (t :~: t) -> m (f t)) -> m (AllFor f ((:~:) t))
assembleAllFor forall (t :: k). (t :~: t) -> m (f t)
getsel = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\f t
ft -> forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall a b. (a -> b) -> a -> b
$ \t :~: t
Refl -> f t
ft) forall a b. (a -> b) -> a -> b
$ forall (t :: k). (t :~: t) -> m (f t)
getsel forall {k} (a :: k). a :~: a
Refl

instance (TestEquality w, FiniteWitness w) => Countable (Some w) where
    countPrevious :: Some w -> Maybe (Some w)
countPrevious = forall a. Finite a => a -> Maybe a
finiteCountPrevious
    countMaybeNext :: Maybe (Some w) -> Maybe (Some w)
countMaybeNext = forall a. Finite a => Maybe a -> Maybe a
finiteCountMaybeNext

instance (TestEquality w, FiniteWitness w) => Searchable (Some w) where
    search :: forall b. (Some w -> Maybe b) -> Maybe b
search = forall a b. Finite a => (a -> Maybe b) -> Maybe b
finiteSearch

instance (TestEquality w, FiniteWitness w) => Finite (Some w) where
    assemble ::
           forall b f. Applicative f
        => (Some w -> f b)
        -> f (Some w -> b)
    assemble :: forall b (f :: Type -> Type).
Applicative f =>
(Some w -> f b) -> f (Some w -> b)
assemble Some w -> f b
afb =
        forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkAllFor forall (t :: k). w t -> Const b t
wtcb) (MkSome w a
wt) -> forall {k} a (b :: k). Const a b -> a
getConst forall a b. (a -> b) -> a -> b
$ forall (t :: k). w t -> Const b t
wtcb w a
wt) forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor forall a b. (a -> b) -> a -> b
$ \w t
wt -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ Some w -> f b
afb forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w t
wt
    allValues :: [Some w]
allValues = forall {k} a (b :: k). Const a b -> a
getConst forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor forall a b. (a -> b) -> a -> b
$ \w t
wt -> forall {k} a (b :: k). a -> Const a b
Const [forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w t
wt]

allWitnesses :: FiniteWitness w => [Some w]
allWitnesses :: forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses = forall {k} a (b :: k). Const a b -> a
getConst forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor forall a b. (a -> b) -> a -> b
$ \w t
wt -> forall {k} a (b :: k). a -> Const a b
Const [forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w t
wt]

allForCodomain :: FiniteWitness w => AllFor f w -> [Some f]
allForCodomain :: forall {k} (w :: k -> Type) (f :: k -> Type).
FiniteWitness w =>
AllFor f w -> [Some f]
allForCodomain AllFor f w
af = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {k} (f :: k -> Type) (w :: k -> Type) (g :: k -> Type).
AllFor f w -> SomeFor g w -> SomeFor g f
allMapSome AllFor f w
af) forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses

instance (FiniteWitness w, AllConstraint Show w, WitnessConstraint Show w) => Show (AllOf w) where
    show :: AllOf w -> String
show (MkAllOf forall t. w t -> t
wtt) = let
        showItem :: Some w -> String
        showItem :: Some w -> String
showItem (MkSome w a
wt) =
            forall k (w :: k -> Type) (t :: k).
AllConstraint Show w =>
w t -> String
allShow w a
wt forall a. [a] -> [a] -> [a]
++
            String
" -> " forall a. [a] -> [a] -> [a]
++
            case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint @_ @Show w a
wt of
                Dict (Show a)
Dict -> forall a. Show a => a -> String
show (forall t. w t -> t
wtt w a
wt)
        in String
"{" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Some w -> String
showItem forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses) forall a. [a] -> [a] -> [a]
++ String
"}"

assembleAllOf :: (FiniteWitness w, Applicative m) => (forall t. w t -> m t) -> m (AllOf w)
assembleAllOf :: forall (w :: Type -> Type) (m :: Type -> Type).
(FiniteWitness w, Applicative m) =>
(forall t. w t -> m t) -> m (AllOf w)
assembleAllOf forall t. w t -> m t
wtmt = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf forall a b. (a -> b) -> a -> b
$ forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type).
(FiniteWitness w, Applicative m) =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor forall a b. (a -> b) -> a -> b
$ \w t
wt -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall t. w t -> m t
wtmt w t
wt