Ticket #1353: Session.hs

File Session.hs, 18.7 KB (added by matthew@…, 8 years ago)

The Magic Code

Line 
1{-# OPTIONS_GHC -fglasgow-exts -fallow-overlapping-instances -fallow-undecidable-instances #-}
2
3module Session
4    (SType(..)
5    ,SessionSpec(..)
6    ,runSessionWithProcs
7    ,Proc(..)
8    ,send
9    ,recv
10    ,sendLog
11    ,recvLog
12    ,(>~>)
13    ,(>~>=)
14    ,returnS
15    ,sliftIO
16    ,sliftIO'
17    ,SendT
18    ,RecvT
19    ,EndT
20    ,SessT
21    ,SessionState
22    ,JustSendsRecvs
23    ,ZeroOrMoreSteps
24    ,mkLoopS
25    ,mkLoop
26    )
27    where
28
29import Control.Monad.Fix
30import Control.Concurrent.MVar
31import Control.Concurrent
32
33data SType :: * -> * where
34              IntS    :: SType Int
35              BoolS   :: SType Bool
36              CharS   :: SType Char
37              StringS :: SType String
38              FloatS  :: SType Float
39              DoubleS :: SType Double
40              AnyS    :: SType a
41              LiftS   :: a -> SType a
42              ListS   :: (SType a) -> SType [a]
43
44instance Show (SType a) where
45    show IntS      = "IntS"
46    show BoolS     = "BoolS"
47    show CharS     = "CharS"
48    show StringS   = "StringS"
49    show FloatS    = "FloatS"
50    show DoubleS   = "DoubleS"
51    show AnyS      = "AnyS"
52    show (LiftS a) = "LiftS"
53    show (ListS a) = "ListS of " ++ (show a)
54
55
56newtype Mu f = In (f (Mu f))
57
58out :: Mu f -> f (Mu f)
59out (In x) = x
60
61data LoopF :: * -> * -> * where
62              Again :: (SessionSpec l) -> a -> LoopF (SessionSpec l) a
63
64type Loop t = Mu (LoopF t)
65
66instance Show (LoopF (SessionSpec l) a) where
67    show (Again l _) = "Loop {" ++ (show l) ++ "}"
68
69again :: SessionSpec l -> Loop (SessionSpec l) -> Loop (SessionSpec l)
70again x xs = In (Again x xs)
71
72mkLoopS :: (SessionSpec LoopEndT -> SessionSpec l) -> SessionSpec (Loop (SessionSpec l))
73mkLoopS x = LoopS l
74    where
75      xl = x LoopEndS
76      l = again xl l
77
78data SendT a n
79data RecvT a n
80data EndT
81data LoopEndT
82data SessT a n
83
84class ReplaceLoopEnd orig replacement result | orig replacement -> result where
85    replaceLoopEnd :: orig -> replacement -> result
86instance ReplaceLoopEnd (SessionSpec EndT) (SessionSpec n) (SessionSpec EndT) where
87    replaceLoopEnd EndS r = EndS
88instance ReplaceLoopEnd (SessionSpec LoopEndT) (SessionSpec n) (SessionSpec n) where
89    replaceLoopEnd LoopEndS r = r
90instance ReplaceLoopEnd (SessionSpec (Loop (SessionSpec l))) (SessionSpec replacement) (SessionSpec (Loop (SessionSpec l))) where
91    replaceLoopEnd (LoopS l) r = (LoopS l)
92instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
93    ReplaceLoopEnd (SessionSpec (SendT t orig)) (SessionSpec replacement) (SessionSpec (SendT t result)) where
94        replaceLoopEnd (SendS t n) r = SendS t (replaceLoopEnd n r)
95instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
96    ReplaceLoopEnd (SessionSpec (RecvT t orig)) (SessionSpec replacement) (SessionSpec (RecvT t result)) where
97        replaceLoopEnd (RecvS t n) r = RecvS t (replaceLoopEnd n r)
98instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
99    ReplaceLoopEnd (SessionSpec (SessT t orig)) (SessionSpec replacement) (SessionSpec (SessT t result)) where
100        replaceLoopEnd = undefined
101
102class UnrollLoop orig result | orig -> result where
103    unroll :: orig -> result
104instance (ReplaceLoopEnd (SessionSpec l) (SessionSpec (Loop (SessionSpec l))) (SessionSpec r)) =>
105    UnrollLoop (SessionSpec (Loop (SessionSpec l))) (SessionSpec r) where
106        unroll (LoopS l) = case out l of
107                            (Again myLoop _) -> replaceLoopEnd myLoop (LoopS l)
108instance UnrollLoop (SessionSpec (EndT)) (SessionSpec (EndT)) where
109    unroll = id
110instance UnrollLoop (SessionSpec (LoopEndT)) (SessionSpec (LoopEndT)) where
111    unroll = id
112instance UnrollLoop (SessionSpec (SendT t n)) (SessionSpec (SendT t n)) where
113    unroll = id
114instance UnrollLoop (SessionSpec (RecvT t n)) (SessionSpec (RecvT t n)) where
115    unroll = id
116instance UnrollLoop (SessionSpec (SessT t n)) (SessionSpec (SessT t n)) where
117    unroll = undefined
118
119data SessionSpec :: * -> * where
120                    RecvS :: (SType t) -> (SessionSpec n) -> SessionSpec (RecvT t n)
121                    SendS :: (SType t) -> (SessionSpec n) -> SessionSpec (SendT t n)
122                    EndS :: SessionSpec EndT
123                    LoopEndS :: SessionSpec LoopEndT
124                    LoopS :: (Loop (SessionSpec l)) -> SessionSpec (Loop (SessionSpec l))
125
126instance Show (SessionSpec n) where
127    show (RecvS t next) = "RecvS " ++ (show t) ++ " . " ++ (show next)
128    show (SendS t next) = "SendS " ++ (show t) ++ " . " ++ (show next)
129    show (EndS) = "EndS"
130    show (LoopEndS) = "LoopEndS"
131    show (LoopS l) = case out l of
132                      (Again myloop _) -> "LoopS {" ++ (show myloop) ++ "}"
133
134class DualT a b | a -> b, b -> a where
135    dual :: a -> b
136instance DualT (SessionSpec EndT) (SessionSpec EndT) where
137    dual EndS = EndS
138instance DualT (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
139    dual LoopEndS = LoopEndS
140instance (DualT (SessionSpec l) (SessionSpec r)) =>
141    DualT (SessionSpec (RecvT t l)) (SessionSpec (SendT t r)) where
142        dual (RecvS t n) = (SendS t (dual n))
143instance (DualT (SessionSpec l) (SessionSpec r)) =>
144    DualT (SessionSpec (SendT t l)) (SessionSpec (RecvT t r)) where
145        dual (SendS t n) = (RecvS t (dual n))
146instance (DualT (SessionSpec l) (SessionSpec r)) =>
147    DualT (SessionSpec (Loop (SessionSpec l))) (SessionSpec (Loop (SessionSpec r))) where
148        dual (LoopS l) = case out l of
149                          (Again myLoop loopTail) ->
150                              let myLoop' = dual myLoop
151                                  l' = again myLoop' l'
152                              in LoopS l'
153
154class NextOp a b | a -> b where
155    nextOp :: a -> b
156instance NextOp (SessionSpec (RecvT t l)) (SessionSpec l) where
157    nextOp (RecvS t n) = n
158instance NextOp (SessionSpec (SendT t l)) (SessionSpec l) where
159    nextOp (SendS t n) = n
160instance NextOp (SessionSpec (SessT t l)) (SessionSpec l) where
161    nextOp = undefined
162
163class ZeroOrMoreSteps a b where
164    stepN :: a -> b
165instance ZeroOrMoreSteps (SessionSpec EndT) (SessionSpec EndT) where
166    stepN x = x
167instance ZeroOrMoreSteps (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
168    stepN x = x
169instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec (RecvT t l)) where
170    stepN x = x
171instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec (SendT t l)) where
172    stepN x = x
173instance ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec (Loop (SessionSpec a))) where
174    stepN x = x
175instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec l) where
176    stepN (RecvS t n) = n
177instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec l) where
178    stepN (SendS t n) = n
179instance ZeroOrMoreSteps (SessionSpec (SessT t l)) (SessionSpec l) where
180    stepN = undefined
181instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
182    ZeroOrMoreSteps (SessionSpec (RecvT t a)) (SessionSpec b) where
183        stepN (RecvS t n) = stepN n
184instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
185    ZeroOrMoreSteps (SessionSpec (SendT t a)) (SessionSpec b) where
186        stepN (SendS t n) = stepN n
187instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
188    ZeroOrMoreSteps (SessionSpec (SessT t a)) (SessionSpec b) where
189        stepN = undefined
190instance (UnrollLoop (SessionSpec (Loop (SessionSpec a))) (SessionSpec b),
191          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c)) =>
192    ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec c) where
193        stepN = stepN . unroll
194instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
195    ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec (Loop (SessionSpec b))) where
196        stepN = undefined
197
198class CommTy a b | a -> b where
199instance CommTy (SessionSpec (SendT t n)) t where
200instance CommTy (SessionSpec (RecvT t n)) t where
201instance CommTy (SessT t n) t where
202
203fooDual :: (DualT l r) => l -> r -> Bool
204fooDual _ _ = True
205
206fooNext :: (NextOp l r) => l -> r -> Bool
207fooNext _ _ = True
208
209fooZeroPlus :: (ZeroOrMoreSteps a b) => a -> b -> Bool
210fooZeroPlus _ _ = True
211
212fooCommTy :: (CommTy a b) => a -> b -> Bool
213fooCommTy _ _ = True
214
215class JustSendsRecvs orig sends recvs | orig -> sends recvs, orig sends -> recvs, orig recvs -> sends where
216instance JustSendsRecvs (SessionSpec EndT) (SessionSpec EndT) (SessionSpec EndT) where
217instance JustSendsRecvs (SessionSpec LoopEndT) (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
218instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
219    JustSendsRecvs (SessionSpec (SendT t n)) (SessionSpec (SessT t s)) (SessionSpec r) where
220instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
221    JustSendsRecvs (SessionSpec (RecvT t n)) (SessionSpec s) (SessionSpec (SessT t r)) where
222instance (JustSendsRecvs (SessionSpec l) (SessionSpec s) (SessionSpec r)) =>
223    JustSendsRecvs (SessionSpec (Loop (SessionSpec l))) (SessionSpec (Loop (SessionSpec s))) (SessionSpec (Loop (SessionSpec r))) where
224instance JustSendsRecvs (SessionState s o i) (SessionSpec o) (SessionSpec i) where
225
226data Cell :: * -> * where
227             Cell :: t -> MVar (Cell ct) -> Cell (SessT t ct)
228             Branch :: (UnrollLoop (SessionSpec l) (SessionSpec u)) => MVar (Cell u) -> Cell l
229
230data SessionState :: * -> * -> * -> * where
231                     SessionState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming)) =>
232                            MVar (Cell outgoing) -> MVar (Cell incoming) ->
233                            SessionState spec outgoing incoming
234
235loop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
236         UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
237         UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
238         JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i)) =>
239        SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il)) ->
240        IO ((), SessionState (SessionSpec s') o i)
241loop (SessionState o i) = do { newEmptyO <- newEmptyMVar
242                             ; didPutO <- tryPutMVar o (Branch newEmptyO)
243                             ; newEmptyI <- newEmptyMVar
244                             ; didPutI <- tryPutMVar i (Branch newEmptyI)
245                             ; return ((), SessionState newEmptyO newEmptyI)
246                             }
247
248
249send :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
250         NextOp (SessionSpec (SessT t o)) (SessionSpec o),
251         ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
252         JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
253         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
254        t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i ->
255        IO ((), SessionState (SessionSpec s) o i)
256send val (SessionState o i) = do { newEmpty <- newEmptyMVar
257                                 ; putMVar o (Cell val newEmpty)
258                                 ; return ((), SessionState newEmpty i)
259                                 }
260
261recv :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
262         NextOp (SessionSpec (SessT t i)) (SessionSpec i),
263         ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
264         JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
265         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
266        SessionState (SessionSpec (RecvT t s)) o (SessT t i) ->
267        IO (t, SessionState (SessionSpec s) o i)
268recv (SessionState o i) = do { (Cell val next) <- takeMVar i
269                             ; return (val, SessionState o next)
270                             }
271
272mkState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming),
273            JustSendsRecvs spec' (SessionSpec incoming) (SessionSpec outgoing),
274            DualT spec spec') => spec ->
275           IO (SessionState spec outgoing incoming, SessionState spec' incoming outgoing)
276mkState _ = do { outgoing <- newEmptyMVar
277               ; incoming <- newEmptyMVar
278               ; let s1 = SessionState outgoing incoming
279               ; let s2 = SessionState incoming outgoing
280               ; return (s1, s2)
281               }
282
283data Proc :: * -> * -> * -> * -> * -> * -> * where
284             Proc :: (ZeroOrMoreSteps s s',
285                      JustSendsRecvs s (SessionSpec o) (SessionSpec i),
286                      JustSendsRecvs s' (SessionSpec o') (SessionSpec i')) =>
287                     (SessionState s o i -> IO ((), SessionState s' o' i')) -> Proc s s' o o' i i'
288
289runSessionWithProcs :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming),
290                        JustSendsRecvs specD (SessionSpec incoming) (SessionSpec outgoing),
291                        DualT spec specD,
292                        JustSendsRecvs spec' (SessionSpec outgoing') (SessionSpec incoming'),
293                        JustSendsRecvs specD' (SessionSpec incoming') (SessionSpec outgoing'),
294                        ZeroOrMoreSteps spec spec',
295                        ZeroOrMoreSteps specD specD'
296                       ) =>
297                       spec
298                    -> Proc spec spec' outgoing outgoing' incoming incoming'
299                    -> Proc specD specD' incoming incoming' outgoing outgoing'
300                    -> IO spec'
301runSessionWithProcs spec (Proc p1) (Proc p2)
302    = do { (s1, s2) <- mkState spec
303         ; let f1 = (p1 s1) >>= return . fst
304         ; let f2 = (p2 s2) >>= return . fst
305         ; forkIO f1
306         ; forkIO f2
307         ; return (stepN spec)
308         }
309
310-- log through stdout and send
311sendLog :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
312            ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
313            JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
314            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
315            Show t) =>
316           t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i
317             -> IO ((), SessionState (SessionSpec s) o i)
318sendLog v = sliftIO (putStrLn $ "Sending '" ++ (show v) ++ "'")
319            >~> send v
320
321-- receive and log through stdout
322recvLog :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
323            ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
324            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
325            JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
326            ZeroOrMoreSteps (SessionSpec s) (SessionSpec s),
327            Show t) =>
328           SessionState (SessionSpec (RecvT t s)) o (SessT t i)
329               -> IO (t, SessionState (SessionSpec s) o i)
330recvLog = recv
331          >~>= (\r -> sliftIO (putStrLn $ "Received '" ++ (show r) ++ "'")
332                >~> returnS r)
333
334infixl 1 >~>
335infixl 1 >~>=
336
337-- (>>) :: (Monad m) => m b -> m c -> m c
338-- (>~>) serves the same purpose as (>>). So it's basically
339-- on the lines of Session-from-a-to-b-with-type-n ->
340--                 Session-from-b-to-c-with-type-m ->
341--                 Session-from-a-to-c-with-type-m
342(>~>) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
343          JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
344          JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
345          ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
346          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
347          ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
348         ((SessionState (SessionSpec a) o i) ->
349          IO (r, (SessionState (SessionSpec b) o' i'))) ->
350         ((SessionState (SessionSpec b) o' i') ->
351          IO (r', (SessionState (SessionSpec c) o'' i''))) ->
352         ((SessionState (SessionSpec a) o i) ->
353          IO (r', (SessionState (SessionSpec c) o'' i'')))
354f >~> g = \s -> f s >>= \(_, s') -> g s'
355
356-- (>>=) :: (Monad m) => m b -> (b -> m c) -> m c
357-- (>~>=) serves the same purpose as (>>=). So it's basically
358-- on the lines of Session-from-a-to-b-with-type-n ->
359--                 (n -> Session-from-b-to-c-with-type-m) ->
360--                 Session-from-a-to-c-with-type-m
361(>~>=) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
362           JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
363           JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
364           ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
365           ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
366           ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
367          ((SessionState (SessionSpec a) o i) ->
368           IO (r, (SessionState (SessionSpec b) o' i'))) ->
369          (r -> (SessionState (SessionSpec b) o' i') ->
370           IO (r', (SessionState (SessionSpec c) o'' i''))) ->
371          ((SessionState (SessionSpec a) o i) ->
372           IO (r', (SessionState (SessionSpec c) o'' i'')))
373f >~>= g = \s -> f s >>= \(r, s') -> g r s'
374
375-- return :: (Monad m) => a -> m a
376-- returnS is pretty much the some as return, lifting a value into a session
377-- returnS :: r -> Session-from-a-to-a-with-type-r
378returnS :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
379            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
380           r -> (SessionState (SessionSpec a) o i) ->
381           IO (r, (SessionState (SessionSpec a) o i))
382returnS v s = return (v, s)
383
384-- lifting just lift an IO straight in:
385-- sliftIO :: IO r -> Session-from-a-to-a-with-type-r
386sliftIO :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
387            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
388           IO r -> ((SessionState (SessionSpec a) o i) ->
389                    IO (r, (SessionState (SessionSpec a) o i)))
390sliftIO f = \s -> f >>= \r -> returnS r s
391
392-- for when the inner function wants to grab a value from outside...
393-- sliftIO' :: (m -> IO n) -> (m -> Session-from-a-to-a-with-type n)
394sliftIO' :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
395             ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
396            (r -> IO r') -> (r -> (SessionState (SessionSpec a) o i) ->
397                             IO (r', (SessionState (SessionSpec a) o i)))
398sliftIO' f = \r -> sliftIO (f r)
399
400
401mkLoop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
402           UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
403           UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
404           JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i),
405           ZeroOrMoreSteps (SessionSpec s') (SessionSpec (Loop (SessionSpec s)))) =>
406         ((SessionState (SessionSpec s') o i) ->
407           IO ((), (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))))) ->
408          (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))) ->
409          IO ((), SessionState (SessionSpec EndT) EndT EndT)
410mkLoop f s = loop s >>= \((), s') -> f s' >>= \((), s'') -> mkLoop f s''