Ticket #1353: SessionPruned.hs

File SessionPruned.hs, 9.2 KB (added by matthew@…, 6 years ago)

Starting to get it smaller...

Line 
1{-# OPTIONS_GHC -fglasgow-exts -fallow-overlapping-instances -fallow-undecidable-instances #-}
2
3module Session where
4
5import Control.Concurrent.MVar
6import Control.Concurrent
7
8data SType :: * -> * where
9              IntS    :: SType Int
10              BoolS   :: SType Bool
11              CharS   :: SType Char
12              StringS :: SType String
13              FloatS  :: SType Float
14              DoubleS :: SType Double
15              AnyS    :: SType a
16              LiftS   :: a -> SType a
17              ListS   :: (SType a) -> SType [a]
18
19instance Show (SType a) where
20    show IntS      = "IntS"
21    show BoolS     = "BoolS"
22    show CharS     = "CharS"
23    show StringS   = "StringS"
24    show FloatS    = "FloatS"
25    show DoubleS   = "DoubleS"
26    show AnyS      = "AnyS"
27    show (LiftS a) = "LiftS"
28    show (ListS a) = "ListS of " ++ (show a)
29
30type Loop a = [a]
31
32mkLoopS :: (SessionSpec LoopEndT -> SessionSpec l) -> SessionSpec (Loop (SessionSpec l))
33mkLoopS x = LoopS (repeat xl)
34    where
35      xl = x LoopEndS
36
37data SendT a n
38data RecvT a n
39data EndT
40data LoopEndT
41data SessT a n
42
43data SessionSpec :: * -> * where
44                    RecvS :: (SType t) -> (SessionSpec n) -> SessionSpec (RecvT t n)
45                    SendS :: (SType t) -> (SessionSpec n) -> SessionSpec (SendT t n)
46                    EndS :: SessionSpec EndT
47                    LoopEndS :: SessionSpec LoopEndT
48                    LoopS :: (Loop (SessionSpec l)) -> SessionSpec (Loop (SessionSpec l))
49
50instance Show (SessionSpec n) where
51    show (RecvS t next) = "RecvS " ++ (show t) ++ " . " ++ (show next)
52    show (SendS t next) = "SendS " ++ (show t) ++ " . " ++ (show next)
53    show (EndS) = "EndS"
54    show (LoopEndS) = "LoopEndS"
55    show (LoopS l) = case l of
56                      (myloop:_) -> "LoopS {" ++ (show myloop) ++ "}"
57
58
59class ReplaceLoopEnd orig replacement result | orig replacement -> result where
60    replaceLoopEnd :: orig -> replacement -> result
61instance ReplaceLoopEnd (SessionSpec EndT) (SessionSpec n) (SessionSpec EndT) where
62    replaceLoopEnd EndS r = EndS
63instance ReplaceLoopEnd (SessionSpec LoopEndT) (SessionSpec n) (SessionSpec n) where
64    replaceLoopEnd LoopEndS r = r
65instance ReplaceLoopEnd (SessionSpec (Loop (SessionSpec l))) (SessionSpec replacement) (SessionSpec (Loop (SessionSpec l))) where
66    replaceLoopEnd (LoopS l) r = (LoopS l)
67instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
68    ReplaceLoopEnd (SessionSpec (SendT t orig)) (SessionSpec replacement) (SessionSpec (SendT t result)) where
69        replaceLoopEnd (SendS t n) r = SendS t (replaceLoopEnd n r)
70instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
71    ReplaceLoopEnd (SessionSpec (RecvT t orig)) (SessionSpec replacement) (SessionSpec (RecvT t result)) where
72        replaceLoopEnd (RecvS t n) r = RecvS t (replaceLoopEnd n r)
73instance (ReplaceLoopEnd (SessionSpec orig) (SessionSpec replacement) (SessionSpec result)) =>
74    ReplaceLoopEnd (SessionSpec (SessT t orig)) (SessionSpec replacement) (SessionSpec (SessT t result)) where
75        replaceLoopEnd = undefined
76
77class UnrollLoop orig result | orig -> result where
78    unroll :: orig -> result
79instance (ReplaceLoopEnd (SessionSpec l) (SessionSpec (Loop (SessionSpec l))) (SessionSpec r)) =>
80    UnrollLoop (SessionSpec (Loop (SessionSpec l))) (SessionSpec r) where
81        unroll (LoopS l) = case l of
82                            (myLoop:_) -> replaceLoopEnd myLoop (LoopS l)
83instance UnrollLoop (SessionSpec (EndT)) (SessionSpec (EndT)) where
84    unroll = id
85instance UnrollLoop (SessionSpec (LoopEndT)) (SessionSpec (LoopEndT)) where
86    unroll = id
87instance UnrollLoop (SessionSpec (SendT t n)) (SessionSpec (SendT t n)) where
88    unroll = id
89instance UnrollLoop (SessionSpec (RecvT t n)) (SessionSpec (RecvT t n)) where
90    unroll = id
91instance UnrollLoop (SessionSpec (SessT t n)) (SessionSpec (SessT t n)) where
92    unroll = undefined
93
94class ZeroOrMoreSteps a b where
95    stepN :: a -> b
96instance ZeroOrMoreSteps (SessionSpec EndT) (SessionSpec EndT) where
97    stepN x = x
98instance ZeroOrMoreSteps (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
99    stepN x = x
100instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec (RecvT t l)) where
101    stepN x = x
102instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec (SendT t l)) where
103    stepN x = x
104instance ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec (Loop (SessionSpec a))) where
105    stepN x = x
106instance ZeroOrMoreSteps (SessionSpec (RecvT t l)) (SessionSpec l) where
107    stepN (RecvS t n) = n
108instance ZeroOrMoreSteps (SessionSpec (SendT t l)) (SessionSpec l) where
109    stepN (SendS t n) = n
110instance ZeroOrMoreSteps (SessionSpec (SessT t l)) (SessionSpec l) where
111    stepN = undefined
112instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
113    ZeroOrMoreSteps (SessionSpec (RecvT t a)) (SessionSpec b) where
114        stepN (RecvS t n) = stepN n
115instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
116    ZeroOrMoreSteps (SessionSpec (SendT t a)) (SessionSpec b) where
117        stepN (SendS t n) = stepN n
118instance (ZeroOrMoreSteps (SessionSpec a) (SessionSpec b)) =>
119    ZeroOrMoreSteps (SessionSpec (SessT t a)) (SessionSpec b) where
120        stepN = undefined
121instance (UnrollLoop (SessionSpec (Loop (SessionSpec a))) (SessionSpec b),
122          ZeroOrMoreSteps (SessionSpec b) (SessionSpec c)) =>
123    ZeroOrMoreSteps (SessionSpec (Loop (SessionSpec a))) (SessionSpec c) where
124        stepN = stepN . unroll
125
126class JustSendsRecvs orig sends recvs | orig -> sends recvs where
127instance JustSendsRecvs (SessionSpec EndT) (SessionSpec EndT) (SessionSpec EndT) where
128instance JustSendsRecvs (SessionSpec LoopEndT) (SessionSpec LoopEndT) (SessionSpec LoopEndT) where
129instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
130    JustSendsRecvs (SessionSpec (SendT t n)) (SessionSpec (SessT t s)) (SessionSpec r) where
131instance (JustSendsRecvs (SessionSpec n) (SessionSpec s) (SessionSpec r)) =>
132    JustSendsRecvs (SessionSpec (RecvT t n)) (SessionSpec s) (SessionSpec (SessT t r)) where
133instance (JustSendsRecvs (SessionSpec l) (SessionSpec s) (SessionSpec r)) =>
134    JustSendsRecvs (SessionSpec (Loop (SessionSpec l))) (SessionSpec (Loop (SessionSpec s))) (SessionSpec (Loop (SessionSpec r))) where
135instance JustSendsRecvs (SessionState s o i) (SessionSpec o) (SessionSpec i) where
136
137data Cell :: * -> * where
138             Cell :: t -> MVar (Cell ct) -> Cell (SessT t ct)
139             Branch :: (UnrollLoop (SessionSpec l) (SessionSpec u)) => MVar (Cell u) -> Cell l
140
141data SessionState :: * -> * -> * -> * where
142                     SessionState :: (JustSendsRecvs spec (SessionSpec outgoing) (SessionSpec incoming)) =>
143                            MVar (Cell outgoing) -> MVar (Cell incoming) ->
144                            SessionState spec outgoing incoming
145
146loop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
147         UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
148         UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
149         JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i)) =>
150        SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il)) ->
151        IO ((), SessionState (SessionSpec s') o i)
152-- TODO: make the code below do something that will work!
153loop (SessionState o i) = do { newEmptyO <- newEmptyMVar
154                             ; didPutO <- tryPutMVar o (Branch newEmptyO)
155                             ; newEmptyI <- newEmptyMVar
156                             ; didPutI <- tryPutMVar i (Branch newEmptyI)
157                             ; return ((), SessionState newEmptyO newEmptyI)
158                             }
159
160data Proc :: * -> * -> * -> * -> * -> * -> * where
161             Proc :: (ZeroOrMoreSteps s s',
162                      JustSendsRecvs s (SessionSpec o) (SessionSpec i),
163                      JustSendsRecvs s' (SessionSpec o') (SessionSpec i')) =>
164                     (SessionState s o i -> IO ((), SessionState s' o' i')) -> Proc s s' o o' i i'
165
166-- return :: (Monad m) => a -> m a
167-- returnS is pretty much the some as return, lifting a value into a session
168-- returnS :: r -> Session-from-a-to-a-with-type-r
169returnS :: (JustSendsRecvs (SessionSpec a) (SessionSpec o) (SessionSpec i),
170            ZeroOrMoreSteps (SessionSpec a) (SessionSpec a)) =>
171           r -> (SessionState (SessionSpec a) o i) ->
172           IO (r, (SessionState (SessionSpec a) o i))
173returnS v s = return (v, s)
174
175mkLoop :: (UnrollLoop (SessionSpec (Loop (SessionSpec s))) (SessionSpec s'),
176           UnrollLoop (SessionSpec (Loop (SessionSpec ol))) (SessionSpec o),
177           UnrollLoop (SessionSpec (Loop (SessionSpec il))) (SessionSpec i),
178           JustSendsRecvs (SessionSpec s') (SessionSpec o) (SessionSpec i),
179           ZeroOrMoreSteps (SessionSpec s') (SessionSpec (Loop (SessionSpec s)))) =>
180         ((SessionState (SessionSpec s') o i) ->
181           IO ((), (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))))) ->
182          (SessionState (SessionSpec (Loop (SessionSpec s))) (Loop (SessionSpec ol)) (Loop (SessionSpec il))) ->
183          IO ((), SessionState (SessionSpec EndT) EndT EndT)
184mkLoop f s = loop s >>= \((), s') -> f s' >>= \((), s'') -> mkLoop f s''