{-# 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
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 Rule t g
r 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' Inherited t (g sem sem)
inh = Synthesized t (g sem sem)
syn
where (Synthesized t (g sem sem)
syn, 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
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 forall a. p a -> a
extract t
t 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 #-}
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 forall a. p a -> a
extract t
t 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 #-}