{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
-- Data.Coerce is Unsafe
#if __GLASGOW_HASKELL__ >=704 && !MIN_VERSION_base(4,7,0)
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >=702
{-# LANGUAGE Trustworthy #-}
#endif
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.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

#if MIN_VERSION_base(4,7,0)
import Data.Coerce (coerce)
#endif

-- $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
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
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
#if MIN_VERSION_base(4,7,0)
   universe :: [Op a b]
universe = [b -> a] -> [Op a b]
coerce ([b -> a]
forall a. Universe a => [a]
universe :: [b -> a])
#else
   universe = map Op universe
#endif
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
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 (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
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 (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)