{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Comp.Multi.Desugar where
import Data.Comp.Multi
class (HFunctor f, HFunctor g) => Desugar f g where
desugHom :: Hom f g
desugHom = f (Context g a) i -> Context g a i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
Desugar f g =>
Alg f (Context g a)
desugHom' (f (Context g a) i -> Context g a i)
-> (f a i -> f (Context g a) i) -> f a i -> Context g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a :-> Context g a) -> f a :-> f (Context g a)
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap a :-> Context g a
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
desugHom' :: Alg f (Context g a)
desugHom' f (Context g a) i
x = Context g (Context g a) i -> Context g a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (f (Context g a) i -> Context g (Context g a) i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom f (Context g a) i
x)
instance {-# OVERLAPPABLE #-} (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
desugHom :: (:+:) f g a i -> Context h a i
desugHom = (f a i -> Context h a i)
-> (g a i -> Context h a i) -> (:+:) f g a i -> Context h a i
forall k (f :: (* -> *) -> k -> *) (a :: * -> *) (b :: k) c
(g :: (* -> *) -> k -> *).
(f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH f a i -> Context h a i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom g a i -> Context h a i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom
desugar :: Desugar f g => Term f :-> Term g
desugar :: Term f :-> Term g
desugar = Hom f g -> CxtFun f g
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom
desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g',
Desugar f g) => Term f' :-> Term g'
desugarA :: Term f' :-> Term g'
desugarA = Hom f' g' -> CxtFun f' g'
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom (Hom f g -> Hom f' g'
forall (f :: (* -> *) -> * -> *) p (f' :: (* -> *) -> * -> *)
(g :: (* -> *) -> * -> *) (g' :: (* -> *) -> * -> *).
(DistAnn f p f', DistAnn g p g', HFunctor g) =>
Hom f g -> Hom f' g'
propAnn Hom f g
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom)
instance {-# OVERLAPPABLE #-} (HFunctor f, HFunctor g, f :<: g) => Desugar f g where
desugHom :: f a i -> Context g a i
desugHom = g a i -> Context g a i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt (g a i -> Context g a i)
-> (f a i -> g a i) -> f a i -> Context g a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a i -> g a i
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(a :: * -> *).
(f :<: g) =>
f a :-> g a
inj