{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Comp.Multi.Sum
(
(:<:),
(:+:),
caseH,
proj,
project,
deepProject,
inj,
inject,
deepInject,
split,
injectConst,
projectConst,
injectCxt,
liftCxt,
substHoles,
) where
import Data.Comp.Multi.Algebra
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.HTraversable
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
project :: (g :<: f) => NatM Maybe (Cxt h f a) (g (Cxt h f a))
project :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project (Hole a i
_) = forall a. Maybe a
Nothing
project (Term f (Cxt h f a) i
t) = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj f (Cxt h f a) i
t
deepProject :: (HTraversable g, g :<: f) => CxtFunM Maybe f g
{-# INLINE deepProject #-}
deepProject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(HTraversable g, g :<: f) =>
CxtFunM Maybe f g
deepProject = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *).
(HTraversable g, Monad m) =>
SigFunM m f g -> CxtFunM m f g
appSigFunM' forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
NatM Maybe (g a) (f a)
proj
inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a
inject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject = forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
f a :-> g a
inj
deepInject :: (HFunctor g, g :<: f) => CxtFun g f
{-# INLINE deepInject #-}
deepInject :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *).
(HFunctor g, g :<: f) =>
CxtFun g f
deepInject = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
HFunctor f =>
SigFun f g -> CxtFun f g
appSigFun forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
f a :-> g a
inj
split :: (f :=: f1 :+: f2) => (f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
split :: forall (f :: (* -> *) -> * -> *) (f1 :: (* -> *) -> * -> *)
(f2 :: (* -> *) -> * -> *) (a :: * -> *).
(f :=: (f1 :+: f2)) =>
(f1 (Term f) :-> a) -> (f2 (Term f) :-> a) -> Term f :-> a
split f1 (Term f) :-> a
f1 f2 (Term f) :-> a
f2 (Term f (Term f) i
t) = forall (f :: (* -> *) -> * -> *) (f1 :: (* -> *) -> * -> *)
(f2 :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *).
(f :=: (f1 :+: f2)) =>
(f1 a :-> b) -> (f2 a :-> b) -> f a :-> b
spl f1 (Term f) :-> a
f1 f2 (Term f) :-> a
f2 f (Term f) i
t
injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h' h
(a :: * -> *).
(HFunctor g, g :<: f) =>
Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt = forall (f :: (* -> *) -> * -> *) (e :: * -> *) h.
HFunctor f =>
Alg f e -> Cxt h f e :-> e
cata' forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject
liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a
liftCxt :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(HFunctor f, g :<: f) =>
g a :-> Context f a
liftCxt g a i
g = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt forall a b. (a -> b) -> a -> b
$ forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
f a :-> g a
inj g a i
g
substHoles :: (HFunctor f, HFunctor g, f :<: g)
=> (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
substHoles :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(v :: * -> *) h (a :: * -> *) h'.
(HFunctor f, HFunctor g, f :<: g) =>
(v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
substHoles v :-> Cxt h g a
f Cxt h' f v i
c = forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h' h
(a :: * -> *).
(HFunctor g, g :<: f) =>
Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt forall a b. (a -> b) -> a -> b
$ forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap v :-> Cxt h g a
f Cxt h' f v i
c
injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
injectConst :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(HFunctor g, g :<: f) =>
Const g :-> Cxt h f a
injectConst = forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
g (Cxt h f a) :-> Cxt h f a
inject forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall a b. a -> b -> a
const forall a. HasCallStack => a
undefined)
projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
projectConst :: forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(HFunctor g, g :<: f) =>
NatM Maybe (Cxt h f a) (Const g)
projectConst = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall a b. a -> b -> a
const (forall a i. a -> K a i
K ()))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *) h
(a :: * -> *).
(g :<: f) =>
NatM Maybe (Cxt h f a) (g (Cxt h f a))
project