{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Aztecs.Entity
  ( Entity (..),
    EntityT,
    FromEntity (..),
    ToEntity (..),
    ConcatT,
    IntersectT,
    Intersect (..),
    DifferenceT,
    Difference (..),
    SplitT,
    Split (..),
    concat,
    (<&>),
    (:&) (..),
  )
where

import Data.Kind (Type)
import Prelude hiding (concat)

data Entity (ts :: [Type]) where
  ENil :: Entity '[]
  ECons :: t -> Entity ts -> Entity (t ': ts)

instance Show (Entity '[]) where
  show :: Entity '[] -> String
show Entity '[]
ENil = String
"[]"

instance (Show a, Show' (Entity as)) => Show (Entity (a ': as)) where
  show :: Entity (a : as) -> String
show (ECons t
x Entity ts
xs) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ Entity ts -> String
forall a. Show' a => a -> String
showRow Entity ts
xs

class Show' a where
  showRow :: a -> String

instance Show' (Entity '[]) where
  showRow :: Entity '[] -> String
showRow Entity '[]
ENil = String
"]"

instance (Show a, Show' (Entity as)) => Show' (Entity (a ': as)) where
  showRow :: Entity (a : as) -> String
showRow (ECons t
x Entity ts
xs) = String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ Entity ts -> String
forall a. Show' a => a -> String
showRow Entity ts
xs

(<&>) :: Entity as -> a -> Entity (a : as)
<&> :: forall (as :: [*]) a. Entity as -> a -> Entity (a : as)
(<&>) Entity as
es a
c = a -> Entity as -> Entity (a : as)
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons a
c Entity as
es

type family ConcatT (a :: [Type]) (b :: [Type]) where
  ConcatT '[] b = b
  ConcatT (a ': as) b = a ': ConcatT as b

concat :: Entity as -> Entity bs -> Entity (ConcatT as bs)
concat :: forall (as :: [*]) (bs :: [*]).
Entity as -> Entity bs -> Entity (ConcatT as bs)
concat Entity as
ENil Entity bs
ys = Entity bs
Entity (ConcatT as bs)
ys
concat (ECons t
x Entity ts
xs) Entity bs
ys = t -> Entity (ConcatT ts bs) -> Entity (t : ConcatT ts bs)
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons t
x (Entity ts -> Entity bs -> Entity (ConcatT ts bs)
forall (as :: [*]) (bs :: [*]).
Entity as -> Entity bs -> Entity (ConcatT as bs)
concat Entity ts
xs Entity bs
ys)

type family SplitT (a :: [Type]) (b :: [Type]) :: [Type] where
  SplitT '[] bs = bs
  SplitT (a ': as) (a ': bs) = SplitT as bs

class Split (a :: [Type]) (b :: [Type]) where
  split :: Entity b -> (Entity a, Entity (SplitT a b))

instance Split '[] bs where
  split :: Entity bs -> (Entity '[], Entity (SplitT '[] bs))
split Entity bs
e = (Entity '[]
ENil, Entity bs
Entity (SplitT '[] bs)
e)

instance forall a as bs. (Split as bs) => Split (a ': as) (a ': bs) where
  split :: Entity (a : bs)
-> (Entity (a : as), Entity (SplitT (a : as) (a : bs)))
split (ECons t
x Entity ts
xs) =
    let (Entity as
as, Entity (SplitT as ts)
bs) = forall (a :: [*]) (b :: [*]).
Split a b =>
Entity b -> (Entity a, Entity (SplitT a b))
split @as Entity ts
xs
     in (a -> Entity as -> Entity (a : as)
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons a
t
x Entity as
as, Entity (SplitT as ts)
Entity (SplitT (a : as) (a : bs))
bs)

data a :& b = a :& b

type family EntityT a where
  EntityT (a :& b) = a ': EntityT b
  EntityT (Entity ts) = ts
  EntityT a = '[a]

class FromEntity a where
  fromEntity :: Entity (EntityT a) -> a

instance {-# OVERLAPS #-} (EntityT a ~ '[a]) => FromEntity a where
  fromEntity :: Entity (EntityT a) -> a
fromEntity (ECons t
a Entity ts
ENil) = a
t
a

instance FromEntity (Entity ts) where
  fromEntity :: Entity (EntityT (Entity ts)) -> Entity ts
fromEntity = Entity ts -> Entity ts
Entity (EntityT (Entity ts)) -> Entity ts
forall a. a -> a
id

instance (FromEntity a, FromEntity b, EntityT (a :& b) ~ (a ': EntityT b)) => FromEntity (a :& b) where
  fromEntity :: Entity (EntityT (a :& b)) -> a :& b
fromEntity (ECons t
a Entity ts
rest) = a
t
a a -> b -> a :& b
forall a b. a -> b -> a :& b
:& Entity (EntityT b) -> b
forall a. FromEntity a => Entity (EntityT a) -> a
fromEntity Entity ts
Entity (EntityT b)
rest

class ToEntity a where
  toEntity :: a -> Entity (EntityT a)

instance {-# OVERLAPS #-} (EntityT a ~ '[a]) => ToEntity a where
  toEntity :: a -> Entity (EntityT a)
toEntity a
a = a -> Entity '[] -> Entity '[a]
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons a
a Entity '[]
ENil

instance ToEntity (Entity ts) where
  toEntity :: Entity ts -> Entity (EntityT (Entity ts))
toEntity = Entity ts -> Entity ts
Entity ts -> Entity (EntityT (Entity ts))
forall a. a -> a
id

instance (ToEntity a, ToEntity b, EntityT (a :& b) ~ (a ': EntityT b)) => ToEntity (a :& b) where
  toEntity :: (a :& b) -> Entity (EntityT (a :& b))
toEntity (a
a :& b
b) = a -> Entity (EntityT b) -> Entity (a : EntityT b)
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons a
a (b -> Entity (EntityT b)
forall a. ToEntity a => a -> Entity (EntityT a)
toEntity b
b)

type family ElemT (a :: Type) (b :: [Type]) :: Bool where
  ElemT a '[] = 'False
  ElemT a (a ': as) = 'True
  ElemT a (b ': as) = ElemT a as

type family If (cond :: Bool) (true :: [Type]) (false :: [Type]) :: [Type] where
  If 'True true false = true
  If 'False true false = false

type family IntersectT (a :: [Type]) (b :: [Type]) :: [Type] where
  IntersectT '[] b = '[]
  IntersectT (a ': as) b = If (ElemT a b) (a ': IntersectT as b) (IntersectT as b)

class Intersect' (flag :: Bool) (a :: [Type]) (b :: [Type]) where
  intersect' :: Entity a -> Entity b -> Entity (IntersectT a b)

instance (Intersect as b, ElemT a b ~ 'True) => Intersect' 'True (a ': as) b where
  intersect' :: Entity (a : as) -> Entity b -> Entity (IntersectT (a : as) b)
intersect' (ECons t
x Entity ts
xs) Entity b
ys = t -> Entity (IntersectT as b) -> Entity (t : IntersectT as b)
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons t
x (Entity ts
xs Entity ts -> Entity b -> Entity (IntersectT ts b)
forall (a :: [*]) (b :: [*]).
Intersect a b =>
Entity a -> Entity b -> Entity (IntersectT a b)
`intersect` Entity b
ys)

instance (Intersect as (b ': bs), ElemT a (b ': bs) ~ 'False) => Intersect' 'False (a ': as) (b ': bs) where
  intersect' :: Entity (a : as)
-> Entity (b : bs) -> Entity (IntersectT (a : as) (b : bs))
intersect' (ECons t
_ Entity ts
xs) = Entity ts -> Entity (b : bs) -> Entity (IntersectT ts (b : bs))
forall (a :: [*]) (b :: [*]).
Intersect a b =>
Entity a -> Entity b -> Entity (IntersectT a b)
intersect Entity ts
xs

class Intersect (a :: [Type]) (b :: [Type]) where
  intersect :: Entity a -> Entity b -> Entity (IntersectT a b)

instance Intersect '[] b where
  intersect :: Entity '[] -> Entity b -> Entity (IntersectT '[] b)
intersect Entity '[]
_ Entity b
_ = Entity '[]
Entity (IntersectT '[] b)
ENil

instance (Intersect' (ElemT a bs) (a ': as) bs) => Intersect (a ': as) bs where
  intersect :: Entity (a : as) -> Entity bs -> Entity (IntersectT (a : as) bs)
intersect = forall (flag :: Bool) (a :: [*]) (b :: [*]).
Intersect' flag a b =>
Entity a -> Entity b -> Entity (IntersectT a b)
intersect' @(ElemT a bs)

type family DifferenceT (a :: [Type]) (b :: [Type]) :: [Type] where
  DifferenceT '[] b = '[]
  DifferenceT (a ': as) b = If (ElemT a b) (DifferenceT as b) (a ': DifferenceT as b)

class Difference' (flag :: Bool) (a :: [Type]) (b :: [Type]) where
  difference' :: Entity a -> Entity b -> Entity (DifferenceT a b)

instance (Difference as b, DifferenceT (a ': as) b ~ DifferenceT as b) => Difference' 'True (a ': as) b where
  difference' :: Entity (a : as) -> Entity b -> Entity (DifferenceT (a : as) b)
difference' (ECons t
_ Entity ts
xs) Entity b
ys = Entity ts
xs Entity ts -> Entity b -> Entity (DifferenceT ts b)
forall (a :: [*]) (b :: [*]).
Difference a b =>
Entity a -> Entity b -> Entity (DifferenceT a b)
`difference` Entity b
ys

instance (Difference as (b ': bs), DifferenceT (a ': as) (b ': bs) ~ (a ': DifferenceT as (b ': bs))) => Difference' 'False (a ': as) (b ': bs) where
  difference' :: Entity (a : as)
-> Entity (b : bs) -> Entity (DifferenceT (a : as) (b : bs))
difference' (ECons t
x Entity ts
xs) Entity (b : bs)
ys = t
-> Entity (DifferenceT as (b : bs))
-> Entity (t : DifferenceT as (b : bs))
forall t (ts :: [*]). t -> Entity ts -> Entity (t : ts)
ECons t
x (Entity ts
xs Entity ts -> Entity (b : bs) -> Entity (DifferenceT ts (b : bs))
forall (a :: [*]) (b :: [*]).
Difference a b =>
Entity a -> Entity b -> Entity (DifferenceT a b)
`difference` Entity (b : bs)
ys)

class Difference (a :: [Type]) (b :: [Type]) where
  difference :: Entity a -> Entity b -> Entity (DifferenceT a b)

instance Difference '[] b where
  difference :: Entity '[] -> Entity b -> Entity (DifferenceT '[] b)
difference Entity '[]
_ Entity b
_ = Entity '[]
Entity (DifferenceT '[] b)
ENil

instance (Difference' (ElemT a bs) (a ': as) bs) => Difference (a ': as) bs where
  difference :: Entity (a : as) -> Entity bs -> Entity (DifferenceT (a : as) bs)
difference = forall (flag :: Bool) (a :: [*]) (b :: [*]).
Difference' flag a b =>
Entity a -> Entity b -> Entity (DifferenceT a b)
difference' @(ElemT a bs)