0 | module Network.HTTP.Pool.IOStuff
 1 |
 2 | import Utils.Handle
 3 | import Utils.Bytes
 4 | import Utils.Misc
 5 | import Utils.Handle.C
 6 | import Control.Linear.LIO
 7 | import Network.Socket
 8 | import Data.String
 9 | import Data.String.Extra
10 | import Network.HTTP.Message
11 | import Network.HTTP.Header
12 | import Utils.String
13 | import Data.Nat
14 | import Data.Vect
15 | import System.Future
16 | import System
17 | import Data.Fin
18 |
19 | %hide Network.Socket.close
20 |
21 | public export
22 | OkOrError : Type -> Type -> Type
23 | OkOrError t_ok t_closed = Res Bool $ \ok => if ok then Res String (const $ Handle' t_ok t_closed) else Res String (const t_closed)
24 |
25 | public export
26 | read_line' : LinearIO m =>
27 |              List Bits8 ->
28 |              (1 _ : Handle' t_ok t_closed) ->
29 |              L1 m $ OkOrError t_ok t_closed
30 | read_line' acc handle = do
31 |   (True # ([char] # handle)) <- read handle 1
32 |   | (True # (char # handle)) => do
33 |     handle' <- close handle
34 |     pure1 (False # ("read line failed, somehow read returns \{show (length char)} bytes instead of 1" # handle'))
35 |   | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
36 |   case char of
37 |     -- \n = 10, \r = 13
38 |     10 => do
39 |       let Just string = utf8_pack $ reverse acc
40 |       | Nothing => do
41 |         handle' <- close handle
42 |         pure1 (False # ("read line failed, cannot parse utf8 line" # handle'))
43 |       pure1 (True # (string # handle))
44 |     13 => do
45 |       (True # ([10] # handle)) <- read handle 1
46 |       | (True # ([char] # handle)) => do
47 |         handle' <- close handle
48 |         pure1 (False # ("read line failed, \\n expected after \\r, got \{show char} instead" # handle'))
49 |       | (True # (char # handle)) => do
50 |         handle' <- close handle
51 |         pure1 (False # ("read line failed, somehow read returns \{show (length char)} bytes instead of 1" # handle'))
52 |       | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
53 |       let Just string = utf8_pack $ reverse acc
54 |       | Nothing => do
55 |         handle' <- close handle
56 |         pure1 (False # ("read line failed, cannot parse utf8 line" # handle'))
57 |       pure1 (True # (string # handle))
58 |     x => read_line' (x :: acc) handle
59 |
60 | public export
61 | read_line : LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
62 | read_line = read_line' []
63 |
64 | public export
65 | read_until_empty_line' : String -> LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
66 | read_until_empty_line' acc handle = do
67 |   (True # (line # handle)) <- read_line handle
68 |   | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
69 |   if null line then pure1 (True # (acc # handle)) else read_until_empty_line' (acc <+> "\n" <+> line) handle
70 |
71 | public export
72 | read_until_empty_line : LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
73 | read_until_empty_line = read_until_empty_line' ""
74 |