Ticket #1353: SessionWithList.hs

File SessionWithList.hs, 18.3 KB (added by matthew@…, 7 years ago)

No Mu, no recursive ADT but an infinite list.

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
55type Loop a = [a]
56
57mkLoopS :: (SessionSpec LoopEndT -> SessionSpec l) -> SessionSpec (Loop (SessionSpec l))
58mkLoopS x = LoopS (repeat xl)
59    where
60      xl = x LoopEndS
61
62data SendT a n
63data RecvT a n
64data EndT
65data LoopEndT
66data SessT a n
67
68data SessionSpec :: * -> * where
69                    RecvS :: (SType t) -> (SessionSpec n) -> SessionSpec (RecvT t n)
70                    SendS :: (SType t) -> (SessionSpec n) -> SessionSpec (SendT t n)
71                    EndS :: SessionSpec EndT
72                    LoopEndS :: SessionSpec LoopEndT
73                    LoopS :: (Loop (SessionSpec l)) -> SessionSpec (Loop (SessionSpec l))
74
75instance Show (SessionSpec n) where
76    show (RecvS t next) = "RecvS " ++ (show t) ++ " . " ++ (show next)
77    show (SendS t next) = "SendS " ++ (show t) ++ " . " ++ (show next)
78    show (EndS) = "EndS"
79    show (LoopEndS) = "LoopEndS"
80    show (LoopS l) = case l of
81                      (myloop:_) -> "LoopS {" ++ (show myloop) ++ "}"
82
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 l of
107                            (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
119class DualT a b | a -> b, b -> a where
120    dual :: a -> b
121instance DualT (SessionSpec EndT) (SessionSpec EndT) where
122    dual EndS = EndS
123instance DualT (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
124    dual LoopEndS = LoopEndS
125instance (DualT (SessionSpec l) (SessionSpec r)) =>
126    DualT (SessionSpec (RecvT t l)) (SessionSpec (SendT t r)) where
127        dual (RecvS t n) = (SendS t (dual n))
128instance (DualT (SessionSpec l) (SessionSpec r)) =>
129    DualT (SessionSpec (SendT t l)) (SessionSpec (RecvT t r)) where
130        dual (SendS t n) = (RecvS t (dual n))
131instance (DualT (SessionSpec l) (SessionSpec r)) =>
132    DualT (SessionSpec (Loop (SessionSpec l))) (SessionSpec (Loop (SessionSpec r))) where
133        dual (LoopS l) = case l of
134                          (myLoop:_) ->
135                              let myLoop' = dual myLoop
136                              in LoopS (repeat myLoop')
137
138class NextOp a b | a -> b where
139    nextOp :: a -> b
140instance NextOp (SessionSpec (RecvT t l)) (SessionSpec l) where
141    nextOp (RecvS t n) = n
142instance NextOp (SessionSpec (SendT t l)) (SessionSpec l) where
143    nextOp (SendS t n) = n
144instance NextOp (SessionSpec (SessT t l)) (SessionSpec l) where
145    nextOp = undefined
146
147class ZeroOrMoreSteps a b where
148    stepN :: a -> b
149instance ZeroOrMoreSteps (SessionSpec EndT) (SessionSpec EndT) where
150    stepN x = x
151instance ZeroOrMoreSteps (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
152    stepN x = x
153instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec (RecvT t l)) where
154    stepN x = x
155instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec (SendT t l)) where
156    stepN x = x
157instance ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec (Loop (SessionSpec a))) where
158    stepN x = x
159instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec l) where
160    stepN (RecvS t n) = n
161instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec l) where
162    stepN (SendS t n) = n
163instance ZeroOrMoreSteps (SessionSpec (SessT t l)) (SessionSpec l) where
164    stepN = undefined
165instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
166    ZeroOrMoreSteps (SessionSpec (RecvT t a)) (SessionSpec b) where
167        stepN (RecvS t n) = stepN n
168instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
169    ZeroOrMoreSteps (SessionSpec (SendT t a)) (SessionSpec b) where
170        stepN (SendS t n) = stepN n
171instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
172    ZeroOrMoreSteps (SessionSpec (SessT t a)) (SessionSpec b) where
173        stepN = undefined
174instance (UnrollLoop (SessionSpec (Loop (SessionSpec a))) (SessionSpec b),
175          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c)) =>
176    ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec c) where
177        stepN = stepN . unroll
178instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
179    ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec (Loop (SessionSpec b))) where
180        stepN = undefined
181
182class CommTy a b | a -> b where
183instance CommTy (SessionSpec (SendT t n)) t where
184instance CommTy (SessionSpec (RecvT t n)) t where
185instance CommTy (SessT t n) t where
186
187fooDual :: (DualT l r) => l -> r -> Bool
188fooDual _ _ = True
189
190fooNext :: (NextOp l r) => l -> r -> Bool
191fooNext _ _ = True
192
193fooZeroPlus :: (ZeroOrMoreSteps a b) => a -> b -> Bool
194fooZeroPlus _ _ = True
195
196fooCommTy :: (CommTy a b) => a -> b -> Bool
197fooCommTy _ _ = True
198
199class JustSendsRecvs orig sends recvs | orig -> sends recvs, orig sends -> recvs, orig recvs -> sends where
200instance JustSendsRecvs (SessionSpec EndT) (SessionSpec EndT) (SessionSpec EndT) where
201instance JustSendsRecvs (SessionSpec LoopEndT) (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
202instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
203    JustSendsRecvs (SessionSpec (SendT t n)) (SessionSpec (SessT t s)) (SessionSpec r) where
204instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
205    JustSendsRecvs (SessionSpec (RecvT t n)) (SessionSpec s) (SessionSpec (SessT t r)) where
206instance (JustSendsRecvs (SessionSpec l) (SessionSpec s) (SessionSpec r)) =>
207    JustSendsRecvs (SessionSpec (Loop (SessionSpec l))) (SessionSpec (Loop (SessionSpec s))) (SessionSpec (Loop (SessionSpec r))) where
208instance JustSendsRecvs (SessionState s o i) (SessionSpec o) (SessionSpec i) where
209
210data Cell :: * -> * where
211             Cell :: t -> MVar (Cell ct) -> Cell (SessT t ct)
212             Branch :: (UnrollLoop (SessionSpec l) (SessionSpec u)) => MVar (Cell u) -> Cell l
213
214data SessionState :: * -> * -> * -> * where
215                     SessionState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming)) =>
216                            MVar (Cell outgoing) -> MVar (Cell incoming) ->
217                            SessionState spec outgoing incoming
218
219loop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
220         UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
221         UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
222         JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i)) =>
223        SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il)) ->
224        IO ((), SessionState (SessionSpec s') o i)
225loop (SessionState o i) = do { newEmptyO <- newEmptyMVar
226                             ; didPutO <- tryPutMVar o (Branch newEmptyO)
227                             ; newEmptyI <- newEmptyMVar
228                             ; didPutI <- tryPutMVar i (Branch newEmptyI)
229                             ; return ((), SessionState newEmptyO newEmptyI)
230                             }
231
232
233send :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
234         NextOp (SessionSpec (SessT t o)) (SessionSpec o),
235         ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
236         JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
237         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
238        t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i ->
239        IO ((), SessionState (SessionSpec s) o i)
240send val (SessionState o i) = do { newEmpty <- newEmptyMVar
241                                 ; putMVar o (Cell val newEmpty)
242                                 ; return ((), SessionState newEmpty i)
243                                 }
244
245recv :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
246         NextOp (SessionSpec (SessT t i)) (SessionSpec i),
247         ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
248         JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
249         JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i)) =>
250        SessionState (SessionSpec (RecvT t s)) o (SessT t i) ->
251        IO (t, SessionState (SessionSpec s) o i)
252recv (SessionState o i) = do { (Cell val next) <- takeMVar i
253                             ; return (val, SessionState o next)
254                             }
255
256mkState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming),
257            JustSendsRecvs spec' (SessionSpec incoming) (SessionSpec outgoing),
258            DualT spec spec') => spec ->
259           IO (SessionState spec outgoing incoming, SessionState spec' incoming outgoing)
260mkState _ = do { outgoing <- newEmptyMVar
261               ; incoming <- newEmptyMVar
262               ; let s1 = SessionState outgoing incoming
263               ; let s2 = SessionState incoming outgoing
264               ; return (s1, s2)
265               }
266
267data Proc :: * -> * -> * -> * -> * -> * -> * where
268             Proc :: (ZeroOrMoreSteps s s',
269                      JustSendsRecvs s (SessionSpec o) (SessionSpec i),
270                      JustSendsRecvs s' (SessionSpec o') (SessionSpec i')) =>
271                     (SessionState s o i -> IO ((), SessionState s' o' i')) -> Proc s s' o o' i i'
272
273runSessionWithProcs :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming),
274                        JustSendsRecvs specD (SessionSpec incoming) (SessionSpec outgoing),
275                        DualT spec specD,
276                        JustSendsRecvs spec' (SessionSpec outgoing') (SessionSpec incoming'),
277                        JustSendsRecvs specD' (SessionSpec incoming') (SessionSpec outgoing'),
278                        ZeroOrMoreSteps spec spec',
279                        ZeroOrMoreSteps specD specD'
280                       ) =>
281                       spec
282                    -> Proc spec spec' outgoing outgoing' incoming incoming'
283                    -> Proc specD specD' incoming incoming' outgoing outgoing'
284                    -> IO spec'
285runSessionWithProcs spec (Proc p1) (Proc p2)
286    = do { (s1, s2) <- mkState spec
287         ; let f1 = (p1 s1) >>= return . fst
288         ; let f2 = (p2 s2) >>= return . fst
289         ; forkIO f1
290         ; forkIO f2
291         ; return (stepN spec)
292         }
293
294-- log through stdout and send
295sendLog :: (NextOp (SessionSpec (SendT t s)) (SessionSpec s),
296            ZeroOrMoreSteps (SessionSpec (SendT t s)) (SessionSpec s),
297            JustSendsRecvs (SessionSpec (SendT t s)) (SessionSpec (SessT t o)) (SessionSpec i),
298            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
299            Show t) =>
300           t -> SessionState (SessionSpec (SendT t s)) (SessT t o) i
301             -> IO ((), SessionState (SessionSpec s) o i)
302sendLog v = sliftIO (putStrLn $ "Sending '" ++ (show v) ++ "'")
303            >~> send v
304
305-- receive and log through stdout
306recvLog :: (NextOp (SessionSpec (RecvT t s)) (SessionSpec s),
307            ZeroOrMoreSteps (SessionSpec (RecvT t s)) (SessionSpec s),
308            JustSendsRecvs (SessionSpec s) (SessionSpec o) (SessionSpec i),
309            JustSendsRecvs (SessionSpec (RecvT t s)) (SessionSpec o) (SessionSpec (SessT t i)),
310            ZeroOrMoreSteps (SessionSpec s) (SessionSpec s),
311            Show t) =>
312           SessionState (SessionSpec (RecvT t s)) o (SessT t i)
313               -> IO (t, SessionState (SessionSpec s) o i)
314recvLog = recv
315          >~>= (\r -> sliftIO (putStrLn $ "Received '" ++ (show r) ++ "'")
316                >~> returnS r)
317
318infixl 1 >~>
319infixl 1 >~>=
320
321-- (>>) :: (Monad m) => m b -> m c -> m c
322-- (>~>) serves the same purpose as (>>). So it's basically
323-- on the lines of Session-from-a-to-b-with-type-n ->
324--                 Session-from-b-to-c-with-type-m ->
325--                 Session-from-a-to-c-with-type-m
326(>~>) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
327          JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
328          JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
329          ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
330          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
331          ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
332         ((SessionState (SessionSpec a) o i) ->
333          IO (r, (SessionState (SessionSpec b) o' i'))) ->
334         ((SessionState (SessionSpec b) o' i') ->
335          IO (r', (SessionState (SessionSpec c) o'' i''))) ->
336         ((SessionState (SessionSpec a) o i) ->
337          IO (r', (SessionState (SessionSpec c) o'' i'')))
338f >~> g = \s -> f s >>= \(_, s') -> g s'
339
340-- (>>=) :: (Monad m) => m b -> (b -> m c) -> m c
341-- (>~>=) serves the same purpose as (>>=). So it's basically
342-- on the lines of Session-from-a-to-b-with-type-n ->
343--                 (n -> Session-from-b-to-c-with-type-m) ->
344--                 Session-from-a-to-c-with-type-m
345(>~>=) :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
346           JustSendsRecvs (SessionSpec b) (SessionSpec o') (SessionSpec i'),
347           JustSendsRecvs (SessionSpec c) (SessionSpec o'') (SessionSpec i''),
348           ZeroOrMoreSteps (SessionSpec a) (SessionSpec b),
349           ZeroOrMoreSteps (SessionSpec b) (SessionSpec c),
350           ZeroOrMoreSteps (SessionSpec a) (SessionSpec c)) =>
351          ((SessionState (SessionSpec a) o i) ->
352           IO (r, (SessionState (SessionSpec b) o' i'))) ->
353          (r -> (SessionState (SessionSpec b) o' i') ->
354           IO (r', (SessionState (SessionSpec c) o'' i''))) ->
355          ((SessionState (SessionSpec a) o i) ->
356           IO (r', (SessionState (SessionSpec c) o'' i'')))
357f >~>= g = \s -> f s >>= \(r, s') -> g r s'
358
359-- return :: (Monad m) => a -> m a
360-- returnS is pretty much the some as return, lifting a value into a session
361-- returnS :: r -> Session-from-a-to-a-with-type-r
362returnS :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
363            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
364           r -> (SessionState (SessionSpec a) o i) ->
365           IO (r, (SessionState (SessionSpec a) o i))
366returnS v s = return (v, s)
367
368-- lifting just lift an IO straight in:
369-- sliftIO :: IO r -> Session-from-a-to-a-with-type-r
370sliftIO :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
371            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
372           IO r -> ((SessionState (SessionSpec a) o i) ->
373                    IO (r, (SessionState (SessionSpec a) o i)))
374sliftIO f = \s -> f >>= \r -> returnS r s
375
376-- for when the inner function wants to grab a value from outside...
377-- sliftIO' :: (m -> IO n) -> (m -> Session-from-a-to-a-with-type n)
378sliftIO' :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
379             ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
380            (r -> IO r') -> (r -> (SessionState (SessionSpec a) o i) ->
381                             IO (r', (SessionState (SessionSpec a) o i)))
382sliftIO' f = \r -> sliftIO (f r)
383
384
385mkLoop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
386           UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
387           UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
388           JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i),
389           ZeroOrMoreSteps (SessionSpec s') (SessionSpec (Loop (SessionSpec s)))) =>
390         ((SessionState (SessionSpec s') o i) ->
391           IO ((), (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))))) ->
392          (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))) ->
393          IO ((), SessionState (SessionSpec EndT) EndT EndT)
394mkLoop f s = loop s >>= \((), s') -> f s' >>= \((), s'') -> mkLoop f s''