{-# LANGUAGE GADTs, Rank2Types #-}
-----------------------------------------------------------------------------
-- Copyright 2010, Open Universiteit Nederland. This file is distributed 
-- under the terms of the GNU General Public License. For more information, 
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
module Service.Types 
   ( -- * Services
     Service, makeService, deprecate 
   , serviceDeprecated, serviceFunction
     -- * Types
   , Type(..), TypedValue(..), tuple2, tuple3, tuple4, maybeTp, optionTp
   , errorTp, equal, isSynonym, useSynonym, TypeSynonym, typeSynonym
   , equalM
   ) where

import Common.Library
import Common.Utils (commaList)
import Control.Monad
import Data.Maybe
import Service.ExercisePackage

-----------------------------------------------------------------------------
-- Services

data Service = Service 
   { serviceId         :: Id
   , serviceDeprecated :: Bool
   , serviceFunction   :: forall a . TypedValue a
   }
   
instance HasId Service where
   getId = serviceId
   changeId f a = a { serviceId = f (serviceId a) }
   
makeService :: String -> String -> (forall a . TypedValue a) -> Service
makeService s descr f = describe descr (Service (newId s) False f)

deprecate :: Service -> Service
deprecate s = s { serviceDeprecated = True }

equalM :: Monad m => Type a t1 -> Type a t2 -> m (t1 -> t2)
equalM t1 t2 = maybe (fail msg) return (equal t1 t2)
 where msg = "Types not equal: " ++ show t1 ++ " and " ++ show t2

equal :: Type a t1 -> Type a t2 -> Maybe (t1 -> t2)
equal type1 type2 =
   case (type1, type2) of
      (Pair a b,    Pair c d   ) -> equalPairs a b c d
      (a :|: b,     c :|: d    ) -> equalChoice a b c d
      (List a,      List b     ) -> liftM map (equal a b)
      (Rule,        Rule       ) -> Just id
      (Unit,        Unit       ) -> Just id
      (StrategyCfg, StrategyCfg) -> Just id
      (Location,    Location   ) -> Just id
      (Id,          Id         ) -> Just id
      (Term,        Term       ) -> Just id
      (ExercisePkg, ExercisePkg) -> Just id
      (Context,     Context    ) -> Just id
      (Bool,        Bool       ) -> Just id
      (String,      String     ) -> Just id
      (Int,         Int        ) -> Just id
      (Iso _ f a,   _          ) -> fmap (. f) (equal a type2)
      (_,           Iso f _ b  ) -> fmap (f .) (equal type1 b)
      (Tag s1 a,    Tag s2 b   ) -> guard (s1==s2) >> equal a b
      _                          -> Nothing
 where
   equalPairs a b c d = 
      liftM2 (\f g (x, y) -> (f x, g y)) (equal a c) (equal b d)
   
   equalChoice a b c d =
      liftM2 (\f g -> either (Left . f) (Right . g)) (equal a c) (equal b d)

infixr 5 :|:

-----------------------------------------------------------------------------
-- Types

infix  2 :::
infixr 3 :->

data TypedValue a = forall t . t ::: Type a t

tuple2 :: Type a t1 -> Type a t2 -> Type a (t1, t2)
tuple2 = Pair

tuple3 :: Type a t1 -> Type a t2 -> Type a t3 -> Type a (t1, t2, t3)
tuple3 t1 t2 t3 = Iso f g (Pair t1 (Pair t2 t3)) 
 where
   f (a, (b, c)) = (a, b, c)
   g (a, b, c)   = (a, (b, c))
   
tuple4 :: Type a t1 -> Type a t2 -> Type a t3 -> Type a t4 -> Type a (t1, t2, t3, t4)
tuple4 t1 t2 t3 t4 = Iso f g (Pair t1 (Pair t2 (Pair t3 t4))) 
 where
   f (a, (b, (c, d))) = (a, b, c, d)
   g (a, b, c, d)     = (a, (b, (c, d)))

maybeTp :: Type a t1 -> Type a (Maybe t1)
maybeTp t = Iso f g (t :|: Unit)
 where
   f = either Just (const Nothing)
   g = maybe (Right ()) Left

optionTp :: t1 -> Type a t1 -> Type a t1
optionTp a t = Iso (fromMaybe a) Just (maybeTp t)

errorTp :: Type a t -> Type a (Either String t)
errorTp t = Iso f g (t :|: IO Unit)
 where
   f = either Right (const (Left "errorTp"))
   g = either (Right . fail) Left

data Type a t where
   -- Type isomorphisms (for defining type synonyms)
   Iso          :: (t1 -> t2) -> (t2 -> t1) -> Type a t1 -> Type a t2
   -- Function type
   (:->)        :: Type a t1 -> Type a t2 -> Type a (t1 -> t2)
   -- Special annotations
   Tag          :: String -> Type a t1 -> Type a t1
   -- Type constructors
   List         :: Type a t -> Type a [t]
   Pair         :: Type a t1 -> Type a t2 -> Type a (t1, t2)
   (:|:)        :: Type a t1 -> Type a t2 -> Type a (Either t1 t2)
   Unit         :: Type a ()
   IO           :: Type a t -> Type a (IO t)
   -- Exercise-specific types
   ExercisePkg  :: Type a (ExercisePackage a)
   Strategy     :: Type a (Strategy (Context a))
   Rule         :: Type a (Rule (Context a))
   Term         :: Type a a
   Context      :: Type a (Context a)
   Location     :: Type a Location
   Id           :: Type a Id
   StrategyCfg  :: Type a StrategyConfiguration
   -- Basic types
   Bool         :: Type a Bool
   Int          :: Type a Int
   String       :: Type a String

instance Show (Type a t) where
   show (Iso _ _ t)    = show t
   show (t1 :-> t2)    = show t1 ++ " -> " ++ show t2 
   show t@(Pair _ _)   = showTuple t
   show (t1 :|: t2)    = show t1 ++ " | " ++ show t2
   show (Tag s _)      = s -- ++ "@(" ++ show t ++ ")"
   show (List t)       = "[" ++ show t ++ "]"
   show (IO t)         = show t
   show t              = fromMaybe "unknown" (groundType t)
   
showTuple :: Type a t -> String
showTuple tp = "(" ++ commaList (collect tp) ++ ")"
 where
   collect :: Type a t -> [String]
   collect (Pair t1 t2) = collect t1 ++ collect t2
   collect (Iso _ _ t)  = collect t
   collect t            = [show t]
   
groundType :: Type a t -> Maybe String
groundType tp =
   case tp of 
      ExercisePkg  -> Just "ExercisePkg"
      Strategy     -> Just "Strategy"
      Rule         -> Just "Rule"
      Term         -> Just "Term"
      Context      -> Just "Context"
      Unit         -> Just "()"
      Bool         -> Just "Bool"
      Int          -> Just "Int"
      String       -> Just "String"
      Location     -> Just "Location"
      Id           -> Just "Id"
      StrategyCfg  -> Just "StrategyConfiguration"
      _            -> Nothing
      
-----------------------------------------------------------------------------
-- Type Synonyms

data TypeSynonym a t = TS 
   { synonymName :: String 
   , useSynonym  :: Type a t
   , isSynonym   :: Monad m => TypedValue a -> m t
   }
   
typeSynonym :: String -> (t2 -> t) -> (t -> t2) -> Type a t2 -> TypeSynonym a t
typeSynonym name to from tp = TS
   { synonymName = name
   , useSynonym  = Tag name (Iso to from tp)
   , isSynonym   = maybe (fail name) return . matchSynonym
   }
 where
   matchSynonym (a ::: t0) = do
      (s, t) <- isTag t0
      guard (s == name)
      f <- equal t tp
      return (to (f a))

isTag :: Type a t -> Maybe (String, Type a t)
isTag (Tag s t) = Just (s, t)
isTag _         = Nothing