{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Desugar
-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This modules defines the 'Desugar' type class for desugaring of terms.
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.Desugar where

import Data.Comp.Multi


-- |The desugaring term homomorphism.
class (HFunctor f, HFunctor g) => Desugar f g where
    desugHom :: Hom f g
    desugHom = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
Desugar f g =>
Alg f (Context g a)
desugHom' 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 :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole
    desugHom' :: Alg f (Context g a)
    desugHom' f (Context g a) i
x = forall (f :: (* -> *) -> * -> *) h (a :: * -> *).
HFunctor f =>
Context f (Cxt h f a) :-> Cxt h f a
appCxt (forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom f (Context g a) i
x)


-- We make the lifting to sums explicit in order to make the Desugar
-- class work with the default instance declaration further below.
instance {-# OVERLAPPABLE #-} (Desugar f h, Desugar g h) => Desugar (f :+: g) h where
    desugHom :: Hom (f :+: g) h
desugHom = forall {k} (f :: (* -> *) -> k -> *) (a :: * -> *) (b :: k) c
       (g :: (* -> *) -> k -> *).
(f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom

-- |Desugar a term.
desugar :: Desugar f g => Term f :-> Term g
desugar :: forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Term f :-> Term g
desugar = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom

-- |Lift desugaring to annotated terms.
desugarA :: (HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g',
             Desugar f g) => Term f' :-> Term g'
desugarA :: forall (f' :: (* -> *) -> * -> *) (g' :: (* -> *) -> * -> *)
       (f :: (* -> *) -> * -> *) p (g :: (* -> *) -> * -> *).
(HFunctor f', HFunctor g', DistAnn f p f', DistAnn g p g',
 Desugar f g) =>
Term f' :-> Term g'
desugarA = forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
(HFunctor f, HFunctor g) =>
Hom f g -> CxtFun f g
appHom (forall (f :: (* -> *) -> * -> *) p (f' :: (* -> *) -> * -> *)
       (g :: (* -> *) -> * -> *) (g' :: (* -> *) -> * -> *).
(DistAnn f p f', DistAnn g p g', HFunctor g) =>
Hom f g -> Hom f' g'
propAnn forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *).
Desugar f g =>
Hom f g
desugHom)

-- |Default desugaring instance.
instance {-# OVERLAPPABLE #-} (HFunctor f, HFunctor g, f :<: g) => Desugar f g where
    desugHom :: Hom f g
desugHom = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i.
HFunctor f =>
f a i -> Context f a i
simpCxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (a :: * -> *).
(f :<: g) =>
f a :-> g a
inj