{-# OPTIONS -XKindSignatures -XRankNTypes -XArrows -XGADTs  #-}


{-| 
    Library for Typed Transformations of Typed Abstract Syntax.

    The library is documented in the paper: /Typed Transformations of Typed Abstract Syntax/

    Bibtex entry: <http://www.cs.uu.nl/wiki/bin/viewfile/Center/TTTAS?rev=1;filename=TTTAS.bib>

    For more documentation see the TTTAS webpage: 
    <http://www.cs.uu.nl/wiki/bin/view/Center/TTTAS>.

    For an example see examples/CSE1.hs 

-}

module Language.AbstractSyntax.TTTAS (
               -- * Typed References and Environments
               module Language.AbstractSyntax.TTTAS.Common,
               

               -- * Transformation Library
               
               -- ** Trafo
               Trafo(..), TrafoE(..),

               -- ** Create New References
               newSRef, extEnv, castSRef, updateSRef,

               -- ** State-like operations on the Final Environment               
               getFinalEnv, putFinalEnv, updateFinalEnv,
 
               -- ** Run a Trafo
               runTrafo,

               -- ** Other Combinators
              sequenceA,


             ) where
 

#if __GLASGOW_HASKELL__ >= 710
import Prelude hiding (lookup,(.), id, sequenceA) 
#else
import Prelude hiding (lookup,(.), id) 
#endif

import Unsafe.Coerce ( unsafeCoerce )
import Control.Category
import Control.Arrow 
import Language.AbstractSyntax.TTTAS.Common



-- | The type 'Trafo' is the type of the transformation steps on a heterogeneous collection.
--   The argument @m@ stands for the type of the meta-data.  
--   A |Trafo| takes the meta-data on the current environment |env1| as input and 
--   yields  meta-data for the (possibly extended) environment |env2|.
--   The type @t@ is the type of the terms stored in the environment.
--   The type variable @s@ represents the type of the final result, which we do expose. 
--   Its role is similar to the @s@ in the type @ST s a@.
--   The arguments @a@ and @b@ are the Arrow's input and output, respectively.




data  Trafo  m t s a b =  
  Trafo (forall env1 . m env1 -> TrafoE m t s env1 a b)

-- | The type 'TrafoE' is used to introduce an existential quantifier into
--   the definition of 'Trafo'.  
--   It can be seen that a 'Trafo' is a function taking as arguments: the input (@a@),
--   a 'Ref'-transformer (@T env2 s@) from the environment constructed in this step 
--   to the final environment, the environment (@Env t s env1@) where the current 
--   transformation starts and the "final environment" (@FinalEnv t s@) 
--   with the updates thus far applied. 
--   The function returns: the output (@b@), 
--   a 'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final 
--   environment, the environment (@Env t s env2@) constructed in this step and the final environment
--   (@FinalEnv t s@) possibly updated.
data  TrafoE m t s env1 a b = 
 forall env2 . TrafoE   (  m env2)
                        (       a  ->  T env2 s ->  Env t s env1 ->  FinalEnv t s
                          -> (  b,     T env1 s,    Env t s env2,    FinalEnv t s)
                        )



-- |  The Trafo 'newSRef' takes a typed term as input, adds it to the environment 
--    and yields a reference pointing to this value.
--    No meta-information on the environment is recorded by 'newSRef';
--    therefore we use the type 'Unit' for the meta-data.  
newSRef :: Trafo Unit t s (t a s) (Ref a s)
newSRef 
 =  Trafo  (\ _->  extEnv Unit)



-- | Change the final environment by the one passed in the input.
putFinalEnv ::  Trafo m t s (FinalEnv t s) ()
putFinalEnv = Trafo $ \m -> (TrafoE m (\fe t e _ -> ((), t, e, fe)))

-- | Return as output the final environment.
getFinalEnv ::  Trafo m t s () (FinalEnv t s)
getFinalEnv = Trafo $ \m -> (TrafoE m (\_ t e fe -> (fe, t, e, fe)))

-- | The function 'updateFinalEnv' returns a 'Trafo' that updates the
--   final environment using the input function 
--   (@FinalEnv t s -> FinalEnv t s@).
updateFinalEnv ::  Trafo m t s (FinalEnv t s -> FinalEnv t s) ()
updateFinalEnv = proc f ->
                  do fe  <- getFinalEnv -< ()
                     putFinalEnv -< f fe
 -- Trafo $ \m -> (TrafoE m (\f t e fe -> ((), t, e, f fe)))


-- | The function 'extEnv' returns a 'TrafoE' that extends the current environment.
extEnv :: m (e,a) -> TrafoE m t s e (t a s) (Ref a s)
extEnv m = TrafoE m $ \ta  (T tr) env  fe ->  (tr Zero,  T (tr . Suc),  Ext env ta, fe )

-- | The function 'castSRef'  returns a 'TrafoE' that casts the reference 
--   passed as parameter (in the constructed environment) to one in the final environment.
castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s)
castSRef m r = TrafoE m $ (\   _ (T t) decls fe ->  (t r, T t, decls, fe))

-- | The function 'updateSRef' returns a 'TrafoE' that updates the value pointed
--   by the reference passed as parameter into the current environment.
updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s)
updateSRef m r f = TrafoE m $ \i (T t) decls fs -> (t r, T t, updateEnv (f i) r decls, fs)


instance Functor (TrafoE m t s e a) where
 fmap f (TrafoE m step) = TrafoE m $ \i t e fe -> case step i t e fe of
                                                  (i',t',e',fe') -> (f i',t',e',fe')



-- | The function 'runTrafo' takes as arguments the 'Trafo' we want to run, meta-information 
--   for the empty environment, and an input value. 
--   The result of 'runTrafo' (type 'Result') is the final environment (@Env t s s@) together 
--   with the resulting meta-data (@m s@), and the output value (@b s@). 
--   The rank-2 type for 'runTrafo' ensures that transformation steps cannot make 
--   any assumptions about the type of final environment (@s@).
runTrafo   ::  (forall s . Trafo m t s a (b s)) ->  m () -> a 
           ->  Result m t b
runTrafo trafo m a = case trafo of
  Trafo trf -> case trf m of
                   TrafoE m2 f ->
                     let (rb, _, env2, fenv) =  f a (T unsafeCoerce) Empty (unsafeCoerce env2) 
                     in  Result  (unsafeCoerce m2)  
                                 rb 
                                 (unsafeCoerce fenv) 



instance Category (Trafo m t s) where
 -- |(.) :: Trafo m t s b c  ->  Trafo m t s a b ->  Trafo m t s a c|
 Trafo t2 . Trafo t1 = 
  Trafo 
  (\m1 -> case t1 m1 of
                                      TrafoE m2 f1 -> case t2 m2 of
                                       TrafoE m3 f2 ->
                                        TrafoE 
                                        m3 
                                        (\a  tt env1 fs ->
                                             let  (b,tt1, env2, fs')   = f1 a tt2 env1 fs
                                                  (c,tt2, env3, fs'')  = f2 b tt env2 fs'
                                             in   (c,tt1, env3, fs'')                                                                    
                                        )
  )

 -- |id :: Trafo m t s a a|
 id =  Trafo  (\m -> TrafoE m (\a t e f -> (a, t, e, f)) )

instance Arrow (Trafo m t s) where

 -- |arr :: (a  -> b) -> Trafo m t s a b|
 arr f =  Trafo  (\m -> TrafoE m (\a t e fs -> (f a, t, e, fs)) )


 -- |first :: Trafo m t s a b -> Trafo m t s (a, c) (b, c)|
 first (Trafo tr) 
  = Trafo (\m1 -> case tr m1 of
        TrafoE m2 f -> 
           TrafoE  
           m2 
           (\  ~(a,c) tt env1 fs -> 
               let (b,tt1,env2, fs') = f a tt env1 fs
               in  ((b,c),tt1, env2, fs'))) 


instance ArrowLoop (Trafo m t s) where
 -- |loop :: Trafo m t s (a, x) (b, x) -> Trafo m t s a b|
 loop (Trafo st) =
   Trafo 
   (\m -> case st m of
           TrafoE m1 f1 ->
            TrafoE  m1
            (\a t e f -> 
              let ((b, x),t1,e1,f') = f1 (a, x) t e f                                                                            
              in (b,t1,e1,f')
            ))



-- | The combinator 'sequenceA' sequentially composes a list
--   of 'Trafo's into a 'Trafo' that yields a list of outputs.
--   Its use is analogous to the combinator 'sequence' combinator
--   for 'Monad's.
sequenceA :: [Trafo m t s a b] -> Trafo m t s a [b]
sequenceA [] = arr (const [])
sequenceA (x:xs) 
     = proc a ->
        do b  <- x -< a
           bs <- sequenceA xs -< a
           returnA -< (b:bs)