{-# Language FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, StandaloneDeriving,
             TypeFamilies, TypeOperators, UndecidableInstances #-}

module Transformation.AG where

import Data.Functor.Identity
import qualified Rank2
import Transformation (Transformation, Domain, Codomain)
import qualified Transformation
import qualified Transformation.Deep as Deep
import qualified Transformation.Full as Full
import qualified Transformation.Shallow as Shallow

type family Atts (f :: * -> *) a

newtype Inherited t a = Inherited{Inherited t a -> Atts (Inherited t) a
inh :: Atts (Inherited t) a}
newtype Synthesized t a = Synthesized{Synthesized t a -> Atts (Synthesized t) a
syn :: Atts (Synthesized t) a}

deriving instance (Show (Atts (Inherited t) a)) => Show (Inherited t a)
deriving instance (Show (Atts (Synthesized t) a)) => Show (Synthesized t a)

type Semantics t = Inherited t Rank2.~> Synthesized t

type Rule t g =  forall sem . sem ~ Semantics t
              => (Inherited   t (g sem sem), g sem (Synthesized t))
              -> (Synthesized t (g sem sem), g sem (Inherited t))

knit :: (Rank2.Apply (g sem), sem ~ Semantics t) => Rule t g -> g sem sem -> sem (g sem sem)
knit :: Rule t g -> g sem sem -> sem (g sem sem)
knit r :: Rule t g
r chSem :: g sem sem
chSem = (Inherited t (g sem sem) -> Synthesized t (g sem sem))
-> Arrow (Inherited t) (Synthesized t) (g sem sem)
forall k (p :: k -> *) (q :: k -> *) (a :: k).
(p a -> q a) -> Arrow p q a
Rank2.Arrow Inherited t (g sem sem) -> Synthesized t (g sem sem)
knit'
   where knit' :: Inherited t (g sem sem) -> Synthesized t (g sem sem)
knit' inh :: Inherited t (g sem sem)
inh = Synthesized t (g sem sem)
syn
            where (syn :: Synthesized t (g sem sem)
syn, chInh :: g sem (Inherited t)
chInh) = (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
Rule t g
r (Inherited t (g sem sem)
inh, g sem (Synthesized t)
chSyn)
                  chSyn :: g sem (Synthesized t)
chSyn = g sem sem
g sem (Semantics t)
chSem g sem (Semantics t) -> g sem (Inherited t) -> g sem (Synthesized t)
forall k (g :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Apply g =>
g (p ~> q) -> g p -> g q
Rank2.<*> g sem (Inherited t)
chInh

class Attribution t g deep shallow where
   attribution :: t -> shallow (g deep deep) -> Rule t g
   bequest     :: forall sem . sem ~ Semantics t =>
                  t -> shallow (g deep deep) -> Atts (Inherited t) (g sem sem) -> g sem (Synthesized t)
               -> g sem (Inherited t)
   synthesis   :: forall sem . sem ~ Semantics t =>
                  t -> shallow (g deep deep) -> Atts (Inherited t) (g sem sem) -> g sem (Synthesized t)
               -> Atts (Synthesized t) (g sem sem)
   attribution t :: t
t l :: shallow (g deep deep)
l (Inherited i :: Atts (Inherited t) (g sem sem)
i, s :: g sem (Synthesized t)
s) = (Atts (Synthesized t) (g sem sem) -> Synthesized t (g sem sem)
forall t a. Atts (Synthesized t) a -> Synthesized t a
Synthesized (Atts (Synthesized t) (g sem sem) -> Synthesized t (g sem sem))
-> Atts (Synthesized t) (g sem sem) -> Synthesized t (g sem sem)
forall a b. (a -> b) -> a -> b
$ t
-> shallow (g deep deep)
-> Atts (Inherited t) (g sem sem)
-> g sem (Synthesized t)
-> Atts (Synthesized t) (g sem sem)
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *) (sem :: * -> *).
(Attribution t g deep shallow, sem ~ Semantics t) =>
t
-> shallow (g deep deep)
-> Atts (Inherited t) (g sem sem)
-> g sem (Synthesized t)
-> Atts (Synthesized t) (g sem sem)
synthesis t
t shallow (g deep deep)
l Atts (Inherited t) (g sem sem)
i g sem (Synthesized t)
s, t
-> shallow (g deep deep)
-> Atts (Inherited t) (g sem sem)
-> g sem (Synthesized t)
-> g sem (Inherited t)
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *) (sem :: * -> *).
(Attribution t g deep shallow, sem ~ Semantics t) =>
t
-> shallow (g deep deep)
-> Atts (Inherited t) (g sem sem)
-> g sem (Synthesized t)
-> g sem (Inherited t)
bequest t
t shallow (g deep deep)
l Atts (Inherited t) (g sem sem)
i g sem (Synthesized t)
s)
   bequest t :: t
t l :: shallow (g deep deep)
l i :: Atts (Inherited t) (g sem sem)
i s :: g sem (Synthesized t)
s = (Synthesized t (g sem sem), g sem (Inherited t))
-> g sem (Inherited t)
forall a b. (a, b) -> b
snd (t
-> shallow (g deep deep)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *).
Attribution t g deep shallow =>
t -> shallow (g deep deep) -> Rule t g
attribution t
t shallow (g deep deep)
l (Atts (Inherited t) (g sem sem) -> Inherited t (g sem sem)
forall t a. Atts (Inherited t) a -> Inherited t a
Inherited Atts (Inherited t) (g sem sem)
i, g sem (Synthesized t)
s))
   synthesis t :: t
t l :: shallow (g deep deep)
l i :: Atts (Inherited t) (g sem sem)
i s :: g sem (Synthesized t)
s = Synthesized t (g sem sem) -> Atts (Synthesized t) (g sem sem)
forall t a. Synthesized t a -> Atts (Synthesized t) a
syn ((Synthesized t (g sem sem), g sem (Inherited t))
-> Synthesized t (g sem sem)
forall a b. (a, b) -> a
fst ((Synthesized t (g sem sem), g sem (Inherited t))
 -> Synthesized t (g sem sem))
-> (Synthesized t (g sem sem), g sem (Inherited t))
-> Synthesized t (g sem sem)
forall a b. (a -> b) -> a -> b
$ t
-> shallow (g deep deep)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *).
Attribution t g deep shallow =>
t -> shallow (g deep deep) -> Rule t g
attribution t
t shallow (g deep deep)
l (Atts (Inherited t) (g sem sem) -> Inherited t (g sem sem)
forall t a. Atts (Inherited t) a -> Inherited t a
Inherited Atts (Inherited t) (g sem sem)
i, g sem (Synthesized t)
s))
   {-# Minimal attribution | bequest, synthesis #-}

instance Transformation (Inherited t a) where
   type Domain (Inherited t a) = Semantics t
   type Codomain (Inherited t a) = Inherited t

instance (Atts (Inherited t) a ~ Atts (Inherited t) b) => Transformation.At (Inherited t a) b where
   $ :: Inherited t a
-> Domain (Inherited t a) b -> Codomain (Inherited t a) b
($) (Inherited i :: Atts (Inherited t) a
i) = Inherited t b
-> Arrow (Inherited t) (Synthesized t) b -> Inherited t b
forall a b. a -> b -> a
const (Atts (Inherited t) b -> Inherited t b
forall t a. Atts (Inherited t) a -> Inherited t a
Inherited Atts (Inherited t) a
Atts (Inherited t) b
i)

passDown :: (sem ~ Semantics t, Shallow.Functor (Inherited t (g sem sem)) (g sem)) =>
            Inherited t (g sem sem) -> g sem sem -> g sem (Inherited t)
passDown :: Inherited t (g sem sem) -> g sem sem -> g sem (Inherited t)
passDown inheritance :: Inherited t (g sem sem)
inheritance node :: g sem sem
node = Inherited t (g sem sem)
inheritance Inherited t (g sem sem)
-> g sem (Domain (Inherited t (g sem sem)))
-> g sem (Codomain (Inherited t (g sem sem)))
forall t (g :: (* -> *) -> *).
Functor t g =>
t -> g (Domain t) -> g (Codomain t)
Shallow.<$> g sem sem
g sem (Domain (Inherited t (g sem sem)))
node

-- | Drop-in implementation of 'Transformation.$'
applyDefault :: (q ~ Semantics t, x ~ g q q, Rank2.Apply (g q), Attribution t g q p)
             => (forall a. p a -> a) -> t -> p x -> q x
applyDefault :: (forall a. p a -> a) -> t -> p x -> q x
applyDefault extract :: forall a. p a -> a
extract t :: t
t x :: p x
x = Rule t g -> g q q -> q (g q q)
forall (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *) t.
(Apply (g sem), sem ~ Semantics t) =>
Rule t g -> g sem sem -> sem (g sem sem)
knit (t -> p (g (Semantics t) (Semantics t)) -> Rule t g
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *).
Attribution t g deep shallow =>
t -> shallow (g deep deep) -> Rule t g
attribution t
t p x
p (g (Semantics t) (Semantics t))
x) (p x -> x
forall a. p a -> a
extract p x
x)
{-# INLINE applyDefault #-}

-- | Drop-in implementation of 'Full.<$>'
fullMapDefault :: (p ~ Domain t, q ~ Semantics t, q ~ Codomain t, x ~ g q q, Rank2.Apply (g q),
                   Deep.Functor t g, Attribution t g p p)
               => (forall a. p a -> a) -> t -> p (g p p) -> q (g q q)
fullMapDefault :: (forall a. p a -> a) -> t -> p (g p p) -> q (g q q)
fullMapDefault extract :: forall a. p a -> a
extract t :: t
t local :: p (g p p)
local = Rule t g -> g q q -> q (g q q)
forall (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *) t.
(Apply (g sem), sem ~ Semantics t) =>
Rule t g -> g sem sem -> sem (g sem sem)
knit (t -> p (g p p) -> Rule t g
forall t (g :: (* -> *) -> (* -> *) -> *) (deep :: * -> *)
       (shallow :: * -> *).
Attribution t g deep shallow =>
t -> shallow (g deep deep) -> Rule t g
attribution t
t p (g p p)
local) (t
t t -> g (Domain t) (Domain t) -> g (Codomain t) (Codomain t)
forall t (g :: (* -> *) -> (* -> *) -> *).
Functor t g =>
t -> g (Domain t) (Domain t) -> g (Codomain t) (Codomain t)
Deep.<$> p (g p p) -> g p p
forall a. p a -> a
extract p (g p p)
local)
{-# INLINE fullMapDefault #-}