{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ConstraintKinds #-}
module Data.FunctorShape(
    Shape(), pattern Shape,
    mapShape, unShape,
    Ignored(..), WeakEq, WeakOrd
) where

import qualified Unsafe.Coerce (unsafeCoerce)
import Data.Functor.Classes (showsUnaryWith)

import Data.PTraversable
import Data.Finitary.Enum
import Data.Profunctor.Cartesian
import Prelude hiding (Enum)
import Data.Profunctor.FinFn (withFinFn)

newtype Shape f = UnsafeMkShape (f Ignored)
type role Shape representational

type WeakEq f = Eq (f Ignored)

instance (WeakEq f) => Eq (Shape f) where
    UnsafeMkShape f Ignored
fa == :: Shape f -> Shape f -> Bool
== UnsafeMkShape f Ignored
fb = f Ignored
fa f Ignored -> f Ignored -> Bool
forall a. Eq a => a -> a -> Bool
== f Ignored
fb

type WeakOrd f = Ord (f Ignored)

instance (WeakOrd f) => Ord (Shape f) where
    UnsafeMkShape f Ignored
fa <= :: Shape f -> Shape f -> Bool
<= UnsafeMkShape f Ignored
fb = f Ignored
fa f Ignored -> f Ignored -> Bool
forall a. Ord a => a -> a -> Bool
<= f Ignored
fb
    compare :: Shape f -> Shape f -> Ordering
compare (UnsafeMkShape f Ignored
fa) (UnsafeMkShape f Ignored
fb) = f Ignored -> f Ignored -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f Ignored
fa f Ignored
fb

instance (Show (f Ignored)) => Show (Shape f) where
    showsPrec :: Int -> Shape f -> ShowS
showsPrec Int
p (UnsafeMkShape f Ignored
fa) = (Int -> f Ignored -> ShowS) -> String -> Int -> f Ignored -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith Int -> f Ignored -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec String
"Shape" Int
p f Ignored
fa

instance PTraversable f => Enum (Shape f) where
    enumeration :: FinFn (Shape f) (Shape f)
enumeration = (Shape f -> f Ignored)
-> (f () -> Shape f)
-> FinFn Ignored ()
-> FinFn (Shape f) (Shape f)
forall (t :: * -> *) (p :: * -> * -> *) as a b bs.
(PTraversable t, Cartesian p, Cocartesian p) =>
(as -> t a) -> (t b -> bs) -> p a b -> p as bs
forall (p :: * -> * -> *) as a b bs.
(Cartesian p, Cocartesian p) =>
(as -> f a) -> (f b -> bs) -> p a b -> p as bs
ptraverseWith Shape f -> f Ignored
forall (f :: * -> *). Shape f -> f Ignored
unShape f () -> Shape f
forall (f :: * -> *) a. f a -> Shape f
Shape FinFn Ignored ()
forall a. FinFn a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
    withEnum :: forall r.
(forall (n :: Nat).
 KnownNat n =>
 (Shape f -> Finite n) -> (Finite n -> Shape f) -> r)
-> r
withEnum = FinFn (Shape f) (Shape f)
-> (forall (n :: Nat).
    KnownNat n =>
    (Shape f -> Finite n) -> (Finite n -> Shape f) -> r)
-> r
forall a b r.
FinFn a b
-> (forall (n :: Nat).
    KnownNat n =>
    (a -> Finite n) -> (Finite n -> b) -> r)
-> r
withFinFn FinFn (Shape f) (Shape f)
forall x. Enum x => FinFn x x
enumeration

{-# COMPLETE Shape #-}
pattern Shape :: f a -> Shape f
pattern $bShape :: forall (f :: * -> *) a. f a -> Shape f
$mShape :: forall {r} {f :: * -> *}.
Shape f -> (forall {a}. f a -> r) -> ((# #) -> r) -> r
Shape x <- UnsafeMkShape x
  where Shape f a
x = f Ignored -> Shape f
forall (f :: * -> *). f Ignored -> Shape f
UnsafeMkShape (f a -> f Ignored
forall (f :: * -> *) a. f a -> f Ignored
forget f a
x)

mapShape :: (forall a. f a -> g a) -> Shape f -> Shape g
mapShape :: forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> Shape f -> Shape g
mapShape forall a. f a -> g a
fg (Shape f a
f) = g a -> Shape g
forall (f :: * -> *) a. f a -> Shape f
Shape (f a -> g a
forall a. f a -> g a
fg f a
f)

unShape :: Shape f -> f Ignored
unShape :: forall (f :: * -> *). Shape f -> f Ignored
unShape (UnsafeMkShape f Ignored
f) = f Ignored
f

data Ignored = Ignored

forget :: f a -> f Ignored
forget :: forall (f :: * -> *) a. f a -> f Ignored
forget = f a -> f Ignored
forall a b. a -> b
Unsafe.Coerce.unsafeCoerce

instance Eq Ignored where
    Ignored
_ == :: Ignored -> Ignored -> Bool
== Ignored
_ = Bool
True

instance Ord Ignored where
    Ignored
_ <= :: Ignored -> Ignored -> Bool
<= Ignored
_ = Bool
True
    compare :: Ignored -> Ignored -> Ordering
compare Ignored
_ Ignored
_ = Ordering
EQ

instance Show Ignored where
    show :: Ignored -> String
show Ignored
_ = String
"_"