
   0 | module Network.HTTP.Message
   1 | 
   2 | import Data.String.Parser
   3 | import Data.String.Extra
   4 | import Derive.Prelude
   5 | import Network.HTTP.Header
   6 | import Network.HTTP.Status
   7 | import Network.HTTP.Method
   8 | 
   9 | import Debug.Trace
  10 | 
  11 | %language ElabReflection
  12 | 
  13 | public export
  14 | RawHeaders : Type
  15 | RawHeaders = List (String, String)
  16 | 
  17 | public export
  18 | record RawHttpMessage where
  19 |   constructor MkRawHttpMessage
  20 |   method : Method
  21 |   path : String
  22 |   headers : RawHeaders
  23 | 
  24 | public export
  25 | record HttpResponse where
  26 |   constructor MkHttpResponse
  27 |   -- stefan-hoeck: The deriving mechanism from elab-util does
  28 |   --               not (yet?) support lambdas in argument types
  29 |   --               because this would force us to keep track of
  30 |   --               variable scope when determining the parameters of
  31 |   --               a type.
  32 |   --
  33 |   --               There are two ways to work around this:
  34 |   --                 a) Use the `DPair` syntax instead of the `**` sugar
  35 |   --                 b) derive `Show` via the `deriveShow` macro, which
  36 |   --                    is slightly more verbose, but also more forgiving.
  37 |   status_code : DPair Nat StatusCode
  38 |   status_name : String
  39 |   headers : RawHeaders
  40 | 
  41 | %runElab derive "RawHttpMessage" [Show]
  42 | %runElab derive "HttpResponse" [Show]
  43 | 
  44 | export
  45 | serialize_http_message : RawHttpMessage -> String
  46 | serialize_http_message message =
  47 |   join "\r\n"
  48 |   $ [ http_method_to_string message.method <+> " " <+> message.path <+> " HTTP/1.1" ]
  49 |   <+> map (\(k,v) => "\{k}: \{v}") message.headers
  50 |   <+> [ "", "" ]
  51 | 
  52 | export
  53 | serialize_http_response : HttpResponse -> String
  54 | serialize_http_response response =
  55 |   join "\r\n"
  56 |   $ [ "HTTP/1.1 " <+> show (response.status_code.fst) <+> response.status_name ]
  57 |   <+> map (\(k,v) => "\{k}: \{v}") response.headers
  58 |   <+> [ "", "" ]
  59 | 
  60 | eol : Monad m => ParseT m ()
  61 | eol = (string "\r\n" <|> string "\n") $> ()
  62 | 
  63 | is_eol : Char -> Bool
  64 | is_eol '\r' = True
  65 | is_eol '\n' = True
  66 | is_eol _ = False
  67 | 
  68 | header : Parser (String, String)
  69 | header = do
  70 |   key <- takeUntil ":"
  71 |   value <- takeWhile1 (not . is_eol)
  72 |   eol
  73 |   pure (key, (ltrim value))
  74 | 
  75 | export
  76 | http_message_praser : Parser RawHttpMessage
  77 | http_message_praser = do
  78 |   method <- string_to_http_method . pack <$> some (satisfy isUpper)
  79 |   _ <- char ' '
  80 |   path <- takeUntil " "
  81 |   _ <- string "HTTP/1.1"
  82 |   eol
  83 |   headers <- many header
  84 |   eol
  85 |   pure (MkRawHttpMessage method path headers)
  86 | 
  87 | export
  88 | deserialize_http_message : String -> Either String RawHttpMessage
  89 | deserialize_http_message = map fst . parse http_message_praser
  90 | 
  91 | export
  92 | http_message_response : Parser HttpResponse
  93 | http_message_response = do
  94 |   _ <- many eol
  95 |   _ <- string "HTTP/1.1 " <|> string "HTTP/1.0 "
  96 |   status_code <- natural
  97 |   _ <- char ' '
  98 |   status_name <- takeWhile1 (not . is_eol)
  99 |   eol
 100 |   headers <- many header
 101 |   case is_status_code_number status_code of
 102 |     Yes ok => pure (MkHttpResponse (status_code ** nat_to_status_code status_code ok) status_name headers)
 103 |     No _ => fail $ "status code " <+> show status_code <+> " is outside of bound" 
 104 | 
 105 | export
 106 | deserialize_http_response : String -> Either String HttpResponse
 107 | deserialize_http_response = map fst . parse http_message_response
 108 |