{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
-- Data.Coerce is Unsafe
{-# LANGUAGE Trustworthy #-}
module Data.Universe.Instances.Extended (
  -- | Instances for 'Universe' and 'Finite' for function-like functors and the empty type.
  Universe(..), Finite(..)
  ) where

import Control.Comonad.Trans.Traced (TracedT (..))
import Data.Coerce (coerce)
import Data.Functor.Contravariant (Op (..), Predicate (..))
import Data.Functor.Rep (Representable (..), Co (..))
import Data.Map (Map)
import Data.Set (Set)
import Data.Universe.Class (Universe (..), Finite (..))
import Data.Universe.Helpers (retag, Tagged, Natural)

import qualified Data.Map as M
import qualified Data.Set as S


-- $setup
--
-- >>> import Data.Int (Int8)
-- >>> import Data.Functor.Contravariant (Predicate (..))
-- >>> import Data.Universe.Helpers (retag, Tagged, Natural)
--
-- -- Show (a -> b) instance (in universe-reverse-instances, but cannot depend on it here).
-- >>> instance (Finite a, Show a, Show b) => Show (a -> b) where showsPrec n f = showsPrec n [(a, f a) | a <- universeF]
--
-- >>> :set -XStandaloneDeriving
-- >>> deriving instance (Finite a, Show a) => Show (Predicate a)

-- | We could do this:
--
-- @
-- instance Universe (f a) => Universe (Co f a) where universe = map Rep universe
-- @
--
-- However, since you probably only apply Rep to functors when you want to
-- think of them as being representable, I think it makes sense to use an
-- instance based on the representable-ness rather than the inherent
-- universe-ness.
--
-- Please complain if you disagree!
--
instance (Representable f, Finite (Rep f), Ord (Rep f), Universe a)
  => Universe (Co f a)
  where universe :: [Co f a]
universe = ((Rep f -> a) -> Co f a) -> [Rep f -> a] -> [Co f a]
forall a b. (a -> b) -> [a] -> [b]
map (Rep f -> a) -> Co f a
(Rep (Co f) -> a) -> Co f a
forall a. (Rep (Co f) -> a) -> Co f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate [Rep f -> a]
forall a. Universe a => [a]
universe
instance (Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Universe a)
  => Universe (TracedT s f a)
  where universe :: [TracedT s f a]
universe = (((s, Rep f) -> a) -> TracedT s f a)
-> [(s, Rep f) -> a] -> [TracedT s f a]
forall a b. (a -> b) -> [a] -> [b]
map ((s, Rep f) -> a) -> TracedT s f a
(Rep (TracedT s f) -> a) -> TracedT s f a
forall a. (Rep (TracedT s f) -> a) -> TracedT s f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate [(s, Rep f) -> a]
forall a. Universe a => [a]
universe

instance (Universe a, Finite b, Ord b) => Universe (Op a b) where
   universe :: [Op a b]
universe = [b -> a] -> [Op a b]
forall a b. Coercible a b => a -> b
coerce ([b -> a]
forall a. Universe a => [a]
universe :: [b -> a])
instance (Finite a, Ord a) => Universe (Predicate a) where
  universe :: [Predicate a]
universe = (Set a -> Predicate a) -> [Set a] -> [Predicate a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Bool) -> Predicate a
forall a. (a -> Bool) -> Predicate a
Predicate ((a -> Bool) -> Predicate a)
-> (Set a -> a -> Bool) -> Set a -> Predicate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set a -> Bool) -> Set a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member) [Set a]
forall a. Universe a => [a]
universe

instance (Representable f, Finite (Rep f), Ord (Rep f), Finite a)
  => Finite (Co f a)
  where universeF :: [Co f a]
universeF = ((Rep f -> a) -> Co f a) -> [Rep f -> a] -> [Co f a]
forall a b. (a -> b) -> [a] -> [b]
map (Rep f -> a) -> Co f a
(Rep (Co f) -> a) -> Co f a
forall a. (Rep (Co f) -> a) -> Co f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate [Rep f -> a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Co f a) Natural
cardinality = Tagged (Rep f -> a) Natural -> Tagged (Co f a) Natural
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (Rep f -> a) Natural
Tagged (Rep (Co f) -> a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (Rep (Co        f) -> a) Natural)
instance (Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Finite a)
  => Finite (TracedT s f a)
  where universeF :: [TracedT s f a]
universeF = (((s, Rep f) -> a) -> TracedT s f a)
-> [(s, Rep f) -> a] -> [TracedT s f a]
forall a b. (a -> b) -> [a] -> [b]
map ((s, Rep f) -> a) -> TracedT s f a
(Rep (TracedT s f) -> a) -> TracedT s f a
forall a. (Rep (TracedT s f) -> a) -> TracedT s f a
forall (f :: * -> *) a. Representable f => (Rep f -> a) -> f a
tabulate [(s, Rep f) -> a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (TracedT s f a) Natural
cardinality = Tagged (s, Rep f) Natural -> Tagged (TracedT s f a) Natural
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (s, Rep f) Natural
Tagged (Rep (TracedT s f)) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (Rep (TracedT s f)) Natural)

instance (Finite a, Finite b, Ord b) => Finite (Op a b) where
  cardinality :: Tagged (Op a b) Natural
cardinality = Tagged (b -> a) Natural -> Tagged (Op a b) Natural
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (b -> a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (b -> a) Natural)

-- |
--
-- >>> mapM_ print (universe :: [Predicate Ordering])
-- Predicate {getPredicate = [(LT,False),(EQ,False),(GT,False)]}
-- Predicate {getPredicate = [(LT,True),(EQ,False),(GT,False)]}
-- Predicate {getPredicate = [(LT,False),(EQ,True),(GT,False)]}
-- Predicate {getPredicate = [(LT,True),(EQ,True),(GT,False)]}
-- Predicate {getPredicate = [(LT,False),(EQ,False),(GT,True)]}
-- Predicate {getPredicate = [(LT,True),(EQ,False),(GT,True)]}
-- Predicate {getPredicate = [(LT,False),(EQ,True),(GT,True)]}
-- Predicate {getPredicate = [(LT,True),(EQ,True),(GT,True)]}
--
-- Beware, function type universes are large...
--
-- >>> cardinality :: Tagged (Predicate Int8) Natural
-- Tagged 115792089237316195423570985008687907853269984665640564039457584007913129639936
--
-- ... but thanks to laziness, you can expect at least few:
--
-- >>> let Predicate f : _ = universe :: [Predicate Int8]
-- >>> f 0
-- False
--
instance (Finite a, Ord a) => Finite (Predicate a) where
  cardinality :: Tagged (Predicate a) Natural
cardinality = Tagged (Set a) Natural -> Tagged (Predicate a) Natural
forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (Set a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (Set a) Natural)