{-# Language FlexibleContexts, FlexibleInstances, GADTs, GeneralizedNewtypeDeriving, ImpredicativeTypes,
             MultiParamTypeClasses, NamedFieldPuns, RankNTypes, ScopedTypeVariables, StandaloneDeriving,
             TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}

-- | An attribute grammar is a particular kind of 'Transformation' that assigns attributes to nodes in a
-- tree. Different node types may have different types of attributes, so the transformation is not natural. All
-- attributes are divided into 'Inherited' and 'Synthesized' attributes.

module Transformation.AG where

import Data.Kind (Type)
import Unsafe.Coerce (unsafeCoerce)

import qualified Rank2
import Transformation (Transformation, Codomain)
import Transformation.Deep (Const2)
import qualified Transformation
import qualified Transformation.Deep as Deep
import qualified Transformation.Full as Full

-- | Type family that maps a node type to the type of its attributes, indexed per type constructor.
type family Atts (f :: Type -> Type) (g :: (Type -> Type) -> (Type -> Type) -> Type)

-- | Type family that lops off the two type parameters
type family NodeConstructor (a :: Type) :: (Type -> Type) -> (Type -> Type) -> Type where
   NodeConstructor (g p q) = g
   NodeConstructor t = Const2 t

-- | Type constructor wrapping the inherited attributes for the given transformation.
newtype Inherited t a = Inherited{forall t a. Inherited t a -> Atts (Inherited t) (NodeConstructor a)
inh :: Atts (Inherited t) (NodeConstructor a)}
-- | Type constructor wrapping the synthesized attributes for the given transformation.
newtype Synthesized t a = Synthesized{forall t a.
Synthesized t a -> Atts (Synthesized t) (NodeConstructor a)
syn :: Atts (Synthesized t) (NodeConstructor a)}

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

mapInherited :: (Atts (Inherited t) (NodeConstructor a) -> Atts (Inherited t) (NodeConstructor b))
             -> Inherited t a -> Inherited t b
mapInherited :: forall t a b.
(Atts (Inherited t) (NodeConstructor a)
 -> Atts (Inherited t) (NodeConstructor b))
-> Inherited t a -> Inherited t b
mapInherited Atts (Inherited t) (NodeConstructor a)
-> Atts (Inherited t) (NodeConstructor b)
f (Inherited Atts (Inherited t) (NodeConstructor a)
a) = Atts (Inherited t) (NodeConstructor b) -> Inherited t b
forall t a. Atts (Inherited t) (NodeConstructor a) -> Inherited t a
Inherited (Atts (Inherited t) (NodeConstructor a)
-> Atts (Inherited t) (NodeConstructor b)
f Atts (Inherited t) (NodeConstructor a)
a)

mapSynthesized :: (Atts (Synthesized t) (NodeConstructor a) -> Atts (Synthesized t) (NodeConstructor b))
               -> Synthesized t a -> Synthesized t b
mapSynthesized :: forall t a b.
(Atts (Synthesized t) (NodeConstructor a)
 -> Atts (Synthesized t) (NodeConstructor b))
-> Synthesized t a -> Synthesized t b
mapSynthesized Atts (Synthesized t) (NodeConstructor a)
-> Atts (Synthesized t) (NodeConstructor b)
f (Synthesized Atts (Synthesized t) (NodeConstructor a)
a) = Atts (Synthesized t) (NodeConstructor b) -> Synthesized t b
forall t a.
Atts (Synthesized t) (NodeConstructor a) -> Synthesized t a
Synthesized (Atts (Synthesized t) (NodeConstructor a)
-> Atts (Synthesized t) (NodeConstructor b)
f Atts (Synthesized t) (NodeConstructor a)
a)

-- | A node's 'Semantics' is a natural tranformation from the node's inherited attributes to its synthesized
-- attributes.
type Semantics t = Inherited t Rank2.~> Synthesized t

-- | The core type class for defining the attribute grammar. The instances of this class typically have a form like
--
-- > instance Attribution MyAttGrammar MyNode Identity where
-- >   attribution MyAttGrammar{} (Identity MyNode{})
-- >               (Inherited   fromParent,
-- >                Synthesized MyNode{firstChild= fromFirstChild, ...})
-- >             = (Synthesized _forMyself,
-- >                Inherited   MyNode{firstChild= _forFirstChild, ...})
--
-- If you prefer to separate the calculation of different attributes, you can split the above instance into two
-- instances of the 'Transformation.AG.Generics.Bequether' and 'Transformation.AG.Generics.Synthesizer' classes
-- instead. If you derive 'GHC.Generics.Generic' instances for your attributes, you can even define each synthesized
-- attribute individually with a 'Transformation.AG.Generics.SynthesizedField' instance.
class Attribution t where
   type Origin t :: Type -> Type
   -- | Unwrap the value from the original attribution domain
   unwrap :: t -> Origin t x -> x

class Attribution t => At t g where
   -- | The attribution rule for a given transformation and node.
   attribution :: forall sem. Rank2.Traversable (g sem)
               => t -> Origin t (g sem sem)
               -> (Inherited   t (g sem sem), g sem (Synthesized t))
               -> (Synthesized t (g sem sem), g sem (Inherited t))

newtype Knit t = Knit t

instance Attribution t => Transformation (Knit t) where
   type Domain (Knit t) = Origin t
   type Codomain (Knit t) = Semantics t

instance (t `At` g, Rank2.Apply (g sem), Rank2.Traversable (g sem), sem ~ Semantics t) =>
         Knit t `Transformation.At` g sem sem where
   Knit t
t $ :: Knit t
-> Domain (Knit t) (g sem sem) -> Codomain (Knit t) (g sem sem)
$ Domain (Knit t) (g sem sem)
x = Rule t g
-> g (Codomain (Knit t)) (Codomain (Knit t))
-> Codomain (Knit t) (g (Codomain (Knit t)) (Codomain (Knit t)))
forall (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *) t.
(Apply (g sem), sem ~ Semantics t) =>
Rule t g -> g sem sem -> sem (g sem sem)
knit (t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall t (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *).
(At t g, Traversable (g sem)) =>
t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall (sem :: * -> *).
Traversable (g sem) =>
t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
attribution t
t Domain (Knit t) (g sem sem)
Origin t (g sem sem)
x) (t
-> Origin t (g (Codomain (Knit t)) (Codomain (Knit t)))
-> g (Codomain (Knit t)) (Codomain (Knit t))
forall x. t -> Origin t x -> x
forall t x. Attribution t => t -> Origin t x -> x
unwrap t
t Domain (Knit t) (g sem sem)
Origin t (g (Codomain (Knit t)) (Codomain (Knit t)))
x)

instance (t `At` g, Rank2.Apply (g (Semantics t)), Rank2.Traversable (g (Semantics t)),
          Functor (Origin t), Rank2.Functor (g (Origin t)), Deep.Functor (Knit t) g) =>
         Full.Functor (Knit t) g where
   <$> :: Knit t
-> Domain (Knit t) (g (Domain (Knit t)) (Domain (Knit t)))
-> Codomain (Knit t) (g (Codomain (Knit t)) (Codomain (Knit t)))
(<$>) = Knit t
-> Domain (Knit t) (g (Domain (Knit t)) (Domain (Knit t)))
-> Codomain (Knit t) (g (Codomain (Knit t)) (Codomain (Knit t)))
forall t (g :: (* -> *) -> (* -> *) -> *).
(Functor t g, At t (g (Codomain t) (Codomain t)),
 Functor (Domain t)) =>
t
-> Domain t (g (Domain t) (Domain t))
-> Codomain t (g (Codomain t) (Codomain t))
Full.mapUpDefault

-- | Transformation wrapper that keeps all the original tree nodes alongside their attributes
newtype Keep t = Keep t deriving ((forall x. Keep t -> Origin (Keep t) x -> x)
-> Attribution (Keep t)
forall x. Keep t -> Origin (Keep t) x -> x
forall t x. Attribution t => Keep t -> Origin (Keep t) x -> x
forall t. (forall x. t -> Origin t x -> x) -> Attribution t
$cunwrap :: forall t x. Attribution t => Keep t -> Origin (Keep t) x -> x
unwrap :: forall x. Keep t -> Origin (Keep t) x -> x
Attribution)

data Kept t a = Kept{forall t a. Kept t a -> Atts (Inherited t) (NodeConstructor a)
inherited   :: Atts (Inherited t) (NodeConstructor a),
                     forall t a. Kept t a -> Atts (Synthesized t) (NodeConstructor a)
synthesized :: Atts (Synthesized t) (NodeConstructor a),
                     forall t a. Kept t a -> Origin t a
original    :: Origin t a}

deriving instance (Show (Atts (Inherited t) (NodeConstructor a)),
                   Show (Atts (Synthesized t) (NodeConstructor a)),
                   Show (Origin t a)) => Show (Kept t a)

type instance Atts (Inherited (Keep t)) g = Atts (Inherited t) g
type instance Atts (Synthesized (Keep t)) g = Kept t (g (Kept t) (Kept t))

instance (Rank2.Functor (g (Semantics (Keep t))), Functor (Origin t), t `At` g) => Keep t `At` g where
   attribution :: forall (sem :: * -> *).
Traversable (g sem) =>
Keep t
-> Origin (Keep t) (g sem sem)
-> (Inherited (Keep t) (g sem sem), g sem (Synthesized (Keep t)))
-> (Synthesized (Keep t) (g sem sem), g sem (Inherited (Keep t)))
attribution (Keep t
t) Origin (Keep t) (g sem sem)
x (Inherited Atts (Inherited (Keep t)) (NodeConstructor (g sem sem))
i, g sem (Synthesized (Keep t))
childSynthesis) = (Atts (Synthesized (Keep t)) (NodeConstructor (g sem sem))
-> Synthesized (Keep t) (g sem sem)
forall t a.
Atts (Synthesized t) (NodeConstructor a) -> Synthesized t a
Synthesized Atts (Synthesized (Keep t)) g
Atts (Synthesized (Keep t)) (NodeConstructor (g sem sem))
synthesis', g sem (Inherited (Keep t))
forall (sem :: * -> *). g sem (Inherited (Keep t))
childInheritance') where
      (Synthesized Atts (Synthesized t) (NodeConstructor (g sem sem))
s, g sem (Inherited t)
childInheritance) = t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall t (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *).
(At t g, Traversable (g sem)) =>
t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
forall (sem :: * -> *).
Traversable (g sem) =>
t
-> Origin t (g sem sem)
-> (Inherited t (g sem sem), g sem (Synthesized t))
-> (Synthesized t (g sem sem), g sem (Inherited t))
attribution t
t Origin t (g sem sem)
Origin (Keep t) (g sem sem)
x (Atts (Inherited t) (NodeConstructor (g sem sem))
-> Inherited t (g sem sem)
forall t a. Atts (Inherited t) (NodeConstructor a) -> Inherited t a
Inherited Atts (Inherited t) (NodeConstructor (g sem sem))
Atts (Inherited (Keep t)) (NodeConstructor (g sem sem))
i :: Inherited t (g sem sem),
                                                           Synthesized (Keep t) a -> Synthesized t a
forall a. Synthesized (Keep t) a -> Synthesized t a
resynthesize (forall a. Synthesized (Keep t) a -> Synthesized t a)
-> g sem (Synthesized (Keep t)) -> g sem (Synthesized t)
forall {k} (g :: (k -> *) -> *) (p :: k -> *) (q :: k -> *).
Functor g =>
(forall (a :: k). p a -> q a) -> g p -> g q
forall (p :: * -> *) (q :: * -> *).
(forall a. p a -> q a) -> g sem p -> g sem q
Rank2.<$> g sem (Synthesized (Keep t))
childSynthesis)
      resynthesize :: forall a. Synthesized (Keep t) a -> Synthesized t a
      resynthesize :: forall a. Synthesized (Keep t) a -> Synthesized t a
resynthesize (Synthesized Kept{Atts
  (Synthesized t)
  (NodeConstructor (NodeConstructor a (Kept t) (Kept t)))
synthesized :: forall t a. Kept t a -> Atts (Synthesized t) (NodeConstructor a)
synthesized :: Atts
  (Synthesized t)
  (NodeConstructor (NodeConstructor a (Kept t) (Kept t)))
synthesized}) = Atts (Synthesized t) (NodeConstructor a) -> Synthesized t a
forall t a.
Atts (Synthesized t) (NodeConstructor a) -> Synthesized t a
Synthesized Atts (Synthesized t) (NodeConstructor a)
Atts
  (Synthesized t)
  (NodeConstructor (NodeConstructor a (Kept t) (Kept t)))
synthesized
      synthesis' :: Atts (Synthesized (Keep t)) g
      synthesis' :: Atts (Synthesized (Keep t)) g
synthesis' = Atts (Inherited t) (NodeConstructor (g (Kept t) (Kept t)))
-> Atts (Synthesized t) (NodeConstructor (g (Kept t) (Kept t)))
-> Origin t (g (Kept t) (Kept t))
-> Kept t (g (Kept t) (Kept t))
forall t a.
Atts (Inherited t) (NodeConstructor a)
-> Atts (Synthesized t) (NodeConstructor a)
-> Origin t a
-> Kept t a
Kept Atts (Inherited t) (NodeConstructor (g (Kept t) (Kept t)))
Atts (Inherited (Keep t)) (NodeConstructor (g sem sem))
i Atts (Synthesized t) (NodeConstructor (g sem sem))
Atts (Synthesized t) (NodeConstructor (g (Kept t) (Kept t)))
s ((forall a b. a -> b
unsafeCoerce @(g _ (Synthesized (Keep t))) g sem (Synthesized (Keep t))
childSynthesis :: g (Kept t) (Kept t)) g (Kept t) (Kept t)
-> Origin (Keep t) (g sem sem)
-> Origin (Keep t) (g (Kept t) (Kept t))
forall a b. a -> Origin (Keep t) b -> Origin (Keep t) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Origin (Keep t) (g sem sem)
x)
      childInheritance' :: g sem (Inherited (Keep t))
      childInheritance' :: forall (sem :: * -> *). g sem (Inherited (Keep t))
childInheritance' = forall a b. a -> b
unsafeCoerce @(g _ (Inherited t)) g sem (Inherited t)
childInheritance

-- | An attribution rule maps a node's inherited attributes and its child nodes' synthesized attributes to the node's
-- synthesized attributes and the children nodes' inherited attributes.
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))

-- | The core function to tie the recursive knot, turning a 'Rule' for a node into its 'Semantics'.
knit :: (Rank2.Apply (g sem), sem ~ Semantics t) => Rule t g -> g sem sem -> sem (g sem sem)
knit :: forall (g :: (* -> *) -> (* -> *) -> *) (sem :: * -> *) t.
(Apply (g sem), sem ~ Semantics t) =>
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
forall (p :: * -> *) (q :: * -> *).
g sem (p ~> q) -> g sem p -> g sem q
Rank2.<*> g sem (Inherited t)
chInh