{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Comp.Desugar where
import Data.Comp
class (Functor f, Functor g) => Desugar f g where
desugHom :: Hom f g
desugHom = Alg f (Context g a)
forall (f :: * -> *) (g :: * -> *) a.
Desugar f g =>
Alg f (Context g a)
desugHom' Alg f (Context g a)
-> (f a -> f (Context g a)) -> f a -> Context g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Context g a) -> f a -> f (Context g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Context g a
forall a (f :: * -> *). a -> Cxt Hole f a
Hole
desugHom' :: Alg f (Context g a)
desugHom' f (Context g a)
x = Context g (Context g a) -> Context g a
forall (f :: * -> *) h a.
Functor f =>
Context f (Cxt h f a) -> Cxt h f a
appCxt (f (Context g a) -> Context g (Context g a)
forall (f :: * -> *) (g :: * -> *). Desugar f g => Hom f g
desugHom f (Context g a)
x)
instance {-# OVERLAPPABLE #-} (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
desugHom :: (:+:) f g a -> Context h a
desugHom = (f a -> Context h a)
-> (g a -> Context h a) -> (:+:) f g a -> Context h a
forall k (f :: k -> *) (a :: k) b (g :: k -> *).
(f a -> b) -> (g a -> b) -> (:+:) f g a -> b
caseF f a -> Context h a
forall (f :: * -> *) (g :: * -> *). Desugar f g => Hom f g
desugHom g a -> Context h a
forall (f :: * -> *) (g :: * -> *). Desugar f g => Hom f g
desugHom
desugar :: Desugar f g => Term f -> Term g
{-# INLINE desugar #-}
desugar :: Term f -> Term g
desugar = Hom f g -> CxtFun f g
forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Hom f g -> CxtFun f g
appHom Hom f g
forall (f :: * -> *) (g :: * -> *). Desugar f g => Hom f g
desugHom
desugarA :: (Functor f', Functor 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 :: * -> *).
(Functor f, Functor 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', Functor g) =>
Hom f g -> Hom f' g'
propAnn Hom f g
forall (f :: * -> *) (g :: * -> *). Desugar f g => Hom f g
desugHom)
instance {-# OVERLAPPABLE #-} (Functor f, Functor g, f :<: g) => Desugar f g where
desugHom :: f a -> Context g a
desugHom = g a -> Context g a
forall (f :: * -> *) a. Functor f => f a -> Context f a
simpCxt (g a -> Context g a) -> (f a -> g a) -> f a -> Context g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. (f :<: g) => f a -> g a
inj