{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Church.ToChurch where
import GHC.Generics
import Church.TF
import Prelude
type family ChurchProd v c where
ChurchProd (K1 a t p) c = t -> c
ChurchProd (U1 p) c = c
ChurchProd ((:*:) l r p) c = ChurchProd (l p) (ChurchProd (r p) c)
ChurchProd (ListTerm p) c = c
type family ToListProd v rest where
ToListProd ((:*:) l r' p) r = ToListProd (l p) (ToListProd (r' p) r)
ToListProd (K1 a t p) r = (K1 a t :*: WithoutParam r) p
ToListProd (U1 p) r = U1 p
class GListProd a r where
toListProd :: a -> r -> ToListProd a r
instance (WithoutParam r) p ~ r => GListProd (U1 p) r where
toListProd = const
instance (WithoutParam r) p ~ r => GListProd (K1 a t p) r where
toListProd = (:*:)
instance (GListProd (l p) (ToListProd (r' p) r), GListProd (r' p) r) => GListProd ((:*:) l r' p) r where
toListProd (l :*: r) rest = toListProd l (toListProd r rest)
class GChurchProd a where prod :: a -> ChurchProd a r -> r
instance GChurchProd (U1 p) where prod _ f = f
instance GChurchProd (K1 a t p) where prod (K1 r) f = f r
instance GChurchProd (r p) => GChurchProd ((K1 a t :*: r) p) where
prod (K1 l :*: r) f = prod r (f l)
instance GChurchProd (ListTerm p) where prod _ f = f
type family ToList v rest where
ToList ((:+:) l r' p) r = ToList (l p) (ToList (r' p) r)
ToList (K1 a t p) r = (K1 a t :+: WithoutParam r) p
ToList ((:*:) l r' p) r = ((l :*: r') :+: WithoutParam r) p
ToList (U1 p) r = (U1 :+: WithoutParam r) p
class GList a r where
toList :: Maybe a -> r -> ToList a r
instance (WithoutParam r) p ~ r => GList (U1 p) r where
toList Nothing r = R1 r
toList (Just a) _ = L1 a
instance (WithoutParam r) p ~ r => GList (K1 a t p) r where
toList Nothing r = R1 r
toList (Just a) _ = L1 a
instance (WithoutParam r) p ~ r => GList ((l :*: r') p) r where
toList Nothing r = R1 r
toList (Just a) _ = L1 a
instance (GList (l p) (ToList (r' p) r),
GList (r' p) r) => GList ((l :+: r') p) r where
toList (Just sum@(L1 l)) r = toList (Just l) (toList (rNot sum) r)
where rNot :: forall l r p. (l :+: r) p -> Maybe (r p)
rNot _ = Nothing
toList (Just sum@(R1 r')) r = toList (lNot sum) (toList (Just r') r)
where lNot :: forall l r p. (l :+: r) p -> Maybe (l p)
lNot _ = Nothing
toList m r = toList (lNot m) (toList (rNot m) r)
where lNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (l p)
lNot _ = Nothing
rNot :: forall l r p. Maybe ((:+:) l r p) -> Maybe (r p)
rNot _ = Nothing
type family ChurchSum v c where
ChurchSum ((:+:) l r p) c = ChurchProd (ToListProd (l p) (ListTerm ())) c -> ChurchSum (r p) c
ChurchSum (ListTerm p) c = c
class Swallow a where swallow :: c -> ChurchSum a c
instance Swallow (ListTerm p) where swallow c = c
instance Swallow (r p) => Swallow ((:+:) l r p) where swallow c = \_ -> swallow @(r p) c
class GChurchSum a r where elim :: a -> ChurchSum a r
instance (GListProd (l p) (ListTerm ()), GChurchProd (ToListProd (l p) (ListTerm ())),
GChurchSum (r' p) r, Swallow (r' p)) =>
GChurchSum ((l :+: r') p) r where
elim sum@(L1 l) = \f -> swallow @(r' p) (prod @_ @r (toListProd l (ListTerm :: ListTerm ())) f)
elim (R1 r) = \_ -> elim @_ @r r
instance GChurchSum (ListTerm p) r where elim _ = error "Malformed generic instance"