{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Symantic.ADT where
import Data.Either (Either(..))
import Data.Void (Void, absurd)
import Data.Function (($), (.), id, const)
import GHC.Generics as Generics
type family EoT (adt :: [[*]]) :: * where
EoT '[] = Void
EoT '[ ps ] = Tuples ps
EoT (ps ': ss) = Either (Tuples ps) (EoT ss)
type family Tuples (as :: [*]) :: (r :: *) where
Tuples '[] = ()
Tuples '[a] = a
Tuples (a ': rest) = (a, Tuples rest)
type ADT (adt :: *) = ListOfRepSums (Rep adt) '[]
type family ListOfRepSums (a :: * -> *) (ss :: [[*]]) :: [[*]]
type instance ListOfRepSums (a:+:b) ss = ListOfRepSums a (ListOfRepSums b ss)
type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss
type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss
type instance ListOfRepSums V1 ss = ss
type family ListOfRepProducts (a :: * -> *) (ps :: [*]) :: [*]
type instance ListOfRepProducts (a:*:b) ps = ListOfRepProducts a (ListOfRepProducts b ps)
type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps
type instance ListOfRepProducts U1 ps = ps
type family TypeOfRepField (a :: * -> *) :: *
type instance TypeOfRepField (K1 _i a) = a
type RepOfEoT a = RepOfEithers (Rep a) '[]
adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
adtOfeot :: EoT (ADT a) -> a
adtOfeot EoT (ADT a)
eot = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
Generics.to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ EoT (ADT a)
-> (Rep a Any -> Rep a Any) -> (EoT '[] -> Rep a Any) -> Rep a Any
forall (a :: * -> *) (ss :: [[*]]) x r.
RepOfEithers a ss =>
EoT (ListOfRepSums a ss) -> (a x -> r) -> (EoT ss -> r) -> r
repOfEithers @_ @'[] EoT (ADT a)
eot Rep a Any -> Rep a Any
forall a. a -> a
id EoT '[] -> Rep a Any
forall a. Void -> a
absurd
class RepOfEithers (a :: * -> *) ss where
repOfEithers ::
EoT (ListOfRepSums a ss) ->
(a x -> r) ->
(EoT ss -> r) ->
r
instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a:+:b) ss where
repOfEithers :: EoT (ListOfRepSums (a :+: b) ss)
-> ((:+:) a b x -> r) -> (EoT ss -> r) -> r
repOfEithers EoT (ListOfRepSums (a :+: b) ss)
eot (:+:) a b x -> r
ok EoT ss -> r
ko =
EoT (ListOfRepSums a (ListOfRepSums b ss))
-> (a x -> r) -> (EoT (ListOfRepSums b ss) -> r) -> r
forall (a :: * -> *) (ss :: [[*]]) x r.
RepOfEithers a ss =>
EoT (ListOfRepSums a ss) -> (a x -> r) -> (EoT ss -> r) -> r
repOfEithers @a @(ListOfRepSums b ss) EoT (ListOfRepSums a (ListOfRepSums b ss))
EoT (ListOfRepSums (a :+: b) ss)
eot
((:+:) a b x -> r
ok ((:+:) a b x -> r) -> (a x -> (:+:) a b x) -> a x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> (:+:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)
(\EoT (ListOfRepSums b ss)
next ->
EoT (ListOfRepSums b ss) -> (b x -> r) -> (EoT ss -> r) -> r
forall (a :: * -> *) (ss :: [[*]]) x r.
RepOfEithers a ss =>
EoT (ListOfRepSums a ss) -> (a x -> r) -> (EoT ss -> r) -> r
repOfEithers @b @ss EoT (ListOfRepSums b ss)
next
((:+:) a b x -> r
ok ((:+:) a b x -> r) -> (b x -> (:+:) a b x) -> b x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> (:+:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1)
EoT ss -> r
ko
)
instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
repOfEithers :: EoT (ListOfRepSums (M1 D c a) ss)
-> (M1 D c a x -> r) -> (EoT ss -> r) -> r
repOfEithers EoT (ListOfRepSums (M1 D c a) ss)
eot M1 D c a x -> r
ok = EoT (ListOfRepSums a ss) -> (a x -> r) -> (EoT ss -> r) -> r
forall (a :: * -> *) (ss :: [[*]]) x r.
RepOfEithers a ss =>
EoT (ListOfRepSums a ss) -> (a x -> r) -> (EoT ss -> r) -> r
repOfEithers @a @ss EoT (ListOfRepSums a ss)
EoT (ListOfRepSums (M1 D c a) ss)
eot (M1 D c a x -> r
ok (M1 D c a x -> r) -> (a x -> M1 D c a x) -> a x -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a x -> M1 D c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
repOfEithers :: EoT (ListOfRepSums (M1 C c a) (ps : ss))
-> (M1 C c a x -> r) -> (EoT (ps : ss) -> r) -> r
repOfEithers EoT (ListOfRepSums (M1 C c a) (ps : ss))
eot M1 C c a x -> r
ok EoT (ps : ss) -> r
ko =
case EoT (ListOfRepSums (M1 C c a) (ps : ss))
eot of
Left ts -> M1 C c a x -> r
ok (M1 C c a x -> r) -> M1 C c a x -> r
forall a b. (a -> b) -> a -> b
$ a x -> M1 C c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a x -> M1 C c a x) -> a x -> M1 C c a x
forall a b. (a -> b) -> a -> b
$ Tuples (ListOfRepProducts a '[])
-> (a x -> Tuples '[] -> a x) -> a x
forall (a :: * -> *) (xs :: [*]) x r.
RepOfTuples a xs =>
Tuples (ListOfRepProducts a xs) -> (a x -> Tuples xs -> r) -> r
repOfTuples @a @'[] Tuples (ListOfRepProducts a '[])
ts a x -> Tuples '[] -> a x
forall a b. a -> b -> a
const
Right ss -> EoT (ps : ss) -> r
ko EoT (ps : ss)
ss
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
repOfEithers :: EoT (ListOfRepSums (M1 C c a) '[])
-> (M1 C c a x -> r) -> (EoT '[] -> r) -> r
repOfEithers EoT (ListOfRepSums (M1 C c a) '[])
eot M1 C c a x -> r
ok EoT '[] -> r
_ko = M1 C c a x -> r
ok (M1 C c a x -> r) -> M1 C c a x -> r
forall a b. (a -> b) -> a -> b
$ a x -> M1 C c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a x -> M1 C c a x) -> a x -> M1 C c a x
forall a b. (a -> b) -> a -> b
$ Tuples (ListOfRepProducts a '[])
-> (a x -> Tuples '[] -> a x) -> a x
forall (a :: * -> *) (xs :: [*]) x r.
RepOfTuples a xs =>
Tuples (ListOfRepProducts a xs) -> (a x -> Tuples xs -> r) -> r
repOfTuples @_ @'[] Tuples (ListOfRepProducts a '[])
EoT (ListOfRepSums (M1 C c a) '[])
eot a x -> Tuples '[] -> a x
forall a b. a -> b -> a
const
instance RepOfEithers V1 ss where
repOfEithers :: EoT (ListOfRepSums V1 ss) -> (V1 x -> r) -> (EoT ss -> r) -> r
repOfEithers EoT (ListOfRepSums V1 ss)
eot V1 x -> r
_ok EoT ss -> r
ko = EoT ss -> r
ko EoT ss
EoT (ListOfRepSums V1 ss)
eot
class RepOfTuples (a :: * -> *) (xs::[*]) where
repOfTuples ::
Tuples (ListOfRepProducts a xs) ->
(a x -> Tuples xs -> r) -> r
instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a:*:b) ps where
repOfTuples :: Tuples (ListOfRepProducts (a :*: b) ps)
-> ((:*:) a b x -> Tuples ps -> r) -> r
repOfTuples Tuples (ListOfRepProducts (a :*: b) ps)
ts (:*:) a b x -> Tuples ps -> r
k =
Tuples (ListOfRepProducts a (ListOfRepProducts b ps))
-> (a x -> Tuples (ListOfRepProducts b ps) -> r) -> r
forall (a :: * -> *) (xs :: [*]) x r.
RepOfTuples a xs =>
Tuples (ListOfRepProducts a xs) -> (a x -> Tuples xs -> r) -> r
repOfTuples @a @(ListOfRepProducts b ps) Tuples (ListOfRepProducts a (ListOfRepProducts b ps))
Tuples (ListOfRepProducts (a :*: b) ps)
ts
(\a x
a Tuples (ListOfRepProducts b ps)
ts' ->
Tuples (ListOfRepProducts b ps) -> (b x -> Tuples ps -> r) -> r
forall (a :: * -> *) (xs :: [*]) x r.
RepOfTuples a xs =>
Tuples (ListOfRepProducts a xs) -> (a x -> Tuples xs -> r) -> r
repOfTuples @b @ps Tuples (ListOfRepProducts b ps)
ts'
(\b x
b -> (:*:) a b x -> Tuples ps -> r
k (a x
aa x -> b x -> (:*:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:b x
b)))
instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
repOfTuples :: Tuples (ListOfRepProducts (M1 S c a) (p : ps))
-> (M1 S c a x -> Tuples (p : ps) -> r) -> r
repOfTuples (a, ts) M1 S c a x -> Tuples (p : ps) -> r
k = M1 S c a x -> Tuples (p : ps) -> r
k (a x -> M1 S c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (TypeOfRepField a -> a x
forall (a :: * -> *) x. RepOfField a => TypeOfRepField a -> a x
repOfField TypeOfRepField a
a)) Tuples (p : ps)
ts
instance RepOfField a => RepOfTuples (M1 S c a) '[] where
repOfTuples :: Tuples (ListOfRepProducts (M1 S c a) '[])
-> (M1 S c a x -> Tuples '[] -> r) -> r
repOfTuples Tuples (ListOfRepProducts (M1 S c a) '[])
a M1 S c a x -> Tuples '[] -> r
k = M1 S c a x -> Tuples '[] -> r
k (a x -> M1 S c a x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (TypeOfRepField a -> a x
forall (a :: * -> *) x. RepOfField a => TypeOfRepField a -> a x
repOfField TypeOfRepField a
Tuples (ListOfRepProducts (M1 S c a) '[])
a)) ()
instance RepOfTuples U1 ps where
repOfTuples :: Tuples (ListOfRepProducts U1 ps) -> (U1 x -> Tuples ps -> r) -> r
repOfTuples Tuples (ListOfRepProducts U1 ps)
ts U1 x -> Tuples ps -> r
k = U1 x -> Tuples ps -> r
k U1 x
forall k (p :: k). U1 p
U1 Tuples ps
Tuples (ListOfRepProducts U1 ps)
ts
class RepOfField (a :: * -> *) where
repOfField :: TypeOfRepField a -> a x
instance RepOfField (K1 i a) where
repOfField :: TypeOfRepField (K1 i a) -> K1 i a x
repOfField = TypeOfRepField (K1 i a) -> K1 i a x
forall k i c (p :: k). c -> K1 i c p
K1
type EoTOfRep a = EithersOfRep (Rep a) '[]
eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
eotOfadt :: a -> EoT (ADT a)
eotOfadt = forall x. EithersOfRep (Rep a) '[] => Rep a x -> EoT (ADT a)
forall (a :: * -> *) (ss :: [[*]]) x.
EithersOfRep a ss =>
a x -> EoT (ListOfRepSums a ss)
eithersOfRepL @_ @'[] (Rep a Any -> EoT (ADT a)) -> (a -> Rep a Any) -> a -> EoT (ADT a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
Generics.from
class EithersOfRep (a :: * -> *) ss where
eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
instance (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
EithersOfRep (a:+:b) ss where
eithersOfRepL :: (:+:) a b x -> EoT (ListOfRepSums (a :+: b) ss)
eithersOfRepL = \case
L1 a x
a -> a x -> EoT (ListOfRepSums a (ListOfRepSums b ss))
forall (a :: * -> *) (ss :: [[*]]) x.
EithersOfRep a ss =>
a x -> EoT (ListOfRepSums a ss)
eithersOfRepL @a @(ListOfRepSums b ss) a x
a
R1 b x
b -> EoT (ListOfRepSums b ss)
-> EoT (ListOfRepSums a (ListOfRepSums b ss))
forall (a :: * -> *) (ss :: [[*]]).
EithersOfRep a ss =>
EoT ss -> EoT (ListOfRepSums a ss)
eithersOfRepR @a @(ListOfRepSums b ss) (b x -> EoT (ListOfRepSums b ss)
forall (a :: * -> *) (ss :: [[*]]) x.
EithersOfRep a ss =>
a x -> EoT (ListOfRepSums a ss)
eithersOfRepL @b @ss b x
b)
eithersOfRepR :: EoT ss -> EoT (ListOfRepSums (a :+: b) ss)
eithersOfRepR EoT ss
ss = EoT (ListOfRepSums b ss)
-> EoT (ListOfRepSums a (ListOfRepSums b ss))
forall (a :: * -> *) (ss :: [[*]]).
EithersOfRep a ss =>
EoT ss -> EoT (ListOfRepSums a ss)
eithersOfRepR @a @(ListOfRepSums b ss) (EoT ss -> EoT (ListOfRepSums b ss)
forall (a :: * -> *) (ss :: [[*]]).
EithersOfRep a ss =>
EoT ss -> EoT (ListOfRepSums a ss)
eithersOfRepR @b @ss EoT ss
ss)
instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
eithersOfRepL :: M1 D c a x -> EoT (ListOfRepSums (M1 D c a) ss)
eithersOfRepL (M1 a x
a) = a x -> EoT (ListOfRepSums a ss)
forall (a :: * -> *) (ss :: [[*]]) x.
EithersOfRep a ss =>
a x -> EoT (ListOfRepSums a ss)
eithersOfRepL @a @ss a x
a
eithersOfRepR :: EoT ss -> EoT (ListOfRepSums (M1 D c a) ss)
eithersOfRepR = EithersOfRep a ss => EoT ss -> EoT (ListOfRepSums a ss)
forall (a :: * -> *) (ss :: [[*]]).
EithersOfRep a ss =>
EoT ss -> EoT (ListOfRepSums a ss)
eithersOfRepR @a @ss
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
eithersOfRepL :: M1 C c a x -> EoT (ListOfRepSums (M1 C c a) '[])
eithersOfRepL (M1 a x
a) = a x -> Tuples '[] -> Tuples (ListOfRepProducts a '[])
forall (a :: * -> *) (ps :: [*]) x.
TuplesOfRep a ps =>
a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
tuplesOfRep @_ @'[] a x
a ()
eithersOfRepR :: EoT '[] -> EoT (ListOfRepSums (M1 C c a) '[])
eithersOfRepR = EoT '[] -> EoT (ListOfRepSums (M1 C c a) '[])
forall a. Void -> a
absurd
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
eithersOfRepL :: M1 C c a x -> EoT (ListOfRepSums (M1 C c a) (ps : ss))
eithersOfRepL (M1 a x
a) = Tuples (ListOfRepProducts a '[])
-> Either (Tuples (ListOfRepProducts a '[])) (EoT (ps : ss))
forall a b. a -> Either a b
Left (Tuples (ListOfRepProducts a '[])
-> Either (Tuples (ListOfRepProducts a '[])) (EoT (ps : ss)))
-> Tuples (ListOfRepProducts a '[])
-> Either (Tuples (ListOfRepProducts a '[])) (EoT (ps : ss))
forall a b. (a -> b) -> a -> b
$ a x -> Tuples '[] -> Tuples (ListOfRepProducts a '[])
forall (a :: * -> *) (ps :: [*]) x.
TuplesOfRep a ps =>
a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
tuplesOfRep @_ @'[] a x
a ()
eithersOfRepR :: EoT (ps : ss) -> EoT (ListOfRepSums (M1 C c a) (ps : ss))
eithersOfRepR = EoT (ps : ss) -> EoT (ListOfRepSums (M1 C c a) (ps : ss))
forall a b. b -> Either a b
Right
instance EithersOfRep V1 ss where
eithersOfRepL :: V1 x -> EoT (ListOfRepSums V1 ss)
eithersOfRepL = \case {}
eithersOfRepR :: EoT ss -> EoT (ListOfRepSums V1 ss)
eithersOfRepR = EoT ss -> EoT (ListOfRepSums V1 ss)
forall a. a -> a
id
class TuplesOfRep (a :: * -> *) (ps::[*]) where
tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a:*:b) ps where
tuplesOfRep :: (:*:) a b x -> Tuples ps -> Tuples (ListOfRepProducts (a :*: b) ps)
tuplesOfRep (a x
a:*:b x
b) Tuples ps
ps =
a x
-> Tuples (ListOfRepProducts b ps)
-> Tuples (ListOfRepProducts a (ListOfRepProducts b ps))
forall (a :: * -> *) (ps :: [*]) x.
TuplesOfRep a ps =>
a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
tuplesOfRep @a @(ListOfRepProducts b ps) a x
a
(b x -> Tuples ps -> Tuples (ListOfRepProducts b ps)
forall (a :: * -> *) (ps :: [*]) x.
TuplesOfRep a ps =>
a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
tuplesOfRep @b @ps b x
b Tuples ps
ps)
instance TuplesOfRep U1 ps where
tuplesOfRep :: U1 x -> Tuples ps -> Tuples (ListOfRepProducts U1 ps)
tuplesOfRep U1 x
U1 Tuples ps
xs = Tuples ps
Tuples (ListOfRepProducts U1 ps)
xs
instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
tuplesOfRep :: M1 S c a x
-> Tuples (x : ps)
-> Tuples (ListOfRepProducts (M1 S c a) (x : ps))
tuplesOfRep (M1 a x
a) Tuples (x : ps)
xs = (a x -> TypeOfRepField a
forall (a :: * -> *) x. FieldOfRep a => a x -> TypeOfRepField a
fieldOfRep a x
a, Tuples (x : ps)
xs)
instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
tuplesOfRep :: M1 S c a x
-> Tuples '[] -> Tuples (ListOfRepProducts (M1 S c a) '[])
tuplesOfRep (M1 a x
a) Tuples '[]
_xs = a x -> TypeOfRepField a
forall (a :: * -> *) x. FieldOfRep a => a x -> TypeOfRepField a
fieldOfRep a x
a
class FieldOfRep (a :: * -> *) where
fieldOfRep :: a x -> TypeOfRepField a
instance FieldOfRep (K1 i a) where
fieldOfRep :: K1 i a x -> TypeOfRepField (K1 i a)
fieldOfRep (K1 a
a) = a
TypeOfRepField (K1 i a)
a