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

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

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

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

             ) where
 
import Prelude hiding (lookup)


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


data Unit s         = Unit

lookupEnv  :: Ref a env -> Env t s env -> t a s
lookupEnv  Zero     (Ext _ t)   =  t
lookupEnv  (Suc r)  (Ext ts _)  =  lookupEnv r ts
lookupEnv  _        _           =  error "Error: The impossible happened!"

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
updateEnv  _  _        _ 
              =  error "Error: The impossible happened!"


-- | 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 '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 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}