0 | module BufConn
 1 |
 2 | import Cont
 3 |
 4 | import Data.Vect as V
 5 | import Data.Bits
 6 | import Data.List
 7 |
 8 | import Control.Monad.State.Interface
 9 | import Control.Monad.State.State
10 | import Control.Monad.Trans
11 |
12 | public export
13 | Overflow: Type
14 | Overflow = List Bits8
15 |
16 | public export
17 | record BufConSt queuedElem where
18 |   constructor MkBufConSt
19 |   overflow : Overflow
20 |   queuedToSend : queuedElem
21 |
22 | public export
23 | DBufferedConn : Type -> Type -> Type -> Type -> Type -> Type
24 | DBufferedConn r queuedElem a altOut altIn =
25 |   StateT
26 |   (BufConSt queuedElem)
27 |   (Cont (DIterator (List Bits8) (List Bits8) altOut altIn r))
28 |   a
29 |
30 | export
31 | send : List Bits8 -> DBufferedConn r a Unit altOut altIn
32 | send bytes = do
33 |   moreData <- lift (yieldGet bytes)
34 |   modify {overflow $= (++ moreData)}
35 |   pure ()
36 |
37 | export
38 | result : r -> DBufferedConn r a b altOut altIn
39 | result res =
40 |   let
41 |     ite : DIterator (List Bits8) (List Bits8) altOut altIn r
42 |     ite = Result res
43 |     cont : Cont (DIterator (List Bits8) (List Bits8) altOut altIn r) b
44 |     cont = ContOf $ \_ => ite
45 |    in
46 |     lift cont
47 |
48 | export
49 | sendAlt : b -> DBufferedConn r a rows rows b
50 | sendAlt str = do
51 |   lift $ yieldGet2 str
52 |
53 | export
54 | read : (n: Nat) -> DBufferedConn r a (V.Vect n Bits8) altOut altIn
55 | read 0 = pure []
56 | read (S next) = do
57 |   st <- get
58 |   let oldOverflow = st.overflow
59 |   case oldOverflow of
60 |     fst :: more => do
61 |       modify {overflow := more}
62 |       V.(::) fst <$> read next
63 |     [] => do
64 |       moreData <- lift (yieldGet [])
65 |       modify {overflow := moreData}
66 |       read (S next)
67 |
68 | export
69 | iteratorFromBufConn: BufConSt a -> DBufferedConn r a r altOut altIn -> DIterator (List Bits8) (List Bits8) altOut altIn r
70 | iteratorFromBufConn st bufCon =
71 |   toIterator (evalStateT st bufCon)
72 |