{-# language UndecidableInstances #-}
module Church.TF where
import GHC.Generics
data ListTerm p = ListTerm
type family WithoutParam v :: * -> * where
WithoutParam ((:+:) l r p) = l :+: r
WithoutParam ((:*:) l r p) = l :*: r
WithoutParam (U1 p) = U1
WithoutParam (M1 a b f p) = M1 a b f
WithoutParam (K1 a t p) = K1 a t
WithoutParam (ListTerm p) = ListTerm
type family StripMeta v where
StripMeta (M1 a b f p) = StripMeta (f p)
StripMeta (K1 a t p) = K1 a t p
StripMeta ((:+:) l r p) =
(:+:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
StripMeta ((:*:) l r p) =
(:*:) (WithoutParam (StripMeta (l p))) (WithoutParam (StripMeta (r p))) p
StripMeta (U1 p) = U1 p
class GStripMeta a where
stripMeta :: a -> StripMeta a
instance GStripMeta (f p) => GStripMeta (M1 a b f p) where
stripMeta (M1 f) = stripMeta f
instance GStripMeta (K1 a t p) where
stripMeta = id
instance GStripMeta (U1 p) where
stripMeta = id
instance (GStripMeta (l p), GStripMeta (r p),
(WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),
(WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>
GStripMeta ((:*:) l r p) where
stripMeta (l :*: r) = stripMeta l :*: stripMeta r
instance (GStripMeta (l p), GStripMeta (r p),
(WithoutParam (StripMeta (l p))) p ~ StripMeta (l p),
(WithoutParam (StripMeta (r p))) p ~ StripMeta (r p)) =>
GStripMeta ((:+:) l r p) where
stripMeta (L1 l) = L1 $ stripMeta l
stripMeta (R1 r) = R1 $ stripMeta r
type family StripK v where StripK (K1 a t p) = t
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys
type family Reverse (xs :: [k]) :: [k] where
Reverse '[] = '[]
Reverse (x ': xs) = Append (Reverse xs) (x ': '[])