-- -- 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 -fallow-undecidable-instances -fallow-overlapping-instances #-} module Control.Concurrent.Session.Loop where import Control.Concurrent.Session.BaseTypes import Control.Concurrent.Session.BaseClasses import Control.Concurrent.Session.List import Control.Concurrent.Session.State import Control.Concurrent.Session.ExtraClasses import Control.Concurrent.MVar import Control.Concurrent.Chan class ReplaceLoopEnd orig replacement result | orig replacement -> result where replaceLoopEnd :: orig -> replacement -> result instance ReplaceLoopEnd (SessionSpec EndT) (SessionSpec n) (SessionSpec EndT) where replaceLoopEnd EndS r = EndS instance ReplaceLoopEnd (SessionSpec LoopEndT) (SessionSpec n) (SessionSpec n) where replaceLoopEnd LoopEndS r = r instance ReplaceLoopEnd (SessionSpec (LoopT (SessionSpec l))) (SessionSpec replacement) (SessionSpec (LoopT (SessionSpec l))) where replaceLoopEnd (LoopS l) r = (LoopS l) instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) => ReplaceLoopEnd (SessionSpec (SendT t orig)) (SessionSpec replacement) (SessionSpec (SendT t result)) where replaceLoopEnd (SendS t n) r = SendS t (replaceLoopEnd n r) instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) => ReplaceLoopEnd (SessionSpec (RecvT t orig)) (SessionSpec replacement) (SessionSpec (RecvT t result)) where replaceLoopEnd (RecvS t n) r = RecvS t (replaceLoopEnd n r) instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) => ReplaceLoopEnd (SessionSpec (SessT t orig)) (SessionSpec replacement) (SessionSpec (SessT t result)) where replaceLoopEnd = undefined instance (ReplaceLoopEnd (List t list) (SessionSpec replacement) (List t list'), SpecList t list, SpecList t list') => ReplaceLoopEnd (SessionSpec (OfferT (List t list))) (SessionSpec replacement) (SessionSpec (OfferT (List t list'))) where replaceLoopEnd (OfferS list) r = OfferS (replaceLoopEnd list r) instance (ReplaceLoopEnd (List t list) (SessionSpec replacement) (List t list'), SpecList t list, SpecList t list') => ReplaceLoopEnd (SessionSpec (SelectT (List t list))) (SessionSpec replacement) (SessionSpec (SelectT (List t list'))) where replaceLoopEnd (SelectS list) r = SelectS (replaceLoopEnd list r) instance (ReplaceLoopEnd (List t list) (SessionSpec replacement) (List t list'), SpecList t list, SpecList t list') => ReplaceLoopEnd (SessionSpec (SessChoiceT (List t list))) (SessionSpec replacement) (SessionSpec (SessChoiceT (List t list'))) where replaceLoopEnd = undefined instance (ReplaceLoopEnd orig (SessionSpec replacement) result) => ReplaceLoopEnd (List t orig) (SessionSpec replacement) (List t result) where replaceLoopEnd (List t a) r = List t (replaceLoopEnd a r) instance ReplaceLoopEnd (Nil Zero) (SessionSpec replacement) (Nil Zero) where replaceLoopEnd Nil _ = nil instance (ReplaceLoopEnd (SessionSpec ltype) (SessionSpec replacement) (SessionSpec rtype), ReplaceLoopEnd ltail (SessionSpec replacement) rtail, ListLength ltail len, ListLength rtail len) => ReplaceLoopEnd (Cons (SessionSpec ltype) (Succ len) ltail) (SessionSpec replacement) (Cons (SessionSpec rtype) (Succ len) rtail) where replaceLoopEnd lst r = cons (replaceLoopEnd val r) (replaceLoopEnd nxt r) where (val, nxt) = decomposeCons lst instance (ReplaceLoopEnd (SessionSpec l) (SessionSpec (LoopT (SessionSpec l))) (SessionSpec r)) => UnrollLoop (SessionSpec (LoopT (SessionSpec l))) (SessionSpec r) where unroll (LoopS l) = replaceLoopEnd l (LoopS l) -- never quite worked out why this is required... instance (Choice generalType typeIndexes len) => Choice (generalType, a, b, c) typeIndexes len where typeIndexes = undefined -- loop, and we've seen it before. But make sure we can get to End. Magically! instance (BuildReductionList (LoopT (SessionSpec a)) (SessionSpec EndT) (Cons (SessionSpec EndT) (Succ Zero) (Nil Zero))) => BuildReductionList (LoopT (SessionSpec a)) (SessionSpec (LoopT (SessionSpec a))) (Cons (SessionSpec (LoopT (SessionSpec a))) (Succ (Succ Zero)) (Cons (SessionSpec EndT) (Succ Zero) (Nil Zero))) where findReduction lastSeenLoop (LoopS loop) = let endNxt = findReduction (LoopS loop) EndS in cons (LoopS loop) endNxt -- loop, but this one we've not seen before instance forall a b val len nxt lstLoop . (UnrollLoop (SessionSpec (LoopT (SessionSpec a))) (SessionSpec b), ReplaceLoopEnd (SessionSpec a) (SessionSpec (LoopT (SessionSpec a))) (SessionSpec b), BuildReductionList (LoopT (SessionSpec a)) (SessionSpec b) (Cons val len nxt)) => BuildReductionList lstLoop (SessionSpec (LoopT (SessionSpec a))) (Cons val len nxt) where findReduction _ (LoopS lp) = findReduction (undefined :: (LoopT (SessionSpec a))) (unroll (LoopS lp)) instance (JustSendsRecvs (SessionSpec l) (SessionSpec s) (SessionSpec r)) => JustSendsRecvs (SessionSpec (LoopT (SessionSpec l))) (SessionSpec (LoopT (SessionSpec s))) (SessionSpec (LoopT (SessionSpec r))) mkLoopS :: (SessionSpec LoopEndT -> SessionSpec l) -> SessionSpec (LoopT (SessionSpec l)) mkLoopS x = LoopS (x LoopEndS) -- the next two functions could be refactored to remove duplicate code. -- however, there are currently issues with unification on GADT pattern matches -- in non-rigid contexts mkLoop :: (UnrollLoop (SessionSpec (LoopT (SessionSpec s))) (SessionSpec sUnrolled), UnrollLoop (SessionSpec (LoopT (SessionSpec o))) (SessionSpec oUnrolled), UnrollLoop (SessionSpec (LoopT (SessionSpec i))) (SessionSpec iUnrolled), ReplaceLoopEnd (SessionSpec s) (SessionSpec (LoopT (SessionSpec s))) (SessionSpec sUnrolled), ReplaceLoopEnd (SessionSpec o) (SessionSpec (LoopT (SessionSpec o))) (SessionSpec oUnrolled), ReplaceLoopEnd (SessionSpec i) (SessionSpec (LoopT (SessionSpec i))) (SessionSpec iUnrolled), JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i), LoopContinue (SessionState (SessionSpec s') o' i'), JustSendsRecvs (SessionSpec (LoopT (SessionSpec s))) (SessionSpec (LoopT (SessionSpec o))) (SessionSpec (LoopT (SessionSpec i))) ) => (r -> SessionState (SessionSpec s) o i -> IO (r, SessionState (SessionSpec s') o' i')) -> r -> SessionState (SessionSpec (LoopT (SessionSpec s))) (LoopT (SessionSpec o)) (LoopT (SessionSpec i)) -> IO ((), (SessionState (SessionSpec EndT) EndT EndT)) mkLoop func arg (SessionState outgoing incoming) = do { licOutE <- newEmptyMVar ; licInE <- newEmptyMVar ; didPutOut <- tryPutMVar outgoing (LoopCell licOutE) ; didPutIn <- tryPutMVar incoming (LoopCell licInE) ; licOut <- if didPutOut then return licOutE else do { (LoopCell licOutF) <- takeMVar outgoing ; return licOutF } ; licIn <- if didPutIn then return licInE else do { (LoopCell licInF) <- takeMVar incoming ; return licInF } ; doLoop func arg licOut licIn } doLoop :: (JustSendsRecvs (SessionSpec spec) (SessionSpec outgoing) (SessionSpec incoming), LoopContinue (SessionState (SessionSpec spec') outgoing' incoming')) => (r -> SessionState (SessionSpec spec) outgoing incoming -> IO (r, SessionState (SessionSpec spec') outgoing' incoming')) -> r -> MVar (LoopIterationCell outgoing) -> MVar (LoopIterationCell incoming) -> IO ((), SessionState (SessionSpec EndT) EndT EndT) doLoop func arg licOutMVar licInMVar = do { mayLicOut <- tryTakeMVar licOutMVar ; (outgoing, licOutMVar') <- case mayLicOut of -- if it's already full then no one else will grab it but us, so safe -- if it's empty, then must be careful, as could fill up in mean time Nothing -> do { outgoingE <- newEmptyMVar ; licOutMVarE <- newEmptyMVar ; didPutOut <- tryPutMVar licOutMVar (LIC outgoingE licOutMVarE) ; if didPutOut then return (outgoingE, licOutMVarE) else do { (LIC outgoingF licOutMVarF) <- takeMVar licOutMVar ; return (outgoingF, licOutMVarF) } } (Just (LIC outgoingF licOutMVarF)) -> return (outgoingF, licOutMVarF) ; mayLicIn <- tryTakeMVar licInMVar ; (incoming, licInMVar') <- case mayLicIn of Nothing -> do { incomingE <- newEmptyMVar ; licInMVarE <- newEmptyMVar ; didPutIn <- tryPutMVar licInMVar (LIC incomingE licInMVarE) ; if didPutIn then return (incomingE, licInMVarE) else do { (LIC incomingF licInMVarF) <- takeMVar licInMVar ; return (incomingF, licInMVarF) } } (Just (LIC incomingF licInMVarF)) -> return (incomingF, licInMVarF) ; let state = SessionState outgoing incoming ; (arg', deadState) <- func arg state -- agh, this should really use LoopContinue but can't due to issue with return type of offer ; doLoop func arg' licOutMVar' licInMVar' } class LoopContinue termState where loopAgain :: (JustSendsRecvs (SessionSpec spec) (SessionSpec outgoing) (SessionSpec incoming), LoopContinue (SessionState (SessionSpec spec') outgoing' incoming')) => termState -> (r -> SessionState (SessionSpec spec) outgoing incoming -> IO (r, SessionState (SessionSpec spec') outgoing' incoming')) -> r -> MVar (LoopIterationCell outgoing) -> MVar (LoopIterationCell incoming) -> IO ((), SessionState (SessionSpec EndT) EndT EndT) instance LoopContinue (SessionState (SessionSpec LoopEndT) LoopEndT LoopEndT) where loopAgain = const doLoop instance LoopContinue (SessionState (SessionSpec EndT) EndT EndT) where loopAgain termState func arg _ _ = return ((), termState) loopEnd :: r -> (SessionState (SessionSpec LoopEndT) LoopEndT LoopEndT) -> IO (r, (SessionState (SessionSpec LoopEndT) LoopEndT LoopEndT)) loopEnd r state = return (r, state)