0 | module Network.HTTP.Header
  1 |
  2 | import Utils.Num
  3 | import Data.Nat
  4 | import Data.Either
  5 | import Data.String.Extra
  6 | import Control.Monad.Error.Either
  7 | import Control.Monad.Trans
  8 | import Network.HTTP.URL
  9 | import Network.HTTP.Cookie
 10 | import Utils.String
 11 | import Generics.Derive
 12 | import Derive.Prelude
 13 |
 14 | %hide Generics.Derive.Eq
 15 | %hide Generics.Derive.Ord
 16 | %hide Generics.Derive.Show
 17 |
 18 | %language ElabReflection
 19 |
 20 | public export
 21 | data Header
 22 |   = Host
 23 |   | ContentType
 24 |   | Accept
 25 |   | Authorization
 26 |   | Cookie
 27 |   | SetCookie
 28 |   | ContentLength
 29 |   | Connection
 30 |   | TransferEncoding
 31 |   | ContentEncoding
 32 |   | Location
 33 |   | Unknown String
 34 |
 35 | %runElab derive "Header" [Generic, Meta, Eq, DecEq, Ord, Show]
 36 |
 37 | public export
 38 | data ConnectionAction : Type where
 39 |   KeepAlive : ConnectionAction
 40 |   Close : ConnectionAction
 41 |
 42 | public export
 43 | data TransferEncodingScheme : Type where
 44 |   Chunked : TransferEncodingScheme
 45 |   Identity : TransferEncodingScheme
 46 |
 47 | public export
 48 | data ContentEncodingScheme : Type where
 49 |   GZip : ContentEncodingScheme
 50 |   Deflate : ContentEncodingScheme
 51 |
 52 | public export
 53 | data AuthorizationScheme : Type where
 54 |   BasicAuthorization  : (credentials : String) -> AuthorizationScheme
 55 |   BearerAuthorization : (token : String)       -> AuthorizationScheme
 56 |
 57 | %runElab derive "ConnectionAction" [Generic, Meta, Eq, DecEq, Ord, Show]
 58 | %runElab derive "TransferEncodingScheme" [Generic, Meta, Eq, DecEq, Ord, Show]
 59 | %runElab derive "ContentEncodingScheme" [Generic, Meta, Eq, DecEq, Ord, Show]
 60 | %runElab derive "AuthorizationScheme" [Generic, Meta, Eq, DecEq, Ord, Show]
 61 |
 62 | public export
 63 | header_value_type : Header -> Type
 64 | header_value_type ContentLength = Integer
 65 | header_value_type Cookie = List (String, String)
 66 | header_value_type Host = Hostname
 67 | header_value_type Connection = ConnectionAction
 68 | header_value_type TransferEncoding = List1 TransferEncodingScheme
 69 | header_value_type ContentEncoding = List1 ContentEncodingScheme
 70 | header_value_type SetCookie = Cookie
 71 | header_value_type Authorization = AuthorizationScheme 
 72 | header_value_type _ = String
 73 |
 74 | export
 75 | header_key_name : Header -> String
 76 | header_key_name ContentType = "Content-Type"
 77 | header_key_name ContentLength = "Content-Length"
 78 | header_key_name TransferEncoding = "Transfer-Encoding"
 79 | header_key_name ContentEncoding = "Content-Encoding"
 80 | header_key_name SetCookie = "Set-Cookie"
 81 | header_key_name Authorization = "Authorization"
 82 | header_key_name (Unknown x) = x
 83 | header_key_name x = show x
 84 |
 85 | public export
 86 | key_name_to_header : String -> Header
 87 | key_name_to_header x =
 88 |   case toLower x of
 89 |     "host" => Host
 90 |     "content-type" => ContentType
 91 |     "accept" => Accept
 92 |     "authorization" => Authorization
 93 |     "cookie" => Cookie
 94 |     "content-length" => ContentLength
 95 |     "connection" => Connection
 96 |     "transfer-encoding" => TransferEncoding
 97 |     "content-encoding" => ContentEncoding
 98 |     "set-cookie" => SetCookie
 99 |     x => Unknown x
100 |
101 | export
102 | FromString Header where
103 |   fromString = key_name_to_header
104 |
105 | export
106 | header_parse_value : (header : Header) -> (String -> Maybe (header_value_type header))
107 | header_parse_value Host = getRight . parse_hostname
108 | header_parse_value ContentType = Just
109 | header_parse_value Accept = Just
110 | header_parse_value Authorization = parse_authorization_encoding . break (' ' ==) . trim where
111 |   parse_authorization_encoding : (String, String) -> Maybe AuthorizationScheme
112 |   parse_authorization_encoding (x, y) =
113 |     case toLower $ trim x of
114 |       "basic"  => Just (BasicAuthorization $ trim y)
115 |       "bearer" => Just (BearerAuthorization $ trim y)
116 |       _        => Nothing
117 | header_parse_value Location = Just
118 | header_parse_value ContentLength = stringToNat' 10
119 | header_parse_value (Unknown x) = Just
120 | header_parse_value Cookie = Just . map (splitBy '=' . ltrim) . forget . split (';' ==)
121 | header_parse_value Connection = (\case "keep-alive" => Just KeepAlive"close" => Just Close_ => Nothing) . toLower . trim
122 | header_parse_value SetCookie = deserialize_cookie
123 | header_parse_value TransferEncoding = traverse parse_transfer_encoding . split (',' ==) where
124 |   parse_transfer_encoding : String -> Maybe TransferEncodingScheme
125 |   parse_transfer_encoding x =
126 |     case toLower $ trim x of
127 |       "chunked" => Just Chunked
128 |       "identity" => Just Identity
129 |       _ => Nothing
130 | header_parse_value ContentEncoding = traverse parse_content_encoding . split (',' ==) where
131 |   parse_content_encoding : String -> Maybe ContentEncodingScheme
132 |   parse_content_encoding x =
133 |     case toLower $ trim x of
134 |       "gzip" => Just GZip
135 |       "deflate" => Just Deflate
136 |       _ => Nothing
137 |
138 | export
139 | header_write_value : (header : Header) -> (header_value_type header -> String)
140 | header_write_value Host = hostname_string
141 | header_write_value ContentType = id
142 | header_write_value Accept = id
143 | header_write_value Authorization = \case (BasicAuthorization creds) => "Basic " ++ creds(BearerAuthorization token) => "Bearer " ++ token
144 | header_write_value Location = id
145 | header_write_value Cookie = join "; " . map (\(a,b) => "\{a}=\{b}")
146 | header_write_value ContentLength = show
147 | header_write_value (Unknown x) = id
148 | header_write_value Connection = \case KeepAlive => "keep-alive"Close => "close"
149 | header_write_value SetCookie = serialize_cookie
150 | header_write_value TransferEncoding = join ", " . map (toLower . show)
151 | header_write_value ContentEncoding = join ", " . map (toLower . show)
152 |
153 | export
154 | Show (DPair Header $ \h => header_value_type h) where
155 |   show (header ** value= (header_key_name header) <+> ": " <+> (header_write_value header value)
156 |
157 | public export
158 | Headers : Type
159 | Headers = List (DPair Header $ \h => header_value_type h)
160 |
161 | export
162 | eq_ignore_case : String -> String -> Bool
163 | eq_ignore_case a b = toUpper a == toUpper b
164 |
165 | export
166 | lookup_header : List (String, String) -> (header : Header) -> Maybe (header_value_type header)
167 | lookup_header headers header = do
168 |   raw_value <- lookupBy eq_ignore_case (header_key_name header) headers
169 |   header_parse_value header raw_value
170 |
171 | export
172 | lookup_headers : List (String, String) -> (header : Header) -> List (header_value_type header)
173 | lookup_headers headers header = mapMaybe go headers where
174 |   go : (String, String) -> Maybe (header_value_type header)
175 |   go (k, v) = do
176 |     guard (eq_ignore_case k (header_key_name header))
177 |     header_parse_value header v
178 |