{-# Language FlexibleContexts, FlexibleInstances,
MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, StandaloneDeriving,
TypeFamilies, TypeOperators, UndecidableInstances #-}
module Transformation.AG where
import Unsafe.Coerce (unsafeCoerce)
import qualified Rank2
import qualified Transformation
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 PreservingSemantics t f = Rank2.Arrow (Inherited t) (Rank2.Product (AllAtts t) f)
data AllAtts t a = AllAtts{AllAtts t a -> Atts (Inherited t) a
allInh :: Atts (Inherited t) a,
AllAtts t a -> Atts (Synthesized t) a
allSyn :: Atts (Synthesized t) a}
type Rule t g = forall sem . sem ~ Semantics t
=> (Inherited t (g sem (Semantics t)), g sem (Synthesized t))
-> (Synthesized t (g sem (Semantics t)), 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 (Semantics t))
-> Synthesized t (g sem (Semantics t)))
-> Arrow (Inherited t) (Synthesized t) (g sem (Semantics t))
forall k (p :: k -> *) (q :: k -> *) (a :: k).
(p a -> q a) -> Arrow p q a
Rank2.Arrow Inherited t (g sem (Semantics t))
-> Synthesized t (g sem (Semantics t))
knit'
where knit' :: Inherited t (g sem (Semantics t))
-> Synthesized t (g sem (Semantics t))
knit' Inherited t (g sem (Semantics t))
inherited = Synthesized t (g sem (Semantics t))
synthesized
where (Synthesized t (g sem (Semantics t))
synthesized, g sem (Inherited t)
chInh) = (Inherited t (g sem (Semantics t)), g sem (Synthesized t))
-> (Synthesized t (g sem (Semantics t)), g sem (Inherited t))
Rule t g
r (Inherited t (g sem (Semantics t))
inherited, 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
knitKeeping :: forall t f g sem. (sem ~ PreservingSemantics t f, Rank2.Apply (g sem),
Atts (Inherited t) (g sem sem) ~ Atts (Inherited t) (g (Semantics t) (Semantics t)),
Atts (Synthesized t) (g sem sem) ~ Atts (Synthesized t) (g (Semantics t) (Semantics t)),
g sem (Synthesized t) ~ g (Semantics t) (Synthesized t),
g sem (Inherited t) ~ g (Semantics t) (Inherited t))
=> (forall a. f a -> a) -> Rule t g -> f (g (PreservingSemantics t f) (PreservingSemantics t f))
-> PreservingSemantics t f (g (PreservingSemantics t f) (PreservingSemantics t f))
knitKeeping :: (forall a. f a -> a)
-> Rule t g
-> f (g (PreservingSemantics t f) (PreservingSemantics t f))
-> PreservingSemantics
t f (g (PreservingSemantics t f) (PreservingSemantics t f))
knitKeeping forall a. f a -> a
extract Rule t g
rule f (g (PreservingSemantics t f) (PreservingSemantics t f))
x = (Inherited
t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Product
(AllAtts t)
f
(g (PreservingSemantics t f) (PreservingSemantics t f)))
-> PreservingSemantics
t f (g (PreservingSemantics t f) (PreservingSemantics t f))
forall k (p :: k -> *) (q :: k -> *) (a :: k).
(p a -> q a) -> Arrow p q a
Rank2.Arrow Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Product
(AllAtts t)
f
(g (PreservingSemantics t f) (PreservingSemantics t f))
knitted
where knitted :: Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Rank2.Product (AllAtts t) f (g (PreservingSemantics t f) (PreservingSemantics t f))
chSem :: g (PreservingSemantics t f) (PreservingSemantics t f)
knitted :: Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Product
(AllAtts t)
f
(g (PreservingSemantics t f) (PreservingSemantics t f))
knitted Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
inherited = AllAtts t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> f (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Product
(AllAtts t)
f
(g (PreservingSemantics t f) (PreservingSemantics t f))
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Rank2.Pair AllAtts :: forall t a.
Atts (Inherited t) a -> Atts (Synthesized t) a -> AllAtts t a
AllAtts{allInh :: Atts
(Inherited t)
(g (PreservingSemantics t f) (PreservingSemantics t f))
allInh= Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Atts
(Inherited t)
(g (PreservingSemantics t f) (PreservingSemantics t f))
forall t a. Inherited t a -> Atts (Inherited t) a
inh Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
inherited, allSyn :: Atts
(Synthesized t)
(g (PreservingSemantics t f) (PreservingSemantics t f))
allSyn= Synthesized
t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Atts
(Synthesized t)
(g (PreservingSemantics t f) (PreservingSemantics t f))
forall t a. Synthesized t a -> Atts (Synthesized t) a
syn Synthesized
t (g (PreservingSemantics t f) (PreservingSemantics t f))
synthesized} f (g (PreservingSemantics t f) (PreservingSemantics t f))
x
where chInh :: g (PreservingSemantics t f) (Inherited t)
chSyn :: g (PreservingSemantics t f) (Synthesized t)
chKept :: g (PreservingSemantics t f) (Rank2.Product (AllAtts t) f)
synthesized :: Synthesized t (g (PreservingSemantics t f) (PreservingSemantics t f))
(Synthesized
t (g (PreservingSemantics t f) (PreservingSemantics t f))
synthesized, g (PreservingSemantics t f) (Inherited t)
chInh) = (Synthesized t (g (Semantics t) (Semantics t)),
g (Semantics t) (Inherited t))
-> (Synthesized
t (g (PreservingSemantics t f) (PreservingSemantics t f)),
g (PreservingSemantics t f) (Inherited t))
forall a b. a -> b
unsafeCoerce ((Inherited t (g (Semantics t) (Semantics t)),
g (Semantics t) (Synthesized t))
-> (Synthesized t (g (Semantics t) (Semantics t)),
g (Semantics t) (Inherited t))
Rule t g
rule (Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
-> Inherited t (g (Semantics t) (Semantics t))
forall a b. a -> b
unsafeCoerce Inherited t (g (PreservingSemantics t f) (PreservingSemantics t f))
inherited, g (PreservingSemantics t f) (Synthesized t)
-> g (Semantics t) (Synthesized t)
forall a b. a -> b
unsafeCoerce g (PreservingSemantics t f) (Synthesized t)
chSyn))
chSyn :: g (PreservingSemantics t f) (Synthesized t)
chSyn = Atts (Synthesized t) a -> Synthesized t a
forall t a. Atts (Synthesized t) a -> Synthesized t a
Synthesized (Atts (Synthesized t) a -> Synthesized t a)
-> (Product (AllAtts t) f a -> Atts (Synthesized t) a)
-> Product (AllAtts t) f a
-> Synthesized t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllAtts t a -> Atts (Synthesized t) a
forall t a. AllAtts t a -> Atts (Synthesized t) a
allSyn (AllAtts t a -> Atts (Synthesized t) a)
-> (Product (AllAtts t) f a -> AllAtts t a)
-> Product (AllAtts t) f a
-> Atts (Synthesized t) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product (AllAtts t) f a -> AllAtts t a
forall k (g :: k -> *) (h :: k -> *) (p :: k). Product g h p -> g p
Rank2.fst (forall a. Product (AllAtts t) f a -> Synthesized t a)
-> g (PreservingSemantics t f) (Product (AllAtts t) f)
-> g (PreservingSemantics t f) (Synthesized t)
forall k (g :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor g =>
(forall (a :: k). p a -> q a) -> g p -> g q
Rank2.<$> g (PreservingSemantics t f) (Product (AllAtts t) f)
chKept
chKept :: g (PreservingSemantics t f) (Product (AllAtts t) f)
chKept = g (PreservingSemantics t f) (PreservingSemantics t f)
chSem g (PreservingSemantics t f) (PreservingSemantics t f)
-> g (PreservingSemantics t f) (Inherited t)
-> g (PreservingSemantics t f) (Product (AllAtts t) f)
forall k (g :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Apply g =>
g (p ~> q) -> g p -> g q
Rank2.<*> g (PreservingSemantics t f) (Inherited t)
chInh
chSem :: g (PreservingSemantics t f) (PreservingSemantics t f)
chSem = f (g (PreservingSemantics t f) (PreservingSemantics t f))
-> g (PreservingSemantics t f) (PreservingSemantics t f)
forall a. f a -> a
extract f (g (PreservingSemantics t f) (PreservingSemantics t f))
x
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 #-}
applyDefaultWithAttributes :: (p ~ Transformation.Domain t, q ~ PreservingSemantics t p, x ~ g q q, Rank2.Apply (g q),
Atts (Inherited t) (g q q) ~ Atts (Inherited t) (g (Semantics t) (Semantics t)),
Atts (Synthesized t) (g q q) ~ Atts (Synthesized t) (g (Semantics t) (Semantics t)),
g q (Synthesized t) ~ g (Semantics t) (Synthesized t),
g q (Inherited t) ~ g (Semantics t) (Inherited t),
Attribution t g (PreservingSemantics t p) p)
=> (forall a. p a -> a) -> t -> p (g (PreservingSemantics t p) (PreservingSemantics t p))
-> PreservingSemantics t p (g (PreservingSemantics t p) (PreservingSemantics t p))
applyDefaultWithAttributes :: (forall a. p a -> a)
-> t
-> p (g (PreservingSemantics t p) (PreservingSemantics t p))
-> PreservingSemantics
t p (g (PreservingSemantics t p) (PreservingSemantics t p))
applyDefaultWithAttributes forall a. p a -> a
extract t
t p (g (PreservingSemantics t p) (PreservingSemantics t p))
x = (forall a. p a -> a)
-> Rule t g
-> p (g (PreservingSemantics t p) (PreservingSemantics t p))
-> PreservingSemantics
t p (g (PreservingSemantics t p) (PreservingSemantics t p))
forall t (f :: * -> *) (g :: (* -> *) -> (* -> *) -> *)
(sem :: * -> *).
(sem ~ PreservingSemantics t f, Apply (g sem),
Atts (Inherited t) (g sem sem)
~ Atts (Inherited t) (g (Semantics t) (Semantics t)),
Atts (Synthesized t) (g sem sem)
~ Atts (Synthesized t) (g (Semantics t) (Semantics t)),
g sem (Synthesized t) ~ g (Semantics t) (Synthesized t),
g sem (Inherited t) ~ g (Semantics t) (Inherited t)) =>
(forall a. f a -> a)
-> Rule t g
-> f (g (PreservingSemantics t f) (PreservingSemantics t f))
-> PreservingSemantics
t f (g (PreservingSemantics t f) (PreservingSemantics t f))
knitKeeping forall a. p a -> a
extract (t
-> p (g (PreservingSemantics t p) (PreservingSemantics t 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 (PreservingSemantics t p) (PreservingSemantics t p))
x) p (g (PreservingSemantics t p) (PreservingSemantics t p))
x
{-# INLINE applyDefaultWithAttributes #-}