0 | module Utils.Handle
 1 |
 2 | import Data.Vect
 3 | import Data.Nat
 4 | import Control.Monad.Error.Either
 5 | import Control.Linear.LIO
 6 |
 7 | public export
 8 | ReadHack : (t_ok : Type) -> (t_read_failed : Type) -> Bool -> Type
 9 | ReadHack t_ok t_read_failed False = t_read_failed
10 | ReadHack t_ok t_read_failed True = Res (List Bits8) (const t_ok)
11 |
12 | public export
13 | WriteHack : (t_ok : Type) -> (t_write_failed : Type) -> Bool -> Type
14 | WriteHack t_ok t_write_failed False = t_write_failed
15 | WriteHack t_ok t_write_failed True = t_ok
16 |
17 | public export
18 | record Handle (t_ok : Type) (t_closed : Type) (t_read_failed : Type) (t_write_failed : Type) where
19 |   constructor MkHandle
20 |   1 underlying : t_ok
21 |   do_read : forall m. LinearIO m => (1 _ : t_ok) -> (len : Nat) -> L1 m $ Res Bool $ ReadHack t_ok t_read_failed
22 |   do_write : forall m. LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m $ Res Bool $ WriteHack t_ok t_write_failed
23 |   do_close : forall m. LinearIO m => (1 _ : t_ok) -> L1 m t_closed
24 |
25 | public export
26 | close : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> L1 m t_closed
27 | close (MkHandle x do_read do_write do_close) = do_close x
28 |
29 | public export
30 | read : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> (len : Nat) -> L1 m $ Res Bool $ \case
31 |   False => t_read_failed
32 |   True => Res (List Bits8) (\_ => Handle t_ok t_closed t_read_failed t_write_failed)
33 | read (MkHandle x do_read do_write do_close) len = do
34 |   (True # (output # x)) <- do_read x len
35 |   | (False # x) => pure1 $ False # x
36 |   pure1 $ True # (output # MkHandle x do_read do_write do_close)
37 |
38 | public export
39 | write : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> (input : List Bits8) -> L1 m $ Res Bool $ \case
40 |   False => t_write_failed
41 |   True => Handle t_ok t_closed t_read_failed t_write_failed
42 | write (MkHandle x do_read do_write do_close) input = do
43 |   (True # x) <- do_write x input
44 |   | (False # x) => pure1 $ False # x
45 |   pure1 $ True # MkHandle x do_read do_write do_close
46 |
47 | public export
48 | Handle' : Type -> Type -> Type
49 | Handle' t_ok t_closed = Handle t_ok t_closed (Res String $ const t_closed) (Res String $ const t_closed)
50 |