{-# LANGUAGE GADTs, RankNTypes, FlexibleInstances, FlexibleContexts #-}

-----------------------------------------------------------------------------

-- Copyright 2018, Ideas project team. This file is distributed under the

-- terms of the Apache License 2.0. For more information, see the files

-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.

-----------------------------------------------------------------------------

-- |

-- Maintainer  :  bastiaan.heeren@ou.nl

-- Stability   :  provisional

-- Portability :  portable (depends on ghc)

--

-----------------------------------------------------------------------------



module Ideas.Service.Types

   ( -- * Services

     Service, makeService, deprecate

   , serviceDeprecated, serviceFunction

     -- * Types

   , TypeRep(..), Const(..), Type, TypedValue(..)

   , Equal(..), ShowF(..), equalM

     -- * Constructing types

   , tEnvironment, tLocation, tRule, tConstraint

   , tUnit, tTuple3, tTuple4, tTuple5, tPair

   , tTerm, tStrategy, tTree, tState, tBool, tMaybe, tString, tList

   , tId, tService, tSomeExercise, tText, tDifficulty, tUserId ,tContext

   , tDerivation, tError, (.->), tIO, tExercise, tTestSuiteResult, tQCGen

   , tScript, tExamples, tStrategyCfg, tMathML, tInt

     -- * Searching a typed value

   , findValuesOfType

   ) where



import Control.Monad

import Data.Char

import Data.List

import Data.Maybe

import Data.Tree

import Ideas.Common.Library

import Ideas.Service.FeedbackScript.Syntax

import Ideas.Service.State

import Ideas.Text.MathML

import Test.QuickCheck.Random (QCGen)

import qualified Ideas.Utils.TestSuite as TestSuite



-----------------------------------------------------------------------------

-- Services



data Service = S

   { serviceId         :: Id

   , serviceDeprecated :: Bool

   , serviceFunction   :: forall a . TypedValue (Type a)

   }



instance Show Service where

   show = showId



instance HasId Service where

   getId = serviceId

   changeId f a = a { serviceId = f (serviceId a) }



makeService :: String -> String -> (forall a . TypedValue (Type a)) -> Service

makeService s descr f = describe descr (S (newId s) False f)



deprecate :: Service -> Service

deprecate s = s { serviceDeprecated = True }



class Equal f where

   equal :: f a -> f b -> Maybe (a -> b)



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



instance Equal f => Equal (TypeRep f) where

   equal (Iso p a)  t2         = fmap (. to p) (equal a t2)

   equal t1         (Iso p b)  = fmap (from p .) (equal t1 b)

   equal (a :-> b)  (c :-> d)  = liftM2 (\f g h -> g . h . f)

                                        (equal c a) (equal b d)

   equal (Pair a b) (Pair c d) = liftM2 (***) (equal a c) (equal b d)

   equal (a :|: b)  (c :|: d)  = liftM2 biMap (equal a c) (equal b d)

   equal (List a)   (List b)   = fmap map (equal a b)

   equal (Tag s1 a) (Tag s2 b) | s1 == s2 = equal a b

   equal Unit       Unit       = Just id

   equal (Const a)  (Const b)  = equal a b

   equal _          _          = Nothing



instance Equal (Const a) where

   equal Int         Int         = Just id

   equal Bool        Bool        = Just id

   equal String      String      = Just id

   equal MathML      MathML      = Just id

   equal Service     Service     = Just id

   equal Exercise    Exercise    = Just id

   equal Strategy    Strategy    = Just id

   equal State       State       = Just id

   equal Rule        Rule        = Just id

   equal Constraint  Constraint  = Just id

   equal Context     Context     = Just id

   equal Id          Id          = Just id

   equal Location    Location    = Just id

   equal Script      Script      = Just id

   equal StratCfg    StratCfg    = Just id

   equal Environment Environment = Just id

   equal Term        Term        = Just id

   equal SomeExercise SomeExercise = Just id

   equal Text        Text        = Just id

   equal QCGen       QCGen       = Just id

   equal Result      Result      = Just id

   equal _           _           = Nothing



infixr 5 :|:



-----------------------------------------------------------------------------

-- Types



infix  2 :::

infixr 3 :->



data TypedValue f where

   (:::) :: t -> f t -> TypedValue f



type Type a = TypeRep (Const a)



data TypeRep f t where

   -- Type isomorphisms (for defining type synonyms)

   Iso   :: Isomorphism t1 t2 -> TypeRep f t1 -> TypeRep f t2

   -- Function type

   (:->) :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (t1 -> t2)

   -- Input/output

   IO    :: TypeRep f t -> TypeRep f (IO t)

   -- Special annotations

   Tag   :: String -> TypeRep f t1 -> TypeRep f t1

   -- Type constructors

   List  :: TypeRep f t  -> TypeRep f [t]

   Pair  :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (t1, t2)

   (:|:) :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (Either t1 t2)

   Unit  :: TypeRep f ()

   -- Type constants

   Const :: f t -> TypeRep f t



data Const a t where

   -- exercise specific

   Service      :: Const a Service

   Exercise     :: Const a (Exercise a)

   Strategy     :: Const a (Strategy (Context a))

   State        :: Const a (State a)

   Rule         :: Const a (Rule (Context a))

   Constraint   :: Const a (Constraint (Context a))

   Context      :: Const a (Context a)

   -- other types

   Id           :: Const a Id

   Location     :: Const a Location

   Script       :: Const a Script

   StratCfg     :: Const a StrategyCfg

   Environment  :: Const a Environment

   Term         :: Const a Term

   Text         :: Const a Text

   QCGen        :: Const a QCGen

   Result       :: Const a TestSuite.Result

   SomeExercise :: Const a (Some Exercise)

   MathML       :: Const a MathML

   -- basic types

   Bool         :: Const a Bool

   Int          :: Const a Int

   String       :: Const a String



class ShowF f where

   showF :: f a -> String



instance ShowF f => ShowF (TypeRep f) where

   showF = show



instance ShowF f => Show (TypeRep f t) where

   show (Iso _ t)      = show t

   show (t1 :-> t2)    = show t1 ++ " -> " ++ show t2

   show (IO t)         = show t

   show t@(Pair _ _)   = showTuple t

   show (t1 :|: t2)    = show t1 ++ " | " ++ show t2

   show (Tag s _)      = s

   show (List t)       = "[" ++ show t ++ "]"

   show Unit           = "()"

   show (Const c)      = showF c



instance Show (TypedValue f) => Show (TypedValue (TypeRep f)) where

   show (val ::: tp) =

      case tp of

         Iso iso t  -> show (to iso val ::: t)

         _ :-> _    -> "<<function>>"

         IO _       -> "<<io>>"

         Tag _ t    -> show (val ::: t)

         List t     -> showAsList (map (show . (::: t)) val)

         Pair t1 t2 -> "(" ++ show (fst val ::: t1) ++

                       "," ++ show (snd val ::: t2) ++ ")"

         t1 :|: t2  -> either (show . (::: t1)) (show . (::: t2)) val

         Unit       -> "()"

         Const t    -> show (val ::: t)



showAsList :: [String] -> String

showAsList xs = "[" ++ intercalate "," xs ++ "]"



instance Show (TypedValue (Const a)) where

   show (val ::: tp) =

      case tp of

         Service          -> showId val

         Exercise         -> showId val

         Strategy         -> show val

         Rule             -> showId val

         Constraint       -> showId val

         Id               -> showId val

         SomeExercise     -> case val of Some ex -> showId ex

         State            -> show val

         Context          -> show (location val, environment val)

         Location         -> show val

         Script           -> show val

         StratCfg         -> show val

         Environment      -> show val

         Term             -> show val

         Text             -> show val

         QCGen            -> show val

         Result           -> show val

         MathML           -> show val

         Bool             -> map toLower (show val)

         Int              -> show val

         String           -> val



instance Show (Const a t) where

   show = showF



instance ShowF (Const a) where

   showF Service      = "Service"

   showF Exercise     = "Exercise"

   showF Strategy     = "Strategy"

   showF State        = "State"

   showF Rule         = "Rule"

   showF Constraint   = "Constraint"

   showF Context      = "Context"

   showF Id           = "Id"

   showF Location     = "Location"

   showF Script       = "Script"

   showF StratCfg     = "StrategyConfiguration"

   showF Environment  = "Environment"

   showF Term         = "Term"

   showF Text         = "TextMessage"

   showF QCGen        = "QCGen"

   showF Result       = "TestSuiteResult"

   showF SomeExercise = "Exercise"

   showF MathML       = "MathML"

   showF Bool         = "Bool"

   showF Int          = "Int"

   showF String       = "String"



showTuple :: ShowF f => TypeRep f t -> String

showTuple tp = "(" ++ intercalate ", " (collect tp) ++ ")"

 where

   collect :: ShowF f => TypeRep f t -> [String]

   collect (Pair t1 t2) = collect t1 ++ collect t2

   collect (Iso _ t)    = collect t

   collect t            = [showF t]



---------------------------------------------------------------



tError :: Type a t -> Type a (Either String t)

tError = (:|:) tString



tDerivation :: Type a t1 -> Type a t2 -> Type a (Derivation t1 t2)

tDerivation t1 t2 = Tag "Derivation" $ Iso (f <-> g) tp

 where

   tp = tPair t2 (tList (tPair t1 t2))

   f (a, xs) = foldl extend (emptyDerivation a) xs

   g d = (firstTerm d, [ (s, a) | (_, s, a) <- triples d ])



tIO :: Type a t -> Type a (IO t)

tIO = IO



tText :: Type a Text

tText = Const Text



infixr 5 .->



(.->) :: Type a t1 -> Type a t2 -> Type a (t1 -> t2)

(.->) = (:->)



tState :: Type a (State a)

tState = Const State



tMaybe :: Type a t -> Type a (Maybe t)

tMaybe t = Iso (f <-> g) (t :|: Unit)

    where

      f = either Just (const Nothing)

      g = maybe (Right ()) Left



tStrategyCfg :: Type a StrategyCfg

tStrategyCfg = Const StratCfg



tList :: Type a t -> Type a [t]

tList = List



tUnit :: Type a ()

tUnit = Unit



tPair :: Type a t1 -> Type a t2 -> Type a (t1, t2)

tPair = Pair



tString :: Type a String

tString = Const String



tExercise :: Type a (Exercise a)

tExercise = Const Exercise



tContext :: Type a (Context a)

tContext = Const Context



tMathML :: Type a MathML

tMathML = Const MathML



tBool :: Type a Bool

tBool = Const Bool



tInt :: Type a Int

tInt = Const Int



tRule :: Type a (Rule (Context a))

tRule = Const Rule



tConstraint :: Type a (Constraint (Context a))

tConstraint = Const Constraint



tLocation :: Type a Location

tLocation = Const Location



tTuple3 :: Type a t1 -> Type a t2 -> Type a t3 -> Type a (t1, t2, t3)

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



tTuple4 :: Type a t1 -> Type a t2 -> Type a t3 -> Type a t4 -> Type a (t1, t2, t3, t4)

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



tTuple5 :: Type a t1 -> Type a t2 -> Type a t3 -> Type a t4 -> Type a t5 -> Type a (t1, t2, t3, t4, t5)

tTuple5 t1 t2 t3 t4 t5 = Iso (f <-> g) (Pair t1 (Pair t2 (Pair t3 (Pair t4 t5))))

    where

      f (a, (b, (c, (d, e)))) = (a, b, c, d, e)

      g (a, b, c, d, e)       = (a, (b, (c, (d, e))))



tEnvironment :: Type a Environment

tEnvironment = Const Environment



tTerm :: Type a Term

tTerm = Const Term



tDifficulty :: Type a Difficulty

tDifficulty = Tag "Difficulty" (Iso (f <-> show) tString)

    where

      f = fromMaybe Medium . readDifficulty



tUserId :: Type a String

tUserId = Tag "UserId" tString



tQCGen :: Type a QCGen

tQCGen = Const QCGen



tExamples :: Type a (Examples (Context a))

tExamples = tList (tPair tDifficulty tContext)



tId :: Type a Id

tId = Const Id



tScript :: Type a Script

tScript = Const Script



tSomeExercise :: Type a (Some Exercise)

tSomeExercise = Const SomeExercise



tService :: Type a Service

tService = Const Service



tStrategy :: Type a (Strategy (Context a))

tStrategy = Const Strategy



tTree :: Type a t -> Type a (Tree t)

tTree t = Tag "Tree" $ Iso (f <-> g) (tPair t (tList (tTree t)))

    where

      f = uncurry Node

      g (Node a xs) = (a, xs)



tTestSuiteResult :: Type a TestSuite.Result

tTestSuiteResult = Const Result



-------------------------------------



findValuesOfType :: Type a t -> TypedValue (Type a) -> [t]

findValuesOfType thisType = rec

 where

   rec tv@(a ::: tp) =

      case equal tp thisType of

         Just f  -> [f a]

         Nothing -> recDown tv



   recDown (a ::: tp) =

      case tp of

         Iso iso t  -> rec (to iso a ::: t)

         Tag _ t    -> rec (a ::: t)

         List t     -> concatMap (\b -> rec (b ::: t)) a

         Pair t1 t2 -> rec (fst a ::: t1) ++ rec (snd a ::: t2)

         t1 :|: t2  -> either (\b -> rec (b ::: t1)) (\b -> rec (b ::: t2)) a

         _          -> []