ideas-0.5.8: src/Service/Types.hs
{-# LANGUAGE GADTs, Rank2Types #-}
-----------------------------------------------------------------------------
-- Copyright 2009, 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 where
import Common.Context (Context, Location, fromContext)
import Common.Exercise (Exercise)
import Common.Transformation (Rule, name)
import Common.Utils (commaList)
import Control.Arrow
import Control.Monad
import Data.Maybe
import Service.TypedAbstractService (State, Result)
import System.IO.Unsafe
infix 2 :::
infixr 3 :->
data TypedValue a = forall t . t ::: Type a t
data Type a t where
-- Function type
(:->) :: Type a t1 -> Type a t2 -> Type a (t1 -> t2)
-- Tuple types
Pair :: Type a t1 -> Type a t2 -> Type a (t1, t2)
Triple :: Type a t1 -> Type a t2 -> Type a t3 -> Type a (t1, t2, t3)
Quadruple :: Type a t1 -> Type a t2 -> Type a t3 -> Type a t4 -> Type a (t1, t2, t3, t4)
-- Special annotations
Tag :: String -> Type a t1 -> Type a t1
Optional :: t1 -> Type a t1 -> Type a t1
Maybe :: Type a t1 -> Type a (Maybe t1)
-- Type constructors
List :: Type a t -> Type a [t]
Elem :: Type a t -> Type a t -- quick fix
IO :: Type a t -> Type a (IO t)
-- Exercise-specific types
State :: Type a (State a)
Exercise :: Type a (Exercise a)
Rule :: Type a (Rule (Context a))
Term :: Type a (Context a)
Result :: Type a (Result a)
-- Basic types
Bool :: Type a Bool
Int :: Type a Int
String :: Type a String
Location :: Type a Location
instance Show (Type a t) where
show (t1 :-> t2) = show t1 ++ " -> " ++ show t2
show (Pair t1 t2) = "(" ++ commaList [show t1, show t2] ++ ")"
show (Triple t1 t2 t3) = "(" ++ commaList [show t1, show t2, show t3] ++ ")"
show (Quadruple t1 t2 t3 t4) = "(" ++ commaList [show t1, show t2, show t3, show t4] ++ ")"
show (Tag _ t) = show t
show (Optional _ t) = "(" ++ show t ++ ")?"
show (Maybe t) = "(" ++ show t ++ ")?"
show (List t) = "[" ++ show t ++ "]"
show (Elem t) = show t
show (IO t) = show t
show t = fromMaybe "unknown" (groundType t)
groundType :: Type a t -> Maybe String
groundType tp =
case tp of
State -> Just "State"
Exercise -> Just "Exercise"
Rule -> Just "Rule"
Term -> Just "Term"
Result -> Just "Result"
Bool -> Just "Bool"
Int -> Just "Int"
String -> Just "String"
Location -> Just "Location"
_ -> Nothing
{- eqType :: Type a1 t1 -> Type a2 t2 -> Bool
eqType (t1 :-> t2) (t3 :-> t4) = eqType t1 t3 && eqType t2 t4
eqType (Pair t1 t2) (Pair t3 t4) = eqType t1 t3 && eqType t2 t4
eqType (Triple t1 t2 t3) (Triple t4 t5 t6) = eqType t1 t4 && eqType t2 t5 && eqType t3 t6
eqType (List t1) (List t2) = eqType t1 t2
eqType (Elem t1) (Elem t2) = eqType t1 t2
eqType (IO t1) (IO t2) = eqType t1 t2
eqType t1 t2 = maybe False ((groundType t1 ==) . Just) (groundType t2) -}
data Evaluator m inp out a = Evaluator
{ encoder :: Encoder m out a
, decoder :: Decoder m inp a
}
data Encoder m s a = Encoder
{ encodeType :: forall t . Type a t -> t -> m s
, encodeTerm :: a -> m s
, encodeTuple :: [s] -> s
}
data Decoder m s a = Decoder
{ decodeType :: forall t . Type a t -> s -> m (t, s)
, decodeTerm :: s -> m a
, decoderExercise :: Exercise a
}
eval :: Monad m => Evaluator m inp out a -> TypedValue a -> inp -> m out
eval f (tv ::: tp) s =
case tp of
t1 :-> t2 -> do
(a, s1) <- decodeType (decoder f) t1 s
eval f (tv a ::: t2) s1
_ ->
encodeType (encoder f) tp tv
decodeDefault :: MonadPlus m => Decoder m s a -> Type a t -> s -> m (t, s)
decodeDefault dec tp s =
case tp of
Pair t1 t2 -> do
(a, s1) <- decodeType dec t1 s
(b, s2) <- decodeType dec t2 s1
return ((a, b), s2)
Triple t1 t2 t3 -> do
(a, s1) <- decodeType dec t1 s
(b, s2) <- decodeType dec t2 s1
(c, s3) <- decodeType dec t3 s2
return ((a, b, c), s3)
Quadruple t1 t2 t3 t4 -> do
(a, s1) <- decodeType dec t1 s
(b, s2) <- decodeType dec t2 s1
(c, s3) <- decodeType dec t3 s2
(d, s4) <- decodeType dec t4 s3
return ((a, b, c, d), s4)
Tag _ t1 ->
decodeType dec t1 s
Optional a t1 ->
decodeType dec t1 s `mplus` return (a, s)
Maybe t1 ->
liftM (first Just) (decodeType dec t1 s) `mplus` return (Nothing, s)
_ ->
fail $ "No support for argument type: " ++ show tp
encodeDefault :: Monad m => Encoder m s a -> Type a t -> t -> m s
encodeDefault enc tp tv =
case tp of
Pair t1 t2 -> do
let (a, b) = tv
x <- encodeType enc t1 a
y <- encodeType enc t2 b
return (encodeTuple enc [x, y])
Triple t1 t2 t3 -> do
let (a, b, c) = tv
x <- encodeType enc t1 a
y <- encodeType enc t2 b
z <- encodeType enc t3 c
return (encodeTuple enc [x, y, z])
Quadruple t1 t2 t3 t4 -> do
let (a, b, c, d) = tv
x <- encodeType enc t1 a
y <- encodeType enc t2 b
z <- encodeType enc t3 c
u <- encodeType enc t4 d
return (encodeTuple enc [x, y, z, u])
Tag _ t1 -> encodeType enc t1 tv
Elem t1 -> encodeType enc t1 tv
Optional _ t1 -> encodeType enc t1 tv
Maybe t1 -> case tv of
Just a -> encodeType enc t1 a
Nothing -> return (encodeTuple enc [])
IO t1 -> encodeType enc t1 (unsafePerformIO tv)
Rule -> encodeType enc String (name tv)
Term -> encodeTerm enc (fromContext tv)
Location -> encodeType enc String (show tv)
_ -> fail "No support for result type"