{-# language UndecidableInstances #-}
module Church.FromChurch where
import GHC.Generics
import Church.TF
import Prelude
data Traverse a c = Meta a c a | InL a a | InR a a | Term a
type family PathArg (t :: [Traverse * Meta]) where
PathArg (Term a ': '[] ) = a
PathArg ('Meta a b p ': rest) = PathArg rest
PathArg (InR l p ': rest) = PathArg rest
PathArg (InL r p ': rest) = PathArg rest
class GEmpty a where empty :: a
instance GEmpty (U1 p) where empty = U1
instance GEmpty (K1 a t p) where empty = K1 (error "Error! The impossible has happened.")
instance GEmpty (f p) => GEmpty (M1 a b f p) where empty = M1 empty
instance (GEmpty (l p), GEmpty (r p)) => GEmpty ((:*:) l r p) where empty = empty :*: empty
type family MakeProdPaths v (m :: [Traverse * Meta]) (r :: [ [Traverse * Meta] ]) :: [[Traverse * Meta]] where
MakeProdPaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all
MakeProdPaths (M1 a b f p) s all = MakeProdPaths (f p) ('Meta a b p ': s) all
MakeProdPaths ((:*:) l r p) s all =
Append (MakeProdPaths (l p) (InL (r p) p ': s) '[])
(Append (MakeProdPaths (r p) (InR (l p) p ': s) '[]) all)
class GUpdate (path :: [Traverse * Meta]) a where update :: a -> PathArg path -> a
instance GUpdate (Term (K1 a t p) ': '[]) (K1 a t p) where update _ a = a
instance GUpdate rest (l p) => GUpdate (InL (r p) p ': rest) ((:*:) l r p) where
update (l :*: r) a = update @rest l a :*: r
instance GUpdate rest (r p) => GUpdate (InR (l p) p ': rest) ((:*:) l r p) where
update (l :*: r) a = l :*: update @rest r a
instance GUpdate rest (f p) => GUpdate ('Meta a b p ': rest) (M1 a b f p) where
update (M1 f) a = M1 (update @rest f a)
type family Fill (paths :: [[Traverse * Meta]]) r where
Fill (x ': xs) r = StripK (PathArg x) -> Fill xs r
Fill '[] r = r
class GFill (paths :: [[Traverse * Meta]]) a where
fill :: (a -> r) -> a -> Fill paths r
instance GFill '[] a where
fill f a = f a
instance (PathArg x ~ K1 m t p, StripK (PathArg x) ~ t, GUpdate x a, GFill xs a) =>
GFill (x ': xs) a where
fill f a = \x -> fill @xs f $ update @x a (K1 x)
type family MakePaths v (m :: [Traverse * Meta]) (r :: [ [Traverse * Meta] ]) :: [[Traverse * Meta]] where
MakePaths ((:+:) l r p) s all =
Append (MakePaths (l p) (InL (r p) p ': s) '[])
(Append (MakePaths (r p) (InR (l p) p ': s) '[]) all)
MakePaths (M1 a b f p) s all = MakePaths (f p) ('Meta a b p ': s) all
MakePaths (K1 a t p) s all = Reverse (Term (K1 a t p) ': s) ': all
MakePaths (U1 p) s all = Reverse (Term (U1 p) ': s) ': all
MakePaths ((:*:) l r p) s all = Reverse (Term ((:*:) l r p) ': s) ': all
type family ReconstructPath (t :: [Traverse * Meta]) where
ReconstructPath (InL r p ': rest) = (WithoutParam (ReconstructPath rest) :+: WithoutParam r) p
ReconstructPath (InR l p ': rest) = (WithoutParam l :+: WithoutParam (ReconstructPath rest)) p
ReconstructPath ('Meta a b p ': rest) = M1 a b (WithoutParam (ReconstructPath rest)) p
ReconstructPath (Term a ': '[]) = a
class GPath' (p :: [Traverse * Meta]) where path' :: PathArg p -> ReconstructPath p
instance GPath' (Term a ': '[]) where path' = id
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)
=> GPath' (InR r p ': rest) where path' a = R1 $ path' @rest a
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)
=> GPath' (InL l p ': rest) where path' a = L1 $ path' @rest a
instance ((WithoutParam (ReconstructPath rest)) p ~ ReconstructPath rest, GPath' rest)
=> GPath' ('Meta a b p ': rest) where path' a = M1 $ path' @rest a
class GBuild (paths :: [[Traverse * Meta]]) f r where build :: f -> r
instance (ReconstructPath x ~ r, GPath' x, GBuild xs f' r, PathArg x ~ U1 p)
=> GBuild (x ': xs) (r -> f') r where build f = build @xs $ f (path' @x U1)
instance ((f -> g) ~ Fill (MakeProdPaths (PathArg x) '[] '[]) r,
ReconstructPath x ~ r, GEmpty (PathArg x), GBuild xs f' r,
(GFill (MakeProdPaths (PathArg x) '[] '[]) (PathArg x)),
GPath' x)
=> GBuild (x ': xs) ((f -> g) -> f') r where
build f = build @xs $ f (fill @(MakeProdPaths (PathArg x) '[] '[]) (path' @x) empty)
instance GBuild '[] r r where build = id