{-# 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