{-# 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 = (f t -> AllFor f ((:~:) t)) -> m (f t) -> m (AllFor f ((:~:) t))
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\f t
ft -> (forall (t :: k). (t :~: t) -> f t) -> AllFor f ((:~:) t)
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall (t :: k). (t :~: t) -> f t) -> AllFor f ((:~:) t))
-> (forall (t :: k). (t :~: t) -> f t) -> AllFor f ((:~:) t)
forall a b. (a -> b) -> a -> b
$ \t :~: t
Refl -> f t
f t
ft) (m (f t) -> m (AllFor f ((:~:) t)))
-> m (f t) -> m (AllFor f ((:~:) t))
forall a b. (a -> b) -> a -> b
$ (t :~: t) -> m (f t)
forall (t :: k). (t :~: t) -> m (f t)
getsel t :~: t
forall {k} (a :: k). a :~: a
Refl

instance (TestEquality w, FiniteWitness w) => Countable (Some w) where
    countPrevious :: Some w -> Maybe (Some w)
countPrevious = Some w -> Maybe (Some w)
forall a. Finite a => a -> Maybe a
finiteCountPrevious
    countMaybeNext :: Maybe (Some w) -> Maybe (Some w)
countMaybeNext = Maybe (Some w) -> Maybe (Some w)
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 = (Some w -> Maybe b) -> Maybe b
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 =
        (AllFor (Const b) w -> Some w -> b)
-> f (AllFor (Const b) w) -> f (Some w -> b)
forall a b. (a -> b) -> f a -> f b
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) -> Const b a -> b
forall {k} a (b :: k). Const a b -> a
getConst (Const b a -> b) -> Const b a -> b
forall a b. (a -> b) -> a -> b
$ w a -> Const b a
forall (t :: k). w t -> Const b t
wtcb w a
wt) (f (AllFor (Const b) w) -> f (Some w -> b))
-> f (AllFor (Const b) w) -> f (Some w -> b)
forall a b. (a -> b) -> a -> b
$ (forall (t :: k). w t -> f (Const b t)) -> f (AllFor (Const b) w)
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)
forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor ((forall (t :: k). w t -> f (Const b t)) -> f (AllFor (Const b) w))
-> (forall (t :: k). w t -> f (Const b t))
-> f (AllFor (Const b) w)
forall a b. (a -> b) -> a -> b
$ \w t
wt -> (b -> Const b t) -> f b -> f (Const b t)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Const b t
forall {k} a (b :: k). a -> Const a b
Const (f b -> f (Const b t)) -> f b -> f (Const b t)
forall a b. (a -> b) -> a -> b
$ Some w -> f b
afb (Some w -> f b) -> Some w -> f b
forall a b. (a -> b) -> a -> b
$ w t -> Some w
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome w t
wt
    allValues :: [Some w]
allValues = Const [Some w] (AllFor Any w) -> [Some w]
forall {k} a (b :: k). Const a b -> a
getConst (Const [Some w] (AllFor Any w) -> [Some w])
-> Const [Some w] (AllFor Any w) -> [Some w]
forall a b. (a -> b) -> a -> b
$ (forall (t :: k). w t -> Const [Some w] (Any t))
-> Const [Some w] (AllFor Any w)
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)
forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor ((forall (t :: k). w t -> Const [Some w] (Any t))
 -> Const [Some w] (AllFor Any w))
-> (forall (t :: k). w t -> Const [Some w] (Any t))
-> Const [Some w] (AllFor Any w)
forall a b. (a -> b) -> a -> b
$ \w t
wt -> [Some w] -> Const [Some w] (Any t)
forall {k} a (b :: k). a -> Const a b
Const [w t -> Some w
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 = Const [Some w] (AllFor Any w) -> [Some w]
forall {k} a (b :: k). Const a b -> a
getConst (Const [Some w] (AllFor Any w) -> [Some w])
-> Const [Some w] (AllFor Any w) -> [Some w]
forall a b. (a -> b) -> a -> b
$ (forall (t :: k). w t -> Const [Some w] (Any t))
-> Const [Some w] (AllFor Any w)
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)
forall (m :: Type -> Type) (f :: k -> Type).
Applicative m =>
(forall (t :: k). w t -> m (f t)) -> m (AllFor f w)
assembleAllFor ((forall (t :: k). w t -> Const [Some w] (Any t))
 -> Const [Some w] (AllFor Any w))
-> (forall (t :: k). w t -> Const [Some w] (Any t))
-> Const [Some w] (AllFor Any w)
forall a b. (a -> b) -> a -> b
$ \w t
wt -> [Some w] -> Const [Some w] (Any t)
forall {k} a (b :: k). a -> Const a b
Const [w t -> Some w
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 = (SomeFor (Const ()) w -> Some f)
-> [SomeFor (Const ()) w] -> [Some f]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (AllFor f w -> SomeFor (Const ()) w -> Some f
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) [SomeFor (Const ()) w]
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) =
            w a -> String
forall k (w :: k -> Type) (t :: k).
AllConstraint Show w =>
w t -> String
allShow w a
wt String -> ShowS
forall a. [a] -> [a] -> [a]
++
            String
" -> " String -> ShowS
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 -> a -> String
forall a. Show a => a -> String
show (w a -> a
forall t. w t -> t
wtt w a
wt)
        in String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Some w -> String) -> [Some w] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Some w -> String
showItem [Some w]
forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses) String -> ShowS
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 = (AllFor Identity w -> AllOf w)
-> m (AllFor Identity w) -> m (AllOf w)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap AllFor Identity w -> AllOf w
forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf (m (AllFor Identity w) -> m (AllOf w))
-> m (AllFor Identity w) -> m (AllOf w)
forall a b. (a -> b) -> a -> b
$ (forall t. w t -> m (Identity t)) -> m (AllFor Identity w)
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)
forall (m :: Type -> Type) (f :: Type -> Type).
Applicative m =>
(forall t. w t -> m (f t)) -> m (AllFor f w)
assembleAllFor ((forall t. w t -> m (Identity t)) -> m (AllFor Identity w))
-> (forall t. w t -> m (Identity t)) -> m (AllFor Identity w)
forall a b. (a -> b) -> a -> b
$ \w t
wt -> (t -> Identity t) -> m t -> m (Identity t)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap t -> Identity t
forall a. a -> Identity a
Identity (m t -> m (Identity t)) -> m t -> m (Identity t)
forall a b. (a -> b) -> a -> b
$ w t -> m t
forall t. w t -> m t
wtmt w t
wt