--
--  Control.Concurrent.Session :: Session Types for Haskell
--  Copyright (C) 2007  Matthew Sackman (matthew@wellquite.org)
--
--  This library is free software; you can redistribute it and/or
--  modify it under the terms of the GNU Lesser General Public
--  License as published by the Free Software Foundation; either
--  version 2.1 of the License, or (at your option) any later version.
--
--  This library is distributed in the hope that it will be useful,
--  but WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
--  Lesser General Public License for more details.
--
--  You should have received a copy of the GNU Lesser General Public
--  License along with this library; if not, write to the Free Software
--  Foundation, Inc., 59 Temple Place, Suite 330, Boston,
--  MA  02111-1307  USA
--
{-# OPTIONS_GHC -fglasgow-exts #-}

module Control.Concurrent.Session.State
    where

import Control.Concurrent.Session.BaseTypes
import Control.Concurrent.Session.BaseClasses
import Control.Concurrent.Session.ExtraClasses
import Control.Concurrent.Session.List
import Control.Concurrent.MVar
import Control.Concurrent.Chan

data ProcCell :: * -> * -> * -> * -> * -> * -> * -> * where
                 ProcCell :: (ZeroOrMoreSteps (SessionSpec s) (SessionSpec s'),
                              JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
                              JustSendsRecvs (SessionSpec s') (SessionSpec o') (SessionSpec i')) =>
                             (Proc r (SessionSpec s) (SessionSpec s') o o' i i') ->
                             SessionState (SessionSpec s) o i ->
                             ProcCell r (SessionSpec s) (SessionSpec s') o o' i i'

data ProcWrapper :: * where
                    PW :: (ZeroOrMoreSteps (SessionSpec s) (SessionSpec s'),
                           JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
                           JustSendsRecvs (SessionSpec s') (SessionSpec o') (SessionSpec i')) =>
                          (ProcCell () (SessionSpec s) (SessionSpec s') o o' i i') ->
                          ProcWrapper

data LoopIterationCell a = LIC (MVar (Cell a)) (MVar (LoopIterationCell a))

data Cell :: * -> * where
             Cell :: t -> MVar (Cell ct) -> Cell (SessT t ct)
             LoopCell :: (UnrollLoop (SessionSpec (LoopT (SessionSpec l))) (SessionSpec ul)) =>
                         (MVar (LoopIterationCell l)) ->
                         Cell (LoopT (SessionSpec l))
             OffersCell :: (ValidOffer generalType procs specsForOffer,
                            ListLength procs len, ListLength specsForOffer len,
                            ListLength specsForSelect len,
                            ChoiceSpecsProcs specsForOffer procs,
                            Choice generalType typeIndexes len,
                            JustSendsRecvs (SessionSpec (OfferT (List generalType specsForOffer)))
                              (SessionSpec (SessChoiceT
                                            (List (generalType, specsForOffer, specsForSelect, procs) specsO)))
                              (SessionSpec (SessChoiceT
                                            (List (generalType, specsForSelect, specsForOffer, procs) specsI)))
                           ) =>
                          (List generalType procs) ->
                          (MVar ProcWrapper) ->
                          Cell (SessChoiceT (List (generalType, specsForOffer, specsForSelect, procs) specsO))

data SessionState :: * -> * -> * -> * where
                     SessionState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming)) =>
                            MVar (Cell outgoing) -> MVar (Cell incoming) ->
                            SessionState spec outgoing incoming

instance JustSendsRecvs (SessionState s o i) (SessionSpec o) (SessionSpec i)

data Proc :: * -> * -> * -> * -> * -> * -> * -> * where
             Proc :: (ZeroOrMoreSteps (SessionSpec s) (SessionSpec s'),
                      JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
                      JustSendsRecvs (SessionSpec s') (SessionSpec o') (SessionSpec i')) =>
                     (SessionState (SessionSpec s) o i ->
                      IO (r, SessionState (SessionSpec s') o' i')) ->
                     Proc r (SessionSpec s) (SessionSpec s') o o' i i'