{-# OPTIONS -fglasgow-exts -farrows #-}

{-| 
    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>.
-}

module TTTAS (
               -- * Typed References and Environments

               -- ** Typed References
               Ref(..), Equal(..), 
               match, lookup, update,

               -- ** Declarations
               Env(..), FinalEnv, T(..),
               lookupEnv, updateEnv,

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

               -- ** Create New References
               Unit(..),
               newSRef, extEnv, castSRef, updateSRef,
 
               -- ** Run a Trafo
               Result(..), 
               runTrafo,

               -- ** Other Combinators
               sequenceA,

               -- * Alternative Transformation Library
               
               -- ** Trafo2
               Trafo2(..), TrafoE2(..),

               -- ** Create New References
               newSRef2,

               -- ** Run a Trafo2 
               runTrafo2,

               -- ** Arrow-style Combinators
               Pair(..), Arrow2(..), ArrowLoop2(..),
               List(..), sequenceA2
             ) where
 
import Unsafe.Coerce ( unsafeCoerce )
import Prelude hiding (lookup)
import Control.Arrow
 

-- | The 'Ref' type for represents typed indices which are
--   labeled with both the type of value to which they
--   refer and the type of the environment (a nested
--   Cartesian product, growing to the right) in which 
--   this value lives.
 --  The constructor 'Zero' expresses that the first
 --   element of the environment has to be of type @a@.
 --  The constructor 'Suc' does not care about the type
 --   of the first element in the environment, 
 --   being polymorphic in the type @b@.
data Ref a env where
 Zero  ::                      Ref a (env',a)
 Suc   ::  Ref a      env' ->  Ref a (env',b)

-- | The 'Equal' type encodes type equality. 
data Equal :: * -> * -> * where 
 Eq :: Equal a a

-- | The function 'match' compares two references for equality.
--   If they refer to the same element in the environment
--   the value @Just Eq@ is returned, expressing the fact that
--   the types of the referred values are the same too.
match :: Ref a env -> Ref b env -> Maybe (Equal a b)
match  Zero     Zero        =  Just Eq
match  (Suc x)  (Suc y)     =  match x y
match  _        _           =  Nothing

-- | The function 'lookup' returns the element indexed in the
--   environment parameter by the 'Ref' parameter. The types
--   guarantee that the lookup succeeds.
lookup :: Ref a env -> env -> a
lookup  Zero     (_,a)  =  a
lookup  (Suc r)  (e,_)  =  lookup r e

-- | The function 'update' takes an additional function as
--   argument, which is used to update the value the 
--   reference addresses.
update :: (a -> a) -> Ref a env -> env -> env  
update f  Zero     (e,a)   =  (e,f a)
update f  (Suc r)  (e,x)   =  (update f r e,x)


-- | The type @Env term use def@ represents a sequence of
--   instantiations of type @forall a. term a use@, where
--   all the instances of @a@ are stored in the type parameter
--   @def@. The type @use@ is a sequence containing the 
--   types to which may be referred from within terms of type
--   @term a use@. 
data Env term use def where
  Empty  ::  Env t use  ()
  Ext    ::  Env t use def' ->  t a use  
         ->  Env t use  (def',a)


lookupEnv  :: Ref a env -> Env t s env -> t a s
lookupEnv  Zero     (Ext _ t)   =  t
lookupEnv  (Suc r)  (Ext ts _)  =  lookupEnv r ts

updateEnv  ::  (t a s -> t a s) -> Ref a env 
           ->  Env t s env ->  Env t s env
updateEnv  f  Zero     (Ext ts t)  
              =        Ext ts (f t) 
updateEnv  f  (Suc r)  (Ext ts t)  
              =        Ext (updateEnv f r ts)  t

-- | When the types @def@ and @use@ of an 'Env' coincide,
--   we can be sure that the references in the terms do not
--   point to values outside the environment but point
--   to terms representing the right type. This kind of
--   environment is the /final environment/ of a transformation.
type FinalEnv t usedef = Env t usedef usedef
 
-- | The type 'T' encodes a 'Ref'-transformer. It is usually used
--   to transform references from an actual environment to 
--   the final one.
newtype T e s  = T {unT :: forall x . Ref x e -> Ref x s}

-- | 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 a b env1)

-- | 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 and the environment (@Env t s env1@) where the 
--   current transformation starts. The function returns: the output (@b@), a 
--   'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final 
--   environment and the environment (@Env t s env2@) constructed in this step.
data  TrafoE m t s a b env1 = 
 forall env2 . TrafoE   (  m env2)
                        (       a  ->  T env2 s ->  Env t s env1
                          -> (  b,     T env1 s,    Env t s env2)
                        )

data Unit s         = Unit

-- |  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)


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

-- | 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 x (Ref a s) e
castSRef m r = TrafoE m $ (\   _ (T t) decls  ->  (t r, T t, decls))

-- | 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 i (Ref a s) e
updateSRef m r f = TrafoE m $ \i (T t) decls -> (t r, T t, updateEnv (f i) r decls)


-- | The type 'Result' is the type of the result of \"running\" a 'Trafo'. 
--   Because @s@ could be anything we have to hide it using existential quantification.
data Result  m t b   
   =  forall s . Result  (m s) (b s) (FinalEnv t s)

-- | 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 -> 
                     case  f a (T unsafeCoerce) Empty of
                       (rb, _, env2) -> 
                         Result  (unsafeCoerce m2)  
                                 rb 
                                 (unsafeCoerce env2) 


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 -> (f a, t, e)) )

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

 -- |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 -> 
               let (b,tt1,env2) = f a tt env1
               in  ((b,c),tt1, env2))) 

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 -> 
              let ((b, x),t1,e1) = f1 ( (a, x)) t e                                                                            
              in (b,t1,e1)
            ))

-- | 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)  




-- | Alternative version of 'Trafo' where the universal quantification 
--   over |s| is moved inside the quantification over |env2|.
--   Note that the type variables |a| and |b| are now labelled with |s|, 
--   and hence have kind |(* -> *)|.
data  Trafo2  m t a b =  
  Trafo2 (forall env1 . m env1 -> TrafoE2 m t a b env1)
data  TrafoE2 m t a b env1 = 
  forall env2 .  TrafoE2
                 (m env2)
                 (forall s .  a s -> T env2 s -> Env t s env1
                              -> (b s, T env1 s, Env t s env2)
                 )

-- | The function 'runTrafo2' takes as arguments the 'Trafo2' we want to run, meta-information 
--   for the empty environment, and an input value. 
--   The result of 'runTrafo2' (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 'runTrafo2' ensures that transformation steps cannot make 
--   any assumptions about the type of final environment (@s@).
--   It is an alternative version of 'runTrafo' which does not use
--   'unsafeCoerce'.
runTrafo2  ::  Trafo2 m t a b -> m () -> (forall s . a s) 
           ->  Result m t b
runTrafo2 trafo m a = 
 case trafo of
  Trafo2 trf -> case trf m of
                   TrafoE2 m2 f -> 
                      let  (rb, _, env2) =  f a (T id) Empty 
                      in   Result m2  rb env2

-- |  The Trafo2 'newSRef2' 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 'newSRef2';
--    therefore we use the type 'Unit' for the meta-data.  
newSRef2 :: Trafo2 Unit t (t a) (Ref a)
newSRef2 
    =  Trafo2  
       (\Unit ->  TrafoE2  
                  Unit
                  (\ta (T tr) env ->
                      ( tr Zero
                      , T (tr . Suc)
                      , Ext env ta
       )          )   )

newtype Pair a b s = P (a s, b s)

class Arrow2 arr where
  arr2    :: (forall s . a s -> b s) -> arr a b
  (>>>>)  :: arr a b -> arr b c -> arr a c
  first2  :: arr a b -> arr (Pair a c) (Pair b c)
  second2 :: arr a b -> arr (Pair c a) (Pair c b)
  (****)  :: arr a b -> arr a' b'
          -> arr (Pair a a') (Pair b b')
  (&&&&)  :: arr a b -> arr a b' -> arr a (Pair b b')

class Arrow2 arr => ArrowLoop2 arr where
  loop2   :: arr (Pair a c) (Pair b c) -> arr a b


instance Arrow2 (Trafo2 m t) where
  arr2 f 
    =  Trafo2  (\m -> TrafoE2 m (\a t e -> (f a, t, e)) )

  (>>>>) (Trafo2 sa) (Trafo2 sb) = 
    Trafo2 
    (\m1 ->
       case sa m1 of 
        TrafoE2 m2 f1 -> case sb m2 of 
         TrafoE2 m3 f2 -> 
           TrafoE2  
           m3 
           (\a t3s e1 -> let  (b, t1s, e2) = f1 a t2s e1
                              (c, t2s, e3) = f2 b t3s e2
                         in   (c, t1s, e3)
           ))
  
  first2 (Trafo2 s) 
    =  Trafo2
       (\m1 -> case s m1 of
          TrafoE2 m2 f -> 
             TrafoE2  m2
                    (\(P (a, c)) t2s e1 -> 
                                      let (b,t12,e2) = f a t2s e1 
                                      in  (P (b, c),t12,e2)
                    )              
       ) 

  second2 f = arr2 swap >>>> first2 f >>>> arr2 swap
              where   swap ~(P (x, y)) = P (y, x)
             
  f **** g =  first2 f >>>> second2 g  
 
  f &&&& g = arr2 (\b -> P (b, b)) >>>> (f **** g)      


instance ArrowLoop2 (Trafo2 m t) where
  loop2 (Trafo2 st) =
    Trafo2 
    (\m -> case st m of
            TrafoE2 m1 f1 ->
             TrafoE2  m1
             (\a t e -> 
               let (P (b, x),t1,e1) = f1 (P (a, x)) t e                                                                            
               in (b,t1,e1)
             ) 
    )


newtype List a s = List [a s]

-- | The combinator 'sequenceA2' sequentially composes a list
--   of 'Trafo2's into a 'Trafo2' that yields a 'List' of outputs.
--   Its use is analogous to the combinator 'sequence' combinator
--   for 'Monad's.
sequenceA2 :: [Trafo2 m t a b] -> Trafo2 m t a (List b)
sequenceA2 [] = arr2 (const (List []))
sequenceA2 (x:xs) 
       =  (x &&&& sequenceA2 xs) >>>> 
          arr2 (\(P (a,List as)) -> List (a:as))